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