Thursday, July 9, 2009

Tiny proof assistant in Clean without Curry-Howard Isomorphism


module PublishND

import StdGeneric, GenEq, StdMisc
from StdEnv import
instance == {#Char}, instance == Int, instance == Real,
&&, class == (..), instance == [a] | == a

Start = let p = pvar "P" in [notI2 p,notE2_nc p,notE3 p,notE3_nc p,errNotE2 p]
where
impOpen r p = impE r (assum p)
mix a b
# r = andI a b
# r = andE r
= r
mix` a b
# r = andI a b
# r = andE` r
= r
/*
p, p -> _|_ |- _|_
-----------------------------
p |- (p -> _|_) -> _|_
*/
notI2 p
# a = assum p
# b = assum (p --> B)
# r = mix` a b
# r = impOpen r p
# r = impI r (p --> B)
= r

/*
~p,~~p |- ~p /\ ~~p
--------------- assum(~p),assum(~~p),andI,contra,absurd(p)
~p
*/
notE2_nc p // !!!!!! [!] !!!!!!!
# np = ~ p
# nnp = ~ np
# a = assum np
# b = assum nnp
# r = contra a b
# r = absurd r p
= r

/*
P |- (P --> _|_) --> _|_
((P --> _|_) --> _|_) --> _|_ |- ((P --> _|_) --> _|_) --> _|_
((P --> _|_) --> _|_) --> _|_, P |- _|_
-------------------------------------------------
((P --> _|_) --> _|_) --> _|_ |- P --> _|_
*/
notE3 p
# n3 = ((p --> B) --> B) --> B
# a = notI2 p
# b = assum n3
# r = contra a b
# r = impI r p
= r

notE3_nc p
# np = ~ p
# nnp = ~ np
# nnnp = ~ nnp
# a = assum nnp
# b = assum nnnp
# r = contra a b
# r = absurd r np
= r

/* doubleNot:
~~~p,p,... |- q /\ ~q
------------- weak(p),contra,notI3,absurd
p |- ~~p
*/
errNotE2 p
# np = ~ p
# nnp = ~ np
# nnnp = ~ nnp
# r = assum (nnp /\ nnnp)
# a = andE r
# b = andE` r
# r = contra a b
// r = absurd r nnp
= r

pvar a = PV a
tvar a = TV a

/* ----------------- TCB (so must be in separate module with ::Deduced as abstract type ----------------------- */

start => EMPTY |- T
assum p => p$ EMPTY WITH p |- p
weak (v |- p) q => q$ v WITH q |- p
impI (v |- p) q | q IN v => q$ v WITHOUT q |- q --> p
impE (v |- p --> q) (w |- p`) | p == p` => v AND w |- q
andI (v |- p) (w |- q) => v AND w |- p /\ q
andE (v |- p /\ q) => v |- p
andE` (v |- p /\ q) => v |- q
orI (v |- p) q => p$ v |- p \/ q
orI` (v |- p) q => q$ v |- q \/ p
orE (v |- r) (w |- r`) (y |- p /\ q) | r == r` && p IN v && q IN w => (v WITHOUT p) AND (w WITHOUT q) AND y |- r
//notI (v |- p) => v |- ~ (~ p)
contra (v |- p) (w |- ~p`) | p == p` => v AND w |- B
contra (v |- p) (w |- p` --> B) | p == p` => v AND w |- B
/* --------- NONCONSTRUCTIVE PART --------------- */
absurd (v |- B) p | ~p IN v => p$ v WITHOUT ~p |- p
botE (v |- B) p => p$ v |- p
midE p => p$ EMPTY |- p \/ ~p

:: Deduced
= (|-) infix 1 (Set Prop) Prop

/* -------------------------------------------- END OF TCB ------------------------------------- */

:: Prop
= (====) infix 4 Term Term | (<) infix 4 Term Term | (>) infix 4 Term Term
| (=<) infix 4 Term Term | (>=) infix 4 Term Term | (-->) infix 5 Prop Prop
| (<--) infix 5 Prop Prop | (<->) infix 5 Prop Prop | (\/) infixr 6 Prop Prop
| (/\) infixr 6 Prop Prop | ~ Prop | A [String] Prop | E [String] Prop
| B /* bottom */ | T /* truth */ | PV String

derive gEq Prop ; instance == Prop where (==) a b = gEq{|*|} a b

:: Term
= I Int | F Real | S String | C String | TV String | (+) infixl 6 Term Term
| (-) infixl 6 Term Term | (*) infixl 7 Term Term | (/) infixl 7 Term Term
| (%) infixl 9 Term Term | (++) infixr 5 Term Term | (^) infixr 8 Term Term

derive gEq Term ; instance == Term where (==) a b = gEq{|*|} a b

:: Set a :== [a]

EMPTY = []
(WITH) infixl 3 :: [Prop] Prop -> [Prop]
(WITH) w p = [p:w WITHOUT p]
(WITHOUT) infixl 3 :: [Prop] Prop -> [Prop]
(WITHOUT) [w:ws] p | w == p = ws ; = [w:ws WITHOUT p]
(WITHOUT) [] _ = []
(AND) infixl 2 :: [Prop] [Prop] -> [Prop]
(AND) w [v:vs] = (w WITH v) AND vs // remove pars?
(AND) w [] = w
(IN) infix 9 :: Prop [Prop] -> Bool
(IN) p [w:ws] | w == p = True ; = p IN ws
(IN) _ [] = False

($) infixr 0 :: Prop a -> a
($) p r | valid p = r ; = abort "SYNTAX"
valid a = True

No comments: