Tactic-tree Proofs

Tactic-tree proofs are just proofs which allow tactic applications as justifications. Since they can be reduced to primitive proofs by executing the tactic, one might think that it is not necessary to give a reflected account of them. But there are reasons for reflecting.

The first reason is that we want to provide a theoretical basis for the idea that if we prove that the tactic works, then we can treat it as a new proof rule. This will both raise the level of abstraction of proofs and save the resources involved with executing the tactic call. Doing this requires that we have a formal definition of a tactic-tree proof since it is exactly objects in this class which will serve as the more abstract proofs.

A second reason to formalize the concept is that we wish to provide a rigorous account of what Nuprl actually does. This account will be a formal explanation of the system. This second reason influences the way we formalize the concept.

A very interesting problem arises as soon as we try to formalize tactic trees because we are now entering the realm of self-reference. A tactic is a Nuprl function, so it must operate on some internal data type, something we will eventually call Proof. But we use the tactic in explaining the top level notion of proof, the concept we have been denoting as $proo\!f$. This concept does not even make sense until we have said how Proof represents $proo\!f$. This involves some level of reflection already.

If we are at a node with sequent s₀ whose subgoals are generated by t as justification, this means that t(s₀) is Proof and the frontier of t(s₀), say $s_1. \ldots, s_n$ represent the sequents which are subgoals of s₀. This would suggest that justifications are

1 + primitive__rules + Proof

In actual practice, we do not write a function application as a justification. We care about the exact computational behavior of the algorithm, so we really write a term t which denotes a function    (Sequent $\rightarrow$ Proof). Since we want to analyze the term, it is more useful, if somewhat more complex, to use an element from Term.

We spell this out precisely using these abbreviations. Let the premises of a proof be the unproven sequents at the leaves, the frontier of the proof tree. Given this frontier of sequents, let $\bar{p}_{1\ldots n}$ denote the sequence of them. Given a proof p, let root(p) be the root of the tree, which is the main goal or the theorem being proved. If j is a proof rule, then let $instance(j, s, roots(\bar{p}_{1\ldots n}))$ be a predicate that checks that the roots of the subtrees $\bar{p}_{1\ldots n}$ are the correct subgoals generated from s by j. Finally we use the relation j reps x to mean that the term j $represents the pre\!\!-\!\!proo\!f x$.

When we write these concepts in bold letters,

$$(j, s, {\bf roots}(x))$$

they apply to the internal notion of proof, Proof.

Now we have these definitions.

Definition

$$\times \times$$

$$is\_a\_proo\!f(<s, j, \bar{p}_1\ldots n\gt)=$$

Tactic-tree Diagram

$$<s, j, [P_1, \ldots, P_n]\gt$$

$$\bigtriangleup s_l\ldots s_n \vdots$$

Tactic-trees Internally

Definition

PreProof == rec(PP. Sequent $\times$ Justification $\times$ PP list)

Justification == 1 + Rule + Term

Proof == $\{p:{\sf PreProof} \vert$IsAProof$(p)\}$ where

$$(<S, J, [P_1, \ldots, P_n]\gt) =$$

Note the internal Reps map.