-- Naive Intuitionistic Proof Search for Propositional Logic
-- 03.01.2018 Simon Wimmer
import Data.Maybe

type VName = String

-- Logic Formulae
data Prop = Atom VName | Imp Prop Prop
    deriving Eq

instance Show Prop where
    show (Atom x) = x
    show (Imp (Atom x) b) = x ++ " --> " ++ show b
    show (Imp a b) = "(" ++ show a ++ ") --> " ++ show b

infixr 7 -->
(-->) = Imp

-- Proof Terms
data Term = V VName | Abs VName Term | App Term Term

showVar x = "'" ++ x ++ "'"

instance Show Term where
    show (V x) = showVar x
    show (Abs x t) = "λ" ++ showVar x ++ ". " ++ show t
    show (App (Abs x t) (V y)) =
        "(" ++ show (Abs x t) ++ ") " ++ showVar y
    show (App (Abs x t) t2) =
        "(" ++ show (Abs x t) ++ ") (" ++ show t2 ++ ")"
    show (App t1 (V x)) = show t1 ++ " " ++ showVar x
    show (App t1 t2) = show t1 ++ " (" ++ show t2 ++ ")"

infixl 7 $$
($$) = App

-- Finds the first successful computation in a list
-- of computations and returns it.
-- Example: firstJust [Nothing, Just 1, Just 3] = Just 1
firstJust :: [Maybe a] -> Maybe a
firstJust = foldr mplus Nothing

type Goal = ([Prop], Prop)

-- Try to solve a goal by assumption
assumption :: Goal -> Maybe Term
assumption (gamma, prop) = if prop `elem` gamma then Just (V (show prop)) else Nothing

-- Try to solve a goal by applying (-> Intro)
-- Second argument is the current 'path'.
intro :: Goal -> [Goal] -> Maybe Term
intro (gamma, Imp a b) hist = do
  -- The if-clause is crucial for termination
  -- t <- solve (if a `elem` gamma then gamma else a : gamma, b) hist
  t <- solve (a : gamma, b) hist
  return $ Abs (show a) t
intro (gamma, _) hist = Nothing

-- Try to solve a goal by applying (-> Elim).
-- Second argument is the current 'path'.
elim :: Goal -> [Goal] -> Maybe Term
elim (gamma, prop) hist = firstJust $ map (\p -> solveElim (V (show p)) p) $ filter isCandidate gamma
  where
    isCandidate (Imp _ b) = b == prop || isCandidate b
    isCandidate _ = False
    
    solveElim l (Imp a b) = do
      r <- solve (gamma, a) hist
      if b == prop then Just (App l r)
                   else solveElim (App l r) b

    
-- Given a goal and a list of previous goals on the current 'path',
-- perform a cycle test and try to solve the goal by trying
-- assumption, intro and elim.
solve :: Goal -> [Goal] -> Maybe Term
solve goal hist =
  if goal `elem` hist then Nothing else
    firstJust [
        assumption goal,
        intro goal (goal : hist),
        elim goal (goal : hist)
        ]

-- Wrapping up solve
prove :: Prop -> Maybe Term
prove prop = solve ([], prop) []

-- Test cases
p = Atom "P"
q = Atom "Q"
r = Atom "R"

p1 = p --> q
p2 = p --> p
p3 = p --> q --> p

-- Example below theorem 4.0.6
p4 = (p --> q --> r) --> (p --> q) --> p --> r
-- This comment should be irrelevant with the new proof method
-- The proof tree we get is slightly different from the lecture. Why?
-- (Solution: we are biased towards intro --> try swapping intro and elim in solve)

peirce = ((((p --> q) --> p) --> p) --> q) --> q
-- This yields the same proof tree as in ex 1

ha3 = ((r --> q) --> q) --> (r --> p) --> (p --> q) --> q
-- Same proof tree as in homework 3

examples = [p, q, r, p1, p2, p3, p4, peirce, ha3]

-- From Homework 4
t = Atom "_|_"
neg p = p --> t

q1 = neg (neg (neg p)) --> neg p
q2 = neg (neg (p --> q)) --> neg (neg p) --> neg (neg q)