A lean prover for minimal logic (related to Gentzen’s LJ sequent calculus)

Lean.hs

module Lean where

-- http://ceur-ws.org/Vol-2271/paper1.pdf

import Control.Monad

data Type
  = Var Int
  | Impl Type Type
  deriving (Eq, Show)

prove :: Type -> Bool
prove = not . null . ljb []

ljb :: [Type] -> Type -> [Type]
ljb env t
  | elem t env = return t
ljb env (Impl a b) = ljb (a : env) b
ljb env t = do
  (Impl a b, env) <- select env
  case a of
    Var a -> guard $ elem (Var a) env
    Impl c d -> void $ ljb (Impl d b : env) (Impl c d)
  ljb (b : env) t

select :: [a] -> [(a, [a])]
select (x:xs) = (x, xs) : map (fmap (x:)) (select xs)
select [] = []

(~>) :: Type -> Type -> Type
(~>) = Impl

infixr 6 ~>

a, b, c :: Type
a = Var 0
b = Var 1
c = Var 2

-- prove $ a ~> a
-- prove $ a ~> b ~> a
-- prove $ (a ~> b ~> c) ~> (a ~> b) ~> a ~> c
-- prove $ (a ~> b) ~> (c ~> a) ~> c ~> b
-- prove $ (a ~> b ~> c) ~> b ~> a ~> c
-- prove $ (a ~> a ~> b) ~> a ~> b
-- prove $ ((a ~> b ~> a) ~> c) ~> c
-- prove $ ((a ~> b) ~> b ~> c) ~> b ~> c