Goal Directed Proof: Tactics and Tacticals
There are three primary devices that together make theorem proving practical in HOL. All three originate with Milner for Edinburgh LCF. The first is the theory as a record of (among other things) facts already proved and thence available as lemmas without having to be re-proved. The second, the subject of Chapter 2, is the derived rule of inference as a meta-language procedure that implements a broad pattern of inference, but that also, at each application, generates every primitive step of the proof. The third device is the tactic as a means of organizing the construction of proofs; and the use of tacticals for composing tactics.
Even with recourse to derived inference rules, it is still surprisingly awkward to work forward,
to find a chain of theorems that culminates in a desired theorem.
This is in part because chains have no structure, while “proof efforts” do.
For instance, if within one sequence, two chains of steps are to be combined in the end by conjunction, then one chain must follow or be interspersed with the other in the overall sequence.
It can also be difficult to direct the proof toward its object when starting from only hypotheses (if any), lemmas (if any), axioms, and theorems following from no hypotheses (e.g., by ASSUME or REFL).
Likewise, it can be equally difficult to reconstruct the plan of the proof effort after the fact, from the linear sequence of theorems; the sequence is unhelpful as documentation.
The idea of goal directed proof is a simple one, well known in artificial intelligence: to organize the search as a tree, and to reverse the process and begin with the objective. The goal is then decomposed, successively if necessary, into what one hopes are more tractable subgoals, each decomposition accompanied by a plan for translating the solution of subgoals into a solution of the goal. The choice of decomposition is an explicit way of expressing a proof “strategy”.
Thus, for example, instead of the linear sequencing of two branches of the proof of the conjunction, each branch starting from scratch, the proof task is organized as a tree search, starting with a conjunctive goal and decomposing it into the two conjunct subgoals (undertaken in optional order), with the intention of conjoining the two solutions when and if found. The proof itself, as a sequence of steps, is the same however it is found; the difference is in the search, and in the preservation, if required, of the structured proof plan.
The representation of this idea in LCF was Milner's inspiration; the idea is similarly central to theorem proving in HOL. Although subgoaling theorem provers had already been built at the time, Milner's particular contribution was in formalizing the method for translating subgoals solutions to solutions of goals.
Tactics, Goals and Validations
A tactic
is an ML function that when applied to a goal
reduces it to (i) a list of (sub)goals, along with (ii) a validation
function mapping a list of theorems to a theorem.
The idea is that this function justifies the decomposition of the goal, and so it is also known as a justification.
A goal is an ML value whose type is isomorphic to, but distinct from, the ML abstract type thm of theorems.
That is, a goal is a list of terms (assumptions)
paired with a term.
These two components correspond, respectively, to the list of hypotheses and the conclusion of a theorem.
The list of assumptions is a working record of facts that may be used in decomposing the goal.
The relation of theorems to goals is achievement: a theorem achieves a goal if the conclusion of the theorem is equal to the term part of the goal (up to $\alpha$-conversion), and if each hypothesis of the theorem is equal (up to $\alpha$-conversion, again) to some assumption of the goal. This definition assures that the theorem purporting to satisfy a goal does not depend on assumptions beyond the working assumptions of the goal.
A tactic is said to solve
a goal if it reduces the goal to the empty set of subgoals.
This depends, obviously, on there being at least one tactic that maps a goal to the empty subgoal list.
The simplest tactic that does this is one that can recognize when a goal is achieved by an axiom or an existing theorem; in HOL, the function ACCEPT_TAC
does this.
ACCEPT_TAC takes a theorem $\mathit{th}$ and produces a tactic that maps a value of type thm to the empty list of subgoals.
It justifies this “decomposition” by a validation function that maps the empty list of theorems to the theorem $\mathit{th}$.
The use of this technical device, or other such tactics, ends the decomposition of subgoals, and allows the proof to be built up.
Unlike theorems, goals need not be defined as an abstract type; they are transparent and can be constructed freely. Thus, an ML type abbreviation is introduced for goals. The operations on goals are therefore just the ordinary pair selectors and constructor. Likewise, type abbreviations are introduced for validations and tactics. Conceptually, the following abbreviations are made in HOL:
goal = term list * term
tactic = goal -> goal list * validation
validation = thm list -> thm
It does not follow, of course, from the type tactic that a particular tactic is well-behaved.
For example, suppose that $T\ g$ = ([$g_1$,$\dots$,$g_n$],$v$), and that the subgoals $g_1$, $\dots$, $g_n$ have been solved.
That means that some theorems $\mathit{th}_1$, $\dots$, $\mathit{th}_n$ have been proved such that each $\mathit{th}_i$ ($1 \leq i \leq n$) achieves the goal $g_i$.
The validation $v$ is intended to be a function that when applied to the list [$\mathit{th}_1$,$\dots$,$\mathit{th}_n$], succeeds in returning a theorem, $\mathit{th}$, achieving the original goal $g$; but, of course, it might sometimes not succeed.
If $v$ succeeds for every list of achieving theorems, then the tactic $T$ is said to be valid.
This does not guarantee, however, that the subgoals are solvable in the first place.
If, in addition to being valid, a tactic always produces solvable subgoals from a solvable goal, it is called strongly valid.
Tactics can be perfectly useful without being strongly valid, or without even being valid; in fact, some of the most basic theorem proving strategies, expressed as tactics, are invalid or not strongly valid. An invalid tactic cannot result in the proof of false theorems; theorems in HOL are always the result of performing a proof in the basic logic, whether the proof is found by goal directed search or forward search. However, an invalid tactic may produce an unintended theorem — one that does not achieve the original goal. The typical case is when a theorem purporting to achieve a goal actually depends on hypotheses that extend beyond the assumptions of the goal. The inconvenience to the HOL user in this case is that the problem may be not immediately obvious; the default print format of theorems has hypotheses abbreviated as dots. Invalidity may also be the result of the failure of the proof function, in the ML sense of failure, when applied to a list of theorems (if, for example, the function were defined incorrectly); but again, no false theorems can result. Likewise, a tactic that is not strongly valid cannot result in a false theorem; the worst outcome of applying such a tactic is the production of unsolvable subgoals.
Tactics are specified using the following notation:
$$ \dfrac{\mathit{goal}} {\mathit{goal}_1\quad\mathit{goal}_2\quad\dots\quad\mathit{goal}_n} $$
For example, the tactic for decomposing conjunctions into two conjunct subgoals is called conj_tac.
(The tactic is also available under the name CONJ_TAC.)
It is described by:
$$ \dfrac{t_1\;\land\;t_2}{t_1\qquad t_2} $$
This indicates that conj_tac reduces a goal of the form ($\Gamma$,$t_1$/\$t_2$) to subgoals ($\Gamma$,$t_1$) and ($\Gamma$,$t_2$).
The fact that the assumptions of the original goal are propagated unchanged to the two subgoals is indicated by the absence of assumptions in the notation.
The notation gives no indication of the proof function.
Another example is numLib.INDUCT_TAC, a low-level tactic for performing mathematical induction on the natural numbers:
$$ \dfrac{\forall n.\;t[n]}{t[\mathtt{0}]\qquad \{t[n]\}\;t[\mathtt{SUC}\;n]} $$
Thus, INDUCT_TAC reduces a goal of the form ($\Gamma,\forall n.\;t[n]$) to a basis subgoal ($\Gamma$,$t[$0$]$) and an induction step subgoal ($\Gamma\cup\{t[n]\}$,$t[$SUC $n]$).
The induction assumption is indicated in the tactic notation with set brackets.
Tactics fail
(in the ML sense) if they are applied to inappropriate goals.
For example, conj_tac will fail if it is applied to a goal whose conclusion is not a conjunction.
Some tactics never fail; for example
all_tac
$$ \dfrac{t}{t} $$
is the identity tactic;
it reduces a goal ($\Gamma$,$t$) to the single subgoal ($\Gamma$,$t$) — i.e., it has no effect.
The all_tac tactic is useful for writing compound tactics, as discussed later (see §Tacticals).
In just the way that the derived rule REWRITE_RULE
can be used in forward proof, the corresponding tactic rewrite_tac
can be used in goal-directed proof.
Given a goal and a list of equational theorems, rewrite_tac transforms the term component of the goal by applying the equations as left-to-right rewrites, recursively and to all depths, until no more changes can be made.
Unless not required, the function includes as rewrites the same standard set of pre-proved tautologies
that REWRITE_RULE uses.
By use of the tautologies, some subgoals can be solved internally by rewriting, and in that case, an empty list of subgoals is returned.
The transformation of the goal is justified in each case by the appropriate chain of inferences.
Rewriting is a simple implementation of an extremely powerful idea.
The more sophisticated simplification functions (e.g., simp) often do a very large share of the work in goal directed proof searches.
A simple example from list theory illustrates the use of tactics.
A conjunctive goal is declared, and conj_tac applied to it:
> val gl0 = ([]:term list,``(HD[1;2;3] = 1) /\ (TL[1;2;3] = [2;3])``);
val gl0 = ([], “HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]”):
term list * term
> val (gl1,p1) = conj_tac gl0;
val gl1 =
[([], “HD [1; 2; 3] = 1”), ([], “TL [1; 2; 3] = [2; 3]”)]:
goal list
val p1 = fn: validation
The subgoals are each rewritten, using the definitions of HD and TL:
> open listTheory; ... output elided ...
> HD;
val it = ⊢ ∀h t. HD (h::t) = h: thm
> TL;
val it = ⊢ ∀h t. TL (h::t) = t: thm
> val (gl1_1,p1_1) = rewrite_tac[HD,TL](hd gl1);
val gl1_1 = []: goal list
val p1_1 = fn: validation
> val (gl1_2,p1_2) = rewrite_tac[HD,TL](hd(tl gl1));
val gl1_2 = []: goal list
val p1_2 = fn: validation
Both of the two subgoals are now solved, so the decomposition is complete and the proof can be built up in stages. First the theorems achieving the subgoals are proved, then from those, the theorem achieving the original goal:
> val th1 = p1_1[];
val th1 = ⊢ HD [1; 2; 3] = 1: thm
> val th2 = p1_2[];
val th2 = ⊢ TL [1; 2; 3] = [2; 3]: thm
> p1[th1,th2];
val it = ⊢ HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]: thm
Although only the theorems achieving the subgoals are “seen” here, the proof functions of the three tactic applications together perform the entire chain
of inferences leading to the theorem achieving the goal.
The same proof could be constructed by forward search, starting from the definitions of HD and TL, but not nearly as easily.
The HOL system provides a very large collection of pre-defined tactics that includes conj_tac, INDUCT_TAC, all_tac and rewrite_tac.
The pre-defined tactics are adequate for many applications.
In addition, there are two means of defining new tactics.
Since a tactic
is an ML function, the user can define a new tactic directly in ML.
Definitions of this sort use ML functions to construct the term part of the subgoals from the term part of the original goal (if any transformation is required); and they specify the justification, which expects a list of theorems achieving the subgoals and returns the theorem achieving (one hopes) the goal.
The proof of the theorem is encoded in the definition of the justification function; that is, the means for deriving the desired theorem from the theorems given.
This typically involves references to axioms and primitive and defined inference rules, and is usually the more difficult part of the project.
A simple example of a tactic written in ML
is afforded by conj_tac, whose definition in HOL is as follows:
fun conj_tac (asl,w) =
let val (l,r) = dest_conj w
in
([(asl,l), (asl,r)], (fn [th1, th2] => CONJ th1 th2))
end
This shows how the subgoals are constructed, and how the proof function is specified in terms of the derived rule CONJ.
The second method is to compose
existing tactics by the use of ML functions called tacticals.
The tacticals provided in HOL are listed in §Tacticals.
For example, two existing tactics can be sequenced
by use of the tactical >> (the function can also be written as THEN or as \\):
if $T_1$ and $T_2$ are tactics, then the ML expression $T_1$ >> $T_2$ evaluates to a tactic that first applies $T_1$ to a goal and then applies $T_2$ to each subgoal produced by $T_1$.
The tactical >> is an infixed ML function.
Complex and powerful tactics can be constructed in this way; and new tacticals can also be defined, although this is unusual.
The example from earlier is continued, to illustrate the use of the tactical >>:
> val (gl2,p2) = (conj_tac >> rewrite_tac [HD, TL]) gl0;
val gl2 = []: goal list
val p2 = fn: thm list -> thm
> p2 [];
val it = ⊢ HD [1; 2; 3] = 1 ∧ TL [1; 2; 3] = [2; 3]: thm
The single tactic conj_tac >> rewrite_tac[HD;TL] solves the goal in one single application.
The chain of inference computed, however, is exactly the same as in the interactive proof; only the search is different.
In general, the second method is both easier and more reliable. It is easier because it does not involve writing ML procedures (usually rather complicated procedures); and more reliable because the composed tactics are valid when the constituent tactics are valid, as a consequence of the way the tacticals are defined. Tactics written directly in ML may fail in a variety of ways, and although, as usual, they cannot cause false theorems to appear, the failures can be difficult to understand and trace. On the other hand, there are some proof strategies that cannot be implemented as compositions of existing tactics, and these have to be implemented directly in ML. Certain sorts of inductions are an example of this; as well as tactics to support some personal styles of proof.
Either sort of tactic can be difficult to apply by hand, as shown in the examples above. There can be a lot of book-keeping required to support such an activity. For this reason, most interactive theorem-proving uses the subgoal or goalstack package.
Some Tactics Built into HOL
This section contains a selection of the more commonly used tactics in the HOL system. (See §REFERENCE for the complete list, with fuller explanations.)
It should be recalled that the ML type thm_tactic abbreviates thm->tactic, and the type conv abbreviates term->thm.
Specialization
gen_tac : tactic
Summary: Specializes a universally quantified theorem to an arbitrary value.
Also available under the name GEN_TAC.
$$ \dfrac{\forall x.\,t[x]}{t[x']} $$
where $x'$ is a variant of $x$ not free in either goal or assumptions.
Use: Solving universally quantified goals.
gen_tac is often the first step of a goal directed proof.
strip_tac (see below) applies gen_tac to universally quantified goals.
Conjunction
conj_tac : tactic
Summary: Splits a goal $t_1\land t_2$ into two subgoals, $t_1$ and $t_2$.
$$ \dfrac{t_1\;\land\;t_2}{t_1\qquad t_2} $$
Use: Solving conjunctive goals.
conj_tac is also invoked by strip_tac (see below).
Combined simple decompositions
strip_tac : tactic
Summary: Breaks a goal apart.
The tactic strip_tac removes one outer connective from the goal, using conj_tac, gen_tac, and other tactics.
If the goal has the form $t_1\land \cdots \land t_n$ ==> $t$ then strip_tac makes each $t_i$ into a separate assumption.
Use: Useful for splitting a goal up into manageable pieces.
Often the best thing to do first is rpt strip_tac, where rpt is the tactical that repeatedly applies a tactic until it fails (see §Repetition).
Case analysis
Cases_on : term quotation -> tactic
Summary: Cases_on $q$, where $q$ is a quotation denoting a term of an algebraic type (e.g., booleans, lists, natural numbers, types defined by the user with Datatype), does case analysis on that term.
Let the relevant type have $m$ constructors $\mathsf{C}_1$ to $\mathsf{C}_m$, where $\mathsf{C}_i$ has $n_i$ arguments.
If the term is a variable, then the variable is substituted out of the goal entirely:
$$ \dfrac{t}{t[q := \mathsf{C}_1\,a_{11}\cdots a_{1n_1}]\quad\cdots\quad t[q := \mathsf{C}_m\,a_{m1}\cdots a_{mn_m}]} $$
If the term denoted by $q$ is not simply a variable (e.g., Cases_on `n + 1` ), then fresh assumptions are introduced:
$$ \dfrac{t}{\{q = \mathsf{C}_1\,a_{11}\cdots a_{1n_1}\}t\quad\cdots\quad\{q = \mathsf{C}_m\,a_{m1}\cdots a_{mn_m}\}t} $$
Use: Case analysis.
Rewriting
rewrite_tac : thm list -> tactic
Summary: rewrite_tac[$\mathit{th}_1$,$\dots$,$\mathit{th}_n$] transforms the term part of a goal by rewriting it with the given theorems $\mathit{th}_1$, $\dots$, $\mathit{th}_n$, and the set of pre-proved standard tautologies.
Also written REWRITE_TAC.
$$ \dfrac{\{t_1, \ldots, t_m\}t}{\{t_1, \ldots, t_m\}t'} $$
where $t'$ is obtained from $t$ as described.
Use: Advancing goals by using definitions and previously proved theorems.
Other rewriting tactics (based on rewrite_tac) are:
-
asm_rewrite_tacadds the assumptions of the goal to the list of theorems used for rewriting. Also writtenASM_REWRITE_TAC.
PURE_ASM_REWRITE_TAC is like asm_rewrite_tac, but it doesn't use any built-in rewrites.
PURE_REWRITE_TAC uses neither the assumptions nor the built-in rewrites.
FILTER_ASM_REWRITE_TAC $p$ [$\mathit{th}_1$,$\dots$,$\mathit{th}_n$] simplifies the goal by rewriting it with the explicitly given theorems $\mathit{th}_1$, $\dots$, $\mathit{th}_n$, together with those assumptions of the goal which satisfy the predicate $p$ and also the standard rewrites.
See also the more powerful simplification tactics described in the simplifier chapter.
Resolution by Modus Ponens
imp_res_tac : thm -> tactic
Summary: imp_res_tac $\mathit{th}$ does a limited amount of automated theorem proving in the form of forward inference; it “resolves” the theorem $\mathit{th}$ with the assumptions of the goal and adds any new results to the assumptions.
The specification for imp_res_tac is:
$$ \dfrac{\{t_1,\ldots,t_m\}t}{\{t_1,\ldots,t_m,u_1,\ldots,u_n\}t} $$
where $u_1$, $\dots$, $u_n$ are derived by “resolving” the theorem $\mathit{th}$ with the existing assumptions $t_1$, $\dots$, $t_m$. Resolution in HOL is not classical resolution, but just Modus Ponens with one-way pattern matching (not unification) and term and type instantiation. The general case is where $\mathit{th}$ is of the canonical form
$$ \vdash \forall x_1\ldots x_p.\;v_1\Rightarrow v_2\Rightarrow\ldots\Rightarrow v_q\Rightarrow v $$
imp_res_tac $\mathit{th}$ then tries to specialize $x_1$, $\dots$, $x_p$ in succession so that $v_1$, $\dots$, $v_q$ match members of $\{t_1,\ldots,t_m\}$.
Each time a match is found for some antecedent $v_i$, for $i$ successively equal to $1$, $2$, $\dots$, $q$, a term and type instantiation is made and the rule of Modus Ponens is applied.
If all the antecedents $v_i$ (for $1 \leq i \leq q$) can be dismissed in this way, then the appropriate instance of $v$ is added to the assumptions.
Otherwise, if only some initial sequence $v_1$, $\dots$, $v_k$ (for some $k$ where $1 < k < q$) of the assumptions can be dismissed, then the remaining implication:
$$ \vdash v_{k+1}\Rightarrow\ldots\Rightarrow v_q\Rightarrow v $$
is added to the assumptions.
For a more detailed description of resolution and imp_res_tac, see §REFERENCE.
Use: Deriving new results from a previously proved implicative theorem, in combination with the current assumptions, so that subsequent tactics can use these new results.
Identity
all_tac : tactic
Summary: The identity tactic for the tactical >> (see the example in §Tactics, Goals and Validations, and §Sequencing).
Useful for writing tactics.
Use:
Writing tacticals (see description of rpt in §Repetition).
With THENL (see §Selective sequencing); for example, if tactic $T$ produces two subgoals and $T_1$ is to be applied to the first while nothing is to be done to the second, then $T$ THENL $[T_1,$ all_tac$]$ is the tactic required.
Splitting logical equivalences
eq_tac : tactic
Summary: eq_tac splits an equational goal into two implications (the “if-case” and the “only-if” case):
$$ \dfrac{u \Leftrightarrow v}{u\Rightarrow v\qquad v\Rightarrow u} $$
Use: Proving logical equivalences, i.e., goals of the form "$u \Leftrightarrow v$" where $u$ and $v$ are boolean terms.
Note that the same end can often be achieved by rewriting with the theorem EQ_IMP_THM, which states
$$ \vdash (u \Leftrightarrow v) \Leftrightarrow (u \Rightarrow v) \land (v \Rightarrow u) $$
Solving existential goals
EXISTS_TAC : term -> tactic
Summary: EXISTS_TAC $u$ reduces an existential goal $\exists x.\;t[x]$ to the subgoal $t[u]$.
(In ASCII form, the existential is printed as a question mark.)
$$ \dfrac{\exists x.\;t[x]}{t[u]} $$
Use: Proving existential goals.
Tacticals
A tactical is not represented by a single ML type, but is in general an ML function that returns a tactic (or tactics) as result. Tacticals may take parameters, and this is reflected in the variety of ML types that the built-in tacticals have. Tacticals are used for building compound tactics. Some important tacticals in the HOL system are listed below. For a complete list of the tacticals in HOL see §REFERENCE.
Alternation
ORELSE : tactic * tactic -> tactic
The tactical ORELSE is an ML infix.
If $T_1$ and $T_2$ are tactics,
then the ML expression $T_1$ ORELSE $T_2$ evaluates to a tactic which applies $T_1$ unless that fails; if it fails, it applies $T_2$.
ORELSE is defined in ML as a curried infix by
(T1 ORELSE T2) g = T1 g handle HOL_ERR _ => T2 g
First success
FIRST : tactic list -> tactic
The tactical FIRST applies the first tactic, in a list of tactics, that succeeds.
FIRST [T1, T2, ..., Tn] = T1 ORELSE T2 ORELSE ... ORELSE Tn
Change detection
CHANGED_TAC : tactic -> tactic
CHANGED_TAC $T$ $g$ fails if the subgoals produced by $T$ are just [$g$]; otherwise it is equivalent to $T\,g$.
It is defined by the following, where
set_eq: 'a list -> 'a list -> bool
tests whether two lists denote the same set (i.e., contain the same elements).
fun CHANGED_TAC tac g =
let val (gl,p) = tac g
in
if set_eq gl [g] then raise ERR "CHANGED_TAC" "no change"
else (gl,p)
end
Sequencing
>> : tactic -> tactic -> tactic
THEN : tactic -> tactic -> tactic
\\ : tactic -> tactic -> tactic
The tactical >> is an ML infix.
Its aliases THEN and \\ are also infixes.
If $T_1$ and $T_2$ are tactics, then the ML expression $T_1\;$>>$\;T_2$ evaluates to a tactic which first applies $T_1$ and then applies $T_2$ to each subgoal produced by $T_1$.
Both >> and THEN associate to the left, which can lead to some counter-intuitive behaviours when they combine with other sequencing operators.
However, chains of tactics connected with >> behave as one might expect.
In particular, if $T_1$ produces $n$ sub-goals, and $T_2$ produces varying numbers of sub-goals when applied to each of those, then the expression
$$ T_1 \texttt{ >> } T_2 \texttt{ >> } T_3 $$
will apply $T_3$ to all of the leaf sub-goals generated by the sequencing of $T_1$ and $T_2$.
Selective sequencing
THENL : tactic -> tactic list -> tactic
>| : tactic -> tactic list -> tactic
If tactic $T$ produces $n$ subgoals and $T_1$, $\dots$, $T_n$ are tactics then $T$ >| [$T_1$,$\dots$,$T_n$] is a tactic which first applies $T$ and then applies $T_i$ to the $i$th subgoal produced by $T$.
The tactical THENL is useful if one wants to apply different tactics to different subgoals.
Successive application
EVERY : tactic list -> tactic
The tactical EVERY applies a list of tactics one after the other.
EVERY [T1, T2, ..., Tn] = T1 >> T2 >> ... >> Tn
Repetition
REPEAT : tactic -> tactic
rpt : tactic -> tactic
If $T$ is a tactic then rpt $T$ is a tactic
that repeatedly applies $T$ until it fails.
It is defined in ML by:
fun REPEAT T g = ((T THEN REPEAT T) ORELSE ALL_TAC) g
(The extra argument g is needed because ML does not use lazy evaluation.)
Tactics for Manipulating Assumptions
There are in general two kinds of tactics in HOL: those that transform the conclusion of a goal without affecting the assumptions, and those that do (also or only) affect the assumptions. The various tactics that rewrite are typical of the first class; those that do “resolution” belong to the second. Often, many of the steps of a proof in HOL are carried out “behind the scenes” on the assumptions, by tactics of the second sort. A tactic that in some way changes the assumptions must also have a justification that “knows how” to restore the corresponding hypotheses of the theorem achieving the subgoal. All of this is explicit, and can be examined by a user moving about the subgoal-proof tree. Using these tactics in the most straightforward way, the assumptions at any point in a goal-directed proof, i.e., at any node in the subgoal tree, form an unordered record of every assumption made, but not yet dismissed, up to that point.
In practice, the straightforward use of assumption-changing tactics, with the tools currently provided in HOL, presents at least two difficulties. The first is that assumption sets can grow to an unwieldy size, the number and/or length of terms making them difficult to read. In addition, forward-search tactics such as resolution often add at least some assumptions that are never subsequently used, and these have to be carried along with the useful assumptions; the straightforward method provides no ready way of intercepting their arrival. Likewise, there is no straightforward way of discarding assumptions after they have been used and are merely adding to the clutter. Although perhaps against the straightforward spirit, this is a perfectly valid strategy, and requires no more than a way of denoting the specific assumptions to be discarded. That, however, raises the more general problem of denoting assumptions in the first place. Assumptions are also denoted so that they can be manipulated: given as parameters, combined to draw inferences, etc. The only straightforward way to denote them in the existing system is to supply their quoted text. Though adequate, this method may result in bulky ML expressions; and it may take some effort to present the text correctly (with necessary type information, etc.).
As always in HOL, there are quite a few ways around the various difficulties. One approach, of course, is the one intended in the original design of Edinburgh LCF, and advocates the rationale for providing a full programming language, ML, rather than a simple proof command set: that is for the user to implement new tactics in ML. For example, resolution tactics can be adapted by the user to add new assumptions more selectively; and case analysis tactics to make direct replacements without adding case assumptions. This, again, is adequate, but can involve the user in extensive amounts of programming, and in debugging exercises for which there is no system support.
Short of implementing new tactics, two other standard approaches are reflected in the current system. Both were originally developed for Cambridge LCF; both reflect fresh views of the assumptions; and both rely on tacticals that transform tactics. The two approaches are partly but not completely complementary.
The first approach, described in this section, implicitly regards the assumption set, already represented as a list, as a stack, with a pop operation, so that the assumption at the top of the stack can be (i) discarded and (ii) denoted without explicit quotation. (The corresponding push adds new assumptions at the head of the list.) The stack can be generalized to an array to allow for access to arbitrary assumptions.
The other approach, described in §Theorem continuations without popping, gives a way of intercepting and manipulating results without them necessarily being added as assumptions in the first place. The two approaches can be combined in HOL interactions.
Theorem continuations with popping
The first proof style, that of popping assumptions
from the assumption “stack”,
is illustrated using its main tool: the tactical POP_ASSUM.
POP_ASSUM : thm_tactic -> tactic
pop_assum : thm_tactic -> tactic
Given a function $f$:thm -> tactic, the tactic pop_assum $f$ applies $f$ to the (assumed) first assumption of a goal (i.e., to the top element of the assumption stack) and then applies the tactic created thereby to the original goal minus its top assumption:
pop_assum f ([t1;...;tn], t) = f (ASSUME t1) ([t2;...;tn], t)
ML functions such as $f$, with type thm -> tactic, abbreviated to thm_tactic,
are called theorem continuations,
suggesting the fact that they take theorems and then continue the proof.
The use of pop_assum can be illustrated by applying it to a particular tactic, namely DISCH_TAC.
DISCH_TAC : tactic
On a goal whose conclusion is an implication $u \Rightarrow v$, DISCH_TAC reflects the natural strategy of attempting to prove $v$ under the assumption $u$, the discharged antecedent.
For example, suppose it were required to prove that $(n = 0) \Rightarrow (n\times n = n)$:
> g `(n = 0) ==> (n * n = n)`;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
n = 0 ⇒ n * n = n
> e DISCH_TAC;
OK..
1 subgoal:
val it =
0. n = 0
------------------------------------
n * n = n
Application of DISCH_TAC to the goal produces one subgoal, as shown, with the added assumption.
To engage the assumption as a simple substitution, the tactic SUBST1_TAC is useful (see §REFERENCE for details).
SUBST1_TAC : thm -> tactic
SUBST1_TAC expects a theorem with an equational conclusion, and substitutes accordingly, into the conclusion of the goal.
At this point in the session, the tactical POP_ASSUM is applied to SUBST1_TAC to form a new tactic.
The new tactic is applied to the current subgoal.
> p();
val it =
0. n = 0
------------------------------------
n * n = n
> e(pop_assum SUBST1_TAC);
OK..
1 subgoal:
val it =
0 * 0 = 0
The result, as shown, is that the assumption is used as a substitution rule and then discarded.
The one subgoal therefore has no assumptions on its stack.
The two tactics used thus far could be combined into one using the tactical >>:
> g `(n = 0) ==> (n * n = n)`;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
n = 0 ⇒ n * n = n
> e(DISCH_TAC >> pop_assum SUBST1_TAC);
OK..
1 subgoal:
val it =
0 * 0 = 0
The goal can now be solved by simplification of arithmetic:
> e(simp[]);
OK..
Goal proved.
⊢ 0 * 0 = 0
val it =
Initial goal proved.
⊢ n = 0 ⇒ n * n = n: proof
A single tactic can, of course, be written to solve the goal (indeed, the tactic simp[] solves the entire goal from the outset):
> restart(); ... output elided ...
> e(DISCH_TAC >> pop_assum SUBST1_TAC >> simp[]);
OK..
val it =
Initial goal proved.
⊢ n = 0 ⇒ n * n = n: proof
This example illustrates how the tactical pop_assum provides access
to the top of the assumption “stack” (a capability that is useful, obviously, only when the most recently pushed assumption is the very one required).
To accomplish this access in the straightforward way would require some more awkward
construct, with explicit assumptions:
> g `(n = 0) ==> (n * n = n)`;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
n = 0 ⇒ n * n = n
> e DISCH_TAC;
OK..
1 subgoal:
val it =
0. n = 0
------------------------------------
n * n = n
> e(SUBST1_TAC(ASSUME ``n = 0``));
OK..
1 subgoal:
val it =
0. n = 0
------------------------------------
0 * 0 = 0
In contrast to the above, the popping example also illustrates the convenient disappearance of an assumption no longer required, by removing it from the stack at the moment when it is accessed and used.
This is valid because any theorem that achieves the subgoal will still achieve the original goal.
Discarding
assumptions is a separate issue from accessing them; there could, if one liked, be another tactical that produced a similar tactic on a theorem continuation to pop_assum but which did not pop the stack.
Finally, pop_assum $f$ induces case splits where $f$ does.
To prove $(n=0 \lor n=1) \Rightarrow (n\times n = n)$, the function DISJ_CASES_TAC can be used.
The tactic
DISJ_CASES_TAC |- $p$\/$q$
splits a goal into two subgoals that have $p$ and $q$, respectively, as new assumptions.
Simply using DISCH_TAC does not cause the disjunction to split when it becomes an assumption.
> g `((n = 0) \/ (n = 1)) ==> (n * n = n)`;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
n = 0 ∨ n = 1 ⇒ n * n = n
> e DISCH_TAC;
OK..
1 subgoal:
val it =
0. n = 0 ∨ n = 1
------------------------------------
n * n = n
So, we can combine pop_assum and DISJ_CASES_TAC to apply the latter to the theorem corresponding to the disjunctive assumption:
> restart(); ... output elided ...
> e(DISCH_TAC >> pop_assum DISJ_CASES_TAC);
OK..
2 subgoals:
val it =
0. n = 1
------------------------------------
n * n = n
0. n = 0
------------------------------------
n * n = n
Indeed, we can then combine this with our earlier use of SUBST1_TAC to have both branches make progress at once:
> restart(); ... output elided ...
> e(DISCH_TAC >> pop_assum DISJ_CASES_TAC >> pop_assum SUBST1_TAC);
OK..
2 subgoals:
val it =
1 * 1 = 1
0 * 0 = 0
As noted earlier, pop_assum is useful when an assumption is required that is still at the top of the stack, as in the examples.
However, it is often necessary to access assumptions made at arbitrary previous times, in order to give them as parameters, combine them, etc.
Two other useful tacticals that can be used to manipulate the assumption list are first_assum and qpat_assum.
The first has an easy characterisation:
first_assum f ([t1, ..., tn], t) =
(f(ASSUME t1) ORELSE ... ORELSE f(ASSUME tn)) ([t1, ..., tn], t)
The
first_x_assum tactical is similar to first_assum, but in addition to assuming one of the goal's assumptions as a theorem and passing this to the function $f$, the goal-state that $f\,(t_i\vdash t_i)$ acts upon has had $t_i$ removed from the assumption list.
It is a “popping” version of first_assum.
The qpat_assum tactical takes a pattern-quotation as its first argument.
The second thm_tactic parameter is then passed the first assumption that matches this pattern.
Thus:
qpat_assum pat f ([t1, ..., tp, ..., tn], t) = f (ASSUME tp) ([t1, ..., tn], t)
where $t_p$ is the first assumption that matches the pattern pat.
Just as with first_assum, there is a “popping” version called qpat_x_assum that removes the matching assumption from the list.
Thus:
qpat_x_assum pat f ([t1, ..., tp, ..., tn], t) =
f (ASSUME tp) ([t1, ..., tp-1, tp+1, ..., tn], t)
where $t_p$ is the first assumption that matches the pattern pat.
While first_assum (and first_x_assum) try to apply their theorem-tactic to every assumption, eventually using the first that succeeds, qpat_assum (and qpat_x_assum) only apply their theorem-tactic to one assumption (the first that matches).
Theorem continuations without popping
The idea of the second approach is suggested by the way the array-style tacticals
supply a list of theorems (the assumed assumptions) to a function.
These tacticals use the function to infer new results from the list of theorems, and then to do something with the results.
In some cases, e.g., the last example, the assumptions need never have been made in the first place, which suggests a different use of tacticals.
The original example for pop_assum illustrates this: namely, to show that $(n = 0) \Rightarrow (n\times n = n)$.
Here, instead of discharging the antecedent by applying DISCH_TAC to the goal, which adds the antecedent as an assumption and returns the consequent as the conclusion, and then supplying the (assumed) added assumption to the theorem continuation SUBST1_TAC and discarding it at the same time, a tactical called disch_then is applied to SUBST1_TAC directly.
disch_then transforms SUBST1_TAC into a new tactic: one that applies SUBST1_TAC directly to the (assumed) antecedent, and the resulting tactic to a subgoal with no new assumptions and the consequent as its conclusion:
> disch_then;
val it = fn: thm_tactic -> tactic
> disch_then SUBST1_TAC;
val it = fn: tactic
> g `(n = 0) ==> (n * n = n)`;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
n = 0 ⇒ n * n = n
> e(disch_then SUBST1_TAC);
OK..
1 subgoal:
val it =
0 * 0 = 0
This gives the same result as the stack method, but more directly, with a more compact ML expression, and with the attractive feature that the term $n=0$ is never an assumption, even for an interval of one step. This technique is often used at the moment when results are available; as above, where the result produced by discharging the antecedent can be immediately passed to substitution. If the result were only needed later, it would have to be held as an assumption. However, results can be manipulated when they are available, and their results either held as assumptions or used immediately. For example, to prove $(0 = n) \Rightarrow (n \times n = n)$, the result $n=0$ could be reversed immediately:
> g `(0 = n) ==> (n * n = n)`;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
0 = n ⇒ n * n = n
> e(disch_then(SUBST1_TAC o SYM));
OK..
1 subgoal:
val it =
0 * 0 = 0
The justification of disch_then SUBST1_TAC is easily constructed from the justification of DISCH_TAC composed with the justification of SUBST1_TAC.
The term $n=0$ is assumed, to yield the theorem that is passed to the theorem continuation SUBST1_TAC, and it is accordingly discharged during the construction of the actual proof; but the assumption happens only internally
to the tactic disch_then SUBST1_TAC, and not as a step in the tactical proof.
In other words, the subgoal tree here has one node fewer than before, when an explicit step (DISCH_TAC) reflected the assumption.
On the goal with the disjunctive antecedent, this method again provides a compact tactic:
> g `((n = 0) \/ (n = 1)) ==> (n * n = n)`;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
n = 0 ∨ n = 1 ⇒ n * n = n
> e(disch_then(DISJ_CASES_THEN SUBST1_TAC));
OK..
2 subgoals:
val it =
1 * 1 = 1
0 * 0 = 0
This avoids the repeated popping and pushing of the stack solution, and likewise, gives a shorter ML expression. Both give a shorter expression than the direct method, which is:
DISCH_TAC
> DISJ_CASES_TAC(ASSUME ``(n = 0) \/ (n = 1)``)
val it = fn: tactic
>| [SUBST1_TAC(ASSUME ``n = 0``);
SUBST1_TAC(ASSUME ``n = 1``)]
To summarize, there are so far at least five ways to solve a goal (and these are often combined in one interaction): directly, using the stack view of the assumptions, using the array view with or without discarding assumptions, and using a tactical to intercept an assumption step. All of the following work on the goal $(n=0) \Rightarrow (n \times n = n)$:
DISCH_TAC
> SUBST1_TAC(ASSUME ``n = 0``)
val it = fn: tactic
> simp[]
val it = fn: tactic
DISCH_TAC
> pop_assum SUBST1_TAC
val it = fn: tactic
> simp[]
val it = fn: tactic
disch_then SUBST1_TAC
> simp[]
val it = fn: tactic
Furthermore, all induce the same sequence of inferences leading to the desired theorem; internally, no inference steps are saved by the economies in the ML text or the subgoal tree. In this sense, the choice is entirely one of style and taste; of how to organize the decomposition into subgoals. The first expression illustrates the verbosity of denoting assumptions by text (the goal with the disjunctive antecedent gave a clearer example); but also the intelligibility of the resulting expression, which, of course, is all that is saved of the interaction, aside from the final theorem. The last expression illustrates both the elegance and the inscrutibility of using functions to manipulate intermediate results directly, rather than as assumptions. The middle expression shows how results can be used as assumptions (discarded when redundant, if desired); and how assumptions can be denoted without recourse to their text.
It is a strength of the LCF approach to theorem proving that many different proof styles are supported, (all in a secure way) and indeed, can be studied in their own right.
HOL provides several other theorem continuation functions analogous to disch_then and DISJ_CASES_THEN.
(Their names always end with _THEN, _THENL or _THEN2.)
Some of these do convenient inferences for the user.
For example:
CHOOSE_THEN : thm_tactical
Where thm_tactical abbreviates thm_tactic -> tactic.
CHOOSE_THEN $f$ ($\vdash\;\exists x.\;t[x]$) is a tactic that, given a goal, generates the subgoal obtained by applying $f$ to ($t[x]\vdash t[x]$).
The intuition is that if |- $\exists x.\,t[x]$ holds then |- $t[x]$ holds for some value of $x$ (as long as the variable $x$ is not free elsewhere in the theorem or current goal).
This gives an easy way of using existentially quantified theorems, something that is otherwise awkward.
The new method has other applications as well, including as an implementation technique.
For example,
taking DISJ_CASES_THEN as basic, DISJ_CASES_TAC can be defined by:
val DISJ_CASES_TAC = DISJ_CASES_THEN ASSUME_TAC
Similarly, the method is useful for modifying existing tactics (e.g., resolution tactics) without having to re-program them in ML. This avoids the danger of introducing tactics whose justifications may fail, a particularly difficult problem to track down; it is also much easier than starting from scratch.
The main theorem continuation functions in the system are:
ANTE_RES_THEN
CHOOSE_THEN X_CHOOSE_THEN
CONJUNCTS_THEN CONJUNCTS_THEN2
DISJ_CASES_THEN DISJ_CASES_THEN2 DISJ_CASES_THENL
DISCH_THEN
IMP_RES_THEN
RES_THEN
STRIP_THM_THEN
STRIP_GOAL_THEN
See §REFERENCE for full details.
Advanced Tactics and Proof Techniques
Proof Suspension and Resumption
HOL's proof suspension and resumption facilities offer users the ability to structure large source files and proof effort by separating out sub-goals to be proved in separate Theorem-Proof-QED blocks.
The first step of the process is to use the suspend tactic to “solve” a subgoal arising in the middle of a normal proof.
This tactic has type:
suspend : string -> bossLib.tactic
The suspend tactic's string argument is the label for the subgoal that is being suspended.
When applied, this tactic immediately ends work on this subgoal as if it had been genuinely proved.
Interactively, the goal stack will move on to any remaining subgoals in the proof.
Theorems that have been “proved” with the help of this tactic are not stored/saved to the current segment (as they are incomplete), and instead a message is emitted indicating as much:
> Theorem to_suspend:
p /\ q ==> q /\ p
Proof
strip_tac >> conj_tac
>- suspend "rtp_q"
>- simp[]
QED
<<HOL message: Stashing suspended theorem to_suspend with pending subgoal: rtp_q.>>
val to_suspend = [.] ⊢ p ∧ q ⇒ q ∧ p: thm
Here the user has decided to suspend the subgoal that has assumptions p and q (these are produced through the strip_tac application) and conclusion q (the first goal produced by conj_tac).
A theorem is bound to the provided name in the SML namespace, but is not yet saved for export (it is incomplete).
To resume work on the unproven subgoal, it is necessary to use the Resume form, specifying the theorem name first, and then providing the subgoal name as if it were a theorem/proof attribute.
(See Chapter 9 for more on the syntax of
attributes.)
Thus:
> Resume to_suspend[rtp_q,smlname=qsubgoal]:
first_assum ACCEPT_TAC
QED
val qsubgoal = [q] ⊢ q: thm
The optional smlname attribute allows for inspection of the theorem corresponding to the sub-goal.
To finish their work on the whole theorem, the user must now “finalise” it.
This step checks that the theorem has indeed had all of its subgoals proved and saves it, possibly alongside the usual collection of attributes:
> Finalise to_suspend[simp]
val to_suspend = [] ⊢ p ∧ q ⇒ q ∧ p: thm
If the subgoals associated with a name have not all been proved, the Finalise step will fail.
Also, if a theorem has not been finalised by the end of the containing script-file, the theory-saving process will fail with an exception.
Niceties
- If the
suspendtactic is called multiple times with the same name within the same goal, resumption at that label will present the user with a complicated looking encoding of multiple goals within just one. In order to convert this one goal back into the multiple goals that were originally saved, the user should use theRESUME_TACtactic. - Goals that have been resumed can again be
suspend-ed, reusing subgoal names, or not. - Editor modes should make it easy to create appropriate goals when working interactively; this functionality is in turn making use of the underlying function
set_suspended_goal : {label_name: string, suspension_name: string} -> proofs