How do 'tactics' work in proof assistants?

Question

Question: How do 'tactics' work in proof assistants? They seem to be ways of specifying how to rewrite a term into an equivalent term (for some definition of 'equivalent'). Presumably there are formal rules for this, how can I learn what they are and how they work? Do they involve more than choice of order for Beta-reduction?

Background about my interest: Several months ago, I decided I wanted to learn formal math. I decided to go with type theory because from preliminary research it seems like The Right Way To Do Things (tm) and because it seems to unify programming and mathematics which is fascinating. I think my eventual goal is to be able to use and understand a proof assistant like Coq (I think especially being able to use dependent types as I am curious about things like representing the types of matrixes). I started off knowing very little, not even rudimentary functional programming, but I'm making slow progress. I've read and understood large chunks of Types and Programming Languages (Pierce) and learned some Haskell and ML.

Answer 1

The basic tactics either run an inference rule forwards or backwards (for example, convert hypotheses $A$ and $B$ into $A\wedge B$ or convert goal $A\wedge B$ into two goals $A$ and $B$ with same hypotheses), apply a lemma (~ function application), split up a lemma about some inductive type into a case for each constructor, and so on. Basic tactics may succeed or fail depending upon the context in which they are applied. More advanced tactics are like little functional programs that run the basic tactics, perform pattern matching over the terms in the goal and/or assumptions, make choices based on the success or failure of tactics, and so forth. More advanced tactics deal with arithmetic and other specific kinds of theories. The key paper on Coq's tactic language is the following:

• D. Delahaye. A Tactic Language for the System Coq. In Proceedings of Logic for Programming and Automated Reasoning (LPAR), Reunion Island, volume 1955 of Lecture Notes in Computer Science, pages 85–95. Springer-Verlag, November 2000.

The formal rules which form the essence of the basic tactics are defined in the Coq users guide here or in Chapter 4 of the pdf.

A quite instructive paper on implementing tactics and tacticals (essentially tactics that take other tactics as arguments) is:

• Amy Felty. Implementing Tactics and Tacticals in a Higher-order Programming Language Journal of Automated Reasoning, 11(1):43-81, August 1993.

Coq's tactic language has the limitation that the proofs written using it hardly resemble proofs one does by hand. Several attempts have been made to enable clearer proofs. These include Isar (for Isabelle/HOL) and Mizar's proof language.

Aside: Did you also know that the programming language ML was originally designed to implement tactics for the LCF theorem prover? Many ideas developed for ML, such as type inference, have influenced modern programming languages.

Answer 2

LCF is indeed the grand-father of all these system: Coq, Isabelle, HOLs, including the ML programming language (which we see today as OCaml, SML, also F#). Yes, I am including Coq as a member of the greater LCF family. Compared to the US-American proof assistants (notably ACL2), or the totally unrelated Mizar, Coq is culturally quite close to Isabelle and the HOLs, mainly due the shared idea of tactics.

So what are tactics anyway, stripped from accidental observations about rewriting, conversions, introducing or eliminating connectives?

The main layering principle here is inherited from Milner's LCF:

• Core inferences (forward reasoning), either as abstract datatype thm in the original LCF-approach, or with separate checking of proof terms in the Type-Theory branch of the family (Coq, Matita). This gives you a certain logical foundation for results that the prover considers as theorems. So you could have a primitive inference that takes ⊢ A and ⊢ B and gives you ⊢ A ∧ B. Another primitive inference could give you ⊢ t = u, where u is the beta-normal form of t. None of these mechanisms are tactics, though, they are inference rules as in standard logic.

• Goal-directed proof (backwards reasoning). The idea is you operate on some notion of "goal state" by refining it, splitting it up into more and more subgoals, close subgoals, until it is all solved. Finishing off the goal state, will make a certain theorem pop out of the process. LCF has introduced certain extra-logical infrastructure for goals, which is still there in the HOLs: a tactic is some ML function that refines a goal, and produces some justification for the refinement. In the very end of the proof, the justfications are replayed in reverse order to produce a proof in forward manner according to the primitive inferences sketched above.

Coq and Matita are still pretty close to this LCF principle. Isabelle is different here: as early as 1989, Larry Paulson reformed the notions of goal and tactic to make them closer to the logic, which is the "Pure" logical framework of Isabelle here. Isabelle/Pure provides minimal higher-order logic with implication ==> and quantifier !! which indicate both the structure of natural deduction rules and goal states.

For example, ⊢ A ==> B ==> A ∧ B is the conjunction introduction rule (of the object logic) as theorem of the logical framework.

Goal states are just theorems as well, starting with ⊢ C ==> C for your initial claim C, which is refined to ⊢ X ==> Y ==> Z ==> C in intermediate states, where X, Y, Z are the current subgoals, and the process ends with ⊢ C (no subgoals).

Now back to tactics, which are more uniform for all these provers: given some notion of goal state (e.g. the Isabelle one above), a tactic is a function that maps a goal state to (0, 1, or more) follow-up goal states. Moreover, a tactical is a combinator of such tactic functions, e.g. to express sequential composition, choice, repeat etc. In fact, the language of tactics and tacticals is related to the "list of successes" approach of parser combinators.

Tactics allow to describe certain strategies of goal refinements systematically. They turned out quite successful since their invention in LCF in the 1970/80-ies, but they produce notoriously unreadable proof scripts.

A recent overview of some aspects of tactic languages is given in the paper by A. Asperti et al, PLMMS 2009, see workshop proceedings page 22.

Mizar and Isabelle/Isar have been mentioned as alternative approaches to human-readable structured reasoning, and they are not based on tactics in that sense. Mizar is unrelated to the LCF family, so it does not know that tactic terminology. Isabelle/Isar incorporates the tactical tradition to some extent, but its notion of proof method is a bit more structured (with explicit Isar proof context, explicit indication of chained facts, and avoidance of internal goal-hacking in the course of reasoning).

Many more reforms and reconsiderations of tactic languages have happened in the past decades. For example, a recent branch of the Coq community favours SSReflect (by G. Gonthier) instead of the traditional Ltac.

Answer 3

How do 'tactics' work in proof assistants?

I suspect this answer will be a bit of a ramble.

First, it isn't enough to ask "how tactics work in proof assistants" because they work differently in different proof assistants. There's two main classes of assistant used today: those derived from the original LCF, like Isabelle, HOL and HOL light, and type theory based proof assistants like Coq and Matita. In these two different classes of proof assistant the tactics work in different ways, a reflection that what's going on under the bonnet in e.g. Isabelle is quite different to what's going on under the bonnet in e.g. Matita.

Ask yourself: what's going on when we attempt to prove a proposition P in Matita? We introduce a metavariable X with type P. We then play a game, so to speak, where we refine X, adding more and more structure to the incomplete term, until we get a complete lambda-term (i.e. containing no more metavariables). Once we are in possession of a complete lambda-term, we type check it with respect to P, making sure it inhabits the required type. We then see that in Coq and Matita, a tactic is merely a function from incomplete proof terms to incomplete proof terms, which hopefully adds a bit of structure to the term after application (this observation has motivated quite a bit of recent work by e.g. Jojgov, Pientka, and others).

For instance, the Matita tactic "intro" introduces a lambda-abstraction over the existing term, "cases" introduces a match expression in the term, and "apply" introduces an application of one term to the other. These basic tactics can be strung together, using higher-order functions, to create more complex ones. The basic idea is always the same though: a tactic is always aiming to add a bit of structure to an incomplete proof term.

Note that, implementers aim to give back a term that typechecks again after every tactic application. Strictly speaking, there's no requirement for them to do so, as all that matters for type theory based proof assistants is that, when the user comes to Qed the proof, we are in possession of a proof term that inhabits the proposition P. How we arrived at this proof term is largely irrelevant. However, both Coq and Matita aim to give the user back a (possibly incomplete) proof term that typechecks after every tactic application. Yet this invariant can (and often does) fail, especially in regard to the two syntactic checks that CIC based proof assistants must implement.

In particular, we can carry out what appears to be a valid proof, applying a series of tactics until there are no open goals left. We then come to Qed the supposed proof, only to discover that Matita's termination checker, or its strict positivity checker, complains, as the proof term that was generated by the tactics has invalidated one of these syntactic checks (i.e. a metavariable in argument position to a recursive call was instantiated with a term that is not syntactically smaller than the original argument). This is a reflection that the CIC type theory is, in some sense, not "strong enough", and does not reflect the positivity or size syntactic requirements in its types (an observation that motivates Abel's sized types, and some recent work on positivity types).

On the other hand, LCF-style proof assistants are quite different. Here, the kernel consists of a module (usually implemented in a variant of ML), containing an abstract type "thm", and functions that implement the inference rules of the proof assistant's logic, mapping "thm" to "thm", and so forth. We rely on the typing discipline of ML to ensure that the only way of constructing a value of type "thm" is via these inference rules (basic tactics). Isabelle's kernel is here.

Proofs then consist of a series of applications of these basic tactics (or more complex, larger tactics, which are again made by stringing together simpler tactics using higher-order functions --- in Isabelle, the higher-order functions, called tacticals, can be seen here). Unlike type theory based proof assistants, there is no need in an LCF-style assistant to keep an explicit proof term witness lying around. Correctness of the proof is guaranteed by construction, and our trust in ML's typing discipline (many assistants, e.g. Isabelle, do, however, generate proof terms for their proofs).