content: = HOL Proof Tactics =
  
  We build a intuitionistic logic theorem prover with link:Hol.html[our version
  of HOL Light].
  
  https://github.com/jrh13/hol-light/blob/master/itab.ml[The original HOL
  Light version] uses a different algorithm.
  https://crypto.stanford.edu/~blynn/compiler/atp.html[Like a previous prover],
  for implications, we use a technique described by Dyckhoff,
  "Contraction free sequent calculi for intuistionistic logic".
  
  \begin{code}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE LambdaCase, TupleSections #-}
  import Control.Applicative
  import Control.Arrow (second)
  import Control.Monad.State
  import Data.Foldable (asum)
  import Data.List (union, unfoldr, find)
  import Hol
  \end{code}
  
  HOL Light is a simply typed lambda calculus that predefines the primitive type
  \(\mathbb{B}\) of Booleans and an equality function \((=) : a \rightarrow a
  \rightarrow \mathbb{B}\) satisfying certain rules.
  All the logic symbols we know and love must be built on top.
  
  To define truth, inspired by the `refl` rule, we pick the identity function on
  booleans \(\lambda p : \mathbb{B} . p\) and equate it to itself.
  
  The universal quantifier `(!)` takes a term \(p\) of type \(a \rightarrow
  \mathbb{B}\) and states \(p = \lambda x . T\), that is, we say \(p\) is
  equivalent to the lambda abstraction that maps all values of type \(a\) to
  truth. We've arranged the parser so that `(!)` is a binder, that is, it first
  acts as a lambda before applying itself to the resulting abstraction.
  
  For falsehood, we use \(\forall p : \mathbb{B} . p\), that is, roughly
  speaking, "everything is true". This embodies the principle of explosion, or
  ex falso quodlibet; if we can prove falsehood, then we can prove any given
  theorem.
  
  We define conjunction with the aid of currying. And soon we get the whole
  gang. Perhaps the least comprehensible is the existential quantifier `(?)`, but
  on closer inspection, it's just a disguised De Morgan dual.
  
  \begin{code}
  mustParse xs = either error id . peruse xs
  basicAxioms = flip execState [] $ do
    def "T" "(^p:Bool.p) = (^p:Bool.p)"
    def "!" "^p:a->Bool.p = ^x.T"
    def "F" "!p:Bool.p"
    def "&" "^p q.(^f:Bool->Bool->Bool.f p q) = (^f.f T T)"
    def "==>" "^p q. p & q <=> p"
    def "~" "^p. p ==> F"
    def "|" "^p q. !r. (p ==> r) ==> ((q ==> r) ==> r)"
    def "?" "^p:a->Bool. !q. (!x. p x ==> q) ==> q"
    where
    def lhs rhs = do
      xs <- get
      put $ (newConstant lhs $ mustParse xs rhs):xs
  
  basic = mustParse basicAxioms
  basicType = typeOf . basic . ("x:" <>)
  falso = basic "F"
  t ==> u = basic "(==>)" @! t @! u
  \end{code}
  
  We check our definitions actually parse:
  
  \begin{code}
  testBasic = putStr . unlines . map show $ basicAxioms
  \end{code}
  
  Some utilities to produce theorems from given theorems and the basic axioms:
  
  \begin{code}
  hyp (a :|- _) = a
  concl (_ :|- w) = w
  
  defThm s = maybe (error "bad constant") id $ find f basicAxioms where
    f (_ :|- Con s' _ := _) = s == s'
  
  -- A |- x = y  /  A |- f x = f y
  apTerm :: Hol -> Thm -> Thm
  apTerm f xy = app (refl f) xy
  
  -- A |- f = g  /  A |- f x = g x
  apThm :: Thm -> Hol -> Thm
  apThm fg x = app fg (refl x)
  
  -- A |- l = r  /  A |- r = l
  sym :: Thm -> Thm
  sym th = ePonens (app (apTerm e th) lth) lth where
    e@(Con "=" _) :$ l :$ _ = concl th
    lth = refl l
  
  --  |- T
  truth :: Thm
  truth = ePonens (sym $ defThm "T") (refl $ basic "^p:Bool. p")
  
  -- A |- t <=> T  /  A |- t
  eqtElim :: Thm -> Thm
  eqtElim th = ePonens (sym th) truth
  
  -- A |- t  /  A |- t <=> T
  eqtIntro :: Thm -> Thm
  eqtIntro th = ePonens (inst [(concl th, b)] pth) th where
    b = basic "b:Bool"
    th1 = deduct (assume b) truth
    pth = deduct (eqtElim (assume $ concl th1)) th1
  
  --  A1 |- t1 ==> t2  A2 |- t2 ==> t1  /  (A1 - {t1}) + (A2 - {t2}) |- t1 <=> t2
  impAntisymRule
    th1@(_ :|- t1 :==> t2)
    th2@(_ :|- t2' :==> t1')
    -- Intended for use with side condition:  | t1 == t1', t2 == t2'
    = deduct (undisch th2) (undisch th1)
  \end{code}
  
  A sanity check. We prove \({x} \vdash x = T\) ("assuming x, x is true").
  
  \begin{code}
  testEqt = eqtIntro $ assume $ basic "x:Bool"
  \end{code}
  
  A `Conv` tries to convert a term into a theorem.
  
  \begin{code}
  type Conv = Hol -> Either String Thm
  betaConv :: Conv
  betaConv (f@(Lam v _) :$ x) = inst [(x, v)] . beta <$> f @@ v
  betaConv _ = Left "betaConv failed"
  
  convRule :: Conv -> Thm -> Thm
  convRule conv th | Right x <- conv $ concl th = ePonens x th
  
  randConv :: Conv -> Conv
  randConv conv (f :$ x) = app (refl f) <$> conv x
  
  ratorConv :: Conv -> Conv
  ratorConv conv (f :$ x) = flip apThm x <$> (conv f)
  
  redepthConv c t = Right $ rep $ go t where
    rep (b, th@(_ :|- _ := r)) = if b
      then case go r of
        (False, _) -> th
        (True, r') -> rep (True, trans th r')
      else th
  
    go t = let
      (b, z@(_ :|- _ := r)) = case t of
        x :$ y -> (xb || yb, app x' y') where
          (xb, x') = go x
          (yb, y') = go y
        Lam x y -> second (lam x) $ go y  -- TODO: Rename var if lam fails.
        _ -> (False, refl t)
      in case trans z <$> c r of
        Left _ -> (b, z)
        Right z' -> (True, z')
  
  betaRule = convRule $ redepthConv betaConv
  
  proveHyp ath bth = if any (concl ath ==) (hyp bth)
    then ePonens (deduct ath bth) ath
    else bth
  
  f @! x = either error id $ f @@ x
  
  alt_conj lth rth = ePonens (proveHyp lth th) rth where
    f = basic "f:Bool->Bool->Bool"
    p = basic "p:Bool"
    q = basic "q:Bool"
    th1 = convRule (randConv betaConv) (apThm (defThm "&") p)
    th2 = convRule (randConv betaConv) (apThm th1 q)
    th3 = ePonens th2 $ assume $ basic "(&)" @! p @! q
    pth1 = eqtElim $ betaRule $ apThm th3 $ basic "^(p:Bool) (q:Bool).q"
    th5 = lam f $ app (apTerm f $ eqtIntro $ assume p) $ eqtIntro $ assume q
    th6 = betaRule $ apThm (apThm (defThm "&") p) q
    pth2 = ePonens (sym th6) th5
    pth = deduct pth1 pth2
    th = inst [(concl lth, p), (concl rth, q)] pth
  
  apThmBeta fg x = convRule (randConv betaConv) $ apThm fg x
  
  -- t1  t2  /  |- t1 & t2 = ((\f.f t1 t2) <=> (\f.f T T))
  andThm t1 t2 = apThmBeta (apThmBeta (defThm "&") t1) t2
  
  -- t1  t2  / |- (t1 ==> t2) = (t1 & t2 <=> t1)
  impThm t1 t2 = apThmBeta (apThmBeta (defThm "==>") t1) t2
  
  -- t1  t1  / |- t1 | t2 = !r.(t1 ==> r) ==> (t2 ==> r) ==> r
  orThm t1 t2 = apThmBeta (apThmBeta (defThm "|") t1) t2
  
  -- t  /  |- ~t = (t ==> F)
  notThm t = apThmBeta (defThm "~") t
  
  fvThm (a :|- w) = foldr union (fv w) (fv <$> a)
  
  -- A |- t1  B |- t2  /  A + B |- t1 & t2
  conj th1 th2 = ePonens (sym (andThm (concl th1) (concl th2))) th where
    f = variant (fvThm th1 `union` fvThm th2) $ basic "f:Bool->Bool->Bool"
    th = lam f $ app (apTerm f (eqtIntro th1)) (eqtIntro th2)
  
  comK = basic "^(x:Bool) (y:Bool).x"
  comKI = basic "^(x:Bool) (y:Bool).y"
  
  -- A |- l & r  /  A |- l
  conjunct1 th@(_ :|- Con "&" _ :$ l :$ r) = eqtElim
    $ sym
    $ convRule (randConv betaConv)
    $ convRule (randConv $ ratorConv betaConv)
    $ convRule (randConv betaConv)
    $ sym
    $ convRule (randConv betaConv)
    $ convRule (randConv $ ratorConv betaConv)
    $ apThmBeta (ePonens (andThm l r) th) comK
  
  -- A |- l & r  /  A |- l
  conjunct2 th@(_ :|- Con "&" _ :$ l :$ r) = eqtElim
    $ sym
    $ convRule (randConv betaConv)
    $ convRule (randConv $ ratorConv betaConv)
    $ convRule (randConv betaConv)
    $ sym
    $ convRule (randConv betaConv)
    $ convRule (randConv $ ratorConv betaConv)
    $ apThmBeta (ePonens (andThm l r) th) comKI
  
  -- A |- t ==> F  /  A |- ~t
  notIntro th@(_ :|- t :==> _) = ePonens (sym (notThm t)) th
  
  -- u  A |- t  /  A - {u} |- u ==> t
  disch u th@(_ :|- t) = ePonens (sym (impThm u t))
    $ deduct (conj (assume u) th)
    (conjunct1 $ assume $ basic "(&)" @! u @! t)
  
  dischAll th@([] :|- _) = th
  dischAll th@((a:_) :|- _) = dischAll $ disch a th
  
  -- A |- t1 ==> t2  /  A + {t1} |- t2
  undisch th@(_ :|- t1 :==> _) = ponens th $ assume t1
  
  -- u  A |- !x. t  /  A |- t[u/x]
  -- The side conditions of `inst` apply.
  spec u th@(a :|- Con "!" _ :$ lxt@(Lam x t)) =
    eqtElim $ inst [(u, x)] $ betaRule th2
    where
    th1 = instType [(typeOf x, basicType "a")] $ defThm "!"
    th2 = apThm (convRule betaConv $ ePonens (apThm th1 lxt) th) x
  
  -- x  A |- t  /  A |- !x.t  |  x not free in A
  gen x th@(_ :|- t) = th3 where
    th1 = instType [(typeOf x, basicType "a")] $ defThm "!"
    th2 = sym $ convRule (randConv betaConv) $ apThm th1 $ mustLam x t
    th3 = ePonens th2 $ lam x $ eqtIntro th
  
  -- A |- t1  t2  /  A |- t1 | t2
  disj1 th@(_ :|- t1) t2 =
    proveHyp th $ inst [(t1, p1), (t2, p2)] $ ePonens th1 th3
    where
    th1 = sym $ orThm p1 p2
    th2 = ponens (assume p1r) $ assume p1
    th3 = gen (basic "r:Bool") $ disch p1r $ disch p2r th2
    p1 = basic "p1:Bool"
    p2 = basic "p2:Bool"
    p1r = basic "p1 ==> r"
    p2r = basic "p2 ==> r"
  
  -- t1  A |- t2  /  A |- t1 | t2
  disj2 t1 th@(_ :|- t2) =
    proveHyp th $ inst [(t1, p1), (t2, p2)] $ ePonens th1 th3
    where
    th1 = sym $ orThm p1 p2
    th2 = ponens (assume p2r) $ assume p2
    th3 = gen (basic "r:Bool") $ disch p1r $ disch p2r th2
    p1 = basic "p1:Bool"
    p2 = basic "p2:Bool"
    p1r = basic "p1 ==> r"
    p2r = basic "p2 ==> r"
  
  -- A |- t1 ==> t2  B |- t1  /  A + B |- t2
  ponens th1@(_ :|- t1 :==> t2) th2 =
    conjunct2 $ eqtElim $ trans (ePonens (impThm t1 t2) th1) (eqtIntro th2)
  
  -- A |- t1 <=> t2  /  A |- t1 ==> t2  A |- t2 ==> t1
  eqImpRule t = (go t, go $ sym t) where
    go th@(_ :|- eq@(t1 :<=> _))
      = ponens (disch eq $ disch t1 $ ePonens (assume eq) (assume t1)) th
  
  -- t  A |- F  /  A |- t
  efq w th@(_ :|- t) | t == falso = ponens
    (disch falso $ spec w $ undisch $ fst $ eqImpRule $ defThm "F")
    th
  \end{code}
  
  These functions help us prove obvious theorems:
  
  \begin{code}
  testSpec = spec (basic "f:(Num->Num) z:Num") (assume $ basic "!x:Num.(x = y)")
  \end{code}
  
  == Tactics ==
  
  In practice, to prove a theorem, sometimes we work backwards. For example, when
  attempting a proof by induction, we might first work on the base case and leave
  the inductive case for later.
  
  We introduce data structures to help organize such efforts. A `Goal` is a
  theorem we wish to prove from given assumptions. Each assumption of a `Goal`
  is a labeled theorem, and the conclusion is a `Hol` term.
  
  Given a `Hol` term to prove, we begin by making it a goal with no assumptions.
  Then we apply a _tactic_ to replace the goal with subgoals, along with a
  justification function that describes how to prove the original goal if each of
  the subgoals are proved. We may apply tactics recursively, thus we wind up with
  a tree. Ultimately, if we prove each leaf theorem, then recursively tracing the
  crumbs we've left behind proves our original goal.
  
  Hence, each node of a `GoalTree` represents a single theorem. Leaf nodes are
  either theorems we have succesfully proved (`Thm`) or theorems we are still
  working on (`Goal`). Each internal node contains a function (`Crumb`) that
  produces its theorem from its child theorems.
  
  A `Tactic` is a function taking a `Goal` to `Either String GoalTree`.
  It might prove a goal, turning it from a `Goal` to a `Thm` in a leaf node.
  It might split a goal into several subgoals. Or it might fail.
  
  \begin{code}
  infix 1 :?-
  type Crumb = (String, [Thm] -> Thm)
  data Goal = [(String, Thm)] :?- Hol
  instance Show Goal where show = flip briefGoal ""
  data GoalTree = Nd Crumb [GoalTree] | Lf (Either Goal Thm)
  type Tactic = Goal -> Either String GoalTree
  \end{code}
  
  Functions for printing goals, and for navigating the tree:
  
  \begin{code}
  brief = \case
    Con s _ -> (s <>)
    Var s _ -> (s <>)
    x :$ y -> ('(':) . brief x . (' ':) . brief y . (')':)
    Lam s t -> ("(\\"<>) . brief s . (". "<>) . brief t . (')':)
  briefThm (a :|- w) = foldr (.) id ((("  "<>) .) . brief <$> a) . (" |- "<>) . brief w
  briefGoal (a :?- w) = foldr (.) id (briefThm . snd <$> a) . (" ?- "<>) . brief w
  
  instance Show GoalTree where
    show (Nd (s, _) ks) = s <> show ks
    show (Lf e) = either show show e
  
  data GoalPos = Loc
    { content :: GoalTree
    , before :: [GoalTree]
    , after :: [GoalTree]
    , parents :: [([GoalTree], Crumb, [GoalTree])]
    }
  
  forest loc = foldl (flip (:)) (content loc : after loc) (before loc)
  
  parent loc = case parents loc of
    [] -> Nothing
    (ls,a,rs):ps -> Just Loc
      { content = Nd a (forest loc)
      , before = ls
      , after = rs
      , parents = ps
      }
  
  nextTree loc = case after loc of
    [] -> Nothing
    (a:as) -> Just Loc
      { content = a
      , before = content loc:before loc
      , after = as
      , parents = parents loc
      }
  
  firstChild loc = case content loc of
    Lf _ -> Nothing
    Nd a (k:ks) -> Just $ Loc
      { content = k
      , before = []
      , after = ks
      , parents = (before loc, a, after loc):parents loc
      }
  
  replace loc t = loc { content = t }
  
  root loc = maybe loc root $ parent loc
  
  fromTree t = Loc t [] [] []
  
  firstLeaf loc = maybe loc firstLeaf $ firstChild loc
  
  nextLeaf loc = firstLeaf <$> go loc where
    go l = nextTree l <|> (go =<< parent l)
  
  leaves t = unfoldr ((\l -> (l, nextLeaf l)) <$>) $ Just $ firstLeaf $ fromTree t
  
  goals = filter (\loc -> isGoal $ content loc) . leaves where
    isGoal (Lf (Left _)) = True
    isGoal _ = False
  \end{code}
  
  We define the zero and one of tactics. The `noTac` tactic always fails, while
  `idTac` turns a given `Goal` into a singleton `GoalTree`.
  
  \begin{code}
  noTac _ = Left "noTac"
  idTac g = Right $ Lf $ Left g
  \end{code}
  
  We write code that carries out the above. We create a singleton `GoalTree`
  consisting of a goal with no hypotheses and conclusion equal to a given term,
  then try to turn it into a theorem with a given tactic.
  
  While the module system forces us to stick to the rules of inference,
  nothing prevents a tactic proving a different theorem to the one we desire.
  We must check for this.
  
  \begin{code}
  prove :: Hol -> Tactic -> Either String Thm
  prove t tac
    | B <- typeOf t = do
      th <- justify =<< by tac =<< idTac ([] :?- t)
      if t == concl th && null (hyp th)
        then Right th
        else Left $ "prove: wrong theorem: " <> flip briefThm "" th
    | otherwise = Left "non-boolean goal"
  
  tackle tac loc = case content loc of
    Lf (Left g) -> replace loc <$> tac g
    _ -> Left "want goal"
  
  by tac tr = case goals tr of
    [] -> Left "no goals"
    (gLoc:_) -> content . root <$> tackle tac gLoc
  
  justify :: GoalTree -> Either String Thm
  justify = \case
    Nd (_, ju) kids -> ju <$> mapM justify kids
    Lf (Right th) -> Right th
    _ -> Left "unsolved goal"
  \end{code}
  
  Now for some tactics. Given a `Goal`, we may already have a `Thm` that proves
  it, yielding an elementary tactic. This `acceptTac` tactic is meant to be used
  with theorems with no hypotheses.
  
  \begin{code}
  on1 f [th1] = f th1
  on2 f [th1, th2] = f th1 th2
  
  acceptTac :: Thm -> Tactic
  acceptTac th (_ :?- w) | w == concl th =
    Right $ Nd ("accept", on1 id) [Lf $ Right th]
  acceptTac _ _ = Left "acceptTac failed"
  \end{code}
  
  Any `Goal` of the form $r = r$ can be proved via the `refl` inference rule:
  
  \begin{code}
  reflTac :: Tactic
  reflTac g@(_ :?- _ := r) = acceptTac (refl r) g
  reflTac _ = Left "reflTac failed"
  \end{code}
  
  We check it works:
  
  \begin{code}
  testTac = prove (basic "(^a:Num.a) = (^b.b)") reflTac
  \end{code}
  
  The discharge tactic takes a goal whose conclusion has the form `a \implies b`
  then adds `a` to the hypotheses and changes the conclusion to `b`. The `Crumb`
  function describes how to undo this transformation via the `disch` helper
  defined above.
  
  \begin{code}
  dischTac :: Tactic
  dischTac (asl :?- w) = case w of
    ant :==> c -> Right $ Nd ("==>", on1 $ disch ant)
      [Lf $ Left $ ("", assume ant):asl :?- c]
    Con "~" _ :$ ant -> Right $ Nd ("~", on1 $ notIntro . disch ant)
      [Lf $ Left $ ("", assume ant):asl :?- falso]
    _ -> Left "dischTac failed"
  \end{code}
  
  We define algebraic operations for tactics, which HOL Light calls ORELSE
  and THEN. The expression `t <||> u` tries `t` on a given goal, and then if
  that fails, tries `u`. This operator is associative and `noTac` is an identity,
  hence we have a monoid.
  
  The expression `t <&&> u` tries `t` on a given goal. On success, it then tries
  `u` on every `Goal` in the resulting `GoalTree`, succeeding if and only if
  `u` succeeded every time. This operator is also associative and `idTac` is an
  identity, so again we have a monoid.
  
  Neither operator is commutative, though we find `(<&&>)` distributes over
  `(<||>)` on either side:
  
  ------------------------------------------------------------------------
  a <&&> (b <||> c) = (a <&&> b) <||> (a <&&> c)
  (b <||> c) <&&> a = (b <&&> a) <||> (c <&&> a)
  ------------------------------------------------------------------------
  
  It looks like we have a
  https://en.wikipedia.org/wiki/Near-semiring[near-semiring] with
  (multiplicative) identity that satisfies the distributive law on both sides.
  
  Similar definitions of `(<&&>)` have the same properties. For example, we could
  tweak the meaning so `t <&&> u` succeeds if `u` succeeds on any `Goal`.
  
  \begin{code}
  -- tac1 <||> tac2 = \g -> tac1 g <|> tac2 g
  (<||>) = liftA2 (<|>)
  
  aasum tacs = \g -> asum $ ($ g) <$> tacs
  
  tac1 <&&> tac2 = \g -> allGoals tac2 =<< tac1 g
  
  allGoals :: Tactic -> GoalTree -> Either String GoalTree
  allGoals tac tr = case tr of
    Nd a ks -> Nd a <$> mapM (allGoals tac) ks
    Lf (Right _) -> pure tr
    Lf (Left g) -> tac g
  \end{code}
  
  More tactics:
  
  \begin{code}
  conjTac :: Tactic
  conjTac (asl :?- Con "&" _ :$ l :$ r) = Right $ Nd ("&", \[x, y] -> conj x y)
    $ (Lf . Left) <$> [asl :?- l, asl :?- r]
  conjTac _ = Left "conjTac failed"
  
  anyHyp :: (Thm -> Tactic) -> Tactic
  anyHyp ttac g@(as :?- _) = asum $ (\(_, th) -> ttac th g) <$> as
  
  untilFail tac = (tac <&&> untilFail tac) <||> idTac
  
  selections bs = unfoldr (\(as, bs) -> case bs of
    [] -> Nothing
    b:bt -> Just ((b, as <> bt), (b:as, bt))) ([], bs)
  
  labelTac s th (as :?- w) =
    Right $ Nd ("label", on1 $ proveHyp th) [Lf $ Left $ (s, th):as :?- w]
  
  assumeTac :: Thm -> Tactic
  assumeTac = labelTac ""
  
  deleteHyp :: (Thm -> Tactic) -> Tactic
  deleteHyp ttac (as :?- w) = asum
    [ttac th $ as' :?- w | ((_, th), as') <- selections as]
  
  efqTac :: Thm -> Tactic
  efqTac cth@(_ :|- t) (_ :?- w)
    | t == falso = Right $ Nd ("efq", on1 $ efq w) [Lf $ Right cth]
    | otherwise  = Left "efqTac failed"
  
  disj1Tac (a :?- Con "|" _ :$ l :$ r) = Right
    $ Nd ("disj1", \[th] -> disj1 th r) [Lf $ Left $ a :?- l]
  disj1Tac _ = Left "disj1Tac failed"
  disj2Tac (a :?- Con "|" _ :$ l :$ r) = Right
    $ Nd ("disj2", \[th] -> disj2 l th) [Lf $ Left $ a :?- r]
  disj2Tac _ = Left "disj2Tac failed"
  
  disjCases th0@(_ :|- Con "|" _ :$ l :$ r) th1@(_ :|- lr) th2@(_ :|- lr') | lr == lr' =
    proveHyp (disch r th2) $ proveHyp (disch l th1) $ proveHyp th0 th
    where
    p1 = basic "p1:Bool"
    p2 = basic "p2:Bool"
    p3 = basic "p3:Bool"
    th = inst [(l, p1), (r, p2), (lr, p3)] $ undisch $ undisch
      $ spec p3 $ ePonens (orThm p1 p2) $ assume $ basic "p1 | p2"
  
  disjCasesTac th@(_ :|- Con "|" _ :$ l :$ r) (a :?- w) = Right
    $ Nd ("disjCases", on2 $ disjCases th)
    $ Lf . Left <$> [("", assume l):a :?- w, ("", assume r):a :?- w]
  disjCasesTac _ _ = Left "disjCasesTac failed"
  
  eqTac (a :?- l := r) = Right $ Nd ("eq", on2 impAntisymRule) $ Lf . Left <$> [a :?- l ==> r, a :?- r ==> l]
  eqTac _ = Left "eqTac failed"
  
  ponensTac th@(_ :|- t) (a :?- w) = Right $ Nd ("ponens", on1 $ flip ponens th) [Lf $ Left $ a :?- t ==> w]
  ponensTac _ _ = Left "ponens failed"
  \end{code}
  
  We build a intuitionistic prover, complete for the propositional fragment,
  and which supports quantifiers when the search step is invertible.
  
  \begin{code}
  eqThm c d = inst [(c, basic "a:Bool"), (d, basic "b:Bool")] th
    where Right th = prove (basic "(a<=>b) <=> ((a==>b) & (b==>a))") proper
  
  proper = (rightInvertible <&&> proper)
    <||> anyHyp acceptTac
    <||> acceptTac truth
    <||> anyHyp efqTac
    <||> (deleteHyp leftInvertible <&&> proper)
    -- Irreversible steps:
    <||> (disj1Tac <&&> proper)
    <||> (disj2Tac <&&> proper)
    <||> (deleteHyp vorobev <&&> proper)
    where
    rightInvertible = aasum
      [ conjTac    -- (&)
      , dischTac   -- (==>) (~)
      , eqTac      -- (<=>)
      , genAutoTac -- (!)
      ]
    leftInvertible thm = aasum $ ($ thm) <$>
      [ conjunctly assumeTac  -- (&)
      , disjCasesTac          -- (|)
      , notTac                -- (~)
      , leftEqTac             -- (<=>)
      , revImplTac            -- reversible (==>)
      , chooseAutoTac         -- (?)
      ]
    leftEqTac th@(_ :|- _ :<=> _) = conjunctly ponensTac $ uncurry conj $ eqImpRule th
    leftEqTac _ = const $ Left "leftEqTac failed"
    conjunctly ttac cth = case cth of
      (_ :|- Con "&" _ :$ _ :$ _) ->
        ttac (conjunct1 cth) <&&> ttac (conjunct2 cth)
      _ -> const $ Left "conjunctly"
    revImplTac (_ :|- t@(im@(Con "==>" _) :$ a :$ b)) g@(as :?- w)
      -- a, b, Gam |- w  /  a ==> b, a, Gam |- w
      | a `elem` (concl . snd <$> as) = assumeTac (undisch $ assume t) g
      -- c ==> (d ==> b), Gam |- w  /  (c & d) ==> b, Gam |- w
      | Con "&" _ :$ c :$ d <- a = assumeTac (disch c $ disch d $ proveHyp (conj (assume c) (assume d)) $ undisch $ assume t) g
      -- c ==> b, d ==> b, Gam |- w  /  (c | d) ==> b, Gam |- w
      | Con "|" _ :$ c :$ d <- a = assumeTac (disch c $ ponens (assume t) $ disj1 (assume c) d)
        <&&> assumeTac (disch d $ ponens (assume t) $ disj2 c $ assume d) $ g
  
      -- Rewrite (~) and (<=>) on left side of (==>).
      | Con "~" _ :$ c <- a = assumeTac (ePonens (apThm (apTerm im $ notThm c) b) $ assume t) g
      | c :<=> d <- a = assumeTac (ePonens (apThm (apTerm im $ eqThm c d) b) $ assume t) g
  
    revImplTac _ _ = Left "revImpl failed"
    -- (d ==> b) ==> (c ==> d) |- ((c ==> d) ==> b) ==> (c ==> d)
    vorobev (_ :|- (c :==> d) :==> b) (as :?- w) = Right
      $ Nd ("vorobev", \[th1, th2] -> ponens (disch b th2) $ ponens (assume $ (c ==> d) ==> b)
      $ ponens (disch (d ==> b) th1) $ disch d $ ponens (assume $ (c ==> d) ==> b) $ disch c $ assume d)
      $ Lf . Left <$> [("", assume (d ==> b)):as :?- c ==> d, ("", assume b):as :?- w]
    vorobev _ _ = Left "vorobev failed"
  
  notTac asm@(_ :|- Con "~" _ :$ t) = assumeTac $ ePonens (notThm t) asm
  notTac _ = const $ Left "notTac failed"
  
  -- If tm1 and tm2 are alpha-equivalent:
  --   |- tm1 = tm2
  alpha :: Hol -> Hol -> Thm
  alpha tm1 tm2 = trans (refl tm1) (refl tm2)
  
  mustvsub = (either (error "BUG!") id .) . vsubst
  
  alphaLam v tm@(Lam x t)
    | x == v = tm
    | otherwise = mustLam v $ mustvsub [(v, x)] t
  
  alphaConv v tm = Right $ alpha tm $ alphaLam v tm
  
  genAlphaConv v tm@(Lam _ _) = alphaConv v tm
  genAlphaConv v tm@(f :$ x) = apTerm f <$> alphaConv v x
  
  genTac v@(Var s t) (as :?- w@(Con "!" _ :$ Lam x b))
    | t /= typeOf x = Left "type mismatch"
    | any (elem s . fv) (w:(concl . snd <$> as)) = Left "variable capture"
    | otherwise = Right $ Nd ("gen", on1 $ convRule (genAlphaConv x) . gen v) [Lf $ Left $ as :?- mustvsub [(v, x)] b]
  genTac _ _ = Left "genTac failed"
  
  genAutoTac g@(as :?- w@(Con "!" _ :$ Lam x _)) = genTac x' g where
    x' = variant (foldr union (fv w) $ fv . concl . snd <$> as) x
  genAutoTac _ = Left "genAutoTac failed"
  
  popAssum :: (Thm -> Tactic) -> Tactic
  popAssum ttac (((_, th):as) :?- w) = ttac th (as :?- w)
  popAssum _ _ = Left "popAssum failed"
  
  pinst tyin tmin = inst (second (tsubst tyin) <$> tmin) . instType tyin
  
  choose (v@(Var s t), th1@(_ :|- Con "?" _ :$ ab@(Lam bv bod))) th2 = ponens (ponens th5 th4) th1
    where
    cmb = ab @! v
    pat = mustvsub [(v, bv)] bod
    th3 = convRule betaConv $ assume cmb
    th4 = gen v $ disch cmb $ ponens (disch pat th2) th3
    th5 = pinst [(t, basicType "a")] [(ab, p), (concl th2, q)] pth
    -- pth is |- (!x.p x ==> q) ==> ((?)p ==> q)
    p = basic "p:a->Bool"
    q = basic "q:Bool"
    x1 = convRule (randConv betaConv) $ apThm (defThm "?") p
    x2 = spec q $ undisch $ fst $ eqImpRule x1
    pth = dischAll $ disch (basic "(?) (p:a->Bool)") (undisch x2)
  
  chooseTac (x'@(Var s t)) xth@(_ :|- Con "?" _ :$ Lam x bod) (as :?- w)
    | t == typeOf x, s `notElem` avoid =
      Right $ Nd ("?", undefined) [Lf $ Left $ ("", assume pat):as :?- w]
    | otherwise = Left "chooseTac: invalid variable"
    where
    pat = either (error "BUG!") id $ vsubst [(x', x)] bod
    avoid = foldr (union . fvThm . snd) (union (fv w) (fvThm xth)) as
  
  chooseAutoTac xth@(_ :|- Con "?" _ :$ x :$ _) g@(as :?- w) = chooseTac x' xth g where
    x' = variant (foldr (union . fvThm . snd) (union (fv w) (fvThm xth)) as) x
  chooseAutoTac _ _ = Left "chooseAutoTac failed"
  \end{code}
  
  We can now spend less energy on proving simple theorems:
  
  \begin{code}
  testProper1 = prove (basic "a ==> ~(~a)") proper
  testProper2 = prove (basic "((a ==> b) ==> c) ==> ((a & b) ==> (d | c | b))") proper
  \end{code}
  