Notes on LCF Tactics

by Alex Nelson, 28 November 2015

Basic Structure of LCF Tactics

Prose Description

Working in first-order logic, we have propositions we’d like to prove. When proven, they’re promoted to theorems. For the most part we can think of propositions as just some logical formula.

We want to prove only true statements, it’d be a catastrophe if we somehow allowed false statements into the system. So we should have a type thm to indicate that the proposition is proven true.

A proof for a theorem then amounts to mapping the premises to the conclusion. That is, a function in the metalanguage expecting a list of thm, and will produce a thm. (We can compose proofs, at least in theory, the same way we compose functions.) For this case, the proof is “forced” to prove only true statements…provided the rules of inference are sound.

But…How do we get from an unproven formula to a theorem?

The basic structure of the formula we will be proving is something of the form: p1 ∧ … ∧ pn ⇒ q. Solving such a goal produces a theorem “⊢ p1 ∧ … ∧ pn ⇒ q.”

We would therefore like to transform one goal into a list of subgoals, equipped with a justification function which (given theorems solving each subgoal) produces a theorem solving the original goal we started with.

Observe that there’s a recursive structure here: to solve a goal, we simply transform it into several sub-goals, then solve the sub-goals. What transformations permit such things?

Tactics transform a set of goals plus their justification function, to another set of goals plus a modified justification function. Why do this?

Well, the basic notion is to set up the goal we’d like to prove, then refine the goal using tactics until the list of subgoals is empty. The justification function is modified on each step, working with fewer and fewer subgoal inputs. The final justification function accepts an empty list, and produces the desired formula embodied in a theorem.

Pseudo-Code Implementation

The basic scheme, in pidgin Haskell, is we have logical formulas we’d like to prove. Once proven, they are promoted to logical theorems. We have

formula :: string --- implementation not important for the moment
thm :: formula
proof :: [thm] -> thm

But we have more! In general, if we are trying to prove a formula, then we have a goal we’d like to prove. Sometimes it’s easier to break it up into smaller “sub-goals”, and prove each case. To handle this case, we want our goal to be a list of formulas.

--- So a goal looks like ((premises, formulaWeWantToProve), justification)
goal :: (([formula], formula), proof)
justify :: goal -> proof
justify (_, pf) = pf

consequent :: goal -> formula
consequent ((sub:fm), _) = fm

hypotheses :: goal -> [formula]
hypotheses ((fms:_), _) = fms

Now, the pièce de résistance of the LCF system: tactics. A tactic transforms a goal into a modified goal, usually through transforming the subgoals via some rule of inference, and the tactic “updates” the proof to reflect this.

tactic :: goal -> goal

Sometimes people make the goal :: ([formula], formula) and extract the proof from the tactic.

Observation 1: Inference is Sound. Perhaps this is the greatest strength of the LCF approach, it is trivial to prove the inference rules are sound.

Observation 2: Custom Tactics. Since a tactic is “just” a function, we can write our own custom tactics! This allows us to extend the theorem prover quite a bit for our own needs.

Minutiae

There’s a number of “small problems” and initial questions we may ask, like: how do we turn a tautology into a theorem? What exactly are the rules of inference for this system? And how are they represented? What does a typical tactic “look like” (i.e., in terms of formal logic)? And what is a simple example of a tactic code snippet?

Proof System

We tried to go too quickly over this, not mentioning it at all. The proof system (for, e.g., first-order logic) consists of two rules of inference: modus ponens and universal generalization. It also consists of a number of axioms (or axiom schemas). In pidgin Haskell, we might have something like this:

type Axiom :: formula -> thm

class ProofSystem a_formula where
  type th a_formula
  --- helper function, cosmetic
  conclusion :: th -> String
  --- Rules of Inference
  modusPonens :: th -> th -> th
  generalization :: a_formula -> th -> th
  --- Axioms
  Axiom.truth :: th
  --- snip

instance ProofSystem formula where
  type th formula = thm
  conclusion (thm fm) = fm
  --- Rules of Inference
  modusPonens p pImpliesQ = case pImpliesQ of
                            Implies(p',q) =>
                          | _ => error "Modus Ponens Failure: "++(show pImpliesQ)
  generalization fm t = case fm of
                        Var x => Forall(x,t)
                      | _ => error "Generalization failure: "++(show fm)
  --- Axioms
  Axiom.truth = Iff(True,Implies(False,False))
  --- other axioms not shown for brevity

Ostensibly, if we wanted to be completely general, we could have made ProofSystem accept any list of “rules of inference”:

RuleOfInference :: [formula]->[thm] -> thm

class GeneralizedProofSystem fm where
  type th fm
  inferenceRules :: [[th] -> th]
  axioms :: [[fm] -> th]

We’d need some pre-conditions to make sure that some rule of inference is given, and while we’re at it…we should probably check some axiom is passed in, too.

Rules of Inference

Well, as we’ve seen, we’ve implemented a rule of inference as a mapping from a finite number of thms to a thm, or possible [formula]->[thm]->thm for first-order generalizations.

From this perspective, we could argue that a rule of inference taking no premises is an “axiom” (or “axiom schema”). More or less, our implementation reflects that intuition. It’s a bit hack-ish, since our Axiom has an input (viz., the formula we want recognized as logically valid).

Tactics and Proof Systems?

So, great, this has been a fascinating detour, how do tactics enter the game?

Before getting started, we should remember how to extract a theorem from a goal. Namely, we apply a number of tactics until the goal has no more subgoals to solve, which means we have produced a justification function capable of proving the desired proposition. Or, in code:

extractThm :: goal -> thm
extractThm (([], fm), pf) = pf []
extractThm (unsolvedGoals, _) = error "Unresolved Goals: "++(show unsolvedGoals)

We get things in motion by declaring we want to prove a theorem with a proof. First we must set the goal. As good practice, we set a post condition checking the resulting theorem indeed proves the desired goal. In pidgin code,

setGoal :: formula -> goal
setGoal p = let verifyThm t = if ProofSystem.conclusion t = p
                              then th
                              else error "setGoal postcondition couldn't match '"++
                              (show $ ProofSystem.conclusion t)++
                              "' with '"++
                              (show p)++"'"
            in ([], p, \th -> verifyThm (modusPonens th ProofSystem.Axiom.Truth))
--- where Axiom.Truth refers to the tautology "True"

Now that we’ve turned the proposition we want to prove p into a goal. We have a helper function which solves a goal g by applying the tactics in the justification function:

tacticProof :: goal -> [tactic] -> stuff
tacticProof g tactics = extractThm (foldr (\g' t -> t g') g (reverse tactics))

--- fancy pants version
--- tacticProof' :: goal -> [tactic] -> goal
--- tacticProof' g [] = g
--- tacticProof' g (t:tactics) = t (tacticProof' g tactics)
--- tacticProof = extractThm $ tacticProof'

There is some subtlety here in tacticProof, because I’m nervous about the “gotchas” with fold. What should be happening is, in clojure-esque code, (reduce (fn [transformed-goal tactic-step] (tactic-step transformed-goal)) initial-goal (reverse tactics)).

But still, we need to transform the given proposition (i.e., a formula) into a goal! And we need to be able to prove it! We combine all the helper functions into one:

prove :: formula -> [tactic] -> thm
prove fm prf = tacticProof (setGoal p) prf

Where’s the Beef?

We just went through a rigmarole demonstrating how to turn a formula into a goal and how to turn tactics applied on a goal into a proof. But what was the point of introducing the ProofSystem class?

Truthfully, the proof system we have “developed” is woefully inadequate. We first need to “prove a few metatheorems” (construct a few helper functions) before we can start blasting away. Since the intricacies behind this is rather dull and boring, I will assume we have constructed a number of such “helper functions”. Namely, we have

--- "p implies q" and "q implies r" gives us "p implies r"
impl_transitivity :: thm -> thm -> thm

--- "p implies q[i]" for i=1, ..., n AND "q[1] implies q[2]
--- implies... implies q[n] implies r" gives us "p implies r"
impl_transitivity_chain :: [thm] -> thm -> thm

So, now we can get to tactics. Arguably, tactics are just “natural deduction in reverse” (which gives credence to the reverse in the clojure-pseudocode above). What does this mean? In natural deduction, we have And-introduction be the following rule of inference (in pseudo-code)

[Implies(Ctxt, p), Implies(Ctxt, q)] ⊢ Implies(Ctxt, And(p,q))

The corresponding tactic will break down And(p,q) into two subgoals: p and q. We also need to “update” the justification function when considering this “tactic transformation”. The original justification expected something like ⊢ Implies(a, And(p,q)), but now should be transformed into something expecting two theorems: ⊢ Implies(a,p) and ⊢ Implies(a,q). The pidgin code for this would be:

--- first tactic!
and_intro :: tactic
and_intro (((assumption1, And(p,q)):gls), jfn) =
  let jfn' (thm_p:thm_q:thms) = jfn (impl_transitivity_chain [thm_p, thm_q]
                                     (thm (And(p,q)))):thms
  in ((assumption1, p):(assumption1, q):gls, jfn')

So we see the generic tactic in action: transform the first goal, without changing the total number. In this particular case (when the number of goals remains invariant), we have an idiomatic construct modifying the justification function:

--- modifies inputs to the justification function
modify_jfn' :: (thm -> proof) -> [thm] -> [thm]
modify_jfn' tfn (th:others) = (tfn th):others
--- modifies the justification function to expect modified inputs
modify_jfn :: proof -> (thm -> proof) -> proof
modify_jfn jfn tfn = jfn $ modify_jfn' tfn

Punchline. The LCF tactics amount to “natural deduction in reverse”, which thus requires having a proof system (equipped with adequate helper functions). This brings us round-circle to where we started.

As A Monoid of Endofunctors on a Symmetric Monoidal Category

Observe that tactics can be thought of as transforming goals, and goals can be thought of as ordered pairs ([formula], formula). The second term is there only as a post-condition, i.e., for coding purposes only (quality control). So really a goal can be thought of as [formula].

Tactics then transform goals into goals. Great, so how are we going to categorify this?

Consider propositional logic for simplicity. The category consists of formulas as objects, and morphisms map one logically equivalent formula into another. So it’s a groupoid. But there’s more: we have a tensor product! What is it?

Well, for us, it’s a fancy-pants way of saying “We can form lists of formulas, and the ordering doesn’t matter.” In other words, we have turned goals into a symmetric monoidal groupoid.

What does a tactic do? It transforms one goal into another, if possible. If not, for the sake of completeness (it has to be “everywhere defined”), it acts like the identity functor.

A sequence of tactics then progressively “proves” a theorem, giving us some program which will act on the empty list of premises and produce the desired formula as a result. This is composing functors!

So the tactic functors’ “flows” from the empty goal (the initial object) describe proofs, and any proposition hit by this flow is “provable”.

Modern Developments

Custom Tactics

One of the disadvantages of writing our own custom tactics is…we have to recompile the entire program from scratch. That’s quite a bummer for a sophisticated prover like Isabelle, since it can take a few minutes on modern computers. (And a bit longer on, say, an 800MHz Pentium III machine.)

Coq has a beautiful solution: have tactics be part of the user-defined language. (Aside from a small core, that is.) In this manner, tactics are like “macros” which are expanded later on.

Declarative Proofs

One of the major disadvantages of the “vanilla” LCF system is the proofs are unreadable by humans. For example:

Lemma canonical_forms_bool : forall t,
  empty ⊢ t ∈ TBool ->
  value t ->
  (t = ttrue) \/ (t = tfalse).
Proof.
  intros t HT HVal.
  inversion HVal; intros; subst; try inversion HT; auto.
Qed.

Lemma canonical_forms_fun : forall t T1 T2,
  empty ⊢ t ∈ (TArrow T1 T2) ->
  value t ->
  exists x u, t = tabs x T1 u.
Proof.
  intros t T1 T2 HT HVal.
  inversion HVal; intros; subst; try inversion HT; subst; auto.
  ∃x0. ∃t0. auto.
Qed.

The alternative style for automated provers is declarative proofs. This more closely resembles how mathematicians write a proof. For example:

theorem Th2:
 ex x, y st x is irrational & y is irrational &
  x.^.y is rational
proof
 set w = sqrt 2;
A1: w is irrational by INT_2:44,Th1;
 w>0 by AXIOMS:22,SQUARE_1:84;
 then
A2: (w.^.w).^.w = w.^.(w * w) by POWER:38
  .= w.^.(w^2) by SQUARE_1:def 3
  .= w.^.2 by SQUARE_1:def 4
  .= w^2 by POWER:53
  .= 2 by SQUARE_1:def 4;
 per cases;
 suppose
A3: w.^.w is rational;
  take w, w;
  thus thesis by A1,A3;
 suppose
A4: w.^.w is irrational;
  take w.^.w, w;
  thus thesis by A1,A2,A4,RAT_1:7;
end;

We can get the best of both worlds by creating “declarative tactics” (c.f., Harrison’s paper and Wiedijk’s paper).

Conclusion

So, we’ve introduced the basic idea behind LCF, specifically tactics and goals. Its soundness is quite simple to prove (it’s a “Look!” type proof).

We’ve looked at one pseudo-specification in pidgin Haskell, discussed recent developments, and undoubtedly have missed quite a few recent developments and open research projects.

References

Historical Documents