# AutoMore Automation

Require Export Smallstep.

# The auto and eauto Tactics

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

Lemma auto_example_1 : ∀P Q R S T U : Prop,

(P → Q) →

(P → R) →

(T → R) →

(S → T → U) →

((P→Q) → (P→S)) →

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
It is also sometimes necessary to add
Here are some Hints we will find useful.

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

# The solve by inversion Tactic

# The try solve Tactic

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

_{1}| t

_{2}| ...] will try to solve the goal by using t

_{1}, t

_{2}, etc. If none of them succeeds in completely solving the goal, then try solve [t

_{1}| t

_{2}| ...] does nothing.

# The f_equal Tactic

# The normalize Tactic

Definition amultistep st := multi (astep st).

Notation " t '/' st '⇒

(at level 40, st at level 39).

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.

Theorem normalize_ex : ∃e',

(AMult (ANum 3) (AMult (ANum 2) (ANum 1))) / empty_state

⇒

Proof.

(* FILL IN HERE *) Admitted.

(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) $ *)