Notes on LCF Tactics
by Alex Nelson, 28 November 2015
Basic Structure of LCF Tactics
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
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
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.
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
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.
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?
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
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
(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
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
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 implies q --- 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
And-introduction be the following rule of inference (in
[Implies(Ctxt, p), Implies(Ctxt, q)] ⊢ Implies(Ctxt, And(p,q))
The corresponding tactic will break down
And(p,q) into two subgoals:
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
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”.
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.
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).
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.
- John Harrison, Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009. See chapter 6 especially.
- John Sterling, Modernized LCF
- Andrea Asperti’s talk A New Type For Tactics at PLLMS 2009.
- Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti, Coen Enrico Tassi, A new type for tactics.
- CStheory.stackexchange thread How do ‘tactics’ work in proof assistants?
- Lawrence Paulson, LCF + Logical Frameworks = Isabelle (25 Years Later) Talk at Milner Symposium, 16 April 2012.
- Robin Milner, Logic for Computable Functions: description of a machine implementation (1972)