-- 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)