Tactics

Recall that in Coq, a proof is represented by a term of its internal programming language. A proposition is represented by a type, and the correctness of a proof is verified by checking that a term has the declared type.

Ultimately, then, proving in Coq is just a matter of programming: in principle, we could do all our proofs by just writing out a proposition as a type, and then writing a term with that type.

However, this tends to be impractical in the real world. Firstly, in order to be able to express complex propositions, Coq's type system is very complicated. This makes writing larger terms with it is very difficult. Second, many of proofs (or parts of proofs) are conceptually trivial, but still require lots of tedious code.

To make proof development more feasible, Coq provides a way to construct proofs interactively using tactics, which are semi-automatic directions for filling out parts of a proof. A proof script is a list of tactics, which Coq executes to create a complete proof term.

The standard style of proof scripts in Coq resembles the transcript of commands issued in a text adventure game. Every command makes sense in the context it is given in, and once you have solved the game, you can replay the script to solve the game again quickly. However, when read by itself, the list of commands makes no sense.

We are not interested only in creating formal proofs by any means available. We are also interested in understanding general proof techniques and the relationship between informal and formal proofs. Thus we would like our proof scripts to read more like stories, with enough context to help the reader make sense of the structure of the proof. Ideally our proofs or proof scripts will look just like informal proofs, only formulated precisely enough that even a mechanical proof checker can verify their correctness.

With this goal in mind, we shall diverge a little from Coq's standard tactics, and use some custom tactics that make the proof script more legible, although it also makes them a bit more verbose.

Proving equality by definition: reflexivity

The primitive notion of equality in Coq is convertibility: roughly, two terms are convertible if they evaluate to the same term. This technical notion captures the idea of equality by definition.

Verifying the convertibility of terms is an essential part of type checking: if Coq thinks that a term t has type T1, but type T2 is expected, then type checking succeeds only if T1 and T2 are convertible.

The equality relation in Coq captures the notion of convertibility. Consider the only constructor of the eq type, refl_equal:

Note that the type of the resulting equality proof is always a = a, for some a. So if a and b are convertible, a = b can be proven with refl_equal. The idiomatic way to do this in a proof script is to use the reflexivity tactic.

This is our first example of a proof script. Firstly, we use the Lemma command to declare the name of the proof and its type, i.e. the proposition want to prove. This is for the most part similar to a Definition, except that we don't give a body of the definition, but instead develop the proof with a script, which is delimited with Proof and Qed. Coq accepts Qed only after it announces that the proof has been completed.

While in the middle of interpreting a proof script, Coq shows us the current goal, i.e. the proposition that we currently need to solve. In the example, the proof script consists only of a single use of the reflexivity tactic, which solves the goal, since 2 + 2 is convertible with 4.

We can use reflexivity to prove many other trivial equalities that are true by definition:

Reflexivity proofs on concrete terms like these are mostly useful for checking that the functions that we have defined behave as we would expect. But to get more interesting results, we need to be able to generalize.

Proving implications and universals: assume (and intros)

Recall that a term of type A -> B is a function, and such functions can be constructed with terms of the form fun a : A => b, where a is a parameter of type A and b is a term of type B, which may be constructed with the use of a. This corresponds to the standard introduction rule of implication, which says that A -> B can be proven if B can be proven from a hypothesis A.

Recall also that forall a : A, B is exactly the same as A -> B, except that a may appear inside B.

In a tactic script, we often prove implications and universal quantifications by introducing the parameter as a hypothesis, and then proving the conclusion. We do this with the custom assume tactic:

Here the assume begins the proof of a universally quantified sentence "for all natural numbers n" by giving a name to the arbitrary natural number (here n) and verifying that it has the type we expect. After this, n is in our current context and can be used like any other variable.

We can then prove 0 + n = n again by reflexivity. Note that even though we cannot compute the value of n, 0 + n and n are still convertible, because plus O n always evaluates to n, i.e. 0 + n is by definition n. On the other hand, what plus n O evaluates to depends on n, so proving it is somewhat more complicated.

Coq's standard tactic for introductions is called intros, which is similar, but doesn't allow us to give the type of the introduced variable explicitly. We use a custom assume tactic which allows this in order to make the scripts more readable.

Finishing proofs: prove

We now introduce a little bit of extra syntax for structuring the proofs. Later on we shall have proof scripts with a number of subgoals, each of which gets proven separately by a proof script fragment. To better keep track of where the proof of a goal is finished, we adopt the convention that we use prove to indicate a terminating tactic. The general syntax is prove goal using tactic where goal is an optional annotation to let us write down the current goal to make the script more legible, and tactic is the tactic which we expect to prove the goal.

Here is another simple proof using the new convention:

Rewriting terms: rewrite

Recall that one way of viewing an equality a = b is to say that in any context, a can be substituted by b. At the level of proof scripts, this principle can be used with the rewrite tactic. If we have a hypothesis H of the form a = b, then we can use it to replace a with b in the goal or in some other hypothesis. The syntax for this is rewrite -> H or rewrite <- H depending on whether we wish to replace a with b or the other way around.

Here is an example of rewriting in use.

Case analysis: per cases

So far all of our proofs have been uniform in the sense that the structure of the proof is not dependent on exact form of an introduced variable: 0 + n = n by definition, regardless of whether n is 0 or some other number.

However, often it happens that we can prove some property P x for any x, but the way it is proven depends on x. In this case, we need to do case analysis on x, and give a different proof for each case. Remember that proof scripts ultimately generate proof terms, which are just programs. At that level, case analysis corresponds to simple pattern matching on x, with a different proof term et each branch of the match expression.

A common situation where case analysis on x is needed is when we are interested in f x, where f is some function that performs pattern matching on x. In this situation, if we want to know anything about the result of f x, we must know enough about the structure of x to know which branch the pattern matching in f will take.

As the simplest example, let's consider the proposition forall b : bool, negb (negb b) = b. We know that b must be one of true and false. If it is true, then, by definition, negb (negb b) evaluates to negb false and ultimately true. Similarly, if it is false, negb (negb b) evaluates to negb true and false. The following proof script formalizes the above reasoning.

NOTE: THIS TACTIC DOESN'T WORK WITH MORE COMPLICATED INDUCTIVE DEFINITIONS. USE THE STANDARD destruct TACTIC INSTEAD.

Coq's standard tactics make it hard to see which case we are handling at which time, so we use a custom tactic per cases, which attempts to simulate the pattern matching syntax and hopefully makes the structure of the proof clearer.

The per cases on b generates two subgoals, one for each constructor of bool. In each subgoal, b has been replaced by a concrete value of type bool. The goals must be proven in the order that the constructors were declared in the definition of the inductive type. In this case, first true, then false.

The custom tactic does some mystical things to the context and the goal for its internal bookkeeping purposes. The only legal thing to do after a per cases tactic is to use suppose it is to begin handling a new case. The suppose tactic checks that we truly are handling the declared case. Once the subgoal has been proven, handling the next case must again be started with a suppose declaration.

The bool type is extraordinarily simple in that none of its constructors take arguments. More commonly, a constructor takes arguments, and by pattern matching we only get to know that e.g. some number n is actually the successor S m of some other number m. The suppose syntax supports a primitive form of pattern matching and allows us to bind a variable to the number than n is a successor of.

Here is a simple example:

Why do we need separate cases here, although we are just using reflexivity in each case? The reason is that in order for us to show that beq_nat (n + 1) 0 evaluates to false, we must first show that n + 1 evaluates to S n', for some n'. It does so, but the reason it does so depends on the value of n. If n is 0, then n + 1 evaluates to 1, i.e. S O, the latter argument. If n is S m, then n + 1 evaluates to S (m + 1). So we must consider each case separately to verify this.

Conversions: change

Sometimes we need to explicitly change the goal or some hypothesis into a convertible but syntactically different form. We may want to do this simply because we think the new form is clearer or more relevant to the proof, or in order to expose a subterm which can then be substituted by another with rewrite.

The change tactic performs this. The goal is converted with change goal where goal should be convertible with the current goal. A hypothesis can be converted with change term in hyp where hyp is some current hypothesis whose type is convertible with term.

Here is an example of its use:

Here the first change is included only for illustration and could be left out. However, the second change is crucial: it converts the goal into a form where m * m appears, and only then can we use rewrite to substitute it with n.

There are also tactics for performing conversion steps without specifying beforehand the desired result form. These include red, simpl and unfold. Such tactics are good for investigating what a goal or hypothesis is convertible to, but in a final proof script these tactics are uninformative to the reader, so change, which is accompanied with the desired result, should often be preferred.

Induction

Induction is the logical counterpart of the kind of recursion that Coq supports. Recall that in Coq, a recursive function f on natural numbers practically must be designed so that:

• we specify directly what f O returns
• we specify what f (S m) returns from the value that f m returns

When we think of the function f as a proof that for each n some property P n holds, the above principle gets the following interpretation:

• we prove directly that P O holds
• we prove that P (S m) holds from the assumption that P m holds

This is the induction principle for natural numbers.

Proving by induction in Coq is very much like proving by cases, except that in an inductive case (for natural numbers, the S m-case) we also get and inductive hypothesis stating that the proposition we are trying to prove for S m already holds for m.

NOTE: THIS TACTIC DOESN'T WORK WITH MORE COMPLICATED INDUCTIVE DEFINITIONS. USE THE STANDARD induction TACTIC INSTEAD.

We use a custom tactic similar to per cases, but it is now called per induction. The inductive hypothesis can be introduced with the assume tactic.

Here is a proof that 0 is the right identity of plus. Note that we also make use of a conversion with change in order to be able to use the inductive hypothesis in rewriting.