
AutoMore Automation
xxxxxxxxxx
1
Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
2
From Coq Require Import Lia.
3
From LF Require Import Maps.
4
From LF Require Import Imp.
Up to now, we've used the more manual part of Coq's tactic
facilities. In this chapter, we'll learn more about some of Coq's
powerful automation features: proof search via the auto tactic,
automated forward reasoning via the Ltac hypothesis matching
machinery, and deferred instantiation of existential variables
using eapply and eauto. Using these features together with
Ltac's scripting facilities will enable us to make our proofs
startlingly short! Used properly, they can also make proofs more
maintainable and robust to changes in underlying definitions. A
deeper treatment of auto and eauto can be found in the
UseAuto chapter in Programming Language Foundations.
There's another major category of automation we haven't discussed
much yet, namely built-in decision procedures for specific kinds
of problems: lia is one example, but there are others. This
topic will be deferred for a while longer.
Our motivating example will be this proof, repeated with just a
few small changes from the Imp chapter. We will simplify
this proof in several stages.
xxxxxxxxxx
5
Theorem ceval_deterministic: ∀ c st st1 st2,
6
st =[ c ] st1
7
st =[ c ] st2
8
st1 = st2.
9
Proof.
10
intros c st st1 st2 E1 E2;
11
generalize dependent st2;
12
induction E1; intros st2 E2; inversion E2; subst.
13
- (* E_Skip *) reflexivity.
14
- (* E_Ass *) reflexivity.
15
- (* E_Seq *)
16
rewrite (IHE1_1 st'0 H1) in *.
17
apply IHE1_2. assumption.
18
(* E_IfTrue *)
19
- (* b evaluates to true *)
20
apply IHE1. assumption.
21
- (* b evaluates to false (contradiction) *)
22
rewrite H in H5. discriminate.
23
(* E_IfFalse *)
24
- (* b evaluates to true (contradiction) *)
25
rewrite H in H5. discriminate.
26
- (* b evaluates to false *)
27
apply IHE1. assumption.
28
(* E_WhileFalse *)
29
- (* b evaluates to false *)
30
reflexivity.
31
- (* b evaluates to true (contradiction) *)
32
rewrite H in H2. discriminate.
33
(* E_WhileTrue *)
34
- (* b evaluates to false (contradiction) *)
35
rewrite H in H4. discriminate.
36
- (* b evaluates to true *)
37
rewrite (IHE1_1 st'0 H3) in *.
38
apply IHE1_2. assumption. Qed.
The auto Tactic
xxxxxxxxxx
44
39
Example auto_example_1 : ∀ (P Q R: ),
40
(P Q) (Q R) P R.
41
Proof.
42
intros P Q R H1 H2 H3.
43
apply H2. apply H1. assumption.
44
Qed.
The auto tactic frees us from this drudgery by searching for a
sequence of applications that will prove the goal:
xxxxxxxxxx
49
45
Example auto_example_1' : ∀ (P Q R: ),
46
(P Q) (Q R) P R.
47
Proof.
48
auto.
49
Qed.
The auto tactic solves goals that are solvable by any combination of
Using auto is always "safe" in the sense that it will never fail
and will never change the proof state: either it completely solves
the current goal, or it does nothing.
Here is a larger example showing auto's power:
- intros and
- apply (of hypotheses from the local context, by default).
xxxxxxxxxx
10
50
Example auto_example_2 : ∀ P Q R S T U : ,
51
(P Q)
52
(P R)
53
(T R)
54
(S T U)
55
((P Q) (P S))
56
T
57
P
58
U.
59
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.
xxxxxxxxxx
60
Example auto_example_3 : ∀ (P Q R S T U: ),
61
(P Q)
62
(Q R)
63
(R S)
64
(S T)
65
(T U)
66
P
67
U.
68
Proof.
69
(* When it cannot solve the goal, auto does nothing *)
70
auto.
71
(* Optional argument says how deep to search (default is 5) *)
72
auto 6.
73
Qed.
When searching for potential proofs of the current goal,
auto considers the hypotheses in the current context together
with a hint database of other lemmas and constructors. Some
common lemmas about equality and logical operators are installed
in this hint database by default.
xxxxxxxxxx
78
74
Example auto_example_4 : ∀ P Q R : ,
75
Q
76
(Q R)
77
P (Q R).
78
Proof. auto. Qed.
If we want to see which facts auto is using, we can use
info_auto instead.
xxxxxxxxxx
79
Example auto_example_5: 2 = 2.
80
Proof.
81
info_auto.
82
Qed.
83
Example auto_example_5' : ∀ (P Q R S T U W: ),
84
(U T)
85
(W U)
86
(R S)
87
(S T)
88
(P R)
89
(U T)
90
P
91
T.
92
Proof.
93
intros.
94
info_auto.
95
Qed.
We can extend the hint database just for the purposes of one
application of auto by writing "auto using ...".
xxxxxxxxxx
104
96
Lemma le_antisym : ∀ n m: , (n m m n) n = m.
97
Proof. lia. Qed.
98
Example auto_example_6 : ∀ n m p : ,
99
(n p (n m m n))
100
n p
101
n = m.
102
Proof.
103
auto using le_antisym.
104
Qed.
Of course, in any given development there will probably be
some specific constructors and lemmas that are used very often in
proofs. We can add these to the global hint database by writing
Hint Resolve T : core.
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 : core.
to tell Coq to do a Hint Resolve for all of the constructors
from the inductive definition of c.
It is also sometimes necessary to add
Hint Unfold d : core.
where d is a defined symbol, so that auto knows to expand uses
of d, thus enabling further possibilities for applying lemmas that
it knows about.
It is also possible to define specialized hint databases (besides
core) that can be activated only when needed; indeed, it is good
style to create your own hint databases instead of polluting
core. See the Coq reference manual for details.
Hint Resolve T : core.
Hint Constructors c : core.
Hint Unfold d : core.
xxxxxxxxxx
124
105
Hint Resolve le_antisym : core.
106
Example auto_example_6' : ∀ n m p : ,
107
(n p (n m m n))
108
n p
109
n = m.
110
Proof.
111
auto. (* picks up hint from database *)
112
Qed.
113
Definition is_fortytwo x := (x = 42).
114
Example auto_example_7: ∀ x,
115
(x 42 42 x) is_fortytwo x.
116
Proof.
117
auto. (* does nothing *)
118
Abort.
119
Hint Unfold is_fortytwo : core.
120
Example auto_example_7' : ∀ x,
121
(x 42 42 x) is_fortytwo x.
122
Proof.
123
auto. (* try also: info_auto. *)
124
Qed.
Let's take a first pass over ceval_deterministic to simplify the
proof script.
xxxxxxxxxx
151
125
Theorem ceval_deterministic': ∀ c st st1 st2,
126
st =[ c ] st1
127
st =[ c ] st2
128
st1 = st2.
129
Proof.
130
intros c st st1 st2 E1 E2.
131
generalize dependent st2;
132
induction E1; intros st2 E2; inversion E2; subst; auto.
133
- (* E_Seq *)
134
rewrite (IHE1_1 st'0 H1) in *.
135
auto.
136
- (* E_IfTrue *)
137
+ (* b evaluates to false (contradiction) *)
138
rewrite H in H5. discriminate.
139
- (* E_IfFalse *)
140
+ (* b evaluates to true (contradiction) *)
141
rewrite H in H5. discriminate.
142
- (* E_WhileFalse *)
143
+ (* b evaluates to true (contradiction) *)
144
rewrite H in H2. discriminate.
145
(* E_WhileTrue *)
146
- (* b evaluates to false (contradiction) *)
147
rewrite H in H4. discriminate.
148
- (* b evaluates to true *)
149
rewrite (IHE1_1 st'0 H3) in *.
150
auto.
151
Qed.
When we are using a particular tactic many times in a proof, we
can use a variant of the Proof command to make that tactic into
a default within the proof. Saying Proof with t (where t is
an arbitrary tactic) allows us to use t1... as a shorthand for
t1;t within the proof. As an illustration, here is an alternate
version of the previous proof, using Proof with auto.
xxxxxxxxxx
29
180
152
Theorem ceval_deterministic'_alt: ∀ c st st1 st2,
153
st =[ c ] st1
154
st =[ c ] st2
155
st1 = st2.
156
157
158
Proof with auto.
159
intros c st st1 st2 E1 E2;
160
generalize dependent st2;
161
induction E1;
162
intros st2 E2; inversion E2; subst...
163
- (* E_Seq *)
164
rewrite (IHE1_1 st'0 H1) in *...
165
- (* E_IfTrue *)
166
+ (* b evaluates to false (contradiction) *)
167
rewrite H in H5. discriminate.
168
- (* E_IfFalse *)
169
+ (* b evaluates to true (contradiction) *)
170
rewrite H in H5. discriminate.
171
- (* E_WhileFalse *)
172
+ (* b evaluates to true (contradiction) *)
173
rewrite H in H2. discriminate.
174
(* E_WhileTrue *)
175
- (* b evaluates to false (contradiction) *)
176
rewrite H in H4. discriminate.
177
- (* b evaluates to true *)
178
rewrite (IHE1_1 st'0 H3) in *...
179
Qed.
180
Searching For Hypotheses
H1: beval st b = false
H2: beval st b = true
xxxxxxxxxx
207
181
Ltac rwd H1 H2 := rewrite H1 in H2; discriminate.
182
Theorem ceval_deterministic'': ∀ c st st1 st2,
183
st =[ c ] st1
184
st =[ c ] st2
185
st1 = st2.
186
Proof.
187
intros c st st1 st2 E1 E2.
188
generalize dependent st2;
189
induction E1; intros st2 E2; inversion E2; subst; auto.
190
- (* E_Seq *)
191
rewrite (IHE1_1 st'0 H1) in *.
192
auto.
193
- (* E_IfTrue *)
194
+ (* b evaluates to false (contradiction) *)
195
rwd H H5.
196
- (* E_IfFalse *)
197
+ (* b evaluates to true (contradiction) *)
198
rwd H H5.
199
- (* E_WhileFalse *)
200
+ (* b evaluates to true (contradiction) *)
201
rwd H H2.
202
(* E_WhileTrue *)
203
- (* b evaluates to false (contradiction) *)
204
rwd H H4.
205
- (* b evaluates to true *)
206
rewrite (IHE1_1 st'0 H3) in *.
207
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.
xxxxxxxxxx
213
208
Ltac find_rwd :=
209
match goal with
210
H1: ?E = true,
211
H2: ?E = false
212
|- _ rwd H1 H2
213
end.
This match goal looks for two distinct hypotheses that
have the form of equalities, with the same arbitrary expression
E on the left and with conflicting boolean values on the right.
If such hypotheses are found, it binds H1 and H2 to their
names and applies the rwd tactic to H1 and H2.
Adding this tactic to the ones that we invoke in each case of the
induction handles all of the contradictory cases.
xxxxxxxxxx
228
214
Theorem ceval_deterministic''': ∀ c st st1 st2,
215
st =[ c ] st1
216
st =[ c ] st2
217
st1 = st2.
218
Proof.
219
intros c st st1 st2 E1 E2.
220
generalize dependent st2;
221
induction E1; intros st2 E2; inversion E2; subst; try find_rwd; auto.
222
- (* E_Seq *)
223
rewrite (IHE1_1 st'0 H1) in *.
224
auto.
225
- (* E_WhileTrue *)
226
+ (* b evaluates to true *)
227
rewrite (IHE1_1 st'0 H3) in *.
228
auto. Qed.
Let's see about the remaining cases. Each of them involves
rewriting a hypothesis after feeding it with the required
condition. We can automate the task of finding the relevant
hypotheses to rewrite with.
xxxxxxxxxx
234
229
Ltac find_eqn :=
230
match goal with
231
H1: ∀ x, ?P x ?L = ?R,
232
H2: ?P ?X
233
|- _ rewrite (H1 X H2) in *
234
end.
The pattern ∀ x, ?P x → ?L = ?R matches any hypothesis of
the form "for all x, some property of x implies some
equality." The property of x is bound to the pattern variable
P, and the left- and right-hand sides of the equality are bound
to L and R. The name of this hypothesis is bound to H1.
Then the pattern ?P ?X matches any hypothesis that provides
evidence that P holds for some concrete X. If both patterns
succeed, we apply the rewrite tactic (instantiating the
quantified x with X and providing H2 as the required
evidence for P X) in all hypotheses and the goal.
xxxxxxxxxx
244
235
Theorem ceval_deterministic'''': ∀ c st st1 st2,
236
st =[ c ] st1
237
st =[ c ] st2
238
st1 = st2.
239
Proof.
240
intros c st st1 st2 E1 E2.
241
generalize dependent st2;
242
induction E1; intros st2 E2; inversion E2; subst; try find_rwd;
243
try find_eqn; auto.
244
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.
xxxxxxxxxx
252
245
Module Repeat.
246
Inductive com : Type :=
247
| CSkip
248
| CAss (x : string) (a : aexp)
249
| CSeq (c1 c2 : com)
250
| CIf (b : bexp) (c1 c2 : com)
251
| CWhile (b : bexp) (c : com)
252
| 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.
xxxxxxxxxx
311
253
Notation "'repeat' x 'until' y 'end'" :=
254
(CRepeat x y)
255
(in custom com at level 0,
256
x at level 99, y at level 99).
257
Notation "'skip'" :=
258
CSkip (in custom com at level 0).
259
Notation "x := y" :=
260
(CAss x y)
261
(in custom com at level 0, x constr at level 0,
262
y at level 85, no associativity).
263
Notation "x ; y" :=
264
(CSeq x y)
265
(in custom com at level 90, right associativity).
266
Notation "'if' x 'then' y 'else' z 'end'" :=
267
(CIf x y z)
268
(in custom com at level 89, x at level 99,
269
y at level 99, z at level 99).
270
Notation "'while' x 'do' y 'end'" :=
271
(CWhile x y)
272
(in custom com at level 89, x at level 99, y at level 99).
273
Reserved Notation "st '=[' c ']=>' st'"
274
(at level 40, c custom com at level 99, st' constr at next level).
275
Inductive ceval : com state state :=
276
| E_Skip : ∀ st,
277
st =[ skip ] st
278
| E_Ass : ∀ st a1 n x,
279
aeval st a1 = n
280
st =[ x := a1 ] (x ! n ; st)
281
| E_Seq : ∀ c1 c2 st st' st'',
282
st =[ c1 ] st'
283
st' =[ c2 ] st''
284
st =[ c1 ; c2 ] st''
285
| E_IfTrue : ∀ st st' b c1 c2,
286
beval st b = true
287
st =[ c1 ] st'
288
st =[ if b then c1 else c2 end ] st'
289
| E_IfFalse : ∀ st st' b c1 c2,
290
beval st b = false
291
st =[ c2 ] st'
292
st =[ if b then c1 else c2 end ] st'
293
| E_WhileFalse : ∀ b st c,
294
beval st b = false
295
st =[ while b do c end ] st
296
| E_WhileTrue : ∀ st st' st'' b c,
297
beval st b = true
298
st =[ c ] st'
299
st' =[ while b do c end ] st''
300
st =[ while b do c end ] st''
301
| E_RepeatEnd : ∀ st st' b c,
302
st =[ c ] st'
303
beval st' b = true
304
st =[ repeat c until b end ] st'
305
| E_RepeatLoop : ∀ st st' st'' b c,
306
st =[ c ] st'
307
beval st' b = false
308
st' =[ repeat c until b end ] st''
309
st =[ repeat c until b end ] st''
310
311
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.
xxxxxxxxxx
329
312
Theorem ceval_deterministic: ∀ c st st1 st2,
313
st =[ c ] st1
314
st =[ c ] st2
315
st1 = st2.
316
Proof.
317
intros c st st1 st2 E1 E2.
318
generalize dependent st2;
319
induction E1;
320
intros st2 E2; inversion E2; subst; try find_rwd; try find_eqn; auto.
321
- (* E_RepeatEnd *)
322
+ (* b evaluates to false (contradiction) *)
323
find_rwd.
324
(* oops: why didn't find_rwd solve this for us already?
325
answer: we did things in the wrong order. *)
326
- (* E_RepeatLoop *)
327
+ (* b evaluates to true (contradiction) *)
328
find_rwd.
329
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.
These examples just give a flavor of what "hyper-automation"
can achieve in Coq. The details of match goal are a bit
tricky (and debugging scripts using it is, frankly, not very
pleasant). But it is well worth adding at least simple uses to
your proofs, both to avoid tedium and to "future proof" them.
To close the chapter, we'll introduce one more convenient feature
of Coq: its ability to delay instantiation of quantifiers. To
motivate this feature, recall this example from the Imp
chapter:
Tactics eapply and eauto
Example ceval_example1:
empty_st =[
X := 2;
if (X ≤ 1)
then Y := 3
else Z := 4
end
]=> (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 to help Coq instantiate a "hidden" argument to
the E_Seq constructor. This was needed because the definition
of E_Seq...
E_Seq : ∀ c1 c2 st st' st'',
st =[ c1 ]=> st' →
st' =[ c2 ]=> st'' →
st =[ c1 ; c2 ]=> st''
is quantified over a variable, st', that does not appear in its
conclusion, so unifying its conclusion with the goal state doesn't
help Coq find a suitable value for this variable. If we leave
out the with, this step fails ("Error: Unable to find an
instance for the variable st'").
What's silly about this error is that the appropriate value for st'
will actually become obvious in the very next step, where we apply
E_Ass. If Coq could just wait until we get to this step, there
would be no need to give the value explicitly. This is exactly what
the eapply tactic gives us:
E_Seq : ∀ c1 c2 st st' st'',
st =[ c1 ]=> st' →
st' =[ c2 ]=> st'' →
st =[ c1 ; c2 ]=> st''
Example ceval'_example1:
empty_st =[
X := 2;
if (X ≤ 1)
then Y := 3
else Z := 4
end
]=> (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.
The eapply H tactic behaves just like apply H except
that, after it finishes unifying the goal state with the
conclusion of H, it does not bother to check whether all the
variables that were introduced in the process have been given
concrete values during unification.
If you step through the proof above, you'll see that the goal
state at position 1 mentions the existential variable ?st'
in both of the generated subgoals. The next step (which gets us
to position 2) replaces ?st' with a concrete value. This new
value contains a new existential variable ?n, which is
instantiated in its turn by the following reflexivity step,
position 3. When we start working on the second
subgoal (position 4), we observe that the occurrence of ?st'
in this subgoal has been replaced by the value that it was given
during the first subgoal.
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 : core.
Hint Transparent state total_map : core.
Example eauto_example : ∃ s',
(Y !-> 1 ; X !-> 2) =[
if (X ≤ Y)
then Z := Y - X
else Y := X + Z
end
]=> s'.
Proof. info_eauto. Qed.
The eauto tactic works just like auto, except that it uses
eapply instead of apply; info_eauto shows us which facts
eauto uses.
Pro tip: One might think that, since eapply and eauto
are more powerful than apply and auto, we should just 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.
In order for Qed to succeed, all existential variables need to
be determined by the end of the proof. Otherwise Coq
will (rightly) refuse to accept the proof. Remember that the Coq
tactics build proof objects, and proof objects containing
existential variables are not complete.
Constraints on Existential Variables
Lemma silly1 : ∀ (P : nat → nat → Prop) (Q : nat → Prop),
(∀ x y : nat, P x y) →
(∀ x y : nat, P x y → Q x) →
Q 42.
Proof.
intros P Q HP HQ. eapply HQ. apply HP.
Fail Qed.
Coq gives a warning after apply HP. ("All the remaining goals
are on the shelf," means that we've finished all our top-level
proof obligations but along the way we've put some aside to be
done later, and we have not finished those.) Trying to close the
proof with Qed gives an error.
Abort.
An additional constraint is that existential variables cannot be
instantiated with terms containing ordinary variables that did not
exist at the time the existential variable was created. (The
reason for this technical restriction is that allowing such
instantiation would lead to inconsistency of Coq's logic.)
Lemma silly2 :
∀ (P : nat → nat → Prop) (Q : nat → Prop),
(∃ y, P 42 y) →
(∀ x y : nat, P x y → Q x) →
Q 42.
Proof.
intros P Q HP HQ. eapply HQ. destruct HP as [y HP'].
Fail apply HP'.
The error we get, with some details elided, is:
cannot instantiate "?y" because "y" is not in its scope
In this case there is an easy fix: doing destruct HP before
doing eapply HQ.
cannot instantiate "?y" because "y" is not in its scope
Abort.
Lemma silly2_fixed :
∀ (P : nat → nat → Prop) (Q : nat → Prop),
(∃ y, P 42 y) →
(∀ x y : nat, P x y → Q x) →
Q 42.
Proof.
intros P Q HP HQ. destruct HP as [y HP'].
eapply HQ. apply HP'.
Qed.
Lemma silly2_fixed :
∀ (P : nat → nat → Prop) (Q : nat → Prop),
(∃ y, P 42 y) →
(∀ x y : nat, P x y → Q x) →
Q 42.
Proof.
intros P Q HP HQ. destruct HP as [y HP'].
eapply HQ. apply HP'.
Qed.
The apply HP' in the last step unifies the existential variable
in the goal with the variable y.
Note that the assumption tactic doesn't work in this case, since
it cannot handle existential variables. However, Coq also
provides an eassumption tactic that solves the goal if one of
the premises matches the goal up to instantiations of existential
variables. We can use it instead of apply HP' if we like.
Lemma silly2_eassumption : ∀ (P : nat → nat → Prop) (Q : nat → Prop),
(∃ y, P 42 y) →
(∀ x y : nat, P x y → Q x) →
Q 42.
Proof.
intros P Q HP HQ. destruct HP as [y HP']. eapply HQ. eassumption.
Qed.
The eauto tactic will use eapply and eassumption, streamlining
the proof even further.