A Haskell implementation of Proust, an interactive proof assistant for intuitionistic propositional logic described in the online textbook Logic and Computation Interwined by Prabhakar Ragde. The deductive system we adopt is given in Chapter 2.

Operators associate to the left, except for λ and →, which are right associative.

expr = λ x ⇒ expr
     | expr : t
     | expr . expr // . is to make parsing easier
     | ∧-intro expr expr
     | ∧-elim0 expr expr
     | ∧-elim1 expr expr 
     | ∨-intro0 expr expr
     | ∨-intro1 expr expr
     | ∨-elim expr expr expr 
     | ⊥-elim expr
     | ?
     | x

t = t → t
  | t ∨ t
  | t ∧ t
  | ¬ t
  | ⊥
  | x

Check validity of proof terms:

Interactively proving:

The interactive part is still work in progress. The second demo is made with Proust.

$ cabal build
$ cabal run