AutoMore Automation

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

Require Export Smallstep.

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:

Lemma auto_example_1 : P Q R S T U : Prop,
  (P Q)
  (P R)
  (T R)
  (S T U)
  ((PQ) (PS))
  T
  P
  U.
Proof. auto. Qed.

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.

Lemma auto_example_2 : P Q R : Prop,
  Q
  (Q R)
  P (Q R).
Proof.
  auto. Qed.

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:

Lemma auto_example_2a : P Q R : Prop,
  Q
  (Q R)
  P (Q R).
Proof.
  auto using conj, or_introl, or_intror. Qed.

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
      Hint Resolve T.
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.
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.
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.

Hint Constructors multi.
Hint Resolve beq_id_eq beq_id_false_not_eq.

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 [t1 | t2 | ...] will try to solve the goal by using t1, t2, etc. If none of them succeeds in completely solving the goal, then try solve [t1 | t2 | ...] 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:

Definition amultistep st := multi (astep st).
Notation " t '/' st 'a*' t' " := (amultistep st t t')
  (at level 40, st at level 39).

Example astep_example1 :
  (APlus (ANum 3) (AMult (ANum 3) (ANum 4))) / empty_state
  a* (ANum 15).
Proof.
  apply multi_step with (APlus (ANum 3) (ANum 12)).
    apply AS_Plus2.
      apply av_num.
      apply AS_Mult.
  apply multi_step with (ANum 15).
    apply AS_Plus.
  apply multi_refl.
Qed.

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.

Hint Constructors astep aval.
Example astep_example1' :
  (APlus (ANum 3) (AMult (ANum 3) (ANum 4))) / empty_state
  a* (ANum 15).
Proof.
  eapply multi_step. auto. simpl.
  eapply multi_step. auto. simpl.
  apply multi_refl.
Qed.

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.

Tactic Notation "print_goal" := match goal with ?x => idtac x end.
Tactic Notation "normalize" :=
   repeat (print_goal; eapply multi_step ;
             [ (eauto 10; fail) | (instantiate; simpl)]);
   apply multi_refl.

Example astep_example1'' :
  (APlus (ANum 3) (AMult (ANum 3) (ANum 4))) / empty_state
  a* (ANum 15).
Proof.
  normalize.
  (* At this point in the proof script, the Coq response shows 
     a trace of how the expression evaluated. 

   (APlus (ANum 3) (AMult (ANum 3) (ANum 4)) / empty_state ==>a* ANum 15)
   (multi (astep empty_state) (APlus (ANum 3) (ANum 12)) (ANum 15))
   (multi (astep empty_state) (ANum 15) (ANum 15))
*)

Qed.

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.

Example astep_example1''' : e',
  (APlus (ANum 3) (AMult (ANum 3) (ANum 4))) / empty_state
  a* e'.
Proof.
  eapply ex_intro. normalize.

(* This time, the trace will be:

    (APlus (ANum 3) (AMult (ANum 3) (ANum 4)) / empty_state ==>a* ??)
    (multi (astep empty_state) (APlus (ANum 3) (ANum 12)) ??)
    (multi (astep empty_state) (ANum 15) ??)

   where ?? is the variable ``guessed'' by eapply.
*)

Qed.

Exercise: 1 star (normalize_ex)

Theorem normalize_ex : e',
  (AMult (ANum 3) (AMult (ANum 2) (ANum 1))) / empty_state
  a* e'.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, optional (normalize_ex')

For comparison, prove it using apply instead of eapply.

Theorem normalize_ex' : e',
  (AMult (ANum 3) (AMult (ANum 2) (ANum 1))) / empty_state
  a* e'.
Proof.
  (* FILL IN HERE *) Admitted.

(* $Date: 2013-04-10 10:12:40 -0400 (Wed, 10 Apr 2013) $ *)