(** * Auto: More Automation *)
Set Warnings "-notation-overridden,-parsing".
From Coq Require Import omega.Omega.
From LF Require Import Maps.
From LF Require Import Imp.
(** Consider the proof below, showing that [ceval] is
deterministic. There's a lot of repetition and a lot of
near-repetition... *)
Theorem ceval_deterministic: forall 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 : forall (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' : forall (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 : forall 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 : forall (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 : forall 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 : forall n m: nat, (n <= m /\ m <= n) -> n = m.
Proof. intros. omega. Qed.
Example auto_example_6 : forall 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' : forall 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: forall x,
(x <= 42 /\ 42 <= x) -> is_fortytwo x.
Proof.
auto. (* does nothing *)
Abort.
Hint Unfold is_fortytwo.
Example auto_example_7' : forall 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': forall 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'': forall 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''': forall 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'''': forall 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: forall 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''''': forall 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 : forall st,
ceval st SKIP st
| E_Ass : forall st a1 n X,
aeval st a1 = n ->
ceval st (X ::= a1) (t_update st X n)
| E_Seq : forall c1 c2 st st' st'',
ceval st c1 st' ->
ceval st' c2 st'' ->
ceval st (c1 ; c2) st''
| E_IfTrue : forall 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 : forall 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 : forall b1 st c1,
beval st b1 = false ->
ceval st (WHILE b1 DO c1 END) st
| E_WhileTrue : forall 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 : forall st st' b1 c1,
ceval st c1 st' ->
beval st' b1 = true ->
ceval st (CRepeat c1 b1) st'
| E_RepeatLoop : forall 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: forall 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': forall 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 : forall 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 [exists],
[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 : exists 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. *)