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

Tiny proof assistant in Clean using Curry-Howard Isomorphism

module CHI

Start = notE3 (|- (((P --> Bot) --> Bot) --> Bot)) (Wff P)  //notI2 (|- P) (Wff P)
where
 notE3 n3 wff_p = impI (hlp1 n3) wff_p
 where
  hlp1 n3 p = nd_contra (notI2 p wff_p) n3

 notI2 p wff_p = impI (hlp p) (nd_not wff_p)
 where
  hlp p pb = impE pb p

 nd_contra p pb = contra p (nd_not_def` pb)
 nd_not wff_p = wff_imp wff_p wff_bot

/* ======================== TCB ========================== */

/* must be hidden in separate module */

/* ------- SYNTAX --------- */

wff_a :: Wff CstA ; wff_a = Wff A ; wff_b :: Wff CstB ; wff_b = Wff B ; wff_p :: Wff CstP ; wff_p = Wff P
wff_c :: Wff CstC ; wff_c = Wff C ; wff_d :: Wff CstD ; wff_d = Wff D ; wff_q :: Wff CstQ ; wff_q = Wff Q

wff_bot :: Wff Bot
wff_bot = Wff Bot

wff_true :: Wff TRUE
wff_true = Wff TRUE

wff_not :: (Wff p) -> Wff (Not p)
wff_not (Wff p) => Wff (~ p)

wff_and :: (Wff p) (Wff q) -> Wff (And p q)
wff_and (Wff p) (Wff q) => Wff (p /\ q)

wff_or :: (Wff p) (Wff q) -> Wff (Or p q)
wff_or (Wff p) (Wff q) => Wff (p \/ q)

wff_imp :: (Wff p) (Wff q) -> Wff (Imp p q)
wff_imp (Wff p) (Wff q) => Wff (p --> q)

/* ----------- CONSTRUCTIVE ---------- */

impI :: ((Deduced p) -> Deduced q) (Wff p) -> Deduced (Imp p q)
impI f (Wff p) => case f (|- p) of |- q -> |- (p --> q)

impE :: (Deduced (Imp p q)) (Deduced p) -> Deduced q
impE (|- (p --> q)) (|- p`) => |- q

andI :: (Deduced p) (Deduced q) -> Deduced (And p q)
andI (|- p) (|- q) => |- (p /\ q)

andE :: (Deduced (And p q)) -> Deduced p
andE (|- (p /\ q)) => |- p

andE` :: (Deduced (And p q)) -> Deduced q
andE` (|- (p /\ q)) => |- q

orI :: (Deduced p) (Wff q) -> Deduced (Or p q)
orI (|- p) (Wff q) => |- (p \/ q)

orI` :: (Deduced p) (Wff q) -> Deduced (Or p q)
orI` (|- p) (Wff q) => |- (p \/ q)

contra :: (Deduced p) (Deduced (Not p)) -> Deduced Bot
contra (|- p) (|- (~ q)) => |- Bot

mp p q = impE p q
nd_not_def (|- (~ p) ) = |- (p --> Bot)
nd_not_def` (|- (p --> Bot)) = |- (~ p)

/* ----------- NONCONSTRUCTIVE (move to separate module) --------- */

absurd :: ((Deduced (Not p)) -> Deduced Bot) (Wff p) -> Deduced p
absurd _ (Wff p) => |- p

bottom_complete :: (Deduced Bot) (Wff p) -> Deduced p
bottom_complete (|- Bot) (Wff p) => |- p

tertium :: (Wff p) -> Deduced (Or p (Not p))
tertium (Wff p) => |- (p \/ ~ p)

:: Deduced p = |- p /* *MUST* be abstract type! */

:: Wff a = Wff a /* *MUST* be abstract type! */

/* ======================== END OF TCB ========================== */

:: CstA = A ; :: CstB = B ; :: CstC = C ; :: CstD = D ; :: CstE = E ; :: CstP = P ; :: CstQ = Q
:: Not a = ~ a
:: Imp a b = (-->) infix 5 a b
:: And a b = (/\) infixr 6 a b
:: Or a b = (\/) infixr 6 a b
:: Bot = Bot
:: TRUE = TRUE