Tactics and Automation

Nuprl uses tactics to automate parts of the proof development process. A tactic is a function that builds part of a proof; it is given a sequent, and it produces a proof whose goal is the sequent. The resulting proof might be incomplete (usually is), and it might not be possible to complete it if the approach is a dead end.

The general idea of tactic-oriented theorem proving was pioneered by Edinburgh LCF [25]. Nuprl has extended this method by introducing the concept of a tactic-tree and by introducing the concept of a transformation tactic. We will not discuss the later idea.

The idea of a tactic-tree is that a justification for a proof step can be a tactic. The subproof built is not displayed, but the frontier of the subproof is listed as the new subgoals to be proved. This makes the tactic look like a new proof rule. So, by writing tactics, users extend the logic, but in a totally $sa\!f\!e$ way. The tactics actually build primitive proofs, so there is no increase in the axiomatic basis of the theory. When a proof is complete, there is a primitive proof built in the background.

Here is an example of the internal proof produced by a tactic called ChainThruHyps.

$$A\Rightarrow B_1 B_1\Rightarrow B_2 B_2\Rightarrow B_3$$

$\vdash A\Rightarrow B_3$ by ChainThruHyps

4.A $\vdash B_3$ by D1 $\vdash A$ by Hyp

5.B₁ $\vdash B_3$ by D2 $\vdash B_1$ by Hyp

6.B₂ $\vdash B_3$ by D3 $\vdash B_2$ by Hyp

7.B₃ $\vdash B_3$ by Hyp

The rule used in chaining is

$$H, f:A\Rightarrow B, H'\vdash G by D f H, f:A\Rightarrow B, H'\vdash A H, f:A\Rightarrow B, H', B\vdash G$$

The more conventional form is

$$\frac{H\vdash A H, A\Rightarrow B, B\vdash G}{H, A\Rightarrow B\vdash G}$$