> module Tactical 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 > type Tactic = Goal -> Maybe ([Goal], Reason) 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 -> Maybe Theorem > tac_prove goal tactic = case tactic goal of > Just ([], reason) -> Just (reason []) > _ -> Nothing The least (most) useful tactic: don't change anything. > all_tac :: Tactic > all_tac g = Just ([g], head) The second least (most) useful tactic: always fails. > no_tac :: Tactic > no_tac _ = Nothing Another useless (useful) tactic: 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 > accept_tac theorem (Goal asl c) > | c == concl theorem && > hyp theorem `subset` asl = Just ([], \_ -> add_assum_list asl theorem) > | otherwise = Nothing > where subset xs ys = foldr (\x b -> b && x `elem` ys) True xs The central operation is to sequence two tactics together: p then_tac q means to perform p, and then perform q. We first refine a goal g by p to get the subgoals [g_1, g_2, ..., g_n] then which subgoal g_i is refined by q, yielding: [g_i_1, g_i_2, ..., g_i_m] The overall result is the collection of all g_i_j, along with the composite reason that chains up the reason of p with the reason of q. > then_tac :: Tactic -> Tactic -> Tactic > then_tac p q = \goal -> > do (a1,r1) <- p goal > (a2s, r2s) <- mapAndUnzipM q a1 > -- note: a2s is a list of lists > return (concat a2s, r1 . mapshape (map length a2s) 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 thenl_tac is like then_tac, but instead of one single second tactic, you can provide a list of second tactics, one for each subgoal. E.g., p thenl_tac [q1, ..., qn] p refines the goal to [g1, ..., gn] then q1 is applied to g1, etc. > thenl_tac :: Tactic -> [Tactic] -> Tactic > thenl_tac p qs = \goal -> > do (a1,r1) <- p goal > (a2s, r2s) <- zipWithM (\$) qs a1 >>= return . unzip > -- note: a2s is a list of lists > return (concat a2s, r1 . mapshape (map length a2s) r2s) Example of a practical tactic: conj_tac breaks a conjunctive goal into the conjuncts. > conj_tac :: Tactic > conj_tac (Goal as (Conj x y)) = Just ([Goal as x, Goal as y], > \(tx:ty:_) -> conj_intro (tx,ty)) > conj_tac _ = Nothing Sample prove using tactics. > thm1 = tac_prove (Goal [parse "a", parse "b"] (parse "a && b")) tac > where tac = conj_tac `thenl_tac` > [accept_tac (assume \$ parse "a"), > accept_tac (assume \$ parse "b")]