Mercurial > cpdt > repo

comparison src/LogicProg.v @ 324:06d11a6363cd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New LogicProg chapter
author Adam Chlipala <adam@chlipala.net>
date Tue, 20 Sep 2011 14:07:21 -0400
parents
children 5e24554175de
comparison
equal deleted inserted replaced
323:3513d8b0531a 324:06d11a6363cd
1 (* Copyright (c) 2011, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11
12 Require Import List.
13
14 Require Import CpdtTactics.
15
16 Set Implicit Arguments.
17
18 (* end hide *)
19
20 (** %\part{Proof Engineering}
21
22 \chapter{Proof Search by Logic Programming}% *)
23
24 (** Exciting new chapter that is missing prose for the new content! Some content was moved from the next chapter, and it may not seem entirely to fit here yet. *)
25
26
27 (** * Introducing Logic Programming *)
28
29 Print plus.
30
31 Inductive plusR : nat -> nat -> nat -> Prop :=
32 | PlusO : forall m, plusR O m m
33 | PlusS : forall n m r, plusR n m r
34 -> plusR (S n) m (S r).
35
36 (* begin thide *)
37 Hint Constructors plusR.
38 (* end thide *)
39
40 Theorem plus_plusR : forall n m,
41 plusR n m (n + m).
42 (* begin thide *)
43 induction n; crush.
44 Qed.
45 (* end thide *)
46
47 Theorem plusR_plus : forall n m r,
48 plusR n m r
49 -> r = n + m.
50 (* begin thide *)
51 induction 1; crush.
52 Qed.
53 (* end thide *)
54
55 Example four_plus_three : 4 + 3 = 7.
56 (* begin thide *)
57 reflexivity.
58 Qed.
59 (* end thide *)
60
61 Example four_plus_three' : plusR 4 3 7.
62 (* begin thide *)
63 auto.
64 Qed.
65 (* end thide *)
66
67 Example five_plus_three' : plusR 5 3 8.
68 (* begin thide *)
69 auto 6.
70 Restart.
71 info auto 6.
72 Qed.
73 (* end thide *)
74
75 (* begin thide *)
76 Hint Constructors ex.
77 (* end thide *)
78
79 Example seven_minus_three : exists x, x + 3 = 7.
80 (* begin thide *)
81 eauto 6.
82 Abort.
83 (* end thide *)
84
85 Example seven_minus_three' : exists x, plusR x 3 7.
86 (* begin thide *)
87 info eauto 6.
88 Qed.
89 (* end thide *)
90
91 Example seven_minus_four' : exists x, plusR 4 x 7.
92 (* begin thide *)
93 info eauto 6.
94 Qed.
95 (* end thide *)
96
97 (* begin thide *)
98 SearchRewrite (O + _).
99
100 Hint Immediate plus_O_n.
101
102 Lemma plusS : forall n m r,
103 n + m = r
104 -> S n + m = S r.
105 crush.
106 Qed.
107
108 Hint Resolve plusS.
109 (* end thide *)
110
111 Example seven_minus_three : exists x, x + 3 = 7.
112 (* begin thide *)
113 info eauto 6.
114 Qed.
115 (* end thide *)
116
117 Example seven_minus_four : exists x, 4 + x = 7.
118 (* begin thide *)
119 info eauto 6.
120 Qed.
121 (* end thide *)
122
123 Example hundred_minus_hundred : exists x, 4 + x + 0 = 7.
124 (* begin thide *)
125 eauto 6.
126 Abort.
127 (* end thide *)
128
129 (* begin thide *)
130 Lemma plusO : forall n m,
131 n = m
132 -> n + 0 = m.
133 crush.
134 Qed.
135
136 Hint Resolve plusO.
137 (* end thide *)
138
139 Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
140 (* begin thide *)
141 info eauto 7.
142 Qed.
143 (* end thide *)
144
145 Check eq_trans.
146
147 Section slow.
148 Hint Resolve eq_trans.
149
150 Example three_minus_four_zero : exists x, 1 + x = 0.
151 Time eauto 1.
152 Time eauto 2.
153 Time eauto 3.
154 Time eauto 4.
155 Time eauto 5.
156 debug eauto 3.
157 Abort.
158 End slow.
159
160 (* begin thide *)
161 Hint Resolve eq_trans : slow.
162 (* end thide *)
163
164 Example three_minus_four_zero : exists x, 1 + x = 0.
165 (* begin thide *)
166 eauto.
167 Abort.
168 (* end thide *)
169
170 Example seven_minus_three_again : exists x, x + 3 = 7.
171 (* begin thide *)
172 eauto 6.
173 Qed.
174 (* end thide *)
175
176 Example needs_trans : forall x y, 1 + x = y
177 -> y = 2
178 -> exists z, z + x = 3.
179 (* begin thide *)
180 info eauto with slow.
181 Qed.
182 (* end thide *)
183
184
185 (** * Searching for Underconstrained Values *)
186
187 Print length.
188
189 Example length_1_2 : length (1 :: 2 :: nil) = 2.
190 auto.
191 Qed.
192
193 Print length_1_2.
194
195 (* begin thide *)
196 Theorem length_O : forall A, length (nil (A := A)) = O.
197 crush.
198 Qed.
199
200 Theorem length_S : forall A (h : A) t n,
201 length t = n
202 -> length (h :: t) = S n.
203 crush.
204 Qed.
205
206 Hint Resolve length_O length_S.
207 (* end thide *)
208
209 Example length_is_2 : exists ls : list nat, length ls = 2.
210 (* begin thide *)
211 eauto.
212
213 Show Proof.
214 Abort.
215 (* end thide *)
216
217 Print Forall.
218
219 Example length_is_2 : exists ls : list nat, length ls = 2
220 /\ Forall (fun n => n >= 1) ls.
221 (* begin thide *)
222 eauto 9.
223 Qed.
224 (* end thide *)
225
226 Definition sum := fold_right plus O.
227
228 (* begin thide *)
229 Lemma plusO' : forall n m,
230 n = m
231 -> 0 + n = m.
232 crush.
233 Qed.
234
235 Hint Resolve plusO'.
236
237 Hint Extern 1 (sum _ = _) => simpl.
238 (* end thide *)
239
240 Example length_and_sum : exists ls : list nat, length ls = 2
241 /\ sum ls = O.
242 (* begin thide *)
243 eauto 7.
244 Qed.
245 (* end thide *)
246
247 Print length_and_sum.
248
249 Example length_and_sum' : exists ls : list nat, length ls = 5
250 /\ sum ls = 42.
251 (* begin thide *)
252 eauto 15.
253 Qed.
254 (* end thide *)
255
256 Print length_and_sum'.
257
258 Example length_and_sum'' : exists ls : list nat, length ls = 2
259 /\ sum ls = 3
260 /\ Forall (fun n => n <> 0) ls.
261 (* begin thide *)
262 eauto 11.
263 Qed.
264 (* end thide *)
265
266 Print length_and_sum''.
267
268
269 (** * Synthesizing Programs *)
270
271 Inductive exp : Set :=
272 | Const : nat -> exp
273 | Var : exp
274 | Plus : exp -> exp -> exp.
275
276 Inductive eval (var : nat) : exp -> nat -> Prop :=
277 | EvalConst : forall n, eval var (Const n) n
278 | EvalVar : eval var Var var
279 | EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
280 -> eval var e2 n2
281 -> eval var (Plus e1 e2) (n1 + n2).
282
283 (* begin thide *)
284 Hint Constructors eval.
285 (* end thide *)
286
287 Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
288 (* begin thide *)
289 auto.
290 Qed.
291 (* end thide *)
292
293 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
294 (* begin thide *)
295 eauto.
296 Abort.
297 (* end thide *)
298
299 (* begin thide *)
300 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1
301 -> eval var e2 n2
302 -> n1 + n2 = n
303 -> eval var (Plus e1 e2) n.
304 crush.
305 Qed.
306
307 Hint Resolve EvalPlus'.
308
309 Hint Extern 1 (_ = _) => abstract omega.
310 (* end thide *)
311
312 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
313 (* begin thide *)
314 eauto.
315 Qed.
316 (* end thide *)
317
318 Print eval1'.
319
320 Example synthesize1 : exists e, forall var, eval var e (var + 7).
321 (* begin thide *)
322 eauto.
323 Qed.
324 (* end thide *)
325
326 Print synthesize1.
327
328 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
329 (* begin thide *)
330 eauto.
331 Qed.
332 (* end thide *)
333
334 Print synthesize2.
335
336 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
337 (* begin thide *)
338 eauto.
339 Qed.
340 (* end thide *)
341
342 Print synthesize3.
343
344 (* begin thide *)
345 Theorem EvalConst' : forall var n m, n = m
346 -> eval var (Const n) m.
347 crush.
348 Qed.
349
350 Hint Resolve EvalConst'.
351
352 Theorem zero_times : forall n m r,
353 r = m
354 -> r = 0 * n + m.
355 crush.
356 Qed.
357
358 Hint Resolve zero_times.
359
360 Theorem EvalVar' : forall var n,
361 var = n
362 -> eval var Var n.
363 crush.
364 Qed.
365
366 Hint Resolve EvalVar'.
367
368 Theorem plus_0 : forall n r,
369 r = n
370 -> r = n + 0.
371 crush.
372 Qed.
373
374 Theorem times_1 : forall n, n = 1 * n.
375 crush.
376 Qed.
377
378 Hint Resolve plus_0 times_1.
379
380 Require Import Arith Ring.
381
382 Theorem combine : forall x k1 k2 n1 n2,
383 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).
384 intros; ring.
385 Qed.
386
387 Hint Resolve combine.
388
389 Theorem linear : forall e, exists k, exists n,
390 forall var, eval var e (k * var + n).
391 induction e; crush; eauto.
392 Qed.
393
394 Print linear.
395 (* end thide *)
396
397
398 (** * More on [auto] Hints *)
399
400 (** Another class of built-in tactics includes [auto], [eauto], and [autorewrite]. These are based on %\textit{%#<i>#hint databases#</i>#%}%, which we have seen extended in many examples so far. These tactics are 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.
401
402 The basic hints for [auto] and [eauto] are [Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; [Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; [Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and [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]. This adds 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.
403
404 All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern]. A few examples should do best to explain how [Hint Extern] works. *)
405
406 Theorem bool_neq : true <> false.
407 (* begin thide *)
408 auto.
409
410 (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
411
412 Abort.
413
414 (** 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. *)
415
416 Hint Extern 1 (_ <> _) => congruence.
417
418 Theorem bool_neq : true <> false.
419 auto.
420 Qed.
421 (* end thide *)
422
423 (** Our hint says: %``%#"#whenever the conclusion matches the pattern [_ <> _], try applying [congruence].#"#%''% The [1] is a cost for this rule. During proof search, whenever multiple rules apply, rules are tried in increasing cost order, so it pays to assign high costs to relatively expensive [Extern] hints.
424
425 [Extern] hints may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
426
427 Section forall_and.
428 Variable A : Set.
429 Variables P Q : A -> Prop.
430
431 Hypothesis both : forall x, P x /\ Q x.
432
433 Theorem forall_and : forall z, P z.
434 (* begin thide *)
435 crush.
436
437 (** [crush] makes no progress beyond what [intros] would have accomplished. [auto] 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. *)
438
439 Hint Extern 1 (P ?X) =>
440 match goal with
441 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
442 end.
443
444 auto.
445 Qed.
446 (* end thide *)
447
448 (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic. [proj1] is a function from the standard library for extracting a proof of [R] from a proof of [R /\ S]. *)
449
450 End forall_and.
451
452 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
453
454 [[
455 Hint Extern 1 (?P ?X) =>
456 match goal with
457 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
458 end.
459
460 User error: Bound head variable
461
462 ]]
463
464 Coq's [auto] hint databases work as tables mapping %\textit{%#<i>#head symbols#</i>#%}% 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].
465
466 This restriction on [Extern] hints is the main limitation of the [auto] mechanism, preventing us from using it for general context simplifications that are not keyed off of the form of the conclusion. This is perhaps just as well, since we can often code more efficient tactics with specialized Ltac programs, and we will see how in the next chapter. *)
467
468
469 (** * Rewrite Hints *)
470
471 (** We have used [Hint Rewrite] in many examples so far. [crush] uses these hints by calling [autorewrite]. Our rewrite hints have taken the form [Hint Rewrite lemma : cpdt], adding them to the [cpdt] rewrite database. This is because, in contrast to [auto], [autorewrite] has no default database. Thus, we set the convention that [crush] uses the [cpdt] database.
472
473 This example shows a direct use of [autorewrite]. *)
474
475 Section autorewrite.
476 Variable A : Set.
477 Variable f : A -> A.
478
479 Hypothesis f_f : forall x, f (f x) = f x.
480
481 Hint Rewrite f_f : my_db.
482
483 Lemma f_f_f : forall x, f (f (f x)) = f x.
484 intros; autorewrite with my_db; reflexivity.
485 Qed.
486
487 (** 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: *)
488
489 Section garden_path.
490 Variable g : A -> A.
491 Hypothesis f_g : forall x, f x = g x.
492 Hint Rewrite f_g : my_db.
493
494 Lemma f_f_f' : forall x, f (f (f x)) = f x.
495 intros; autorewrite with my_db.
496 (** [[
497 ============================
498 g (g (g x)) = g x
499 ]]
500 *)
501
502 Abort.
503
504 (** 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. *)
505
506 Reset garden_path.
507
508 (** [autorewrite] also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
509
510 Section garden_path.
511 Variable P : A -> Prop.
512 Variable g : A -> A.
513 Hypothesis f_g : forall x, P x -> f x = g x.
514 Hint Rewrite f_g : my_db.
515
516 Lemma f_f_f' : forall x, f (f (f x)) = f x.
517 intros; autorewrite with my_db.
518 (** [[
519
520 ============================
521 g (g (g x)) = g x
522
523 subgoal 2 is:
524 P x
525 subgoal 3 is:
526 P (f x)
527 subgoal 4 is:
528 P (f x)
529 ]]
530 *)
531
532 Abort.
533
534 (** The inappropriate rule fired the same three times as before, even though we know we will not be able to prove the premises. *)
535
536 Reset garden_path.
537
538 (** 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. *)
539
540 Section garden_path.
541 Variable P : A -> Prop.
542 Variable g : A -> A.
543 Hypothesis f_g : forall x, P x -> f x = g x.
544 (* begin thide *)
545 Hint Rewrite f_g using assumption : my_db.
546 (* end thide *)
547
548 Lemma f_f_f' : forall x, f (f (f x)) = f x.
549 (* begin thide *)
550 intros; autorewrite with my_db; reflexivity.
551 Qed.
552 (* end thide *)
553
554 (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *)
555
556 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
557 (* begin thide *)
558 intros; autorewrite with my_db; reflexivity.
559 (* end thide *)
560 Qed.
561 End garden_path.
562
563 (** remove printing * *)
564
565 (** It can also be useful to use the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *)
566
567 (** printing * $*$ *)
568
569 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
570 -> f x = f (f (f y)).
571 (* begin thide *)
572 intros; autorewrite with my_db in *; assumption.
573 (* end thide *)
574 Qed.
575
576 End autorewrite.