Proof System on Haskell (incomplete)

overview.md

IDEA

example = do
  axiom (p : Prop)
  apply init
  apply ...
  qed $ p /\ q -> p

みたいな感じで証明を作っておき, これをrunProofしたら証明を組み立てて, どこかに間違いがあればエラーを吐くProof System. 函数のEqualityは与えられた論理式とそのdomainで値が等しいこと $\forall x. f(x) = \forall x. g(x) <=> f = g$ でとりあえずはよしとしたい.

PROBLEM

• axiom (p : Prop) とする前にpを束縛する必要がある(美しくない)
• Propの束縛を回避するために式を (\p -> ~~~) の形にしておくと, そもそもこれが函数になるので Formula a b と型が合わないためrunProofできない.

• そもそもλ式つかったらProof Systemの意味があまりない.
  

ProofSystem.hs

{-# LANGUAGE DeriveFunctor, TypeOperators #-}

import Prelude hiding (True, False, init, id)
import Control.Category
import Control.Arrow
import Control.Monad.Free

newtype Atom a b = Atom { runAtom :: a -> b }
 
data Formula a b = True
                 | False
                 | Or (Formula a b) (Formula a b)
                 | And (Formula a b) (Formula a b)
                 | Then (Formula a b) (Formula a b)
                 | Forall a (Formula a b)
                 | Exists a (Formula a b)
                 | Atomic (Atom a b)

type Prop a b = Formula a b

data Proof a next = Axiom a next | Qed a next | Apply a next
                  deriving Functor

type State a b = Free (Proof (Formula a b)) ()

(/\) :: Formula a b -> Formula a b -> Formula a b
(/\) = And

(.->) :: Formula a b -> Formula a b -> Formula a b
(.->) = Then

qed :: Formula a b -> State a b
qed f = liftF $ Qed f ()

axiom :: Formula a b -> State a b
axiom f = liftF $ Axiom f ()

apply :: State a b -> State a b
apply (Free (Qed f _)) = liftF $ Apply f ()
apply (Free (Apply _ next)) = apply next
apply (Free (Axiom _ next)) = apply next

init :: State a b
-- init = qed $ \p -> p .-> p
init = undefined

example :: State a b
example = do
  apply init
--  qed $ \p -> p .-> p


runProof = undefined