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