In a machine-checked proof, every single detail has to be justified. This can result in huge proof scripts. Fortunately, Coq comes with a proof-search mechanism and with several decision procedures that enable the system to automatically synthesize simple pieces of proof. Automation is very powerful when set up appropriately. The purpose of this chapter is to explain the basics of how automation works in Coq. The chapter is organized in two parts. The first part focuses on a general mechanism called "proof search." In short, proof search consists in naively trying to apply lemmas and assumptions in all possible ways. The second part describes "decision procedures", which are tactics that are very good at solving proof obligations that fall in some particular fragments of the logic of Coq. Many of the examples used in this chapter consist of small lemmas that have been made up to illustrate particular aspects of automation. These examples are completely independent from the rest of the Software Foundations course. This chapter also contains some bigger examples which are used to explain how to use automation in realistic proofs. These examples are taken from other chapters of the course (mostly from STLC), and the proofs that we present make use of the tactics from the library LibTactics.v, which is presented in the chapter UseTactics.

Basic Features of Proof Search

The idea of proof search is to replace a sequence of tactics applying lemmas and assumptions with a call to a single tactic, for example auto. This form of proof automation saves a lot of effort. It typically leads to much shorter proof scripts, and to scripts that are typically more robust to change. If one makes a little change to a definition, a proof that exploits automation probably won't need to be modified at all. Of course, using too much automation is a bad idea. When a proof script no longer records the main arguments of a proof, it becomes difficult to fix it when it gets broken after a change in a definition. Overall, a reasonable use of automation is generally a big win, as it saves a lot of time both in building proof scripts and in subsequently maintaining those proof scripts.

Strength of Proof Search

We are going to study four proof-search tactics: auto, eauto, iauto and jauto. The tactics auto and eauto are builtin in Coq. The tactic iauto is a shorthand for the builtin tactic try solve [intuition eauto]. The tactic jauto is defined in the library LibTactics, and simply performs some preprocessing of the goal before calling eauto. The goal of this chapter is to explain the general principles of proof search and to give rule of thumbs for guessing which of the four tactics mentioned above is best suited for solving a given goal. Proof search is a compromise between efficiency and expressiveness, that is, a tradeoff between how complex goals the tactic can solve and how much time the tactic requires for terminating. The tactic auto builds proofs only by using the basic tactics reflexivity, assumption, and apply. The tactic eauto can also exploit eapply. The tactic jauto extends eauto by being able to open conjunctions and existentials that occur in the context. The tactic iauto is able to deal with conjunctions, disjunctions, and negation in a quite clever way; however it is not able to open existentials from the context. Also, iauto usually becomes very slow when the goal involves several disjunctions. Note that proof search tactics never perform any rewriting step (tactics rewrite, subst), nor any case analysis on an arbitrary data structure or property (tactics destruct and inversion), nor any proof by induction (tactic induction). So, proof search is really intended to automate the final steps from the various branches of a proof. It is not able to discover the overall structure of a proof.

Basics

The tactic auto is able to solve a goal that can be proved using a sequence of intros, apply, assumption, and reflexivity. Two examples follow. The first one shows the ability for auto to call reflexivity at any time. In fact, calling reflexivity is always the first thing that auto tries to do.

The second example illustrates a proof where a sequence of two calls to apply are needed. The goal is to prove that if Q n implies P n for any n and if Q n holds for any n, then P 2 holds.

If we are interested to see which proof auto came up with, one possibility is to look at the generated proof-term, using the command: Print solving_by_apply. The proof term is: fun (P Q : nat → Prop) (H : ∀ n : nat, Q n → P n) (H₀ : ∀ n : nat, Q n) ⇒ H 2 (H₀ 2) This essentially means that auto applied the hypothesis H (the first one), and then applied the hypothesis H₀ (the second one). A more practical approach is to invoke the tactic info_auto, which reveals the proof script that auto used to complete the proof. The tactic auto can invoke apply but not eapply. So, auto cannot exploit lemmas whose instantiation cannot be directly deduced from the proof goal. To exploit such lemmas, one needs to invoke the tactic eauto, which is able to call eapply. In the following example, the first hypothesis asserts that P n is true when Q m is true for some m, and the goal is to prove that Q 1 implies P 2. This implication follows directly from the hypothesis by instantiating m as the value 1. The following proof script shows that eauto successfully solves the goal, whereas auto is not able to do so.

Conjunctions

So far, we've seen that eauto is stronger than auto in the sense that it can deal with eapply. In the same way, we are going to see how jauto and iauto are stronger than auto and eauto in the sense that they provide better support for conjunctions. The tactics auto and eauto can prove a goal of the form F ∧ F', where F and F' are two propositions, as soon as both F and F' can be proved in the current context. An example follows.

However, when an assumption is a conjunction, auto and eauto are not able to exploit this conjunction. It can be quite surprising at first that eauto can prove very complex goals but that it fails to prove that F ∧ F' implies F. The tactics iauto and jauto are able to decompose conjunctions from the context. Here is an example.

The tactic jauto is implemented by first calling a pre-processing tactic called jauto_set, and then calling eauto. So, to understand how jauto works, one can directly call the tactic jauto_set.

Next is a more involved goal that can be solved by iauto and jauto.

The strategy of iauto and jauto is to run a global analysis of the top-level conjunctions, and then call eauto. For this reason, those tactics are not good at dealing with conjunctions that occur as the conclusion of some universally quantified hypothesis. The following example illustrates a general weakness of Coq proof search mechanisms.

This situation is slightly disappointing, since automation is able to prove the following goal, which is very similar. The only difference is that the universal quantification has been distributed over the conjunction.

Disjunctions

The tactics auto and eauto can handle disjunctions that occur in the goal.

However, only iauto is able to automate reasoning on the disjunctions that appear in the context. For example, iauto can prove that F ∨ F' entails F' ∨ F.

More generally, iauto can deal with complex combinations of conjunctions, disjunctions, and negations. Here is an example.

However, the ability of iauto to automatically perform a case analysis on disjunctions comes with a downside: iauto may be very slow. If the context involves several hypotheses with disjunctions, iauto typically generates an exponential number of subgoals on which eauto is called. One major advantage of jauto compared with iauto is that it never spends time performing this kind of case analyses.

Existentials

The tactics eauto, iauto, and jauto can prove goals whose conclusion is an existential. For example, if the goal is ∃ x, f x, the tactic eauto introduces an existential variable, say ?25, in place of x. The remaining goal is f ?25, and eauto tries to solve this goal, allowing itself to instantiate ?25 with any appropriate value. For example, if an assumption f 2 is available, then the variable ?25 gets instantiated with 2 and the goal is solved, as shown below.

A major strength of jauto over the other proof search tactics is that it is able to exploit the existentially-quantified hypotheses, i.e., those of the form ∃ x, P.

Negation

The tactics auto and eauto suffer from some limitations with respect to the manipulation of negations, mostly related to the fact that negation, written ¬ P, is defined as P → False but that the unfolding of this definition is not performed automatically. Consider the following example.

For this reason, the tactics iauto and jauto systematically invoke unfold not in × as part of their pre-processing. So, they are able to solve the previous goal right away.

We will come back later on to the behavior of proof search with respect to the unfolding of definitions.

Equalities

Coq's proof-search feature is not good at exploiting equalities. It can do very basic operations, like exploiting reflexivity and symmetry, but that's about it. Here is a simple example that auto can solve, by first calling symmetry and then applying the hypothesis.

To automate more advanced reasoning on equalities, one should rather try to use the tactic congruence, which is presented at the end of this chapter in the "Decision Procedures" section.

How Proof Search Works

Search Depth

The tactic auto works as follows. It first tries to call reflexivity and assumption. If one of these calls solves the goal, the job is done. Otherwise auto tries to apply the most recently introduced assumption that can be applied to the goal without producing an error. This application produces subgoals. There are two possible cases. If the sugboals produced can be solved by a recursive call to auto, then the job is done. Otherwise, if this application produces at least one subgoal that auto cannot solve, then auto starts over by trying to apply the second most recently introduced assumption. It continues in a similar fashion until it finds a proof or until no assumption remains to be tried. It is very important to have a clear idea of the backtracking process involved in the execution of the auto tactic; otherwise its behavior can be quite puzzling. For example, auto is not able to solve the following triviality.

The reason auto fails to solve the goal is because there are too many conjunctions. If there had been only five of them, auto would have successfully solved the proof, but six is too many. The tactic auto limits the number of lemmas and hypotheses that can be applied in a proof, so as to ensure that the proof search eventually terminates. By default, the maximal number of steps is five. One can specify a different bound, writing for example auto 6 to search for a proof involving at most six steps. For example, auto 6 would solve the previous lemma. (Similarly, one can invoke eauto 6 or intuition eauto 6.) The argument n of auto n is called the "search depth." The tactic auto is simply defined as a shorthand for auto 5. The behavior of auto n can be summarized as follows. It first tries to solve the goal using reflexivity and assumption. If this fails, it tries to apply a hypothesis (or a lemma that has been registered in the hint database), and this application produces a number of sugoals. The tactic auto (n-1) is then called on each of those subgoals. If all the subgoals are solved, the job is completed, otherwise auto n tries to apply a different hypothesis. During the process, auto n calls auto (n-1), which in turn might call auto (n-2), and so on. The tactic auto 0 only tries reflexivity and assumption, and does not try to apply any lemma. Overall, this means that when the maximal number of steps allowed has been exceeded, the auto tactic stops searching and backtracks to try and investigate other paths. The following lemma admits a unique proof that involves exactly three steps. So, auto n proves this goal iff n is greater than three.

We can generalize the example by introducing an assumption asserting that P k is derivable from P (k-1) for all k, and keep the assumption P 0. The tactic auto, which is the same as auto 5, is able to derive P k for all values of k less than 5. For example, it can prove P 4.

However, to prove P 5, one needs to call at least auto 6.

Because auto looks for proofs at a limited depth, there are cases where auto can prove a goal F and can prove a goal F' but cannot prove F ∧ F'. In the following example, auto can prove P 4 but it is not able to prove P 4 ∧ P 4, because the splitting of the conjunction consumes one proof step. To prove the conjunction, one needs to increase the search depth, using at least auto 6.

Backtracking

In the previous section, we have considered proofs where at each step there was a unique assumption that auto could apply. In general, auto can have several choices at every step. The strategy of auto consists of trying all of the possibilities (using a depth-first search exploration). To illustrate how automation works, we are going to extend the previous example with an additional assumption asserting that P k is also derivable from P (k + 1). Adding this hypothesis offers a new possibility that auto could consider at every step. There exists a special commands, named info_auto and info_eauto, that one can use to see what tactics auto uses to solve a goal. There also exists more verbose commands, named debug auto and debug eauto, that one can use for tracing all the steps that considered during a proof-search.

The output message produced by debug eauto is as follows.

  1 depth=5
  1.1 depth=4 simple apply H2
  1.1.1 depth=3 simple apply H2
  1.1.1.1 depth=3 exact H1

The depth indicates the value of n with which eauto n is called. The tactics shown in the message indicate that the first thing that eauto has tried to do is to apply H₂. The effect of applying H₂ is to replace the goal P 2 with the goal P 1. Then, again, H₂ has been applied, changing the goal P 1 into P 0. At that point, the goal was exactly the hypothesis H₁. It seems that eauto was quite lucky there, as it never even tried to use the hypothesis H₃ at any time. The reason is that auto always tried to use the H₂ first. So, let's permute the hypotheses H₂ and H₃ and see what happens.

This time, the output message suggests that the proof search investigates many possibilities. If we print the proof term: Print working_of_auto_2. we observe that the proof term refers to H₃. Thus the proof is not the simplest one, since only H₂ and H₁ are needed. In turns out that the proof goes through the proof obligation P 3, even though it is not required to do so. The following tree drawing describes all the goals that eauto has been going through.

    |5||4||3||2||1||0| -- below, tabulation indicates the depth

    [P 2]
    -> [P 3]
       -> [P 4]
          -> [P 5]
             -> [P 6]
                -> [P 7]
                -> [P 5]
             -> [P 4]
                -> [P 5]
                -> [P 3]
          --> [P 3]
             -> [P 4]
                -> [P 5]
                -> [P 3]
             -> [P 2]
                -> [P 3]
                -> [P 1]
       -> [P 2]
          -> [P 3]
             -> [P 4]
                -> [P 5]
                -> [P 3]
             -> [P 2]
                -> [P 3]
                -> [P 1]
          -> [P 1]
             -> [P 2]
                -> [P 3]
                -> [P 1]
             -> [P 0]
                -> !! Done !!

The first few lines read as follows. To prove P 2, eauto 5 has first tried to apply H₃, producing the subgoal P 3. To solve it, eauto 4 has tried again to apply H₃, producing the goal P 4. Similarly, the search goes through P 5, P 6 and P 7. When reaching P 7, the tactic eauto 0 is called but as it is not allowed to try and apply any lemma, it fails. So, we come back to the goal P 6, and try this time to apply hypothesis H₂, producing the subgoal P 5. Here again, eauto 0 fails to solve this goal. The process goes on and on, until backtracking to P 3 and trying to apply H₃ three times in a row, going through P 2 and P 1 and P 0. This search tree explains why eauto came up with a proof term starting with an application of H₃.

Adding Hints

By default, auto (and eauto) only tries to apply the hypotheses that appear in the proof context. There are three possibilities for telling auto to exploit a lemma that have been proved previously: either add the lemma as a on-the-fly hint with auto using lemma; or add the lemma as an assumption just before calling auto; or add the lemma as a hint, so that it can be used by every calls to auto. The first and second possibilities are useful to have auto exploit a lemma that only serves at this particular point. Note: to add a lemma as an hypothesis, one can type generalize mylemma; intro, or simply lets: mylemma, if using LibTactics.v. The third possibility is useful for lemmas that need to be exploited accross several lemmas. The syntax for adding a lemma as a hint is Hint Resolve mylemma. For example:

The standard library adds a few lemmas in the hint database. For example, the eq_sym lemma, which characterizes symmetry of equality, is registered in module Coq.Init.Logic via the line Hint Immediate eq_sym not_eq_sym: core.. There Hint Immediate is used instead of Hint Resolve to limit the search depth after symmetry is exploited. In practice, auto is able to prove a result such as the following one.

A convenient shorthand for adding all the constructors of an inductive datatype as hints is the command Hint Constructors mydatatype. Warning: some lemmas, such as transitivity results, should not be added as hints as they would very badly affect the performance of proof search. The description of this problem and the presentation of a general work-around for transitivity lemmas appear further on.

Integration of Automation in Tactics

The library "LibTactics" introduces a convenient feature for invoking automation after calling a tactic. In short, it suffices to add the symbol star (×) to the name of a tactic. For example, apply× H is equivalent to apply H; auto_star, where auto_star is a tactic that can be defined as needed. The definition of auto_star, which determines the meaning of the star symbol, can be modified whenever needed. Simply write:
       Ltac auto_star ::= a_new_definition. Observe the use of ::= instead of :=, which indicates that the tactic is being rebound to a new definition. So, the default definition is as follows.

Nearly all standard Coq tactics and all the tactics from "LibTactics" can be called with a star symbol. For example, one can invoke subst×, destruct× H, inverts× H, lets× I: H x, specializes× H x, and so on... There are two notable exceptions. The tactic auto× is just another name for the tactic auto_star. And the tactic apply× H calls eapply H (or the more powerful applys H if needed), and then calls auto_star. Note that there is no eapply× H tactic, use apply× H instead. In large developments, it can be convenient to use two degrees of automation. Typically, one would use a fast tactic, like auto, and a slower but more powerful tactic, like jauto. To allow for a smooth coexistence of the two form of automation, LibTactics.v also defines a "tilde" version of tactics, like apply¬ H, destruct¬ H, subst¬, auto¬ and so on. The meaning of the tilde symbol is described by the auto_tilde tactic, whose default implementation is auto.

In the examples that follow, only auto_star is needed. An alternative, possibly more efficient version of auto_star is the following:
    Ltac auto_star ::= try solve [ eassumption | auto | jauto ]. With the above definition, auto_star first tries to solve the goal using the assumptions; if it fails, it tries using auto, and if this still fails, then it calls jauto. Even though jauto is strictly stronger than eassumption and auto, it makes sense to call these tactics first, because, when the succeed, they save a lot of time, and when they fail to prove the goal, they fail very quickly..

Example Proofs using Automation

Let's see how to use proof search in practice on the main theorems of the "Software Foundations" course, proving in particular results such as determinism, preservation and progress.

Determinism

Recall the original proof of the determinism lemma for the IMP language, shown below.

Exercise: rewrite this proof using auto whenever possible. (The solution uses auto 9 times.)

In fact, using automation is not just a matter of calling auto in place of one or two other tactics. Using automation is about rethinking the organization of sequences of tactics so as to minimize the effort involved in writing and maintaining the proof. This process is eased by the use of the tactics from LibTactics.v. So, before trying to optimize the way automation is used, let's first rewrite the proof of determinism:

• use introv H instead of intros x H,
• use gen x instead of generalize dependent x,
• use inverts H instead of inversion H; subst,
• use tryfalse to handle contradictions, and get rid of the cases where beval st b₁ = true and beval st b₁ = false both appear in the context.

To obtain a nice clean proof script, we have to remove the calls assert (st' = st'0). Such a tactic call is not nice because it refers to some variables whose name has been automatically generated. This kind of tactics tend to be very brittle. The tactic assert (st' = st'0) is used to assert the conclusion that we want to derive from the induction hypothesis. So, rather than stating this conclusion explicitly, we are going to ask Coq to instantiate the induction hypothesis, using automation to figure out how to instantiate it. The tactic forwards, described in LibTactics.v precisely helps with instantiating a fact. So, let's see how it works out on our example.

To polish the proof script, it remains to factorize the calls to auto, using the star symbol. The proof of determinism can then be rewritten in just 4 lines, including no more than 10 tactics.

Preservation for STLC

To investigate how to automate the proof of the lemma preservation, let us first import the definitions required to state that lemma.

Consider the proof of perservation of STLC, shown below. This proof already uses eauto through the triple-dot mechanism.

Exercise: rewrite this proof using tactics from LibTactics and calling automation using the star symbol rather than the triple-dot notation. More precisely, make use of the tactics inverts× and applys× to call auto× after a call to inverts or to applys.

Progress for STLC

Consider the proof of the progress theorem.

Exercise: optimize the above proof. Hint: make use of destruct× and inverts×. The solution fits on 10 short lines.

BigStep and SmallStep

Consider the proof relating a small-step reduction judgment to a big-step reduction judgment.

Our goal is to optimize the above proof. It is generally easier to isolate inductions into separate lemmas. So, we are going to first prove an intermediate result that consists of the judgment over which the induction is being performed. Exercise: prove the following result, using tactics introv, induction and subst, and apply×. The solution fits on 3 short lines.

Exercise: using the lemma above, simplify the proof of the result multistep__eval. You should use the tactics introv, inverts, split× and apply×. The solution fits on 2 lines.

If we try to combine the two proofs into a single one, we will likely fail, because of a limitation of the induction tactic. Indeed, this tactic loses information when applied to a property whose arguments are not reduced to variables, such as t -->* (C n). You will thus need to use the more powerful tactic called dependent induction. (This tactic is available only after importing the Program library, as we did above.) Exercise: prove the lemma multistep__eval without invoking the lemma multistep_eval_ind, that is, by inlining the proof by induction involved in multistep_eval_ind, using the tactic dependent induction instead of induction. The solution fits on 6 lines.

Preservation for STLCRef

The proof of preservation for STLCRef can be found in chapter References. The optimized proof script is more than twice shorter. The following material explains how to build the optimized proof script. The resulting optimized proof script for the preservation theorem appears afterwards.

Let's come back to the proof case that was hard to optimize. The difficulty comes from the statement of nth_eq_last, which takes the form nth (length l) (l ++ x::nil) d = x. This lemma is hard to exploit because its first argument, length l, mentions a list l that has to be exactly the same as the l occurring in l ++ x::nil. In practice, the first argument is often a natural number n that is provably equal to length l yet that is not syntactically equal to length l. There is a simple fix for making nth_eq_last easy to apply: introduce the intermediate variable n explicitly, so that the goal becomes nth n (l ++ x::nil) d = x, with a premise asserting n = length l.

The proof case for ref from the preservation theorem then becomes much easier to prove, because rewrite nth_eq_last' now succeeds.

The optimized proof of preservation is summarized next.

Progress for STLCRef

The proof of progress for STLCRef can be found in chapter References. The optimized proof script is, here again, about half the length.

Subtyping

Consider the inversion lemma for typing judgment of abstractions in a type system with subtyping.

Exercise: optimize the proof script, using introv, lets and inverts×. In particular, you will find it useful to replace the pattern apply K in H. destruct H as I with lets I: K H. The solution fits on 3 lines.

Advanced Topics in Proof Search

Stating Lemmas in the Right Way

Due to its depth-first strategy, eauto can get exponentially slower as the depth search increases, even when a short proof exists. In general, to make proof search run reasonably fast, one should avoid using a depth search greater than 5 or 6. Moreover, one should try to minimize the number of applicable lemmas, and usually put first the hypotheses whose proof usefully instantiates the existential variables. In fact, the ability for eauto to solve certain goals actually depends on the order in which the hypotheses are stated. This point is illustrated through the following example, in which P is a property of natural numbers. This property is such that P n holds for any n as soon as P m holds for at least one m different from zero. The goal is to prove that P 2 implies P 1. When the hypothesis about P is stated in the form ∀ n m, P m → m ≠ 0 → P n, then eauto works. However, with ∀ n m, m ≠ 0 → P m → P n, the tactic eauto fails.