Before we start on the next major topic, let's spend a little time learning to use some of Coq's more powerful automation features...

The auto and eauto Tactics

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

• intros,
• apply (with a local hypothesis, by default), and
• reflexivity.

The eauto tactic works just like auto, except that it uses eapply instead of apply. 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 contrived example:

When searching for potential proofs of the current goal, auto and eauto consider the hypotheses in the current context together with a hint database of other lemmas and constructors. Some of the lemmas and constructors we've already seen — e.g., conj, or_introl, and or_intror — are installed in this hint database by default.

We can extend the hint database just for the purposes of one application of auto or eauto by writing auto using .... E.g., if conj, or_introl, and or_intror had not already been in the hint database, we could have done this instead:

Of course, in any given development there will also be some of our own specific constructors and lemmas that are used very often in proofs. We can add these to the global hint database by writing 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 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 where d is a defined symbol, so that auto knows to expand uses of d and enable further possibilities for applying lemmas that it knows about. Here are some Hints we will find useful.

Warning: Just as with Coq's other automation facilities, it is easy to overuse auto and eauto and wind up with proofs that are impossible to understand later! Also, overuse of eauto can make proof scripts very slow. Get in the habit of using auto most of the time and eauto only when necessary. For much more detailed information about using auto and eauto, see the chapter UseAuto.

The Proof with Tactic

If you start a proof by saying Proof with (tactic) instead of just Proof, then writing ... instead of . after a tactic in the body of the proof will try to solve all generated subgoals with tactic (and fail if this doesn't work). One common use of this facility is "Proof with auto" (or eauto). We'll see many examples of this later in the file.

The solve by inversion Tactic

Here's another nice automation feature: it often arises that the context contains a contradictory assumption and we want to use inversion on it to solve the goal. We'd like to be able to say to Coq, "find a contradictory assumption and invert it" without giving its name explicitly. Doing solve by inversion will find a hypothesis that can be inverted to solve the goal, if there is one. The tactics solve by inversion 2 and solve by inversion 3 are slightly fancier versions which will perform two or three inversions in a row, if necessary, to solve the goal. (These tactics are not actually built into Coq — their definitions are in Sflib.) Caution: Overuse of solve by inversion can lead to slow proof scripts.

The try solve Tactic

If t is a tactic, then try solve [t] is a tactic that

• if t solves the goal, behaves just like t, or
• if t cannot completely solve the goal, does nothing.

More generally, try solve [t₁ | t₂ | ...] will try to solve the goal by using t₁, t₂, etc. If none of them succeeds in completely solving the goal, then try solve [t₁ | t₂ | ...] does nothing.

The f_equal Tactic

f_equal replaces a goal of the form f x1 x2 ... xn = f y1 y2 ... yn, where f is some function, with the subgoals x1 = y1, x2 = y2,...,xn = yn. It is useful for avoiding explicit rewriting steps, and often the generated subgoals can be quickly cleared by auto. This tactic is not fundamental, in the sense that it can always be replaced by a sequence of asserts. However in some cases it can be very handy.

The normalize Tactic

When experimenting with definitions of programming languages in Coq, we often want to see what a particular concrete term steps to — i.e., we want to find proofs for goals of the form t ⇒* t', where t is a completely concrete term and t' is unknown. These proofs are simple but repetitive to do by hand. Consider for example reducing an arithmetic expression using the small-step relation astep defined in the previous chapter:

We repeatedly apply multi_step until we get to a normal form. The proofs that the intermediate steps are possible are simple enough that auto, with appropriate hints, can solve them.

The following custom Tactic Notation definition captures this pattern. In addition, before each multi_step we print out the current goal, so that the user can follow how the term is being evaluated.

The normalize tactic also provides a simple way to calculate what the normal form of a term is, by proving a goal with an existential variable in it.

Exercise: 1 star (normalize_ex)

☐

Exercise: 1 star, optional (normalize_ex')

For comparison, prove it using apply instead of eapply.

☐