# 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: *p*_{1} ∧ … ∧ *p*_{n} ⇒ *q*. Solving
such a goal produces a theorem “⊢ *p*_{1} ∧ … ∧ *p*_{n} ⇒ *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 `thm`

s 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

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

## Historical Documents

- Robin Milner, Logic for Computable Functions: description of a machine implementation (1972)