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 larger 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.
If we want to see which facts auto is using, we can use info_auto instead.

Example auto_example_5: 2 = 2.
Proof.
  info_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
It is also possible to define specialized hint databases that can be activated only when needed. See the Coq reference manual for details.

Hint Resolve le_antisym.
Example auto_example_6' : ∀ n m p : nat,
  (n≤ p → (n ≤ m ∧ m ≤ n)) →
  n ≤ p →
  n = m.
Proof.
  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. (* try also: info_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 as a 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 expression ?E to both 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.

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;
    try 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
  | 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 "x '::=' a" :=
  (CAss x a) (at level 60).
Notation "c1 ;; c2" :=
  (CSeq c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity).
Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" :=
  (CIf c1 c2 c3) (at level 80, right associativity).
Notation "'REPEAT' c 'UNTIL' b 'END'" :=
  (CRepeat c b) (at level 80, right associativity).

Reserved Notation "st '=[' c ']=>' st'"
                  (at level 40).
Inductive ceval : com → state → state → Prop :=
  | E_Skip : ∀ st,
      st =[ SKIP ]=> st
  | E_Ass : ∀ st a1 n x,
      aeval st a1 = n →
      st =[ x ::= a1 ]=> (x !-> n ; st)
  | E_Seq : ∀ c1 c2 st st' st'',
      st =[ c1 ]=> st' →
      st' =[ c2 ]=> st'' →
      st =[ c1 ;; c2 ]=> st''
  | E_IfTrue : ∀ st st' b c1 c2,
      beval st b = true →
      st =[ c1 ]=> st' →
      st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
  | E_IfFalse : ∀ st st' b c1 c2,
      beval st b = false →
      st =[ c2 ]=> st' →
      st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
  | E_WhileFalse : ∀ b st c,
      beval st b = false →
      st =[ WHILE b DO c END ]=> st
  | E_WhileTrue : ∀ st st' st'' b c,
      beval st b = true →
      st =[ c ]=> st' →
      st' =[ WHILE b DO c END ]=> st'' →
      st =[ WHILE b DO c END ]=> st''
  | E_RepeatEnd : ∀ st st' b c,
      st =[ c ]=> st' →
      beval st' b = true →
      st =[ REPEAT c UNTIL b END ]=> st'
  | E_RepeatLoop : ∀ st st' st'' b c,
      st =[ c ]=> st' →
      beval st' b = false →
      st' =[ REPEAT c UNTIL b END ]=> st'' →
      st =[ REPEAT c UNTIL b END ]=> st''

  where "st =[ c ]=> st'" := (ceval c 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,
    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; try 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; try find_eqn; try find_rwd; auto.
Qed.
End Repeat.

Tactics eapply and eauto

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. The eauto tactic works like auto, except that it uses eapply instead of apply. Tactic info_eauto shows us which tactics eauto uses in its proof search.
Below is an example of eauto. Before using it, we need to give some hints to auto about using the constructors of ceval and the definitions of state and total_map as part of its proof search.

Hint Constructors ceval.
Hint Transparent state total_map.
Example eauto_example : ∃ s',
  (Y !-> 1; X !-> 2) =[
    TEST X ≤ Y
      THEN Z ::= Y - X
      ELSE Y ::= X + Z
    FI
  ]=> s'.
Proof. info_eauto. Qed.