Theoretical Computer Science
lo.logic type-theory proof-assistants
Updated Wed, 15 Jun 2022 13:11:45 GMT

How do 'tactics' work in proof assistants?


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.

Solution

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

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.

Comments (1)

  • +3 – Great answer. Adam Chlipala's Certified Programming with Dependent Types ( adam.chlipala.net/cpdt ) is another good resource on the use of tactics in Coq. — Mar 29, 2011 at 02:46  

External Links

External links referenced by this document:

References