|
adam@534
|
1 (* Copyright (c) 2011-2012, 2015, Adam Chlipala
|
|
adam@324
|
2 *
|
|
adam@324
|
3 * This work is licensed under a
|
|
adam@324
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
|
adam@324
|
5 * Unported License.
|
|
adam@324
|
6 * The license text is available at:
|
|
adam@324
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
|
adam@324
|
8 *)
|
|
adam@324
|
9
|
|
adam@324
|
10 (* begin hide *)
|
|
adam@324
|
11
|
|
adam@534
|
12 Require Import List Omega.
|
|
adam@324
|
13
|
|
adam@534
|
14 Require Import Cpdt.CpdtTactics.
|
|
adam@324
|
15
|
|
adam@324
|
16 Set Implicit Arguments.
|
|
adam@534
|
17 Set Asymmetric Patterns.
|
|
adam@324
|
18 (* end hide *)
|
|
adam@324
|
19
|
|
adam@324
|
20 (** %\part{Proof Engineering}
|
|
adam@324
|
21
|
|
adam@324
|
22 \chapter{Proof Search by Logic Programming}% *)
|
|
adam@324
|
23
|
|
adam@430
|
24 (** The Curry-Howard correspondence tells us that proving is "just" programming, but the pragmatics of the two activities are very different. Generally we care about properties of a program besides its type, but the same is not true about proofs. Any proof of a theorem will do just as well. As a result, automated proof search is conceptually simpler than automated programming.
|
|
adam@372
|
25
|
|
adam@395
|
26 The paradigm of %\index{logic programming}%logic programming%~\cite{LogicProgramming}%, as embodied in languages like %\index{Prolog}%Prolog%~\cite{Prolog}%, is a good match for proof search in higher-order logic. This chapter introduces the details, attempting to avoid any dependence on past logic programming experience. *)
|
|
adam@324
|
27
|
|
adam@324
|
28
|
|
adam@324
|
29 (** * Introducing Logic Programming *)
|
|
adam@324
|
30
|
|
adam@372
|
31 (** Recall the definition of addition from the standard library. *)
|
|
adam@372
|
32
|
|
adam@324
|
33 Print plus.
|
|
adam@372
|
34 (** %\vspace{-.15in}%[[
|
|
adam@372
|
35 plus =
|
|
adam@372
|
36 fix plus (n m : nat) : nat := match n with
|
|
adam@372
|
37 | 0 => m
|
|
adam@372
|
38 | S p => S (plus p m)
|
|
adam@372
|
39 end
|
|
adam@372
|
40
|
|
adam@372
|
41 ]]
|
|
adam@372
|
42
|
|
adam@372
|
43 This is a recursive definition, in the style of functional programming. We might also follow the style of logic programming, which corresponds to the inductive relations we have defined in previous chapters. *)
|
|
adam@324
|
44
|
|
adam@324
|
45 Inductive plusR : nat -> nat -> nat -> Prop :=
|
|
adam@324
|
46 | PlusO : forall m, plusR O m m
|
|
adam@324
|
47 | PlusS : forall n m r, plusR n m r
|
|
adam@324
|
48 -> plusR (S n) m (S r).
|
|
adam@324
|
49
|
|
adam@372
|
50 (** Intuitively, a fact [plusR n m r] only holds when [plus n m = r]. It is not hard to prove this correspondence formally. *)
|
|
adam@372
|
51
|
|
adam@324
|
52 (* begin thide *)
|
|
adam@324
|
53 Hint Constructors plusR.
|
|
adam@324
|
54 (* end thide *)
|
|
adam@324
|
55
|
|
adam@324
|
56 Theorem plus_plusR : forall n m,
|
|
adam@324
|
57 plusR n m (n + m).
|
|
adam@324
|
58 (* begin thide *)
|
|
adam@324
|
59 induction n; crush.
|
|
adam@324
|
60 Qed.
|
|
adam@324
|
61 (* end thide *)
|
|
adam@324
|
62
|
|
adam@324
|
63 Theorem plusR_plus : forall n m r,
|
|
adam@324
|
64 plusR n m r
|
|
adam@324
|
65 -> r = n + m.
|
|
adam@324
|
66 (* begin thide *)
|
|
adam@324
|
67 induction 1; crush.
|
|
adam@324
|
68 Qed.
|
|
adam@324
|
69 (* end thide *)
|
|
adam@324
|
70
|
|
adam@372
|
71 (** With the functional definition of [plus], simple equalities about arithmetic follow by computation. *)
|
|
adam@372
|
72
|
|
adam@324
|
73 Example four_plus_three : 4 + 3 = 7.
|
|
adam@324
|
74 (* begin thide *)
|
|
adam@324
|
75 reflexivity.
|
|
adam@324
|
76 Qed.
|
|
adam@324
|
77 (* end thide *)
|
|
adam@324
|
78
|
|
adam@430
|
79 (* begin hide *)
|
|
adam@437
|
80 (* begin thide *)
|
|
adam@430
|
81 Definition er := @eq_refl.
|
|
adam@437
|
82 (* end thide *)
|
|
adam@430
|
83 (* end hide *)
|
|
adam@430
|
84
|
|
adam@372
|
85 Print four_plus_three.
|
|
adam@372
|
86 (** %\vspace{-.15in}%[[
|
|
adam@372
|
87 four_plus_three = eq_refl
|
|
adam@372
|
88 ]]
|
|
adam@372
|
89
|
|
adam@372
|
90 With the relational definition, the same equalities take more steps to prove, but the process is completely mechanical. For example, consider this simple-minded manual proof search strategy. The steps with error messages shown afterward will be omitted from the final script.
|
|
adam@372
|
91 *)
|
|
adam@372
|
92
|
|
adam@324
|
93 Example four_plus_three' : plusR 4 3 7.
|
|
adam@324
|
94 (* begin thide *)
|
|
adam@372
|
95 (** %\vspace{-.2in}%[[
|
|
adam@372
|
96 apply PlusO.
|
|
adam@372
|
97 ]]
|
|
adam@372
|
98 %\vspace{-.2in}%
|
|
adam@372
|
99 <<
|
|
adam@372
|
100 Error: Impossible to unify "plusR 0 ?24 ?24" with "plusR 4 3 7".
|
|
adam@372
|
101 >> *)
|
|
adam@372
|
102 apply PlusS.
|
|
adam@372
|
103 (** %\vspace{-.2in}%[[
|
|
adam@372
|
104 apply PlusO.
|
|
adam@372
|
105 ]]
|
|
adam@372
|
106 %\vspace{-.2in}%
|
|
adam@372
|
107 <<
|
|
adam@372
|
108 Error: Impossible to unify "plusR 0 ?25 ?25" with "plusR 3 3 6".
|
|
adam@372
|
109 >> *)
|
|
adam@372
|
110 apply PlusS.
|
|
adam@372
|
111 (** %\vspace{-.2in}%[[
|
|
adam@372
|
112 apply PlusO.
|
|
adam@372
|
113 ]]
|
|
adam@372
|
114 %\vspace{-.2in}%
|
|
adam@372
|
115 <<
|
|
adam@372
|
116 Error: Impossible to unify "plusR 0 ?26 ?26" with "plusR 2 3 5".
|
|
adam@372
|
117 >> *)
|
|
adam@372
|
118 apply PlusS.
|
|
adam@372
|
119 (** %\vspace{-.2in}%[[
|
|
adam@372
|
120 apply PlusO.
|
|
adam@372
|
121 ]]
|
|
adam@372
|
122 %\vspace{-.2in}%
|
|
adam@372
|
123 <<
|
|
adam@372
|
124 Error: Impossible to unify "plusR 0 ?27 ?27" with "plusR 1 3 4".
|
|
adam@372
|
125 >> *)
|
|
adam@372
|
126 apply PlusS.
|
|
adam@372
|
127 apply PlusO.
|
|
adam@372
|
128
|
|
adam@506
|
129 (** At this point the proof is completed. It is no doubt clear that a simple procedure could find all proofs of this kind for us. We are just exploring all possible proof trees, built from the two candidate steps [apply PlusO] and [apply PlusS]. The built-in tactic %\index{tactics!auto}%[auto] follows exactly this strategy, since above we used %\index{Vernacular commands!Hint Constructors}%[Hint Constructors] to register the two candidate proof steps as hints. *)
|
|
adam@372
|
130
|
|
adam@372
|
131 Restart.
|
|
adam@324
|
132 auto.
|
|
adam@324
|
133 Qed.
|
|
adam@324
|
134 (* end thide *)
|
|
adam@324
|
135
|
|
adam@372
|
136 Print four_plus_three'.
|
|
adam@372
|
137 (** %\vspace{-.15in}%[[
|
|
adam@372
|
138 four_plus_three' = PlusS (PlusS (PlusS (PlusS (PlusO 3))))
|
|
adam@372
|
139 ]]
|
|
adam@372
|
140 *)
|
|
adam@372
|
141
|
|
adam@372
|
142 (** Let us try the same approach on a slightly more complex goal. *)
|
|
adam@372
|
143
|
|
adam@372
|
144 Example five_plus_three : plusR 5 3 8.
|
|
adam@324
|
145 (* begin thide *)
|
|
adam@372
|
146 auto.
|
|
adam@372
|
147
|
|
adam@372
|
148 (** This time, [auto] is not enough to make any progress. Since even a single candidate step may lead to an infinite space of possible proof trees, [auto] is parameterized on the maximum depth of trees to consider. The default depth is 5, and it turns out that we need depth 6 to prove the goal. *)
|
|
adam@372
|
149
|
|
adam@324
|
150 auto 6.
|
|
adam@372
|
151
|
|
adam@459
|
152 (** Sometimes it is useful to see a description of the proof tree that [auto] finds, with the %\index{tactics!info}%[info] tactical. (This tactical is not available in Coq 8.4 as of this writing, but I hope it reappears soon. The special case %\index{tactics!info\_auto}%[info_auto] tactic is provided as a chatty replacement for [auto].) *)
|
|
adam@372
|
153
|
|
adam@324
|
154 Restart.
|
|
adam@324
|
155 info auto 6.
|
|
adam@372
|
156 (** %\vspace{-.15in}%[[
|
|
adam@372
|
157 == apply PlusS; apply PlusS; apply PlusS; apply PlusS;
|
|
adam@372
|
158 apply PlusS; apply PlusO.
|
|
adam@372
|
159 ]]
|
|
adam@372
|
160 *)
|
|
adam@324
|
161 Qed.
|
|
adam@324
|
162 (* end thide *)
|
|
adam@324
|
163
|
|
adam@410
|
164 (** The two key components of logic programming are%\index{backtracking}% _backtracking_ and%\index{unification}% _unification_. To see these techniques in action, consider this further silly example. Here our candidate proof steps will be reflexivity and quantifier instantiation. *)
|
|
adam@324
|
165
|
|
adam@324
|
166 Example seven_minus_three : exists x, x + 3 = 7.
|
|
adam@324
|
167 (* begin thide *)
|
|
adam@372
|
168 (** For explanatory purposes, let us simulate a user with minimal understanding of arithmetic. We start by choosing an instantiation for the quantifier. Recall that [ex_intro] is the constructor for existentially quantified formulas. *)
|
|
adam@372
|
169
|
|
adam@372
|
170 apply ex_intro with 0.
|
|
adam@372
|
171 (** %\vspace{-.2in}%[[
|
|
adam@372
|
172 reflexivity.
|
|
adam@372
|
173 ]]
|
|
adam@372
|
174 %\vspace{-.2in}%
|
|
adam@372
|
175 <<
|
|
adam@372
|
176 Error: Impossible to unify "7" with "0 + 3".
|
|
adam@372
|
177 >>
|
|
adam@372
|
178
|
|
adam@398
|
179 This seems to be a dead end. Let us _backtrack_ to the point where we ran [apply] and make a better alternate choice.
|
|
adam@372
|
180 *)
|
|
adam@372
|
181
|
|
adam@372
|
182 Restart.
|
|
adam@372
|
183 apply ex_intro with 4.
|
|
adam@372
|
184 reflexivity.
|
|
adam@372
|
185 Qed.
|
|
adam@324
|
186 (* end thide *)
|
|
adam@324
|
187
|
|
adam@372
|
188 (** The above was a fairly tame example of backtracking. In general, any node in an under-construction proof tree may be the destination of backtracking an arbitrarily large number of times, as different candidate proof steps are found not to lead to full proof trees, within the depth bound passed to [auto].
|
|
adam@372
|
189
|
|
adam@372
|
190 Next we demonstrate unification, which will be easier when we switch to the relational formulation of addition. *)
|
|
adam@372
|
191
|
|
adam@324
|
192 Example seven_minus_three' : exists x, plusR x 3 7.
|
|
adam@324
|
193 (* begin thide *)
|
|
adam@459
|
194 (** We could attempt to guess the quantifier instantiation manually as before, but here there is no need. Instead of [apply], we use %\index{tactics!eapply}%[eapply], which proceeds with placeholder%\index{unification variable}% _unification variables_ standing in for those parameters we wish to postpone guessing. *)
|
|
adam@372
|
195
|
|
adam@372
|
196 eapply ex_intro.
|
|
adam@372
|
197 (** [[
|
|
adam@372
|
198 1 subgoal
|
|
adam@372
|
199
|
|
adam@372
|
200 ============================
|
|
adam@372
|
201 plusR ?70 3 7
|
|
adam@372
|
202 ]]
|
|
adam@372
|
203
|
|
adam@372
|
204 Now we can finish the proof with the right applications of [plusR]'s constructors. Note that new unification variables are being generated to stand for new unknowns. *)
|
|
adam@372
|
205
|
|
adam@372
|
206 apply PlusS.
|
|
adam@372
|
207 (** [[
|
|
adam@372
|
208 ============================
|
|
adam@372
|
209 plusR ?71 3 6
|
|
adam@372
|
210 ]]
|
|
adam@372
|
211 *)
|
|
adam@372
|
212 apply PlusS. apply PlusS. apply PlusS.
|
|
adam@372
|
213 (** [[
|
|
adam@372
|
214 ============================
|
|
adam@372
|
215 plusR ?74 3 3
|
|
adam@372
|
216 ]]
|
|
adam@372
|
217 *)
|
|
adam@372
|
218 apply PlusO.
|
|
adam@372
|
219
|
|
adam@372
|
220 (** The [auto] tactic will not perform these sorts of steps that introduce unification variables, but the %\index{tactics!eauto}%[eauto] tactic will. It is helpful to work with two separate tactics, because proof search in the [eauto] style can uncover many more potential proof trees and hence take much longer to run. *)
|
|
adam@372
|
221
|
|
adam@372
|
222 Restart.
|
|
adam@324
|
223 info eauto 6.
|
|
adam@372
|
224 (** %\vspace{-.15in}%[[
|
|
adam@372
|
225 == eapply ex_intro; apply PlusS; apply PlusS;
|
|
adam@372
|
226 apply PlusS; apply PlusS; apply PlusO.
|
|
adam@372
|
227 ]]
|
|
adam@372
|
228 *)
|
|
adam@324
|
229 Qed.
|
|
adam@324
|
230 (* end thide *)
|
|
adam@324
|
231
|
|
adam@372
|
232 (** This proof gives us our first example where logic programming simplifies proof search compared to functional programming. In general, functional programs are only meant to be run in a single direction; a function has disjoint sets of inputs and outputs. In the last example, we effectively ran a logic program backwards, deducing an input that gives rise to a certain output. The same works for deducing an unknown value of the other input. *)
|
|
adam@372
|
233
|
|
adam@324
|
234 Example seven_minus_four' : exists x, plusR 4 x 7.
|
|
adam@324
|
235 (* begin thide *)
|
|
adam@372
|
236 eauto 6.
|
|
adam@324
|
237 Qed.
|
|
adam@324
|
238 (* end thide *)
|
|
adam@324
|
239
|
|
adam@372
|
240 (** By proving the right auxiliary facts, we can reason about specific functional programs in the same way as we did above for a logic program. Let us prove that the constructors of [plusR] have natural interpretations as lemmas about [plus]. We can find the first such lemma already proved in the standard library, using the %\index{Vernacular commands!SearchRewrite}%[SearchRewrite] command to find a library function proving an equality whose lefthand or righthand side matches a pattern with wildcards. *)
|
|
adam@372
|
241
|
|
adam@324
|
242 (* begin thide *)
|
|
adam@324
|
243 SearchRewrite (O + _).
|
|
adam@372
|
244 (** %\vspace{-.15in}%[[
|
|
adam@372
|
245 plus_O_n: forall n : nat, 0 + n = n
|
|
adam@372
|
246 ]]
|
|
adam@372
|
247
|
|
adam@372
|
248 The command %\index{Vernacular commands!Hint Immediate}%[Hint Immediate] asks [auto] and [eauto] to consider this lemma as a candidate step for any leaf of a proof tree. *)
|
|
adam@324
|
249
|
|
adam@324
|
250 Hint Immediate plus_O_n.
|
|
adam@324
|
251
|
|
adam@372
|
252 (** The counterpart to [PlusS] we will prove ourselves. *)
|
|
adam@372
|
253
|
|
adam@324
|
254 Lemma plusS : forall n m r,
|
|
adam@324
|
255 n + m = r
|
|
adam@324
|
256 -> S n + m = S r.
|
|
adam@324
|
257 crush.
|
|
adam@324
|
258 Qed.
|
|
adam@324
|
259
|
|
adam@372
|
260 (** The command %\index{Vernacular commands!Hint Resolve}%[Hint Resolve] adds a new candidate proof step, to be attempted at any level of a proof tree, not just at leaves. *)
|
|
adam@372
|
261
|
|
adam@324
|
262 Hint Resolve plusS.
|
|
adam@324
|
263 (* end thide *)
|
|
adam@324
|
264
|
|
adam@372
|
265 (** Now that we have registered the proper hints, we can replicate our previous examples with the normal, functional addition [plus]. *)
|
|
adam@372
|
266
|
|
adam@372
|
267 Example seven_minus_three'' : exists x, x + 3 = 7.
|
|
adam@324
|
268 (* begin thide *)
|
|
adam@372
|
269 eauto 6.
|
|
adam@324
|
270 Qed.
|
|
adam@324
|
271 (* end thide *)
|
|
adam@324
|
272
|
|
adam@324
|
273 Example seven_minus_four : exists x, 4 + x = 7.
|
|
adam@324
|
274 (* begin thide *)
|
|
adam@372
|
275 eauto 6.
|
|
adam@324
|
276 Qed.
|
|
adam@324
|
277 (* end thide *)
|
|
adam@324
|
278
|
|
adam@372
|
279 (** This new hint database is far from a complete decision procedure, as we see in a further example that [eauto] does not finish. *)
|
|
adam@372
|
280
|
|
adam@372
|
281 Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
|
|
adam@324
|
282 (* begin thide *)
|
|
adam@324
|
283 eauto 6.
|
|
adam@324
|
284 Abort.
|
|
adam@324
|
285 (* end thide *)
|
|
adam@324
|
286
|
|
adam@372
|
287 (** A further lemma will be helpful. *)
|
|
adam@372
|
288
|
|
adam@324
|
289 (* begin thide *)
|
|
adam@324
|
290 Lemma plusO : forall n m,
|
|
adam@324
|
291 n = m
|
|
adam@324
|
292 -> n + 0 = m.
|
|
adam@324
|
293 crush.
|
|
adam@324
|
294 Qed.
|
|
adam@324
|
295
|
|
adam@324
|
296 Hint Resolve plusO.
|
|
adam@324
|
297 (* end thide *)
|
|
adam@324
|
298
|
|
adam@372
|
299 (** Note that, if we consider the inputs to [plus] as the inputs of a corresponding logic program, the new rule [plusO] introduces an ambiguity. For instance, a sum [0 + 0] would match both of [plus_O_n] and [plusO], depending on which operand we focus on. This ambiguity may increase the number of potential search trees, slowing proof search, but semantically it presents no problems, and in fact it leads to an automated proof of the present example. *)
|
|
adam@372
|
300
|
|
adam@324
|
301 Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
|
|
adam@324
|
302 (* begin thide *)
|
|
adam@372
|
303 eauto 7.
|
|
adam@324
|
304 Qed.
|
|
adam@324
|
305 (* end thide *)
|
|
adam@324
|
306
|
|
adam@372
|
307 (** Just how much damage can be done by adding hints that grow the space of possible proof trees? A classic gotcha comes from unrestricted use of transitivity, as embodied in this library theorem about equality: *)
|
|
adam@372
|
308
|
|
adam@324
|
309 Check eq_trans.
|
|
adam@372
|
310 (** %\vspace{-.15in}%[[
|
|
adam@372
|
311 eq_trans
|
|
adam@372
|
312 : forall (A : Type) (x y z : A), x = y -> y = z -> x = z
|
|
adam@372
|
313 ]]
|
|
adam@372
|
314 *)
|
|
adam@372
|
315
|
|
adam@372
|
316 (** Hints are scoped over sections, so let us enter a section to contain the effects of an unfortunate hint choice. *)
|
|
adam@324
|
317
|
|
adam@324
|
318 Section slow.
|
|
adam@324
|
319 Hint Resolve eq_trans.
|
|
adam@324
|
320
|
|
adam@372
|
321 (** The following fact is false, but that does not stop [eauto] from taking a very long time to search for proofs of it. We use the handy %\index{Vernacular commands!Time}%[Time] command to measure how long a proof step takes to run. None of the following steps make any progress. *)
|
|
adam@372
|
322
|
|
adam@484
|
323 Example zero_minus_one : exists x, 1 + x = 0.
|
|
adam@324
|
324 Time eauto 1.
|
|
adam@372
|
325 (** %\vspace{-.15in}%
|
|
adam@372
|
326 <<
|
|
adam@372
|
327 Finished transaction in 0. secs (0.u,0.s)
|
|
adam@372
|
328 >>
|
|
adam@372
|
329 *)
|
|
adam@372
|
330
|
|
adam@324
|
331 Time eauto 2.
|
|
adam@372
|
332 (** %\vspace{-.15in}%
|
|
adam@372
|
333 <<
|
|
adam@372
|
334 Finished transaction in 0. secs (0.u,0.s)
|
|
adam@372
|
335 >>
|
|
adam@372
|
336 *)
|
|
adam@372
|
337
|
|
adam@324
|
338 Time eauto 3.
|
|
adam@372
|
339 (** %\vspace{-.15in}%
|
|
adam@372
|
340 <<
|
|
adam@372
|
341 Finished transaction in 0. secs (0.008u,0.s)
|
|
adam@372
|
342 >>
|
|
adam@372
|
343 *)
|
|
adam@372
|
344
|
|
adam@324
|
345 Time eauto 4.
|
|
adam@372
|
346 (** %\vspace{-.15in}%
|
|
adam@372
|
347 <<
|
|
adam@372
|
348 Finished transaction in 0. secs (0.068005u,0.004s)
|
|
adam@372
|
349 >>
|
|
adam@372
|
350 *)
|
|
adam@372
|
351
|
|
adam@324
|
352 Time eauto 5.
|
|
adam@372
|
353 (** %\vspace{-.15in}%
|
|
adam@372
|
354 <<
|
|
adam@372
|
355 Finished transaction in 2. secs (1.92012u,0.044003s)
|
|
adam@372
|
356 >>
|
|
adam@372
|
357 *)
|
|
adam@372
|
358
|
|
adam@372
|
359 (** We see worrying exponential growth in running time, and the %\index{tactics!debug}%[debug] tactical helps us see where [eauto] is wasting its time, outputting a trace of every proof step that is attempted. The rule [eq_trans] applies at every node of a proof tree, and [eauto] tries all such positions. *)
|
|
adam@372
|
360
|
|
adam@437
|
361 (* begin hide *)
|
|
adam@437
|
362 (* begin thide *)
|
|
adam@437
|
363 Definition syms := (eq_sym, plus_n_O, eq_add_S, f_equal2).
|
|
adam@437
|
364 (* end thide *)
|
|
adam@437
|
365 (* end hide *)
|
|
adam@437
|
366
|
|
adam@324
|
367 debug eauto 3.
|
|
adam@372
|
368 (** [[
|
|
adam@372
|
369 1 depth=3
|
|
adam@372
|
370 1.1 depth=2 eapply ex_intro
|
|
adam@372
|
371 1.1.1 depth=1 apply plusO
|
|
adam@372
|
372 1.1.1.1 depth=0 eapply eq_trans
|
|
adam@372
|
373 1.1.2 depth=1 eapply eq_trans
|
|
adam@372
|
374 1.1.2.1 depth=1 apply plus_n_O
|
|
adam@372
|
375 1.1.2.1.1 depth=0 apply plusO
|
|
adam@372
|
376 1.1.2.1.2 depth=0 eapply eq_trans
|
|
adam@372
|
377 1.1.2.2 depth=1 apply @eq_refl
|
|
adam@372
|
378 1.1.2.2.1 depth=0 apply plusO
|
|
adam@372
|
379 1.1.2.2.2 depth=0 eapply eq_trans
|
|
adam@372
|
380 1.1.2.3 depth=1 apply eq_add_S ; trivial
|
|
adam@372
|
381 1.1.2.3.1 depth=0 apply plusO
|
|
adam@372
|
382 1.1.2.3.2 depth=0 eapply eq_trans
|
|
adam@372
|
383 1.1.2.4 depth=1 apply eq_sym ; trivial
|
|
adam@372
|
384 1.1.2.4.1 depth=0 eapply eq_trans
|
|
adam@372
|
385 1.1.2.5 depth=0 apply plusO
|
|
adam@372
|
386 1.1.2.6 depth=0 apply plusS
|
|
adam@372
|
387 1.1.2.7 depth=0 apply f_equal (A:=nat)
|
|
adam@372
|
388 1.1.2.8 depth=0 apply f_equal2 (A1:=nat) (A2:=nat)
|
|
adam@372
|
389 1.1.2.9 depth=0 eapply eq_trans
|
|
adam@372
|
390 ]]
|
|
adam@372
|
391 *)
|
|
adam@324
|
392 Abort.
|
|
adam@324
|
393 End slow.
|
|
adam@324
|
394
|
|
adam@459
|
395 (** Sometimes, though, transitivity is just what is needed to get a proof to go through automatically with [eauto]. For those cases, we can use named%\index{hint databases}% _hint databases_ to segregate hints into different groups that may be called on as needed. Here we put [eq_trans] into the database [slow]. *)
|
|
adam@372
|
396
|
|
adam@324
|
397 (* begin thide *)
|
|
adam@324
|
398 Hint Resolve eq_trans : slow.
|
|
adam@324
|
399 (* end thide *)
|
|
adam@324
|
400
|
|
adam@539
|
401 Example from_one_to_zero : exists x, 1 + x = 0.
|
|
adam@324
|
402 (* begin thide *)
|
|
adam@372
|
403 Time eauto.
|
|
adam@372
|
404 (** %\vspace{-.15in}%
|
|
adam@372
|
405 <<
|
|
adam@372
|
406 Finished transaction in 0. secs (0.004u,0.s)
|
|
adam@372
|
407 >>
|
|
adam@372
|
408
|
|
adam@469
|
409 This [eauto] fails to prove the goal, but at least it takes substantially less than the 2 seconds required above! *)
|
|
adam@372
|
410
|
|
adam@324
|
411 Abort.
|
|
adam@324
|
412 (* end thide *)
|
|
adam@324
|
413
|
|
adam@437
|
414 (** One simple example from before runs in the same amount of time, avoiding pollution by transitivity. *)
|
|
adam@372
|
415
|
|
adam@324
|
416 Example seven_minus_three_again : exists x, x + 3 = 7.
|
|
adam@324
|
417 (* begin thide *)
|
|
adam@372
|
418 Time eauto 6.
|
|
adam@372
|
419 (** %\vspace{-.15in}%
|
|
adam@372
|
420 <<
|
|
adam@372
|
421 Finished transaction in 0. secs (0.004001u,0.s)
|
|
adam@372
|
422 >>
|
|
adam@372
|
423 %\vspace{-.2in}% *)
|
|
adam@372
|
424
|
|
adam@324
|
425 Qed.
|
|
adam@324
|
426 (* end thide *)
|
|
adam@324
|
427
|
|
adam@398
|
428 (** When we _do_ need transitivity, we ask for it explicitly. *)
|
|
adam@372
|
429
|
|
adam@324
|
430 Example needs_trans : forall x y, 1 + x = y
|
|
adam@324
|
431 -> y = 2
|
|
adam@324
|
432 -> exists z, z + x = 3.
|
|
adam@324
|
433 (* begin thide *)
|
|
adam@324
|
434 info eauto with slow.
|
|
adam@372
|
435 (** %\vspace{-.2in}%[[
|
|
adam@372
|
436 == intro x; intro y; intro H; intro H0; simple eapply ex_intro;
|
|
adam@372
|
437 apply plusS; simple eapply eq_trans.
|
|
adam@372
|
438 exact H.
|
|
adam@372
|
439
|
|
adam@372
|
440 exact H0.
|
|
adam@372
|
441 ]]
|
|
adam@372
|
442 *)
|
|
adam@324
|
443 Qed.
|
|
adam@324
|
444 (* end thide *)
|
|
adam@324
|
445
|
|
adam@372
|
446 (** The [info] trace shows that [eq_trans] was used in just the position where it is needed to complete the proof. We also see that [auto] and [eauto] always perform [intro] steps without counting them toward the bound on proof tree depth. *)
|
|
adam@372
|
447
|
|
adam@324
|
448
|
|
adam@324
|
449 (** * Searching for Underconstrained Values *)
|
|
adam@324
|
450
|
|
adam@373
|
451 (** Recall the definition of the list length function. *)
|
|
adam@373
|
452
|
|
adam@324
|
453 Print length.
|
|
adam@373
|
454 (** %\vspace{-.15in}%[[
|
|
adam@373
|
455 length =
|
|
adam@373
|
456 fun A : Type =>
|
|
adam@373
|
457 fix length (l : list A) : nat :=
|
|
adam@373
|
458 match l with
|
|
adam@373
|
459 | nil => 0
|
|
adam@373
|
460 | _ :: l' => S (length l')
|
|
adam@373
|
461 end
|
|
adam@373
|
462 ]]
|
|
adam@373
|
463
|
|
adam@373
|
464 This function is easy to reason about in the forward direction, computing output from input. *)
|
|
adam@324
|
465
|
|
adam@324
|
466 Example length_1_2 : length (1 :: 2 :: nil) = 2.
|
|
adam@324
|
467 auto.
|
|
adam@324
|
468 Qed.
|
|
adam@324
|
469
|
|
adam@324
|
470 Print length_1_2.
|
|
adam@373
|
471 (** %\vspace{-.15in}%[[
|
|
adam@373
|
472 length_1_2 = eq_refl
|
|
adam@373
|
473 ]]
|
|
adam@373
|
474
|
|
adam@373
|
475 As in the last section, we will prove some lemmas to recast [length] in logic programming style, to help us compute inputs from outputs. *)
|
|
adam@324
|
476
|
|
adam@324
|
477 (* begin thide *)
|
|
adam@324
|
478 Theorem length_O : forall A, length (nil (A := A)) = O.
|
|
adam@324
|
479 crush.
|
|
adam@324
|
480 Qed.
|
|
adam@324
|
481
|
|
adam@324
|
482 Theorem length_S : forall A (h : A) t n,
|
|
adam@324
|
483 length t = n
|
|
adam@324
|
484 -> length (h :: t) = S n.
|
|
adam@324
|
485 crush.
|
|
adam@324
|
486 Qed.
|
|
adam@324
|
487
|
|
adam@324
|
488 Hint Resolve length_O length_S.
|
|
adam@324
|
489 (* end thide *)
|
|
adam@324
|
490
|
|
adam@484
|
491 (** Let us apply these hints to prove that a [list nat] of length 2 exists. (Here we register [length_O] with [Hint Resolve] instead of [Hint Immediate] merely as a convenience to use the same command as for [length_S]; [Resolve] and [Immediate] have the same meaning for a premise-free hint.) *)
|
|
adam@373
|
492
|
|
adam@324
|
493 Example length_is_2 : exists ls : list nat, length ls = 2.
|
|
adam@324
|
494 (* begin thide *)
|
|
adam@324
|
495 eauto.
|
|
adam@373
|
496 (** <<
|
|
adam@373
|
497 No more subgoals but non-instantiated existential variables:
|
|
adam@373
|
498 Existential 1 = ?20249 : [ |- nat]
|
|
adam@373
|
499 Existential 2 = ?20252 : [ |- nat]
|
|
adam@373
|
500 >>
|
|
adam@373
|
501
|
|
adam@398
|
502 Coq complains that we finished the proof without determining the values of some unification variables created during proof search. The error message may seem a bit silly, since _any_ value of type [nat] (for instance, 0) can be plugged in for either variable! However, for more complex types, finding their inhabitants may be as complex as theorem-proving in general.
|
|
adam@373
|
503
|
|
adam@373
|
504 The %\index{Vernacular commands!Show Proof}%[Show Proof] command shows exactly which proof term [eauto] has found, with the undetermined unification variables appearing explicitly where they are used. *)
|
|
adam@324
|
505
|
|
adam@324
|
506 Show Proof.
|
|
adam@373
|
507 (** <<
|
|
adam@373
|
508 Proof: ex_intro (fun ls : list nat => length ls = 2)
|
|
adam@373
|
509 (?20249 :: ?20252 :: nil)
|
|
adam@373
|
510 (length_S ?20249 (?20252 :: nil)
|
|
adam@373
|
511 (length_S ?20252 nil (length_O nat)))
|
|
adam@373
|
512 >>
|
|
adam@373
|
513 %\vspace{-.2in}% *)
|
|
adam@373
|
514
|
|
adam@324
|
515 Abort.
|
|
adam@324
|
516 (* end thide *)
|
|
adam@324
|
517
|
|
adam@373
|
518 (** We see that the two unification variables stand for the two elements of the list. Indeed, list length is independent of data values. Paradoxically, we can make the proof search process easier by constraining the list further, so that proof search naturally locates appropriate data elements by unification. The library predicate [Forall] will be helpful. *)
|
|
adam@373
|
519
|
|
adam@430
|
520 (* begin hide *)
|
|
adam@437
|
521 (* begin thide *)
|
|
adam@430
|
522 Definition Forall_c := (@Forall_nil, @Forall_cons).
|
|
adam@437
|
523 (* end thide *)
|
|
adam@430
|
524 (* end hide *)
|
|
adam@430
|
525
|
|
adam@324
|
526 Print Forall.
|
|
adam@373
|
527 (** %\vspace{-.15in}%[[
|
|
adam@373
|
528 Inductive Forall (A : Type) (P : A -> Prop) : list A -> Prop :=
|
|
adam@373
|
529 Forall_nil : Forall P nil
|
|
adam@373
|
530 | Forall_cons : forall (x : A) (l : list A),
|
|
adam@373
|
531 P x -> Forall P l -> Forall P (x :: l)
|
|
adam@373
|
532 ]]
|
|
adam@373
|
533 *)
|
|
adam@324
|
534
|
|
adam@324
|
535 Example length_is_2 : exists ls : list nat, length ls = 2
|
|
adam@324
|
536 /\ Forall (fun n => n >= 1) ls.
|
|
adam@324
|
537 (* begin thide *)
|
|
adam@324
|
538 eauto 9.
|
|
adam@324
|
539 Qed.
|
|
adam@324
|
540 (* end thide *)
|
|
adam@324
|
541
|
|
adam@373
|
542 (** We can see which list [eauto] found by printing the proof term. *)
|
|
adam@373
|
543
|
|
adam@430
|
544 (* begin hide *)
|
|
adam@437
|
545 (* begin thide *)
|
|
adam@430
|
546 Definition conj' := (conj, le_n).
|
|
adam@437
|
547 (* end thide *)
|
|
adam@430
|
548 (* end hide *)
|
|
adam@430
|
549
|
|
adam@373
|
550 Print length_is_2.
|
|
adam@373
|
551 (** %\vspace{-.15in}%[[
|
|
adam@373
|
552 length_is_2 =
|
|
adam@373
|
553 ex_intro
|
|
adam@373
|
554 (fun ls : list nat => length ls = 2 /\ Forall (fun n : nat => n >= 1) ls)
|
|
adam@373
|
555 (1 :: 1 :: nil)
|
|
adam@373
|
556 (conj (length_S 1 (1 :: nil) (length_S 1 nil (length_O nat)))
|
|
adam@373
|
557 (Forall_cons 1 (le_n 1)
|
|
adam@373
|
558 (Forall_cons 1 (le_n 1) (Forall_nil (fun n : nat => n >= 1)))))
|
|
adam@373
|
559 ]]
|
|
adam@373
|
560 *)
|
|
adam@373
|
561
|
|
adam@459
|
562 (** Let us try one more, fancier example. First, we use a standard higher-order function to define a function for summing all data elements of a list. *)
|
|
adam@373
|
563
|
|
adam@324
|
564 Definition sum := fold_right plus O.
|
|
adam@324
|
565
|
|
adam@373
|
566 (** Another basic lemma will be helpful to guide proof search. *)
|
|
adam@373
|
567
|
|
adam@324
|
568 (* begin thide *)
|
|
adam@324
|
569 Lemma plusO' : forall n m,
|
|
adam@324
|
570 n = m
|
|
adam@324
|
571 -> 0 + n = m.
|
|
adam@324
|
572 crush.
|
|
adam@324
|
573 Qed.
|
|
adam@324
|
574
|
|
adam@324
|
575 Hint Resolve plusO'.
|
|
adam@324
|
576
|
|
adam@373
|
577 (** Finally, we meet %\index{Vernacular commands!Hint Extern}%[Hint Extern], the command to register a custom hint. That is, we provide a pattern to match against goals during proof search. Whenever the pattern matches, a tactic (given to the right of an arrow [=>]) is attempted. Below, the number [1] gives a priority for this step. Lower priorities are tried before higher priorities, which can have a significant effect on proof search time. *)
|
|
adam@373
|
578
|
|
adam@324
|
579 Hint Extern 1 (sum _ = _) => simpl.
|
|
adam@324
|
580 (* end thide *)
|
|
adam@324
|
581
|
|
adam@373
|
582 (** Now we can find a length-2 list whose sum is 0. *)
|
|
adam@373
|
583
|
|
adam@324
|
584 Example length_and_sum : exists ls : list nat, length ls = 2
|
|
adam@324
|
585 /\ sum ls = O.
|
|
adam@324
|
586 (* begin thide *)
|
|
adam@324
|
587 eauto 7.
|
|
adam@324
|
588 Qed.
|
|
adam@324
|
589 (* end thide *)
|
|
adam@324
|
590
|
|
adam@373
|
591 (* begin hide *)
|
|
adam@324
|
592 Print length_and_sum.
|
|
adam@373
|
593 (* end hide *)
|
|
adam@373
|
594
|
|
adam@373
|
595 (** Printing the proof term shows the unsurprising list that is found. Here is an example where it is less obvious which list will be used. Can you guess which list [eauto] will choose? *)
|
|
adam@324
|
596
|
|
adam@324
|
597 Example length_and_sum' : exists ls : list nat, length ls = 5
|
|
adam@324
|
598 /\ sum ls = 42.
|
|
adam@324
|
599 (* begin thide *)
|
|
adam@324
|
600 eauto 15.
|
|
adam@324
|
601 Qed.
|
|
adam@324
|
602 (* end thide *)
|
|
adam@324
|
603
|
|
adam@373
|
604 (* begin hide *)
|
|
adam@324
|
605 Print length_and_sum'.
|
|
adam@373
|
606 (* end hide *)
|
|
adam@373
|
607
|
|
adam@373
|
608 (** We will give away part of the answer and say that the above list is less interesting than we would like, because it contains too many zeroes. A further constraint forces a different solution for a smaller instance of the problem. *)
|
|
adam@324
|
609
|
|
adam@324
|
610 Example length_and_sum'' : exists ls : list nat, length ls = 2
|
|
adam@324
|
611 /\ sum ls = 3
|
|
adam@324
|
612 /\ Forall (fun n => n <> 0) ls.
|
|
adam@324
|
613 (* begin thide *)
|
|
adam@324
|
614 eauto 11.
|
|
adam@324
|
615 Qed.
|
|
adam@324
|
616 (* end thide *)
|
|
adam@324
|
617
|
|
adam@373
|
618 (* begin hide *)
|
|
adam@324
|
619 Print length_and_sum''.
|
|
adam@373
|
620 (* end hide *)
|
|
adam@373
|
621
|
|
adam@398
|
622 (** We could continue through exercises of this kind, but even more interesting than finding lists automatically is finding _programs_ automatically. *)
|
|
adam@324
|
623
|
|
adam@324
|
624
|
|
adam@324
|
625 (** * Synthesizing Programs *)
|
|
adam@324
|
626
|
|
adam@374
|
627 (** Here is a simple syntax type for arithmetic expressions, similar to those we have used several times before in the book. In this case, we allow expressions to mention exactly one distinguished variable. *)
|
|
adam@374
|
628
|
|
adam@324
|
629 Inductive exp : Set :=
|
|
adam@324
|
630 | Const : nat -> exp
|
|
adam@324
|
631 | Var : exp
|
|
adam@324
|
632 | Plus : exp -> exp -> exp.
|
|
adam@324
|
633
|
|
adam@374
|
634 (** An inductive relation specifies the semantics of an expression, relating a variable value and an expression to the expression value. *)
|
|
adam@374
|
635
|
|
adam@324
|
636 Inductive eval (var : nat) : exp -> nat -> Prop :=
|
|
adam@324
|
637 | EvalConst : forall n, eval var (Const n) n
|
|
adam@324
|
638 | EvalVar : eval var Var var
|
|
adam@324
|
639 | EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
|
|
adam@324
|
640 -> eval var e2 n2
|
|
adam@324
|
641 -> eval var (Plus e1 e2) (n1 + n2).
|
|
adam@324
|
642
|
|
adam@324
|
643 (* begin thide *)
|
|
adam@324
|
644 Hint Constructors eval.
|
|
adam@324
|
645 (* end thide *)
|
|
adam@324
|
646
|
|
adam@374
|
647 (** We can use [auto] to execute the semantics for specific expressions. *)
|
|
adam@374
|
648
|
|
adam@324
|
649 Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
|
|
adam@324
|
650 (* begin thide *)
|
|
adam@324
|
651 auto.
|
|
adam@324
|
652 Qed.
|
|
adam@324
|
653 (* end thide *)
|
|
adam@324
|
654
|
|
adam@374
|
655 (** Unfortunately, just the constructors of [eval] are not enough to prove theorems like the following, which depends on an arithmetic identity. *)
|
|
adam@374
|
656
|
|
adam@324
|
657 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
|
|
adam@324
|
658 (* begin thide *)
|
|
adam@324
|
659 eauto.
|
|
adam@324
|
660 Abort.
|
|
adam@324
|
661 (* end thide *)
|
|
adam@324
|
662
|
|
adam@484
|
663 (** To help prove [eval1'], we prove an alternate version of [EvalPlus] that inserts an extra equality premise. This sort of staging is helpful to get around limitations of [eauto]'s unification: [EvalPlus] as a direct hint will only match goals whose results are already expressed as additions, rather than as constants. With the alternate version below, to prove the first two premises, [eauto] is given free reign in deciding the values of [n1] and [n2], while the third premise can then be proved by [reflexivity], no matter how each of its sides is decomposed as a tree of additions. *)
|
|
adam@374
|
664
|
|
adam@324
|
665 (* begin thide *)
|
|
adam@324
|
666 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1
|
|
adam@324
|
667 -> eval var e2 n2
|
|
adam@324
|
668 -> n1 + n2 = n
|
|
adam@324
|
669 -> eval var (Plus e1 e2) n.
|
|
adam@324
|
670 crush.
|
|
adam@324
|
671 Qed.
|
|
adam@324
|
672
|
|
adam@324
|
673 Hint Resolve EvalPlus'.
|
|
adam@324
|
674
|
|
adam@374
|
675 (** Further, we instruct [eauto] to apply %\index{tactics!omega}%[omega], a standard tactic that provides a complete decision procedure for quantifier-free linear arithmetic. Via [Hint Extern], we ask for use of [omega] on any equality goal. The [abstract] tactical generates a new lemma for every such successful proof, so that, in the final proof term, the lemma may be referenced in place of dropping in the full proof of the arithmetic equality. *)
|
|
adam@374
|
676
|
|
adam@324
|
677 Hint Extern 1 (_ = _) => abstract omega.
|
|
adam@324
|
678 (* end thide *)
|
|
adam@324
|
679
|
|
adam@374
|
680 (** Now we can return to [eval1'] and prove it automatically. *)
|
|
adam@374
|
681
|
|
adam@324
|
682 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
|
|
adam@324
|
683 (* begin thide *)
|
|
adam@324
|
684 eauto.
|
|
adam@324
|
685 Qed.
|
|
adam@324
|
686 (* end thide *)
|
|
adam@324
|
687
|
|
adam@324
|
688 Print eval1'.
|
|
adam@374
|
689 (** %\vspace{-.15in}%[[
|
|
adam@374
|
690 eval1' =
|
|
adam@374
|
691 fun var : nat =>
|
|
adam@374
|
692 EvalPlus' (EvalVar var) (EvalPlus (EvalConst var 8) (EvalVar var))
|
|
adam@374
|
693 (eval1'_subproof var)
|
|
adam@374
|
694 : forall var : nat,
|
|
adam@374
|
695 eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8)
|
|
adam@374
|
696 ]]
|
|
adam@374
|
697 *)
|
|
adam@374
|
698
|
|
adam@374
|
699 (** The lemma [eval1'_subproof] was generated by [abstract omega].
|
|
adam@374
|
700
|
|
adam@374
|
701 Now we are ready to take advantage of logic programming's flexibility by searching for a program (arithmetic expression) that always evaluates to a particular symbolic value. *)
|
|
adam@324
|
702
|
|
adam@324
|
703 Example synthesize1 : exists e, forall var, eval var e (var + 7).
|
|
adam@324
|
704 (* begin thide *)
|
|
adam@324
|
705 eauto.
|
|
adam@324
|
706 Qed.
|
|
adam@324
|
707 (* end thide *)
|
|
adam@324
|
708
|
|
adam@324
|
709 Print synthesize1.
|
|
adam@374
|
710 (** %\vspace{-.15in}%[[
|
|
adam@374
|
711 synthesize1 =
|
|
adam@374
|
712 ex_intro (fun e : exp => forall var : nat, eval var e (var + 7))
|
|
adam@374
|
713 (Plus Var (Const 7))
|
|
adam@374
|
714 (fun var : nat => EvalPlus (EvalVar var) (EvalConst var 7))
|
|
adam@374
|
715 ]]
|
|
adam@374
|
716 *)
|
|
adam@374
|
717
|
|
adam@374
|
718 (** Here are two more examples showing off our program synthesis abilities. *)
|
|
adam@324
|
719
|
|
adam@324
|
720 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
|
|
adam@324
|
721 (* begin thide *)
|
|
adam@324
|
722 eauto.
|
|
adam@324
|
723 Qed.
|
|
adam@324
|
724 (* end thide *)
|
|
adam@324
|
725
|
|
adam@374
|
726 (* begin hide *)
|
|
adam@324
|
727 Print synthesize2.
|
|
adam@374
|
728 (* end hide *)
|
|
adam@324
|
729
|
|
adam@324
|
730 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
|
|
adam@324
|
731 (* begin thide *)
|
|
adam@324
|
732 eauto.
|
|
adam@324
|
733 Qed.
|
|
adam@324
|
734 (* end thide *)
|
|
adam@324
|
735
|
|
adam@374
|
736 (* begin hide *)
|
|
adam@324
|
737 Print synthesize3.
|
|
adam@374
|
738 (* end hide *)
|
|
adam@374
|
739
|
|
adam@374
|
740 (** These examples show linear expressions over the variable [var]. Any such expression is equivalent to [k * var + n] for some [k] and [n]. It is probably not so surprising that we can prove that any expression's semantics is equivalent to some such linear expression, but it is tedious to prove such a fact manually. To finish this section, we will use [eauto] to complete the proof, finding [k] and [n] values automatically.
|
|
adam@374
|
741
|
|
adam@374
|
742 We prove a series of lemmas and add them as hints. We have alternate [eval] constructor lemmas and some facts about arithmetic. *)
|
|
adam@324
|
743
|
|
adam@324
|
744 (* begin thide *)
|
|
adam@324
|
745 Theorem EvalConst' : forall var n m, n = m
|
|
adam@324
|
746 -> eval var (Const n) m.
|
|
adam@324
|
747 crush.
|
|
adam@324
|
748 Qed.
|
|
adam@324
|
749
|
|
adam@324
|
750 Hint Resolve EvalConst'.
|
|
adam@324
|
751
|
|
adam@324
|
752 Theorem zero_times : forall n m r,
|
|
adam@324
|
753 r = m
|
|
adam@324
|
754 -> r = 0 * n + m.
|
|
adam@324
|
755 crush.
|
|
adam@324
|
756 Qed.
|
|
adam@324
|
757
|
|
adam@324
|
758 Hint Resolve zero_times.
|
|
adam@324
|
759
|
|
adam@324
|
760 Theorem EvalVar' : forall var n,
|
|
adam@324
|
761 var = n
|
|
adam@324
|
762 -> eval var Var n.
|
|
adam@324
|
763 crush.
|
|
adam@324
|
764 Qed.
|
|
adam@324
|
765
|
|
adam@324
|
766 Hint Resolve EvalVar'.
|
|
adam@324
|
767
|
|
adam@324
|
768 Theorem plus_0 : forall n r,
|
|
adam@324
|
769 r = n
|
|
adam@324
|
770 -> r = n + 0.
|
|
adam@324
|
771 crush.
|
|
adam@324
|
772 Qed.
|
|
adam@324
|
773
|
|
adam@324
|
774 Theorem times_1 : forall n, n = 1 * n.
|
|
adam@324
|
775 crush.
|
|
adam@324
|
776 Qed.
|
|
adam@324
|
777
|
|
adam@324
|
778 Hint Resolve plus_0 times_1.
|
|
adam@324
|
779
|
|
adam@539
|
780 (** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the _ring_ algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *)
|
|
adam@374
|
781
|
|
adam@324
|
782 Require Import Arith Ring.
|
|
adam@324
|
783
|
|
adam@324
|
784 Theorem combine : forall x k1 k2 n1 n2,
|
|
adam@324
|
785 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).
|
|
adam@324
|
786 intros; ring.
|
|
adam@324
|
787 Qed.
|
|
adam@324
|
788
|
|
adam@324
|
789 Hint Resolve combine.
|
|
adam@324
|
790
|
|
adam@374
|
791 (** Our choice of hints is cheating, to an extent, by telegraphing the procedure for choosing values of [k] and [n]. Nonetheless, with these lemmas in place, we achieve an automated proof without explicitly orchestrating the lemmas' composition. *)
|
|
adam@374
|
792
|
|
adam@324
|
793 Theorem linear : forall e, exists k, exists n,
|
|
adam@324
|
794 forall var, eval var e (k * var + n).
|
|
adam@324
|
795 induction e; crush; eauto.
|
|
adam@324
|
796 Qed.
|
|
adam@324
|
797
|
|
adam@374
|
798 (* begin hide *)
|
|
adam@324
|
799 Print linear.
|
|
adam@374
|
800 (* end hide *)
|
|
adam@324
|
801 (* end thide *)
|
|
adam@324
|
802
|
|
adam@374
|
803 (** By printing the proof term, it is possible to see the procedure that is used to choose the constants for each input term. *)
|
|
adam@374
|
804
|
|
adam@324
|
805
|
|
adam@324
|
806 (** * More on [auto] Hints *)
|
|
adam@324
|
807
|
|
adam@430
|
808 (** Let us stop at this point and take stock of the possibilities for [auto] and [eauto] hints. Hints are contained within _hint databases_, which we have seen extended in many examples so far. When no hint database is specified, a default database is used. Hints in the default database are always used by [auto] or [eauto]. The chance to extend hint databases imperatively is important, because, in Ltac programming, we cannot create "global variables" whose values can be extended seamlessly by different modules in different source files. We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments. In fact, [crush] is defined in terms of [auto], which explains how we achieve this extensibility. Other user-defined tactics can take similar advantage of [auto] and [eauto].
|
|
adam@324
|
809
|
|
adam@506
|
810 The basic hints for [auto] and [eauto] are: %\index{Vernacular commands!Hint Immediate}%[Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; %\index{Vernacular commands!Hint Resolve}%[Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; %\index{Vernacular commands!Hint Constructors}%[Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and %\index{Vernacular commands!Hint Unfold}%[Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal. Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db], to add the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db]. An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db]. The default depth is 5.
|
|
adam@324
|
811
|
|
adam@484
|
812 All of these [Hint] commands can be expressed with a more primitive hint kind, [Extern]. A few more examples of [Hint Extern] should illustrate more of the possibilities. *)
|
|
adam@324
|
813
|
|
adam@324
|
814 Theorem bool_neq : true <> false.
|
|
adam@324
|
815 (* begin thide *)
|
|
adam@324
|
816 auto.
|
|
adam@324
|
817
|
|
adam@410
|
818 (** A call to [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
|
|
adam@324
|
819
|
|
adam@324
|
820 Abort.
|
|
adam@324
|
821
|
|
adam@430
|
822 (* begin hide *)
|
|
adam@437
|
823 (* begin thide *)
|
|
adam@430
|
824 Definition boool := bool.
|
|
adam@437
|
825 (* end thide *)
|
|
adam@430
|
826 (* end hide *)
|
|
adam@430
|
827
|
|
adam@375
|
828 (** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove. Luckily, a simpler form suffices, by appealing to the built-in tactic %\index{tactics!congruence}%[congruence], a complete procedure for the theory of equality, uninterpreted functions, and datatype constructors. *)
|
|
adam@324
|
829
|
|
adam@324
|
830 Hint Extern 1 (_ <> _) => congruence.
|
|
adam@324
|
831
|
|
adam@324
|
832 Theorem bool_neq : true <> false.
|
|
adam@324
|
833 auto.
|
|
adam@324
|
834 Qed.
|
|
adam@324
|
835 (* end thide *)
|
|
adam@324
|
836
|
|
adam@410
|
837 (** A [Hint Extern] may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
|
|
adam@324
|
838
|
|
adam@324
|
839 Section forall_and.
|
|
adam@324
|
840 Variable A : Set.
|
|
adam@324
|
841 Variables P Q : A -> Prop.
|
|
adam@324
|
842
|
|
adam@324
|
843 Hypothesis both : forall x, P x /\ Q x.
|
|
adam@324
|
844
|
|
adam@324
|
845 Theorem forall_and : forall z, P z.
|
|
adam@324
|
846 (* begin thide *)
|
|
adam@324
|
847 crush.
|
|
adam@324
|
848
|
|
adam@375
|
849 (** The [crush] invocation makes no progress beyond what [intros] would have accomplished. An [auto] invocation will not apply the hypothesis [both] to prove the goal, because the conclusion of [both] does not unify with the conclusion of the goal. However, we can teach [auto] to handle this kind of goal. *)
|
|
adam@324
|
850
|
|
adam@324
|
851 Hint Extern 1 (P ?X) =>
|
|
adam@324
|
852 match goal with
|
|
adam@324
|
853 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
|
|
adam@324
|
854 end.
|
|
adam@324
|
855
|
|
adam@324
|
856 auto.
|
|
adam@324
|
857 Qed.
|
|
adam@324
|
858 (* end thide *)
|
|
adam@324
|
859
|
|
adam@459
|
860 (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic. The function [proj1] is from the standard library, for extracting a proof of [U] from a proof of [U /\ V]. *)
|
|
adam@324
|
861
|
|
adam@324
|
862 End forall_and.
|
|
adam@324
|
863
|
|
adam@430
|
864 (* begin hide *)
|
|
adam@437
|
865 (* begin thide *)
|
|
adam@430
|
866 Definition noot := (not, @eq).
|
|
adam@437
|
867 (* end thide *)
|
|
adam@430
|
868 (* end hide *)
|
|
adam@430
|
869
|
|
adam@324
|
870 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
|
|
adam@324
|
871 [[
|
|
adam@430
|
872 Hint Extern 1 (?P ?X) =>
|
|
adam@430
|
873 match goal with
|
|
adam@430
|
874 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
|
|
adam@430
|
875 end.
|
|
adam@375
|
876 ]]
|
|
adam@375
|
877 <<
|
|
adam@375
|
878 User error: Bound head variable
|
|
adam@375
|
879 >>
|
|
adam@324
|
880
|
|
adam@410
|
881 Coq's [auto] hint databases work as tables mapping%\index{head symbol}% _head symbols_ to lists of tactics to try. Because of this, the constant head of an [Extern] pattern must be determinable statically. In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P].
|
|
adam@324
|
882
|
|
adam@375
|
883 Fortunately, a more basic form of [Hint Extern] also applies. We may simply leave out the pattern to the left of the [=>], incorporating the corresponding logic into the Ltac script. *)
|
|
adam@324
|
884
|
|
adam@375
|
885 Hint Extern 1 =>
|
|
adam@375
|
886 match goal with
|
|
adam@375
|
887 | [ H : forall x, ?P x /\ _ |- ?P ?X ] => apply (proj1 (H X))
|
|
adam@375
|
888 end.
|
|
adam@375
|
889
|
|
adam@398
|
890 (** Be forewarned that a [Hint Extern] of this kind will be applied at _every_ node of a proof tree, so an expensive Ltac script may slow proof search significantly. *)
|
|
adam@324
|
891
|
|
adam@324
|
892
|
|
adam@324
|
893 (** * Rewrite Hints *)
|
|
adam@324
|
894
|
|
adam@375
|
895 (** Another dimension of extensibility with hints is rewriting with quantified equalities. We have used the associated command %\index{Vernacular commands!Hint Rewrite}%[Hint Rewrite] in many examples so far. The [crush] tactic uses these hints by calling the built-in tactic %\index{tactics!autorewrite}%[autorewrite]. Our rewrite hints have taken the form [Hint Rewrite lemma], which by default adds them to the default hint database [core]; but alternate hint databases may also be specified just as with, e.g., [Hint Resolve].
|
|
adam@324
|
896
|
|
adam@375
|
897 The next example shows a direct use of [autorewrite]. Note that, while [Hint Rewrite] uses a default database, [autorewrite] requires that a database be named. *)
|
|
adam@324
|
898
|
|
adam@324
|
899 Section autorewrite.
|
|
adam@324
|
900 Variable A : Set.
|
|
adam@324
|
901 Variable f : A -> A.
|
|
adam@324
|
902
|
|
adam@324
|
903 Hypothesis f_f : forall x, f (f x) = f x.
|
|
adam@324
|
904
|
|
adam@375
|
905 Hint Rewrite f_f.
|
|
adam@324
|
906
|
|
adam@324
|
907 Lemma f_f_f : forall x, f (f (f x)) = f x.
|
|
adam@375
|
908 intros; autorewrite with core; reflexivity.
|
|
adam@324
|
909 Qed.
|
|
adam@324
|
910
|
|
adam@430
|
911 (** There are a few ways in which [autorewrite] can lead to trouble when insufficient care is taken in choosing hints. First, the set of hints may define a nonterminating rewrite system, in which case invocations to [autorewrite] may not terminate. Second, we may add hints that "lead [autorewrite] down the wrong path." For instance: *)
|
|
adam@324
|
912
|
|
adam@324
|
913 Section garden_path.
|
|
adam@324
|
914 Variable g : A -> A.
|
|
adam@324
|
915 Hypothesis f_g : forall x, f x = g x.
|
|
adam@375
|
916 Hint Rewrite f_g.
|
|
adam@324
|
917
|
|
adam@324
|
918 Lemma f_f_f' : forall x, f (f (f x)) = f x.
|
|
adam@375
|
919 intros; autorewrite with core.
|
|
adam@324
|
920 (** [[
|
|
adam@324
|
921 ============================
|
|
adam@324
|
922 g (g (g x)) = g x
|
|
adam@324
|
923 ]]
|
|
adam@324
|
924 *)
|
|
adam@324
|
925
|
|
adam@324
|
926 Abort.
|
|
adam@324
|
927
|
|
adam@430
|
928 (** Our new hint was used to rewrite the goal into a form where the old hint could no longer be applied. This "non-monotonicity" of rewrite hints contrasts with the situation for [auto], where new hints may slow down proof search but can never "break" old proofs. The key difference is that [auto] either solves a goal or makes no changes to it, while [autorewrite] may change goals without solving them. The situation for [eauto] is slightly more complicated, as changes to hint databases may change the proof found for a particular goal, and that proof may influence the settings of unification variables that appear elsewhere in the proof state. *)
|
|
adam@324
|
929
|
|
adam@324
|
930 Reset garden_path.
|
|
adam@324
|
931
|
|
adam@375
|
932 (** The [autorewrite] tactic also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
|
|
adam@324
|
933
|
|
adam@324
|
934 Section garden_path.
|
|
adam@324
|
935 Variable P : A -> Prop.
|
|
adam@324
|
936 Variable g : A -> A.
|
|
adam@324
|
937 Hypothesis f_g : forall x, P x -> f x = g x.
|
|
adam@375
|
938 Hint Rewrite f_g.
|
|
adam@324
|
939
|
|
adam@324
|
940 Lemma f_f_f' : forall x, f (f (f x)) = f x.
|
|
adam@375
|
941 intros; autorewrite with core.
|
|
adam@324
|
942 (** [[
|
|
adam@324
|
943 ============================
|
|
adam@324
|
944 g (g (g x)) = g x
|
|
adam@324
|
945
|
|
adam@324
|
946 subgoal 2 is:
|
|
adam@324
|
947 P x
|
|
adam@324
|
948 subgoal 3 is:
|
|
adam@324
|
949 P (f x)
|
|
adam@324
|
950 subgoal 4 is:
|
|
adam@324
|
951 P (f x)
|
|
adam@324
|
952 ]]
|
|
adam@324
|
953 *)
|
|
adam@324
|
954
|
|
adam@324
|
955 Abort.
|
|
adam@324
|
956
|
|
adam@324
|
957 (** The inappropriate rule fired the same three times as before, even though we know we will not be able to prove the premises. *)
|
|
adam@324
|
958
|
|
adam@324
|
959 Reset garden_path.
|
|
adam@324
|
960
|
|
adam@324
|
961 (** Our final, successful, attempt uses an extra argument to [Hint Rewrite] that specifies a tactic to apply to generated premises. Such a hint is only used when the tactic succeeds for all premises, possibly leaving further subgoals for some premises. *)
|
|
adam@324
|
962
|
|
adam@324
|
963 Section garden_path.
|
|
adam@324
|
964 Variable P : A -> Prop.
|
|
adam@324
|
965 Variable g : A -> A.
|
|
adam@324
|
966 Hypothesis f_g : forall x, P x -> f x = g x.
|
|
adam@324
|
967 (* begin thide *)
|
|
adam@375
|
968 Hint Rewrite f_g using assumption.
|
|
adam@324
|
969 (* end thide *)
|
|
adam@324
|
970
|
|
adam@324
|
971 Lemma f_f_f' : forall x, f (f (f x)) = f x.
|
|
adam@324
|
972 (* begin thide *)
|
|
adam@375
|
973 intros; autorewrite with core; reflexivity.
|
|
adam@324
|
974 Qed.
|
|
adam@324
|
975 (* end thide *)
|
|
adam@324
|
976
|
|
adam@375
|
977 (** We may still use [autorewrite] to apply [f_g] when the generated premise is among our assumptions. *)
|
|
adam@324
|
978
|
|
adam@324
|
979 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
|
|
adam@324
|
980 (* begin thide *)
|
|
adam@375
|
981 intros; autorewrite with core; reflexivity.
|
|
adam@324
|
982 (* end thide *)
|
|
adam@324
|
983 Qed.
|
|
adam@324
|
984 End garden_path.
|
|
adam@324
|
985
|
|
adam@375
|
986 (** It can also be useful to apply the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *)
|
|
adam@324
|
987
|
|
adam@324
|
988 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
|
|
adam@324
|
989 -> f x = f (f (f y)).
|
|
adam@324
|
990 (* begin thide *)
|
|
adam@375
|
991 intros; autorewrite with core in *; assumption.
|
|
adam@324
|
992 (* end thide *)
|
|
adam@324
|
993 Qed.
|
|
adam@324
|
994
|
|
adam@324
|
995 End autorewrite.
|
|
adam@375
|
996
|
|
adam@475
|
997 (** Many proofs can be automated in pleasantly modular ways with deft combinations of [auto] and [autorewrite]. *)
|
