HOL Proof Tactics

We build a intuitionistic logic theorem prover with our version of HOL Light.

The original HOL Light version uses a different algorithm. Like a previous prover, for implications, we use a technique described by Dyckhoff, "Contraction free sequent calculi for intuistionistic logic".

{-# 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

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.

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

We check our definitions actually parse:

testBasic = putStr . unlines . map show $ basicAxioms

Some utilities to produce theorems from given theorems and the basic axioms:

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)

A sanity check. We prove ${x} \vdash x = T$ ("assuming x, x is true").

testEqt = eqtIntro $ assume $ basic "x:Bool"

A Conv tries to convert a term into a theorem.

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

These functions help us prove obvious theorems:

testSpec = spec (basic "f:(Num->Num) z:Num") (assume $ basic "!x:Num.(x = y)")

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.

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

Functions for printing goals, and for navigating the tree:

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

We define the zero and one of tactics. The noTac tactic always fails, while idTac turns a given Goal into a singleton GoalTree.

noTac _ = Left "noTac"
idTac g = Right $ Lf $ Left g

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.

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"

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.

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"

Any Goal of the form $r = r$ can be proved via the refl inference rule:

reflTac :: Tactic
reflTac g@(_ :?- _ := r) = acceptTac (refl r) g
reflTac _ = Left "reflTac failed"

We check it works:

testTac = prove (basic "(^a:Num.a) = (^b.b)") reflTac

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.

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"

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

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

More tactics:

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"

We build a intuitionistic prover, complete for the propositional fragment, and which supports quantifiers when the search step is invertible.

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"

We can now spend less energy on proving simple theorems:

testProper1 = prove (basic "a ==> ~(~a)") proper
testProper2 = prove (basic "((a ==> b) ==> c) ==> ((a & b) ==> (d | c | b))") proper

Ben Lynn blynn@cs.stanford.edu 💡

HOL Proof Tactics

Tactics

Contents