Up to now, we've used the more manual part of Coq's tactic facilities. In this chapter, we'll learn more about some of Coq's powerful automation features: proof search via the auto tactic, automated forward reasoning via the Ltac hypothesis matching machinery, and deferred instantiation of existential variables using eapply and eauto. Using these features together with Ltac's scripting facilities will enable us to make our proofs startlingly short! Used properly, they can also make proofs more maintainable and robust to changes in underlying definitions. A deeper treatment of auto and eauto can be found in the UseAuto chapter in Programming Language Foundations. There's another major category of automation we haven't discussed much yet, namely built-in decision procedures for specific kinds of problems: lia is one example, but there are others. This topic will be deferred for a while longer. Our motivating example will be this proof, repeated with just a few small changes from the Imp chapter. We will simplify this proof in several stages.

The auto Tactic

Thus far, our proof scripts mostly apply relevant hypotheses or lemmas by name, and only one at a time.

The auto tactic tries to free us from this drudgery by searching for a sequence of applications that will prove the goal:

The auto tactic solves goals that are solvable by any combination of

• intros

and

• apply (of hypotheses from the local context, by default).

Using auto is always "safe" in the sense that it will never fail and will never change the proof state: either it completely solves the current goal, or it does nothing. Here is a larger example showing auto's power:

Proof search could, in principle, take an arbitrarily long time, so there are limits to how deep auto will search by default. If auto is not solving our goal as expected we can use debug auto to see a trace.

When searching for potential proofs of the current goal, auto considers the hypotheses in the current context together with a hint database of other lemmas and constructors. Some common lemmas about equality and logical operators are installed in this hint database by default.

If we want to see which facts auto is using, we can use info_auto instead.

We can extend the hint database just for the purposes of one application of auto by writing "auto using ...".

Of course, in any given development there will probably be some specific constructors and lemmas that are used very often in proofs. We can add these to the global hint database by writing
      Hint Resolve T : core. at the top level, where T is a top-level theorem or a constructor of an inductively defined proposition (i.e., anything whose type is an implication). As a shorthand, we can write
      Hint Constructors c : core. to tell Coq to do a Hint Resolve for all of the constructors from the inductive definition of c. It is also sometimes necessary to add
      Hint Unfold d : core. where d is a defined symbol, so that auto knows to expand uses of d, thus enabling further possibilities for applying lemmas that it knows about. It is also possible to define specialized hint databases (besides core) that can be activated only when needed; indeed, it is good style to create your own hint databases instead of polluting core. See the Coq reference manual for details.

(Note that the Hint Unfold is_fortytwo command above the example is needed because, unlike the apply tactic, the "apply" steps that are performed by auto do not do any automatic unfolding. Let's take a first pass over ceval_deterministic to simplify the proof script.

When we are using a particular tactic many times in a proof, we can use a variant of the Proof command to make that tactic into a default within the proof. Saying Proof with t (where t is an arbitrary tactic) allows us to use t₁... as a shorthand for t₁;t within the proof. As an illustration, here is an alternate version of the previous proof, using Proof with auto.

Searching For Hypotheses

The proof has become simpler, but there is still an annoying amount of repetition. Let's start by tackling the contradiction cases. Each of them occurs in a situation where we have both
      H₁: beval st b = false and
      H₂: beval st b = true as hypotheses. The contradiction is evident, but demonstrating it is a little complicated: we have to locate the two hypotheses H₁ and H₂ and do a rewrite following by a discriminate. We'd like to automate this process. (In fact, Coq has a built-in tactic congruence that will do the job in this case. But we'll ignore the existence of this tactic for now, in order to demonstrate how to build forward search tactics by hand.) As a first step, we can abstract out the piece of script in question by writing a little function in Ltac.

That was a bit better, but we really want Coq to discover the relevant hypotheses for us. We can do this by using the match goal facility of Ltac.

This match goal looks for two distinct hypotheses that have the form of equalities, with the same arbitrary expression E on the left and with conflicting boolean values on the right. If such hypotheses are found, it binds H₁ and H₂ to their names and applies the rwd tactic to H₁ and H₂. Adding this tactic to the ones that we invoke in each case of the induction handles all of the contradictory cases.

Let's see about the remaining cases. Each of them involves rewriting a hypothesis after feeding it with the required condition. We can automate the task of finding the relevant hypotheses to rewrite with.

The pattern ∀ x, ?P x → ?L = ?R matches any hypothesis of the form "for all x, some property of x implies some equality." The property of x is bound to the pattern variable P, and the left- and right-hand sides of the equality are bound to L and R. The name of this hypothesis is bound to H₁. Then the pattern ?P ?X matches any hypothesis that provides evidence that P holds for some concrete X. If both patterns succeed, we apply the rewrite tactic (instantiating the quantified x with X and providing H₂ as the required evidence for P X) in all hypotheses and the goal.

The big payoff in this approach is that our proof script should be more robust in the face of modest changes to our language. To test this, let's try adding a REPEAT command to the language.

REPEAT behaves like while, except that the loop guard is checked after each execution of the body, with the loop repeating as long as the guard stays false. Because of this, the body will always execute at least once.

Our first attempt at the determinacy proof does not quite succeed: the E_RepeatEnd and E_RepeatLoop cases are not handled by our previous automation.

Fortunately, to fix this, we just have to swap the invocations of find_eqn and find_rwd.

These examples just give a flavor of what "hyper-automation" can achieve in Coq. The details of match goal are a bit tricky (and debugging scripts using it is, frankly, not very pleasant). But it is well worth adding at least simple uses to your proofs, both to avoid tedium and to "future proof" them.

The eapply and eauto tactics

To close the chapter, we'll introduce one more convenient feature of Coq: its ability to delay instantiation of quantifiers. To motivate this feature, recall this example from the Imp chapter:

In the first step of the proof, we had to explicitly provide a longish expression to help Coq instantiate a "hidden" argument to the E_Seq constructor. This was needed because the definition of E_Seq...
          E_Seq : ∀ c₁ c₂ st st' st'',
            st =[ c₁ ]=> st' →
            st' =[ c₂ ]=> st'' →
            st =[ c₁ ; c₂ ]=> st'' is quantified over a variable, st', that does not appear in its conclusion, so unifying its conclusion with the goal state doesn't help Coq find a suitable value for this variable. If we leave out the with, this step fails ("Error: Unable to find an instance for the variable st'"). What's silly about this error is that the appropriate value for st' will actually become obvious in the very next step, where we apply E_Asgn. If Coq could just wait until we get to this step, there would be no need to give the value explicitly. This is exactly what the eapply tactic gives us:

The eapply H tactic behaves just like apply H except that, after it finishes unifying the goal state with the conclusion of H, it does not bother to check whether all the variables that were introduced in the process have been given concrete values during unification. If you step through the proof above, you'll see that the goal state at position 1 mentions the existential variable ?st' in both of the generated subgoals. The next step (which gets us to position 2) replaces ?st' with a concrete value. This new value contains a new existential variable ?n, which is instantiated in its turn by the following reflexivity step, position 3. When we start working on the second subgoal (position 4), we observe that the occurrence of ?st' in this subgoal has been replaced by the value that it was given during the first subgoal. Several of the tactics that we've seen so far, including ∃, constructor, and auto, have similar variants. The eauto tactic works like auto, except that it uses eapply instead of apply. Tactic info_eauto shows us which tactics eauto uses in its proof search. Below is an example of eauto. Before using it, we need to give some hints to auto about using the constructors of ceval and the definitions of state and total_map as part of its proof search.

The eauto tactic works just like auto, except that it uses eapply instead of apply; info_eauto shows us which facts eauto uses. Pro tip: One might think that, since eapply and eauto are more powerful than apply and auto, we should just use them all the time. Unfortunately, they are also significantly slower especially eauto. Coq experts tend to use apply and auto most of the time, only switching to the e variants when the ordinary variants don't do the job.

Constraints on Existential Variables

In order for Qed to succeed, all existential variables need to be determined by the end of the proof. Otherwise Coq will (rightly) refuse to accept the proof. Remember that the Coq tactics build proof objects, and proof objects containing existential variables are not complete.

Coq gives a warning after apply HP: "All the remaining goals are on the shelf," means that we've finished all our top-level proof obligations but along the way we've put some aside to be done later, and we have not finished those. Trying to close the proof with Qed would yield an error. (Try it!)

An additional constraint is that existential variables cannot be instantiated with terms containing ordinary variables that did not exist at the time the existential variable was created. (The reason for this technical restriction is that allowing such instantiation would lead to inconsistency of Coq's logic.)

The error we get, with some details elided, is:
      cannot instantiate "?y" because "y" is not in its scope In this case there is an easy fix: doing destruct HP before doing eapply HQ.

The apply HP' in the last step unifies the existential variable in the goal with the variable y. Note that the assumption tactic doesn't work in this case, since it cannot handle existential variables. However, Coq also provides an eassumption tactic that solves the goal if one of the premises matches the goal up to instantiations of existential variables. We can use it instead of apply HP' if we like.

The eauto tactic will use eapply and eassumption, streamlining the proof even further.