> module MonadicTactical where > import Theorem > import InfLib > import List This module defines goal-directed (backward) proofs, following HOL. The backward inference rules are called tactics. A goal is a theorem-wannabe: a list/set of assumptions and a term to be proved. > data Goal = Goal {ghyp :: [Term], gconcl :: Term} We show a goal like a theorem, but with the turnstile "|-" changed to an uncertain turnstile "?-". > instance Show Goal where > showsPrec _ (Goal hs c) = showsPrec 0 hs . showString " ?- " . > showsPrec 0 c A tactic takes a goal and refines it by some subgoals. Not only that, but it also provides a reason --- a forward inference rule to justify the refinement, i.e., if you can successfully prove the subgoals as lemmata, just submit them to the reason and get the theorem sought. There are times when a tactic is inappropriate because the goal is not in a suitable form. So, again, we use a Maybe type. For example, in order to prove A ?- x && y the conj_tac tactic (shown later) refines it by the two goals A ?- x, A ?- y So conj_tac satisfies this specification: conj_tac (A ?- x && y) = Just ([A ?- x, A ?- y], reason) where reason [A |- x, A |- y] = A |- x && y > type Reason = [Theorem] -> Theorem > newtype Tactic a = Tactic {tactic :: Goal -> Maybe ([(Goal,a)], Reason)} Ok, that declaration doesn't exactly look like what we just described. In fact, you can see that we are setting up ourselves to make tactics monads! The type variable 'a', when used cleverly, can serve as a hint given by one tactic to the next tactic. Examples below. When does a backward proof stop? If a tactic outputs an empty subgoal list, there is no more to do: you just give [] to the reason, and you get the theorem. This is reflected by the driver function of backward proof: "tac_prove" takes a goal and a tactic, and runs the tactic to prove the goal: > tac_prove :: Goal -> Tactic a -> Maybe Theorem > tac_prove goal (Tactic tac) = > case tac goal of Just ([], reason) -> Just (reason []) > _ -> Nothing We now cast a tactic as a monad. > instance Monad Tactic where > -- return is like all_tac: changes nothing, just returns the parameter > return a = Tactic (\g -> Just ([(g,a)], head)) > -- >>= is like then_tac, only better > (Tactic p) >>= qm = > Tactic \$ \goal -> > do (g1, r1) <- p goal > (g2s, r2s) <- mapAndUnzipM (\(g,a)->tactic (qm a) g) g1 > -- note: g2s is a list of lists > return (concat g2s, r1 . mapshape (map length g2s) r2s) where mapshape is a helper function for applying a list of mappings to a concatenated list, e.g., mapshape [2,3,1] [f,g,h] [x1,x2,x3,x4,x5,x6] = [map f [x1,x2], map g [x3,x4,x5], map h [x6]] > mapshape [] _ _ = [] > mapshape (n:ns) (f:fs) xs = f xs1 : mapshape ns fs xs2 > where (xs1,xs2) = splitAt n xs In fact tactic is also a monad with zero and plus. > instance MonadPlus Tactic where > -- mzero is no_tac > mzero = Tactic (\_ -> Nothing) > -- mplus is try one tactic, and if it fails, try the other. > mplus (Tactic p) (Tactic q) = > Tactic \$ \goal -> mplus (p goal) (q goal) Now the practical tactics. accept_tac: use a known theorem to prove a goal that equals the theorem (conclusions must be the same; assumptions of the goal must be a superset of assumptions of the theorem). > accept_tac :: Theorem -> Tactic a > accept_tac theorem = Tactic tac > where > tac (Goal asl c) = if c == concl theorem && hyp theorem `subset` asl > then Just ([], \_ -> add_assum_list asl theorem) > else Nothing > where subset xs ys = foldr (\x b -> b && x `elem` ys) True xs conj_tac: breaks a conjunctive goal "x && y" into the conjuncts. The return value attached to the subgoal "x" is the theorem "x |- x"; same for the subgoal "y". This aids the tactic after conj_tac to do the right thing. > conj_tac :: Tactic Theorem > conj_tac = Tactic tac > where tac (Goal as (Conj x y)) = > Just ([(Goal as x, assume x), (Goal as y, assume y)], > \(tx:ty:_) -> conj_intro (tx,ty)) > tac _ = Nothing Let us prove "a,b |- a && b" again, this time taking advantage of the syntactic sugar for monads and the return values of conj_tac. > thm1 = tac_prove (Goal [parse "a", parse "b"] (parse "a && b")) > (do t <- conj_tac > accept_tac t)