AutoMore Automation

Consider the proof below, showing that ceval is deterministic. There's a lot of repetition and a lot of near-repetition...
Theorem ceval_deterministic: ∀c st st1 st2,
    st =[ c ]⇒ st1 →
    st =[ c ]⇒ st2 →
    st1 = st2.
Proof.
  intros c st st1 st2 E1 E2;
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst.
  - (* E_Skip *) reflexivity.
  - (* E_Ass *) reflexivity.
  - (* E_Seq *)
    assert (st' = st'0) as EQ1.
    { (* Proof of assertion *) apply IHE1_1; apply H1. }
    subst st'0.
    apply IHE1_2. assumption.
  (* E_IfTrue *)
  - (* b evaluates to true *)
    apply IHE1. assumption.
  - (* b evaluates to false (contradiction) *)
    rewrite H in H5. discriminate.
  (* E_IfFalse *)
  - (* b evaluates to true (contradiction) *)
    rewrite H in H5. discriminate.
  - (* b evaluates to false *)
    apply IHE1. assumption.
  (* E_WhileFalse *)
  - (* b evaluates to false *)
    reflexivity.
  - (* b evaluates to true (contradiction) *)
    rewrite H in H2. discriminate.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rewrite H in H4. discriminate.
  - (* b evaluates to true *)
    assert (st' = st'0) as EQ1.
    { (* Proof of assertion *) apply IHE1_1; assumption. }
    subst st'0.
    apply IHE1_2. assumption. Qed.

The auto Tactic

Thus far, our proof scripts mostly apply relevant hypotheses or lemmas by name, and one at a time.
Example auto_example_1 : ∀(P Q R: Prop),
  (P → Q) → (Q → R) → P → R.
Proof.
  intros P Q R H1 H2 H3.
  apply H2. apply H1. assumption.
Qed.
The auto tactic frees us from this drudgery by searching for a sequence of applications that will prove the goal:
Example auto_example_1' : ∀(P Q R: Prop),
  (P → Q) → (Q → R) → P → R.
Proof.
  auto.
Qed.

The auto tactic solves goals that are solvable by any combination of
  • intros and
  • apply (of hypotheses from the local context, by default).
Here is a more interesting example showing auto's power:
Example auto_example_2 : ∀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.

Proof search could, in principle, take an arbitrarily long time, so there are limits to how far auto will search by default.
Example auto_example_3 : ∀(P Q R S T U: Prop),
  (P → Q) →
  (Q → R) →
  (R → S) →
  (S → T) →
  (T → U) →
  P →
  U.
Proof.
  (* When it cannot solve the goal, auto does nothing *)
  auto.
  (* Optional argument says how deep to search (default is 5) *)
  auto 6.
Qed.

auto considers the hypotheses in the current context together with a hint database of other lemmas and constructors. Some common facts about equality and logical operators are installed in the hint database by default.
Example auto_example_4 : ∀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 by writing "auto using ...".
Lemma le_antisym : ∀n m: nat, (n ≤ m ∧ m ≤ n) → n = m.
Proof. intros. omega. Qed.
Example auto_example_6 : ∀n m p : nat,
  (n ≤ p → (n ≤ m ∧ m ≤ n)) →
  n ≤ p →
  n = m.
Proof.
  intros.
  auto using le_antisym.
Qed.

We can also permanently extend the hint database:
  • Hint Resolve T.
    Add theorem or constructor T to the global DB
  • Hint Constructors c.
    Add all constructors of c to the global DB
  • Hint Unfold d.
    Automatically expand defined symbol d during auto
It is also possible to define specialized hint databases that can be activated only when needed. See the Coq reference manual for more.

Hint Resolve le_antisym.
Example auto_example_6' : ∀n m p : nat,
  (n≤ p → (n ≤ m ∧ m ≤ n)) →
  n ≤ p →
  n = m.
Proof.
  intros.
  auto. (* picks up hint from database *)
Qed.

Definition is_fortytwo x := (x = 42).
Example auto_example_7: ∀x,
  (x ≤ 42 ∧ 42 ≤ x) → is_fortytwo x.
Proof.
  auto. (* does nothing *)
Abort.
Hint Unfold is_fortytwo.
Example auto_example_7' : ∀x,
  (x ≤ 42 ∧ 42 ≤ x) → is_fortytwo x.
Proof. auto. Qed.

Let's take a first pass over ceval_deterministic to simplify the proof script.
Theorem ceval_deterministic': ∀c st st1 st2,
    st =[ c ]⇒ st1 →
    st =[ c ]⇒ st2 →
    st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
       induction E1; intros st2 E2; inversion E2; subst; auto.
  - (* E_Seq *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto.
  - (* E_IfTrue *)
    + (* b evaluates to false (contradiction) *)
      rewrite H in H5. discriminate.
  - (* E_IfFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H5. discriminate.
  - (* E_WhileFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H2. discriminate.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rewrite H in H4. discriminate.
  - (* b evaluates to true *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto.
Qed.

Searching For Hypotheses

The proof has become simpler, but there is still an annoying amount of repetition.
Let's first tackle the contradiction cases. Each occurs where we have hypothesis of the form
      H1: beval st b = false
as well as:
      H2: beval st b = true
First step: abstracting out that piece of script in Ltac.
Ltac rwd H1 H2 := rewrite H1 in H2; discriminate.

Using rwd...
Theorem ceval_deterministic'': ∀c st st1 st2,
    st =[ c ]⇒ st1 →
    st =[ c ]⇒ st2 →
    st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst; auto.
  - (* E_Seq *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto.
  - (* E_IfTrue *)
    + (* b evaluates to false (contradiction) *)
      rwd H H5.
  - (* E_IfFalse *)
    + (* b evaluates to true (contradiction) *)
      rwd H H5.
  - (* E_WhileFalse *)
    + (* b evaluates to true (contradiction) *)
      rwd H H2.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rwd H H4.
  - (* b evaluates to true *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto. Qed.

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.
Ltac find_rwd :=
  match goal with
    H1: ?E = true,
    H2: ?E = false
    ⊢ _ ⇒ rwd H1 H2
  end.
The match goal tactic looks for hypotheses matching the pattern specified. In this case, we're looking for two equalities H1 and H2 equating the same thing ?E to true and false.

Theorem ceval_deterministic''': ∀c st st1 st2,
    st =[ c ]⇒ st1 →
    st =[ c ]⇒ st2 →
    st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst; try find_rwd; auto.
  - (* E_Seq *)
    assert (st' = st'0) as EQ1 by auto.
    subst st'0.
    auto.
  - (* E_WhileTrue *)
    + (* b evaluates to true *)
      assert (st' = st'0) as EQ1 by auto.
      subst st'0.
      auto. Qed.

Now for the remaining cases. Each applies a conditional hypothesis to extract an equality. Let's first rephrase a bit, replacing our use of assertions by equivalent rewriting.
Theorem ceval_deterministic'''': ∀c st st1 st2,
    st =[ c ]⇒ st1 →
    st =[ c ]⇒ st2 →
    st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst; try find_rwd; auto.
  - (* E_Seq *)
    rewrite (IHE1_1 st'0 H1) in *. auto.
  - (* E_WhileTrue *)
    + (* b evaluates to true *)
      rewrite (IHE1_1 st'0 H3) in *. auto. Qed.

Now we can automate the task of finding the relevant hypotheses to rewrite with.
Ltac find_eqn :=
  match goal with
    H1: ∀x, ?P x → ?L = ?R,
    H2: ?P ?X
    ⊢ _ ⇒ rewrite (H1 X H2) in *
  end.

Now we can make use of find_eqn to repeatedly rewrite with the appropriate hypothesis, wherever it may be found.
In our example proof, we repeat find_eqn, which will repeatedly rewrite until only trivial rewrites are available (since rewrite fails when given a trivial equation).
Theorem ceval_deterministic''''': ∀c st st1 st2,
    st =[ c ]⇒ st1 →
    st =[ c ]⇒ st2 →
    st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst; try find_rwd;
    repeat find_eqn; auto.
Qed.

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.
Module Repeat.
Inductive com : Type :=
  | CSkip
  | CAsgn (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com)
  | CRepeat (c : com) (b : bexp).
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.

Notation "'SKIP'" :=
  CSkip.
Notation "c1 ; c2" :=
  (CSeq c1 c2) (at level 80, right associativity).
Notation "X '::=' a" :=
  (CAsgn X a) (at level 60).
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity).
Notation "'TEST' e1 'THEN' e2 'ELSE' e3 'FI'" :=
  (CIf e1 e2 e3) (at level 80, right associativity).
Notation "'REPEAT' e1 'UNTIL' b2 'END'" :=
  (CRepeat e1 b2) (at level 80, right associativity).

Inductive ceval : state → com → state → Prop :=
  | E_Skip : ∀st,
      ceval st SKIP st
  | E_Ass : ∀st a1 n X,
      aeval st a1 = n →
      ceval st (X ::= a1) (t_update st X n)
  | E_Seq : ∀c1 c2 st st' st'',
      ceval st c1 st' →
      ceval st' c2 st'' →
      ceval st (c1 ; c2) st''
  | E_IfTrue : ∀st st' b1 c1 c2,
      beval st b1 = true →
      ceval st c1 st' →
      ceval st (TEST b1 THEN c1 ELSE c2 FI) st'
  | E_IfFalse : ∀st st' b1 c1 c2,
      beval st b1 = false →
      ceval st c2 st' →
      ceval st (TEST b1 THEN c1 ELSE c2 FI) st'
  | E_WhileFalse : ∀b1 st c1,
      beval st b1 = false →
      ceval st (WHILE b1 DO c1 END) st
  | E_WhileTrue : ∀st st' st'' b1 c1,
      beval st b1 = true →
      ceval st c1 st' →
      ceval st' (WHILE b1 DO c1 END) st'' →
      ceval st (WHILE b1 DO c1 END) st''
  | E_RepeatEnd : ∀st st' b1 c1,
      ceval st c1 st' →
      beval st' b1 = true →
      ceval st (CRepeat c1 b1) st'
  | E_RepeatLoop : ∀st st' st'' b1 c1,
      ceval st c1 st' →
      beval st' b1 = false →
      ceval st' (CRepeat c1 b1) st'' →
      ceval st (CRepeat c1 b1) st''.
Notation "st '=[' c ']⇒' st'" := (ceval st c st')
                                 (at level 40).

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.
Theorem ceval_deterministic: ∀c st st1 st2,
    st =[ c ]⇒ st1 →
    st =[ c ]⇒ st2 →
    st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1;
    intros st2 E2; inversion E2; subst; try find_rwd; repeat find_eqn; auto.
  - (* E_RepeatEnd *)
    + (* b evaluates to false (contradiction) *)
       find_rwd.
       (* oops: why didn't find_rwd solve this for us already?
          answer: we did things in the wrong order. *)
  - (* E_RepeatLoop *)
     + (* b evaluates to true (contradiction) *)
        find_rwd.
Qed.

Fortunately, to fix this, we just have to swap the invocations of find_eqn and find_rwd.
Theorem ceval_deterministic': ∀c st st1 st2,
    st =[ c ]⇒ st1 →
    st =[ c ]⇒ st2 →
    st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1;
    intros st2 E2; inversion E2; subst; repeat find_eqn; try find_rwd; auto.
Qed.
End Repeat.

The eapply and eauto variants

Recall this example from the Imp chapter:
Example ceval_example1:
  empty_st =[
    X ::= 2;;
    TEST X ≤ 1
      THEN Y ::= 3
      ELSE Z ::= 4
    FI
  ]⇒ (Z !-> 4 ; X !-> 2).
Proof.
  (* We supply the intermediate state st'... *)
  apply E_Seq with (X !-> 2).
  - apply E_Ass. reflexivity.
  - apply E_IfFalse. reflexivity. apply E_Ass. reflexivity.
Qed.
In the first step of the proof, we had to explicitly provide a longish expression, due to the "hidden" argument st' to the E_Seq constructor:
          E_Seq : ∀c1 c2 st st' st'',
            st  =[ c1 ]⇒ st'  →
            st' =[ c2 ]⇒ st'' →
            st  =[ c1 ;; c2 ]⇒ st''
If we leave out the with, this step fails, because Coq cannot find an instance for the variable st'. But this is silly! The appropriate value for st' will become obvious in the very next step.

With eapply, we can eliminate this silliness:
Example ceval'_example1:
  empty_st =[
    X ::= 2;;
    TEST X ≤ 1
      THEN Y ::= 3
      ELSE Z ::= 4
    FI
  ]⇒ (Z !-> 4 ; X !-> 2).
Proof.
  eapply E_Seq. (* 1 *)
  - apply E_Ass. (* 2 *)
    reflexivity. (* 3 *)
  - (* 4 *) apply E_IfFalse. reflexivity. apply E_Ass. reflexivity.
Qed.

Several of the tactics that we've seen so far, including ∃, constructor, and auto, have similar variants. For example, here's a proof using eauto:
Hint Constructors ceval.
Hint Transparent state.
Hint Transparent total_map.
Definition st12 := (Y !-> 2 ; X !-> 1).
Definition st21 := (Y !-> 1 ; X !-> 2).
Example eauto_example : ∃s',
  st21 =[
    TEST X ≤ Y
      THEN Z ::= Y - X
      ELSE Y ::= X + Z
    FI
  ]⇒ s'.
Proof. eauto. Qed.
The eauto tactic works just like auto, except that it uses eapply instead of apply.
Pro tip: One might think that, since eapply and eauto are more powerful than apply and auto, it would be a good idea to 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.