Mercurial > cpdt > repo

annotate src/LogicProg.v @ 351:bb1a470c1757

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Well-founded recursion
author Adam Chlipala <adam@chlipala.net>
date Wed, 26 Oct 2011 15:12:21 -0400
parents 386b7ad8849b
children 549d604c3d16
rev   line source
adam@324 1 (* Copyright (c) 2011, 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@324 12 Require Import List.
adam@324 13
adam@324 14 Require Import CpdtTactics.
adam@324 15
adam@324 16 Set Implicit Arguments.
adam@324 17
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@324 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. *)
adam@324 25
adam@324 26
adam@324 27 (** * Introducing Logic Programming *)
adam@324 28
adam@324 29 Print plus.
adam@324 30
adam@324 31 Inductive plusR : nat -> nat -> nat -> Prop :=
adam@324 32 | PlusO : forall m, plusR O m m
adam@324 33 | PlusS : forall n m r, plusR n m r
adam@324 34 -> plusR (S n) m (S r).
adam@324 35
adam@324 36 (* begin thide *)
adam@324 37 Hint Constructors plusR.
adam@324 38 (* end thide *)
adam@324 39
adam@324 40 Theorem plus_plusR : forall n m,
adam@324 41 plusR n m (n + m).
adam@324 42 (* begin thide *)
adam@324 43 induction n; crush.
adam@324 44 Qed.
adam@324 45 (* end thide *)
adam@324 46
adam@324 47 Theorem plusR_plus : forall n m r,
adam@324 48 plusR n m r
adam@324 49 -> r = n + m.
adam@324 50 (* begin thide *)
adam@324 51 induction 1; crush.
adam@324 52 Qed.
adam@324 53 (* end thide *)
adam@324 54
adam@324 55 Example four_plus_three : 4 + 3 = 7.
adam@324 56 (* begin thide *)
adam@324 57 reflexivity.
adam@324 58 Qed.
adam@324 59 (* end thide *)
adam@324 60
adam@324 61 Example four_plus_three' : plusR 4 3 7.
adam@324 62 (* begin thide *)
adam@324 63 auto.
adam@324 64 Qed.
adam@324 65 (* end thide *)
adam@324 66
adam@324 67 Example five_plus_three' : plusR 5 3 8.
adam@324 68 (* begin thide *)
adam@324 69 auto 6.
adam@324 70 Restart.
adam@324 71 info auto 6.
adam@324 72 Qed.
adam@324 73 (* end thide *)
adam@324 74
adam@324 75 (* begin thide *)
adam@324 76 Hint Constructors ex.
adam@324 77 (* end thide *)
adam@324 78
adam@324 79 Example seven_minus_three : exists x, x + 3 = 7.
adam@324 80 (* begin thide *)
adam@324 81 eauto 6.
adam@324 82 Abort.
adam@324 83 (* end thide *)
adam@324 84
adam@324 85 Example seven_minus_three' : exists x, plusR x 3 7.
adam@324 86 (* begin thide *)
adam@324 87 info eauto 6.
adam@324 88 Qed.
adam@324 89 (* end thide *)
adam@324 90
adam@324 91 Example seven_minus_four' : exists x, plusR 4 x 7.
adam@324 92 (* begin thide *)
adam@324 93 info eauto 6.
adam@324 94 Qed.
adam@324 95 (* end thide *)
adam@324 96
adam@324 97 (* begin thide *)
adam@324 98 SearchRewrite (O + _).
adam@324 99
adam@324 100 Hint Immediate plus_O_n.
adam@324 101
adam@324 102 Lemma plusS : forall n m r,
adam@324 103 n + m = r
adam@324 104 -> S n + m = S r.
adam@324 105 crush.
adam@324 106 Qed.
adam@324 107
adam@324 108 Hint Resolve plusS.
adam@324 109 (* end thide *)
adam@324 110
adam@324 111 Example seven_minus_three : exists x, x + 3 = 7.
adam@324 112 (* begin thide *)
adam@324 113 info eauto 6.
adam@324 114 Qed.
adam@324 115 (* end thide *)
adam@324 116
adam@324 117 Example seven_minus_four : exists x, 4 + x = 7.
adam@324 118 (* begin thide *)
adam@324 119 info eauto 6.
adam@324 120 Qed.
adam@324 121 (* end thide *)
adam@324 122
adam@324 123 Example hundred_minus_hundred : exists x, 4 + x + 0 = 7.
adam@324 124 (* begin thide *)
adam@324 125 eauto 6.
adam@324 126 Abort.
adam@324 127 (* end thide *)
adam@324 128
adam@324 129 (* begin thide *)
adam@324 130 Lemma plusO : forall n m,
adam@324 131 n = m
adam@324 132 -> n + 0 = m.
adam@324 133 crush.
adam@324 134 Qed.
adam@324 135
adam@324 136 Hint Resolve plusO.
adam@324 137 (* end thide *)
adam@324 138
adam@324 139 Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
adam@324 140 (* begin thide *)
adam@324 141 info eauto 7.
adam@324 142 Qed.
adam@324 143 (* end thide *)
adam@324 144
adam@324 145 Check eq_trans.
adam@324 146
adam@324 147 Section slow.
adam@324 148 Hint Resolve eq_trans.
adam@324 149
adam@324 150 Example three_minus_four_zero : exists x, 1 + x = 0.
adam@324 151 Time eauto 1.
adam@324 152 Time eauto 2.
adam@324 153 Time eauto 3.
adam@324 154 Time eauto 4.
adam@324 155 Time eauto 5.
adam@324 156 debug eauto 3.
adam@324 157 Abort.
adam@324 158 End slow.
adam@324 159
adam@324 160 (* begin thide *)
adam@324 161 Hint Resolve eq_trans : slow.
adam@324 162 (* end thide *)
adam@324 163
adam@324 164 Example three_minus_four_zero : exists x, 1 + x = 0.
adam@324 165 (* begin thide *)
adam@324 166 eauto.
adam@324 167 Abort.
adam@324 168 (* end thide *)
adam@324 169
adam@324 170 Example seven_minus_three_again : exists x, x + 3 = 7.
adam@324 171 (* begin thide *)
adam@324 172 eauto 6.
adam@324 173 Qed.
adam@324 174 (* end thide *)
adam@324 175
adam@324 176 Example needs_trans : forall x y, 1 + x = y
adam@324 177 -> y = 2
adam@324 178 -> exists z, z + x = 3.
adam@324 179 (* begin thide *)
adam@324 180 info eauto with slow.
adam@324 181 Qed.
adam@324 182 (* end thide *)
adam@324 183
adam@324 184
adam@324 185 (** * Searching for Underconstrained Values *)
adam@324 186
adam@324 187 Print length.
adam@324 188
adam@324 189 Example length_1_2 : length (1 :: 2 :: nil) = 2.
adam@324 190 auto.
adam@324 191 Qed.
adam@324 192
adam@324 193 Print length_1_2.
adam@324 194
adam@324 195 (* begin thide *)
adam@324 196 Theorem length_O : forall A, length (nil (A := A)) = O.
adam@324 197 crush.
adam@324 198 Qed.
adam@324 199
adam@324 200 Theorem length_S : forall A (h : A) t n,
adam@324 201 length t = n
adam@324 202 -> length (h :: t) = S n.
adam@324 203 crush.
adam@324 204 Qed.
adam@324 205
adam@324 206 Hint Resolve length_O length_S.
adam@324 207 (* end thide *)
adam@324 208
adam@324 209 Example length_is_2 : exists ls : list nat, length ls = 2.
adam@324 210 (* begin thide *)
adam@324 211 eauto.
adam@324 212
adam@324 213 Show Proof.
adam@324 214 Abort.
adam@324 215 (* end thide *)
adam@324 216
adam@324 217 Print Forall.
adam@324 218
adam@324 219 Example length_is_2 : exists ls : list nat, length ls = 2
adam@324 220 /\ Forall (fun n => n >= 1) ls.
adam@324 221 (* begin thide *)
adam@324 222 eauto 9.
adam@324 223 Qed.
adam@324 224 (* end thide *)
adam@324 225
adam@324 226 Definition sum := fold_right plus O.
adam@324 227
adam@324 228 (* begin thide *)
adam@324 229 Lemma plusO' : forall n m,
adam@324 230 n = m
adam@324 231 -> 0 + n = m.
adam@324 232 crush.
adam@324 233 Qed.
adam@324 234
adam@324 235 Hint Resolve plusO'.
adam@324 236
adam@324 237 Hint Extern 1 (sum _ = _) => simpl.
adam@324 238 (* end thide *)
adam@324 239
adam@324 240 Example length_and_sum : exists ls : list nat, length ls = 2
adam@324 241 /\ sum ls = O.
adam@324 242 (* begin thide *)
adam@324 243 eauto 7.
adam@324 244 Qed.
adam@324 245 (* end thide *)
adam@324 246
adam@324 247 Print length_and_sum.
adam@324 248
adam@324 249 Example length_and_sum' : exists ls : list nat, length ls = 5
adam@324 250 /\ sum ls = 42.
adam@324 251 (* begin thide *)
adam@324 252 eauto 15.
adam@324 253 Qed.
adam@324 254 (* end thide *)
adam@324 255
adam@324 256 Print length_and_sum'.
adam@324 257
adam@324 258 Example length_and_sum'' : exists ls : list nat, length ls = 2
adam@324 259 /\ sum ls = 3
adam@324 260 /\ Forall (fun n => n <> 0) ls.
adam@324 261 (* begin thide *)
adam@324 262 eauto 11.
adam@324 263 Qed.
adam@324 264 (* end thide *)
adam@324 265
adam@324 266 Print length_and_sum''.
adam@324 267
adam@324 268
adam@324 269 (** * Synthesizing Programs *)
adam@324 270
adam@324 271 Inductive exp : Set :=
adam@324 272 | Const : nat -> exp
adam@324 273 | Var : exp
adam@324 274 | Plus : exp -> exp -> exp.
adam@324 275
adam@324 276 Inductive eval (var : nat) : exp -> nat -> Prop :=
adam@324 277 | EvalConst : forall n, eval var (Const n) n
adam@324 278 | EvalVar : eval var Var var
adam@324 279 | EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
adam@324 280 -> eval var e2 n2
adam@324 281 -> eval var (Plus e1 e2) (n1 + n2).
adam@324 282
adam@324 283 (* begin thide *)
adam@324 284 Hint Constructors eval.
adam@324 285 (* end thide *)
adam@324 286
adam@324 287 Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
adam@324 288 (* begin thide *)
adam@324 289 auto.
adam@324 290 Qed.
adam@324 291 (* end thide *)
adam@324 292
adam@324 293 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
adam@324 294 (* begin thide *)
adam@324 295 eauto.
adam@324 296 Abort.
adam@324 297 (* end thide *)
adam@324 298
adam@324 299 (* begin thide *)
adam@324 300 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1
adam@324 301 -> eval var e2 n2
adam@324 302 -> n1 + n2 = n
adam@324 303 -> eval var (Plus e1 e2) n.
adam@324 304 crush.
adam@324 305 Qed.
adam@324 306
adam@324 307 Hint Resolve EvalPlus'.
adam@324 308
adam@324 309 Hint Extern 1 (_ = _) => abstract omega.
adam@324 310 (* end thide *)
adam@324 311
adam@324 312 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
adam@324 313 (* begin thide *)
adam@324 314 eauto.
adam@324 315 Qed.
adam@324 316 (* end thide *)
adam@324 317
adam@324 318 Print eval1'.
adam@324 319
adam@324 320 Example synthesize1 : exists e, forall var, eval var e (var + 7).
adam@324 321 (* begin thide *)
adam@324 322 eauto.
adam@324 323 Qed.
adam@324 324 (* end thide *)
adam@324 325
adam@324 326 Print synthesize1.
adam@324 327
adam@324 328 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
adam@324 329 (* begin thide *)
adam@324 330 eauto.
adam@324 331 Qed.
adam@324 332 (* end thide *)
adam@324 333
adam@324 334 Print synthesize2.
adam@324 335
adam@324 336 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
adam@324 337 (* begin thide *)
adam@324 338 eauto.
adam@324 339 Qed.
adam@324 340 (* end thide *)
adam@324 341
adam@324 342 Print synthesize3.
adam@324 343
adam@324 344 (* begin thide *)
adam@324 345 Theorem EvalConst' : forall var n m, n = m
adam@324 346 -> eval var (Const n) m.
adam@324 347 crush.
adam@324 348 Qed.
adam@324 349
adam@324 350 Hint Resolve EvalConst'.
adam@324 351
adam@324 352 Theorem zero_times : forall n m r,
adam@324 353 r = m
adam@324 354 -> r = 0 * n + m.
adam@324 355 crush.
adam@324 356 Qed.
adam@324 357
adam@324 358 Hint Resolve zero_times.
adam@324 359
adam@324 360 Theorem EvalVar' : forall var n,
adam@324 361 var = n
adam@324 362 -> eval var Var n.
adam@324 363 crush.
adam@324 364 Qed.
adam@324 365
adam@324 366 Hint Resolve EvalVar'.
adam@324 367
adam@324 368 Theorem plus_0 : forall n r,
adam@324 369 r = n
adam@324 370 -> r = n + 0.
adam@324 371 crush.
adam@324 372 Qed.
adam@324 373
adam@324 374 Theorem times_1 : forall n, n = 1 * n.
adam@324 375 crush.
adam@324 376 Qed.
adam@324 377
adam@324 378 Hint Resolve plus_0 times_1.
adam@324 379
adam@324 380 Require Import Arith Ring.
adam@324 381
adam@324 382 Theorem combine : forall x k1 k2 n1 n2,
adam@324 383 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).
adam@324 384 intros; ring.
adam@324 385 Qed.
adam@324 386
adam@324 387 Hint Resolve combine.
adam@324 388
adam@324 389 Theorem linear : forall e, exists k, exists n,
adam@324 390 forall var, eval var e (k * var + n).
adam@324 391 induction e; crush; eauto.
adam@324 392 Qed.
adam@324 393
adam@324 394 Print linear.
adam@324 395 (* end thide *)
adam@324 396
adam@324 397
adam@324 398 (** * More on [auto] Hints *)
adam@324 399
adam@324 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.
adam@324 401
adam@324 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.
adam@324 403
adam@324 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. *)
adam@324 405
adam@324 406 Theorem bool_neq : true <> false.
adam@324 407 (* begin thide *)
adam@324 408 auto.
adam@324 409
adam@324 410 (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
adam@324 411
adam@324 412 Abort.
adam@324 413
adam@324 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. *)
adam@324 415
adam@324 416 Hint Extern 1 (_ <> _) => congruence.
adam@324 417
adam@324 418 Theorem bool_neq : true <> false.
adam@324 419 auto.
adam@324 420 Qed.
adam@324 421 (* end thide *)
adam@324 422
adam@324 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.
adam@324 424
adam@324 425 [Extern] hints may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
adam@324 426
adam@324 427 Section forall_and.
adam@324 428 Variable A : Set.
adam@324 429 Variables P Q : A -> Prop.
adam@324 430
adam@324 431 Hypothesis both : forall x, P x /\ Q x.
adam@324 432
adam@324 433 Theorem forall_and : forall z, P z.
adam@324 434 (* begin thide *)
adam@324 435 crush.
adam@324 436
adam@324 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. *)
adam@324 438
adam@324 439 Hint Extern 1 (P ?X) =>
adam@324 440 match goal with
adam@324 441 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@324 442 end.
adam@324 443
adam@324 444 auto.
adam@324 445 Qed.
adam@324 446 (* end thide *)
adam@324 447
adam@324 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]. *)
adam@324 449
adam@324 450 End forall_and.
adam@324 451
adam@324 452 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
adam@324 453
adam@324 454 [[
adam@324 455 Hint Extern 1 (?P ?X) =>
adam@324 456 match goal with
adam@324 457 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@324 458 end.
adam@324 459
adam@324 460 User error: Bound head variable
adam@324 461
adam@324 462 ]]
adam@324 463
adam@324 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].
adam@324 465
adam@324 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. *)
adam@324 467
adam@324 468
adam@324 469 (** * Rewrite Hints *)
adam@324 470
adam@324 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.
adam@324 472
adam@324 473 This example shows a direct use of [autorewrite]. *)
adam@324 474
adam@324 475 Section autorewrite.
adam@324 476 Variable A : Set.
adam@324 477 Variable f : A -> A.
adam@324 478
adam@324 479 Hypothesis f_f : forall x, f (f x) = f x.
adam@324 480
adam@324 481 Hint Rewrite f_f : my_db.
adam@324 482
adam@324 483 Lemma f_f_f : forall x, f (f (f x)) = f x.
adam@324 484 intros; autorewrite with my_db; reflexivity.
adam@324 485 Qed.
adam@324 486
adam@324 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: *)
adam@324 488
adam@324 489 Section garden_path.
adam@324 490 Variable g : A -> A.
adam@324 491 Hypothesis f_g : forall x, f x = g x.
adam@324 492 Hint Rewrite f_g : my_db.
adam@324 493
adam@324 494 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 495 intros; autorewrite with my_db.
adam@324 496 (** [[
adam@324 497 ============================
adam@324 498 g (g (g x)) = g x
adam@324 499 ]]
adam@324 500 *)
adam@324 501
adam@324 502 Abort.
adam@324 503
adam@324 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. *)
adam@324 505
adam@324 506 Reset garden_path.
adam@324 507
adam@324 508 (** [autorewrite] also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
adam@324 509
adam@324 510 Section garden_path.
adam@324 511 Variable P : A -> Prop.
adam@324 512 Variable g : A -> A.
adam@324 513 Hypothesis f_g : forall x, P x -> f x = g x.
adam@324 514 Hint Rewrite f_g : my_db.
adam@324 515
adam@324 516 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 517 intros; autorewrite with my_db.
adam@324 518 (** [[
adam@324 519
adam@324 520 ============================
adam@324 521 g (g (g x)) = g x
adam@324 522
adam@324 523 subgoal 2 is:
adam@324 524 P x
adam@324 525 subgoal 3 is:
adam@324 526 P (f x)
adam@324 527 subgoal 4 is:
adam@324 528 P (f x)
adam@324 529 ]]
adam@324 530 *)
adam@324 531
adam@324 532 Abort.
adam@324 533
adam@324 534 (** 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 535
adam@324 536 Reset garden_path.
adam@324 537
adam@324 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. *)
adam@324 539
adam@324 540 Section garden_path.
adam@324 541 Variable P : A -> Prop.
adam@324 542 Variable g : A -> A.
adam@324 543 Hypothesis f_g : forall x, P x -> f x = g x.
adam@324 544 (* begin thide *)
adam@324 545 Hint Rewrite f_g using assumption : my_db.
adam@324 546 (* end thide *)
adam@324 547
adam@324 548 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 549 (* begin thide *)
adam@324 550 intros; autorewrite with my_db; reflexivity.
adam@324 551 Qed.
adam@324 552 (* end thide *)
adam@324 553
adam@324 554 (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *)
adam@324 555
adam@324 556 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
adam@324 557 (* begin thide *)
adam@324 558 intros; autorewrite with my_db; reflexivity.
adam@324 559 (* end thide *)
adam@324 560 Qed.
adam@324 561 End garden_path.
adam@324 562
adam@324 563 (** remove printing * *)
adam@324 564
adam@324 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. *)
adam@324 566
adam@324 567 (** printing * $*$ *)
adam@324 568
adam@324 569 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
adam@324 570 -> f x = f (f (f y)).
adam@324 571 (* begin thide *)
adam@324 572 intros; autorewrite with my_db in *; assumption.
adam@324 573 (* end thide *)
adam@324 574 Qed.
adam@324 575
adam@324 576 End autorewrite.
adam@325 577
adam@325 578
adam@334 579 (* begin thide *)
adam@325 580 (** * Exercises *)
adam@325 581
adam@325 582 (** printing * $\cdot$ *)
adam@325 583
adam@325 584 (** %\begin{enumerate}%#<ol>#
adam@325 585
adam@325 586 %\item%#<li># I did a Google search for group theory and found #<a href="http://dogschool.tripod.com/housekeeping.html">#a page that proves some standard theorems#</a>#%\footnote{\url{http://dogschool.tripod.com/housekeeping.html}}%. This exercise is about proving all of the theorems on that page automatically.
adam@325 587
adam@325 588 For the purposes of this exercise, a group is a set [G], a binary function [f] over [G], an identity element [e] of [G], and a unary inverse function [i] for [G]. The following laws define correct choices of these parameters. We follow standard practice in algebra, where all variables that we mention are quantified universally implicitly at the start of a fact. We write infix [*] for [f], and you can set up the same sort of notation in your code with a command like [Infix "*" := f.].
adam@325 589
adam@325 590 %\begin{itemize}%#<ul>#
adam@325 591 %\item%#<li># %\textbf{%#<b>#Associativity#</b>#%}%: [(a * b) * c = a * (b * c)]#</li>#
adam@325 592 %\item%#<li># %\textbf{%#<b>#Right Identity#</b>#%}%: [a * e = a]#</li>#
adam@325 593 %\item%#<li># %\textbf{%#<b>#Right Inverse#</b>#%}%: [a * i a = e]#</li>#
adam@325 594 #</ul> </li>#%\end{itemize}%
adam@325 595
adam@325 596 The task in this exercise is to prove each of the following theorems for all groups, where we define a group exactly as above. There is a wrinkle: every theorem or lemma must be proved by either a single call to [crush] or a single call to [eauto]! It is allowed to pass numeric arguments to [eauto], where appropriate. Recall that a numeric argument sets the depth of proof search, where 5 is the default. Lower values can speed up execution when a proof exists within the bound. Higher values may be necessary to find more involved proofs.
adam@325 597
adam@325 598 %\begin{itemize}%#<ul>#
adam@325 599 %\item%#<li># %\textbf{%#<b>#Characterizing Identity#</b>#%}%: [a * a = a -> a = e]#</li>#
adam@325 600 %\item%#<li># %\textbf{%#<b>#Left Inverse#</b>#%}%: [i a * a = e]#</li>#
adam@325 601 %\item%#<li># %\textbf{%#<b>#Left Identity#</b>#%}%: [e * a = a]#</li>#
adam@325 602 %\item%#<li># %\textbf{%#<b>#Uniqueness of Left Identity#</b>#%}%: [p * a = a -> p = e]#</li>#
adam@325 603 %\item%#<li># %\textbf{%#<b>#Uniqueness of Right Inverse#</b>#%}%: [a * b = e -> b = i a]#</li>#
adam@325 604 %\item%#<li># %\textbf{%#<b>#Uniqueness of Left Inverse#</b>#%}%: [a * b = e -> a = i b]#</li>#
adam@325 605 %\item%#<li># %\textbf{%#<b>#Right Cancellation#</b>#%}%: [a * x = b * x -> a = b]#</li>#
adam@325 606 %\item%#<li># %\textbf{%#<b>#Left Cancellation#</b>#%}%: [x * a = x * b -> a = b]#</li>#
adam@325 607 %\item%#<li># %\textbf{%#<b>#Distributivity of Inverse#</b>#%}%: [i (a * b) = i b * i a]#</li>#
adam@327 608 %\item%#<li># %\textbf{%#<b>#Double Inverse#</b>#%}%: [i (][i a) = a]#</li>#
adam@325 609 %\item%#<li># %\textbf{%#<b>#Identity Inverse#</b>#%}%: [i e = e]#</li>#
adam@325 610 #</ul> </li>#%\end{itemize}%
adam@325 611
adam@325 612 One more use of tactics is allowed in this problem. The following lemma captures one common pattern of reasoning in algebra proofs: *)
adam@325 613
adam@325 614 (* begin hide *)
adam@325 615 Variable G : Set.
adam@325 616 Variable f : G -> G -> G.
adam@325 617 Infix "*" := f.
adam@325 618 (* end hide *)
adam@325 619
adam@325 620 Lemma mult_both : forall a b c d1 d2,
adam@325 621 a * c = d1
adam@325 622 -> b * c = d2
adam@325 623 -> a = b
adam@325 624 -> d1 = d2.
adam@325 625 crush.
adam@325 626 Qed.
adam@325 627
adam@325 628 (** That is, we know some equality [a = b], which is the third hypothesis above. We derive a further equality by multiplying both sides by [c], to yield [a * c = b * c]. Next, we do algebraic simplification on both sides of this new equality, represented by the first two hypotheses above. The final result is a new theorem of algebra.
adam@325 629
adam@325 630 The next chapter introduces more details of programming in Ltac, but here is a quick teaser that will be useful in this problem. Include the following hint command before you start proving the main theorems of this exercise: *)
adam@325 631
adam@325 632 Hint Extern 100 (_ = _) =>
adam@325 633 match goal with
adam@325 634 | [ _ : True |- _ ] => fail 1
adam@325 635 | _ => assert True by constructor; eapply mult_both
adam@325 636 end.
adam@325 637
adam@325 638 (** This hint has the effect of applying [mult_both] %\emph{%#<i>#at most once#</i>#%}% during a proof. After the next chapter, it should be clear why the hint has that effect, but for now treat it as a useful black box. Simply using [Hint Resolve mult_both] would increase proof search time unacceptably, because there are just too many ways to use [mult_both] repeatedly within a proof.
adam@325 639
adam@325 640 The order of the theorems above is itself a meta-level hint, since I found that order to work well for allowing the use of earlier theorems as hints in the proofs of later theorems.
adam@325 641
adam@325 642 The key to this problem is coming up with further lemmas like [mult_both] that formalize common patterns of reasoning in algebraic proofs. These lemmas need to be more than sound: they must also fit well with the way that [eauto] does proof search. For instance, if we had given [mult_both] a traditional statement, we probably would have avoided %``%#"#pointless#"#%''% equalities like [a = b], which could be avoided simply by replacing all occurrences of [b] with [a]. However, the resulting theorem would not work as well with automated proof search! Every additional hint you come up with should be registered with [Hint Resolve], so that the lemma statement needs to be in a form that [eauto] understands %``%#"#natively.#"#%''%
adam@325 643
adam@325 644 I recommend testing a few simple rules corresponding to common steps in algebraic proofs. You can apply them manually with any tactics you like (e.g., [apply] or [eapply]) to figure out what approaches work, and then switch to [eauto] once you have the full set of hints.
adam@325 645
adam@325 646 I also proved a few hint lemmas tailored to particular theorems, but which do not give common algebraic simplification rules. You will probably want to use some, too, in cases where [eauto] does not find a proof within a reasonable amount of time. In total, beside the main theorems to be proved, my sample solution includes 6 lemmas, with a mix of the two kinds of lemmas. You may use more in your solution, but I suggest trying to minimize the number.
adam@325 647
adam@325 648 #</ol>#%\end{enumerate}% *)
adam@334 649 (* end thide *)