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