Tiny proof assistant in Clean without Curry-Howard Isomorphism

module tst

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