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,
     c / st \\ st1 →
     c / st \\ 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 *)
    apply IHE1_1 in H1. subst.
    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 *)
    apply IHE1_1 in H3. subst.
    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.
  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
In general, we want to put our own tactics in their own databases, so they don't clutter up (and slow down) the default database. For this lecture, we'll use the example database ex_db which we invoke via auto with ex_db

Hint Resolve le_antisym : ex_db.
Example auto_example_6' : ∀ n m p : nat,
  (n≤ p → (n ≤ m ∧ m ≤ n)) →
  n ≤ p →
  n = m.
Proof.
  intros.
  auto with ex_db. (* 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 with ex_db. (* does nothing *)
Abort.
Hint Unfold is_fortytwo : ex_db.
Example auto_example_7' : ∀ x,
  (x ≤ 42 ∧ 42 ≤ x) → is_fortytwo x.
Proof. auto with ex_db. Qed.
We can check which hints are in our database via the following command
Print HintDb ex_db.

Let's take a first pass over ceval_deterministic to simplify the proof script.
Theorem ceval_deterministic': ∀ c st st1 st2,
     c / st \\ st1 →
     c / st \\ 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 *)
    apply IHE1_1 in H1. subst. auto.
  - (* E_IfTrue *)
    + (* b evaluates to false (contradiction) *)
      rewrite H in H5. inversion H5.
  - (* E_IfFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H5. inversion H5.
  - (* E_WhileFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H2. inversion H2.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rewrite H in H4. inversion H4.
  - (* b evaluates to true *)
    apply IHE1_1 in H3. subst. 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 Coq's tactic scripting language, Ltac.
Ltac rwdisc H1 H2 := rewrite H1 in H2; discriminate.
(* NOTE: RNR: Also, inv isn't necessary *and* our students already
   know about the discriminate tactic! *)

Using rwinv...
Theorem ceval_deterministic'': ∀ c st st1 st2,
     c / st \\ st1 →
     c / st \\ 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 *)
    apply IHE1_1 in H1. subst. auto.
  - (* E_IfTrue *)
    + (* b evaluates to false (contradiction) *)
      rwdisc H H5.
  - (* E_IfFalse *)
    + (* b evaluates to true (contradiction) *)
      rwdisc H H5.
  - (* E_WhileFalse *)
    + (* b evaluates to true (contradiction) *)
      rwdisc H H2.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rwdisc H H4.
  - (* b evaluates to true *)
    apply IHE1_1 in H3. subst. 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_rwdisc :=
  match goal with
    H1: ?E = true, H2: ?E = false |- _ ⇒ rwdisc 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,
     c / st \\ st1 →
     c / st \\ st2 →
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst; try find_rwdisc; auto.
  - (* E_Seq *)
    apply IHE1_1 in H1. subst. auto.
  - (* E_WhileTrue *)
    apply IHE1_1 in H3. subst. auto.
Qed.

Now for the remaining cases. Each applies a conditional hypothesis to extract an equality. Let's automate this task!
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,
     c / st \\ st1 →
     c / st \\ st2 →
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst; try find_rwdisc;
    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 whether it really is, let's try adding a REPEAT command to the language.
Module Repeat.
(* NOTE: RNR: CAsgn is CAss in Imp.v. Consistency would be nice. Also,
   what happened to our nice definition of ceval with notations??? 
   Actually, going to fix these in my version. *)
Inductive com : Type :=
  | CSkip
  | CAss (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" :=
  (CAss X a) (at level 60).
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity).
Notation "'IFB' 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).

Reserved Notation "c1 '/' st '\\' st'"
                  (at level 40, st at level 39).
Inductive ceval : com → state → state → Prop :=
  | E_Skip : ∀ st,
      SKIP / st \\ st
  | E_Ass : ∀ st a1 n x,
      aeval st a1 = n →
      (x ::= a1) / st \\ st & { x --> n }
  | E_Seq : ∀ c1 c2 st st' st'',
      c1 / st \\ st' →
      c2 / st' \\ st'' →
      (c1 ;; c2) / st \\ st''
  | E_IfTrue : ∀ st st' b c1 c2,
      beval st b = true →
      c1 / st \\ st' →
      (IFB b THEN c1 ELSE c2 FI) / st \\ st'
  | E_IfFalse : ∀ st st' b c1 c2,
      beval st b = false →
      c2 / st \\ st' →
      (IFB b THEN c1 ELSE c2 FI) / st \\ st'
  | E_WhileFalse : ∀ b st c,
      beval st b = false →
      (WHILE b DO c END) / st \\ st
  | E_WhileTrue : ∀ st st' st'' b c,
      beval st b = true →
      c / st \\ st' →
      (WHILE b DO c END) / st' \\ st'' →
      (WHILE b DO c END) / st \\ st''
  | E_RepeatEnd : ∀ st st' b1 c1,
      c1 / st \\ st' →
      beval st' b1 = true →
      (CRepeat c1 b1) / st \\ st'
  | E_RepeatLoop : ∀ st st' st'' b1 c1,
      c1 / st \\ st' →
      beval st' b1 = false →
      (CRepeat c1 b1) / st' \\ st'' →
      (CRepeat c1 b1) / st \\ st''

  where "c1 '/' st '\\' st'" := (ceval c1 st st').

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

Fortunately, to fix this, we just have to swap the invocations of find_eqn and find_rwinv.
Theorem ceval_deterministic': ∀ c st st1 st2,
     c / st \\ st1 →
     c / st \\ 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_rwdisc; auto.
Qed.
End Repeat.

The eapply and eauto variants

Recall this example from the Imp chapter:
Example ceval_example1:
    (X ::= 2;;
     IFB X ≤ 1
       THEN Y ::= 3
       ELSE Z ::= 4
     FI)
   / { --> 0 }
   \\ { X --> 2 ; Z --> 4 }.
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'',
            c1 / st  \\ st' →
            c2 / st' \\ st'' →
            (c1 ;; c2) / st \\ 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:
    (X ::= 2;;
     IFB X ≤ 1
       THEN Y ::= 3
       ELSE Z ::= 4
     FI)
   / { --> 0 }
   \\ { X --> 2 ; Z --> 4 }.
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 e... variants. For example, here's a proof using eauto:
Hint Constructors ceval : ex_db.
Hint Transparent state : ex_db.
Hint Transparent total_map : ex_db.
Definition st12 := { X --> 1 ; Y --> 2 }.
Definition st21 := { X --> 2 ; Y --> 1 }.
Example eauto_example : ∃ s',
  (IFB X ≤ Y
    THEN Z ::= Y - X
    ELSE Y ::= X + Z
  FI) / st21 \\ s'.
Proof. eauto with ex_db. 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.

Homework

No homework for this chapter - don't bother turning it in. But go back to earlier chapters and do some exercises using automation!