annotate src/LogicProg.v @ 432:17d01e51256c

Pass through Reflection, to incorporate new coqdoc features
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 14:57:38 -0400
parents 610568369aee
children 8077352044b2
rev   line source
adam@372 1 (* Copyright (c) 2011-2012, 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@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@430 80 Definition er := @eq_refl.
adam@430 81 (* end hide *)
adam@430 82
adam@372 83 Print four_plus_three.
adam@372 84 (** %\vspace{-.15in}%[[
adam@372 85 four_plus_three = eq_refl
adam@372 86 ]]
adam@372 87
adam@372 88 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 89 *)
adam@372 90
adam@324 91 Example four_plus_three' : plusR 4 3 7.
adam@324 92 (* begin thide *)
adam@372 93 (** %\vspace{-.2in}%[[
adam@372 94 apply PlusO.
adam@372 95 ]]
adam@372 96 %\vspace{-.2in}%
adam@372 97 <<
adam@372 98 Error: Impossible to unify "plusR 0 ?24 ?24" with "plusR 4 3 7".
adam@372 99 >> *)
adam@372 100 apply PlusS.
adam@372 101 (** %\vspace{-.2in}%[[
adam@372 102 apply PlusO.
adam@372 103 ]]
adam@372 104 %\vspace{-.2in}%
adam@372 105 <<
adam@372 106 Error: Impossible to unify "plusR 0 ?25 ?25" with "plusR 3 3 6".
adam@372 107 >> *)
adam@372 108 apply PlusS.
adam@372 109 (** %\vspace{-.2in}%[[
adam@372 110 apply PlusO.
adam@372 111 ]]
adam@372 112 %\vspace{-.2in}%
adam@372 113 <<
adam@372 114 Error: Impossible to unify "plusR 0 ?26 ?26" with "plusR 2 3 5".
adam@372 115 >> *)
adam@372 116 apply PlusS.
adam@372 117 (** %\vspace{-.2in}%[[
adam@372 118 apply PlusO.
adam@372 119 ]]
adam@372 120 %\vspace{-.2in}%
adam@372 121 <<
adam@372 122 Error: Impossible to unify "plusR 0 ?27 ?27" with "plusR 1 3 4".
adam@372 123 >> *)
adam@372 124 apply PlusS.
adam@372 125 apply PlusO.
adam@372 126
adam@372 127 (** 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] does exactly that, since above we used [Hint Constructors] to register the two candidate proof steps as hints. *)
adam@372 128
adam@372 129 Restart.
adam@324 130 auto.
adam@324 131 Qed.
adam@324 132 (* end thide *)
adam@324 133
adam@372 134 Print four_plus_three'.
adam@372 135 (** %\vspace{-.15in}%[[
adam@372 136 four_plus_three' = PlusS (PlusS (PlusS (PlusS (PlusO 3))))
adam@372 137 ]]
adam@372 138 *)
adam@372 139
adam@372 140 (** Let us try the same approach on a slightly more complex goal. *)
adam@372 141
adam@372 142 Example five_plus_three : plusR 5 3 8.
adam@324 143 (* begin thide *)
adam@372 144 auto.
adam@372 145
adam@372 146 (** 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 147
adam@324 148 auto 6.
adam@372 149
adam@410 150 (** 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.) *)
adam@372 151
adam@324 152 Restart.
adam@324 153 info auto 6.
adam@372 154 (** %\vspace{-.15in}%[[
adam@372 155 == apply PlusS; apply PlusS; apply PlusS; apply PlusS;
adam@372 156 apply PlusS; apply PlusO.
adam@372 157 ]]
adam@372 158 *)
adam@324 159 Qed.
adam@324 160 (* end thide *)
adam@324 161
adam@410 162 (** 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 163
adam@324 164 Example seven_minus_three : exists x, x + 3 = 7.
adam@324 165 (* begin thide *)
adam@372 166 (** 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 167
adam@372 168 apply ex_intro with 0.
adam@372 169 (** %\vspace{-.2in}%[[
adam@372 170 reflexivity.
adam@372 171 ]]
adam@372 172 %\vspace{-.2in}%
adam@372 173 <<
adam@372 174 Error: Impossible to unify "7" with "0 + 3".
adam@372 175 >>
adam@372 176
adam@398 177 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 178 *)
adam@372 179
adam@372 180 Restart.
adam@372 181 apply ex_intro with 4.
adam@372 182 reflexivity.
adam@372 183 Qed.
adam@324 184 (* end thide *)
adam@324 185
adam@372 186 (** 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 187
adam@372 188 Next we demonstrate unification, which will be easier when we switch to the relational formulation of addition. *)
adam@372 189
adam@324 190 Example seven_minus_three' : exists x, plusR x 3 7.
adam@324 191 (* begin thide *)
adam@410 192 (** 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] instead, which proceeds with placeholder%\index{unification variable}% _unification variables_ standing in for those parameters we wish to postpone guessing. *)
adam@372 193
adam@372 194 eapply ex_intro.
adam@372 195 (** [[
adam@372 196 1 subgoal
adam@372 197
adam@372 198 ============================
adam@372 199 plusR ?70 3 7
adam@372 200 ]]
adam@372 201
adam@372 202 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 203
adam@372 204 apply PlusS.
adam@372 205 (** [[
adam@372 206 ============================
adam@372 207 plusR ?71 3 6
adam@372 208 ]]
adam@372 209 *)
adam@372 210 apply PlusS. apply PlusS. apply PlusS.
adam@372 211 (** [[
adam@372 212 ============================
adam@372 213 plusR ?74 3 3
adam@372 214 ]]
adam@372 215 *)
adam@372 216 apply PlusO.
adam@372 217
adam@372 218 (** 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 219
adam@372 220 Restart.
adam@324 221 info eauto 6.
adam@372 222 (** %\vspace{-.15in}%[[
adam@372 223 == eapply ex_intro; apply PlusS; apply PlusS;
adam@372 224 apply PlusS; apply PlusS; apply PlusO.
adam@372 225 ]]
adam@372 226 *)
adam@324 227 Qed.
adam@324 228 (* end thide *)
adam@324 229
adam@372 230 (** 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 231
adam@324 232 Example seven_minus_four' : exists x, plusR 4 x 7.
adam@324 233 (* begin thide *)
adam@372 234 eauto 6.
adam@324 235 Qed.
adam@324 236 (* end thide *)
adam@324 237
adam@372 238 (** 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 239
adam@324 240 (* begin thide *)
adam@324 241 SearchRewrite (O + _).
adam@372 242 (** %\vspace{-.15in}%[[
adam@372 243 plus_O_n: forall n : nat, 0 + n = n
adam@372 244 ]]
adam@372 245
adam@372 246 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 247
adam@324 248 Hint Immediate plus_O_n.
adam@324 249
adam@372 250 (** The counterpart to [PlusS] we will prove ourselves. *)
adam@372 251
adam@324 252 Lemma plusS : forall n m r,
adam@324 253 n + m = r
adam@324 254 -> S n + m = S r.
adam@324 255 crush.
adam@324 256 Qed.
adam@324 257
adam@372 258 (** 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 259
adam@324 260 Hint Resolve plusS.
adam@324 261 (* end thide *)
adam@324 262
adam@372 263 (** Now that we have registered the proper hints, we can replicate our previous examples with the normal, functional addition [plus]. *)
adam@372 264
adam@372 265 Example seven_minus_three'' : exists x, x + 3 = 7.
adam@324 266 (* begin thide *)
adam@372 267 eauto 6.
adam@324 268 Qed.
adam@324 269 (* end thide *)
adam@324 270
adam@324 271 Example seven_minus_four : exists x, 4 + x = 7.
adam@324 272 (* begin thide *)
adam@372 273 eauto 6.
adam@324 274 Qed.
adam@324 275 (* end thide *)
adam@324 276
adam@372 277 (** 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 278
adam@372 279 Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
adam@324 280 (* begin thide *)
adam@324 281 eauto 6.
adam@324 282 Abort.
adam@324 283 (* end thide *)
adam@324 284
adam@372 285 (** A further lemma will be helpful. *)
adam@372 286
adam@324 287 (* begin thide *)
adam@324 288 Lemma plusO : forall n m,
adam@324 289 n = m
adam@324 290 -> n + 0 = m.
adam@324 291 crush.
adam@324 292 Qed.
adam@324 293
adam@324 294 Hint Resolve plusO.
adam@324 295 (* end thide *)
adam@324 296
adam@372 297 (** 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 298
adam@324 299 Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
adam@324 300 (* begin thide *)
adam@372 301 eauto 7.
adam@324 302 Qed.
adam@324 303 (* end thide *)
adam@324 304
adam@372 305 (** 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 306
adam@324 307 Check eq_trans.
adam@372 308 (** %\vspace{-.15in}%[[
adam@372 309 eq_trans
adam@372 310 : forall (A : Type) (x y z : A), x = y -> y = z -> x = z
adam@372 311 ]]
adam@372 312 *)
adam@372 313
adam@372 314 (** Hints are scoped over sections, so let us enter a section to contain the effects of an unfortunate hint choice. *)
adam@324 315
adam@324 316 Section slow.
adam@324 317 Hint Resolve eq_trans.
adam@324 318
adam@372 319 (** 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 320
adam@324 321 Example three_minus_four_zero : exists x, 1 + x = 0.
adam@324 322 Time eauto 1.
adam@372 323 (** %\vspace{-.15in}%
adam@372 324 <<
adam@372 325 Finished transaction in 0. secs (0.u,0.s)
adam@372 326 >>
adam@372 327 *)
adam@372 328
adam@324 329 Time eauto 2.
adam@372 330 (** %\vspace{-.15in}%
adam@372 331 <<
adam@372 332 Finished transaction in 0. secs (0.u,0.s)
adam@372 333 >>
adam@372 334 *)
adam@372 335
adam@324 336 Time eauto 3.
adam@372 337 (** %\vspace{-.15in}%
adam@372 338 <<
adam@372 339 Finished transaction in 0. secs (0.008u,0.s)
adam@372 340 >>
adam@372 341 *)
adam@372 342
adam@324 343 Time eauto 4.
adam@372 344 (** %\vspace{-.15in}%
adam@372 345 <<
adam@372 346 Finished transaction in 0. secs (0.068005u,0.004s)
adam@372 347 >>
adam@372 348 *)
adam@372 349
adam@324 350 Time eauto 5.
adam@372 351 (** %\vspace{-.15in}%
adam@372 352 <<
adam@372 353 Finished transaction in 2. secs (1.92012u,0.044003s)
adam@372 354 >>
adam@372 355 *)
adam@372 356
adam@372 357 (** 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 358
adam@324 359 debug eauto 3.
adam@372 360 (** [[
adam@372 361 1 depth=3
adam@372 362 1.1 depth=2 eapply ex_intro
adam@372 363 1.1.1 depth=1 apply plusO
adam@372 364 1.1.1.1 depth=0 eapply eq_trans
adam@372 365 1.1.2 depth=1 eapply eq_trans
adam@372 366 1.1.2.1 depth=1 apply plus_n_O
adam@372 367 1.1.2.1.1 depth=0 apply plusO
adam@372 368 1.1.2.1.2 depth=0 eapply eq_trans
adam@372 369 1.1.2.2 depth=1 apply @eq_refl
adam@372 370 1.1.2.2.1 depth=0 apply plusO
adam@372 371 1.1.2.2.2 depth=0 eapply eq_trans
adam@372 372 1.1.2.3 depth=1 apply eq_add_S ; trivial
adam@372 373 1.1.2.3.1 depth=0 apply plusO
adam@372 374 1.1.2.3.2 depth=0 eapply eq_trans
adam@372 375 1.1.2.4 depth=1 apply eq_sym ; trivial
adam@372 376 1.1.2.4.1 depth=0 eapply eq_trans
adam@372 377 1.1.2.5 depth=0 apply plusO
adam@372 378 1.1.2.6 depth=0 apply plusS
adam@372 379 1.1.2.7 depth=0 apply f_equal (A:=nat)
adam@372 380 1.1.2.8 depth=0 apply f_equal2 (A1:=nat) (A2:=nat)
adam@372 381 1.1.2.9 depth=0 eapply eq_trans
adam@372 382 ]]
adam@372 383 *)
adam@324 384 Abort.
adam@324 385 End slow.
adam@324 386
adam@410 387 (** 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 segragate hints into different groups that may be called on as needed. Here we put [eq_trans] into the database [slow]. *)
adam@372 388
adam@324 389 (* begin thide *)
adam@324 390 Hint Resolve eq_trans : slow.
adam@324 391 (* end thide *)
adam@324 392
adam@324 393 Example three_minus_four_zero : exists x, 1 + x = 0.
adam@324 394 (* begin thide *)
adam@372 395 Time eauto.
adam@372 396 (** %\vspace{-.15in}%
adam@372 397 <<
adam@372 398 Finished transaction in 0. secs (0.004u,0.s)
adam@372 399 >>
adam@372 400
adam@372 401 This [eauto] fails to prove the goal, but it least it takes substantially less than the 2 seconds required above! *)
adam@372 402
adam@324 403 Abort.
adam@324 404 (* end thide *)
adam@324 405
adam@372 406 (** One simple example from before runs in the same amount of time, avoiding pollution by transivity. *)
adam@372 407
adam@324 408 Example seven_minus_three_again : exists x, x + 3 = 7.
adam@324 409 (* begin thide *)
adam@372 410 Time eauto 6.
adam@372 411 (** %\vspace{-.15in}%
adam@372 412 <<
adam@372 413 Finished transaction in 0. secs (0.004001u,0.s)
adam@372 414 >>
adam@372 415 %\vspace{-.2in}% *)
adam@372 416
adam@324 417 Qed.
adam@324 418 (* end thide *)
adam@324 419
adam@398 420 (** When we _do_ need transitivity, we ask for it explicitly. *)
adam@372 421
adam@324 422 Example needs_trans : forall x y, 1 + x = y
adam@324 423 -> y = 2
adam@324 424 -> exists z, z + x = 3.
adam@324 425 (* begin thide *)
adam@324 426 info eauto with slow.
adam@372 427 (** %\vspace{-.2in}%[[
adam@372 428 == intro x; intro y; intro H; intro H0; simple eapply ex_intro;
adam@372 429 apply plusS; simple eapply eq_trans.
adam@372 430 exact H.
adam@372 431
adam@372 432 exact H0.
adam@372 433 ]]
adam@372 434 *)
adam@324 435 Qed.
adam@324 436 (* end thide *)
adam@324 437
adam@372 438 (** 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 439
adam@324 440
adam@324 441 (** * Searching for Underconstrained Values *)
adam@324 442
adam@373 443 (** Recall the definition of the list length function. *)
adam@373 444
adam@324 445 Print length.
adam@373 446 (** %\vspace{-.15in}%[[
adam@373 447 length =
adam@373 448 fun A : Type =>
adam@373 449 fix length (l : list A) : nat :=
adam@373 450 match l with
adam@373 451 | nil => 0
adam@373 452 | _ :: l' => S (length l')
adam@373 453 end
adam@373 454 ]]
adam@373 455
adam@373 456 This function is easy to reason about in the forward direction, computing output from input. *)
adam@324 457
adam@324 458 Example length_1_2 : length (1 :: 2 :: nil) = 2.
adam@324 459 auto.
adam@324 460 Qed.
adam@324 461
adam@324 462 Print length_1_2.
adam@373 463 (** %\vspace{-.15in}%[[
adam@373 464 length_1_2 = eq_refl
adam@373 465 ]]
adam@373 466
adam@373 467 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 468
adam@324 469 (* begin thide *)
adam@324 470 Theorem length_O : forall A, length (nil (A := A)) = O.
adam@324 471 crush.
adam@324 472 Qed.
adam@324 473
adam@324 474 Theorem length_S : forall A (h : A) t n,
adam@324 475 length t = n
adam@324 476 -> length (h :: t) = S n.
adam@324 477 crush.
adam@324 478 Qed.
adam@324 479
adam@324 480 Hint Resolve length_O length_S.
adam@324 481 (* end thide *)
adam@324 482
adam@373 483 (** Let us apply these hints to prove that a [list nat] of length 2 exists. *)
adam@373 484
adam@324 485 Example length_is_2 : exists ls : list nat, length ls = 2.
adam@324 486 (* begin thide *)
adam@324 487 eauto.
adam@373 488 (** <<
adam@373 489 No more subgoals but non-instantiated existential variables:
adam@373 490 Existential 1 = ?20249 : [ |- nat]
adam@373 491 Existential 2 = ?20252 : [ |- nat]
adam@373 492 >>
adam@373 493
adam@398 494 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 495
adam@373 496 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 497
adam@324 498 Show Proof.
adam@373 499 (** <<
adam@373 500 Proof: ex_intro (fun ls : list nat => length ls = 2)
adam@373 501 (?20249 :: ?20252 :: nil)
adam@373 502 (length_S ?20249 (?20252 :: nil)
adam@373 503 (length_S ?20252 nil (length_O nat)))
adam@373 504 >>
adam@373 505 %\vspace{-.2in}% *)
adam@373 506
adam@324 507 Abort.
adam@324 508 (* end thide *)
adam@324 509
adam@373 510 (** 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 511
adam@430 512 (* begin hide *)
adam@430 513 Definition Forall_c := (@Forall_nil, @Forall_cons).
adam@430 514 (* end hide *)
adam@430 515
adam@324 516 Print Forall.
adam@373 517 (** %\vspace{-.15in}%[[
adam@373 518 Inductive Forall (A : Type) (P : A -> Prop) : list A -> Prop :=
adam@373 519 Forall_nil : Forall P nil
adam@373 520 | Forall_cons : forall (x : A) (l : list A),
adam@373 521 P x -> Forall P l -> Forall P (x :: l)
adam@373 522 ]]
adam@373 523 *)
adam@324 524
adam@324 525 Example length_is_2 : exists ls : list nat, length ls = 2
adam@324 526 /\ Forall (fun n => n >= 1) ls.
adam@324 527 (* begin thide *)
adam@324 528 eauto 9.
adam@324 529 Qed.
adam@324 530 (* end thide *)
adam@324 531
adam@373 532 (** We can see which list [eauto] found by printing the proof term. *)
adam@373 533
adam@430 534 (* begin hide *)
adam@430 535 Definition conj' := (conj, le_n).
adam@430 536 (* end hide *)
adam@430 537
adam@373 538 Print length_is_2.
adam@373 539 (** %\vspace{-.15in}%[[
adam@373 540 length_is_2 =
adam@373 541 ex_intro
adam@373 542 (fun ls : list nat => length ls = 2 /\ Forall (fun n : nat => n >= 1) ls)
adam@373 543 (1 :: 1 :: nil)
adam@373 544 (conj (length_S 1 (1 :: nil) (length_S 1 nil (length_O nat)))
adam@373 545 (Forall_cons 1 (le_n 1)
adam@373 546 (Forall_cons 1 (le_n 1) (Forall_nil (fun n : nat => n >= 1)))))
adam@373 547 ]]
adam@373 548 *)
adam@373 549
adam@373 550 (** Let us try one more, fancier example. First, we use a standard high-order function to define a function for summing all data elements of a list. *)
adam@373 551
adam@324 552 Definition sum := fold_right plus O.
adam@324 553
adam@373 554 (** Another basic lemma will be helpful to guide proof search. *)
adam@373 555
adam@324 556 (* begin thide *)
adam@324 557 Lemma plusO' : forall n m,
adam@324 558 n = m
adam@324 559 -> 0 + n = m.
adam@324 560 crush.
adam@324 561 Qed.
adam@324 562
adam@324 563 Hint Resolve plusO'.
adam@324 564
adam@373 565 (** 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 566
adam@324 567 Hint Extern 1 (sum _ = _) => simpl.
adam@324 568 (* end thide *)
adam@324 569
adam@373 570 (** Now we can find a length-2 list whose sum is 0. *)
adam@373 571
adam@324 572 Example length_and_sum : exists ls : list nat, length ls = 2
adam@324 573 /\ sum ls = O.
adam@324 574 (* begin thide *)
adam@324 575 eauto 7.
adam@324 576 Qed.
adam@324 577 (* end thide *)
adam@324 578
adam@373 579 (* begin hide *)
adam@324 580 Print length_and_sum.
adam@373 581 (* end hide *)
adam@373 582
adam@373 583 (** 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 584
adam@324 585 Example length_and_sum' : exists ls : list nat, length ls = 5
adam@324 586 /\ sum ls = 42.
adam@324 587 (* begin thide *)
adam@324 588 eauto 15.
adam@324 589 Qed.
adam@324 590 (* end thide *)
adam@324 591
adam@373 592 (* begin hide *)
adam@324 593 Print length_and_sum'.
adam@373 594 (* end hide *)
adam@373 595
adam@373 596 (** 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 597
adam@324 598 Example length_and_sum'' : exists ls : list nat, length ls = 2
adam@324 599 /\ sum ls = 3
adam@324 600 /\ Forall (fun n => n <> 0) ls.
adam@324 601 (* begin thide *)
adam@324 602 eauto 11.
adam@324 603 Qed.
adam@324 604 (* end thide *)
adam@324 605
adam@373 606 (* begin hide *)
adam@324 607 Print length_and_sum''.
adam@373 608 (* end hide *)
adam@373 609
adam@398 610 (** We could continue through exercises of this kind, but even more interesting than finding lists automatically is finding _programs_ automatically. *)
adam@324 611
adam@324 612
adam@324 613 (** * Synthesizing Programs *)
adam@324 614
adam@374 615 (** 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 616
adam@324 617 Inductive exp : Set :=
adam@324 618 | Const : nat -> exp
adam@324 619 | Var : exp
adam@324 620 | Plus : exp -> exp -> exp.
adam@324 621
adam@374 622 (** An inductive relation specifies the semantics of an expression, relating a variable value and an expression to the expression value. *)
adam@374 623
adam@324 624 Inductive eval (var : nat) : exp -> nat -> Prop :=
adam@324 625 | EvalConst : forall n, eval var (Const n) n
adam@324 626 | EvalVar : eval var Var var
adam@324 627 | EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
adam@324 628 -> eval var e2 n2
adam@324 629 -> eval var (Plus e1 e2) (n1 + n2).
adam@324 630
adam@324 631 (* begin thide *)
adam@324 632 Hint Constructors eval.
adam@324 633 (* end thide *)
adam@324 634
adam@374 635 (** We can use [auto] to execute the semantics for specific expressions. *)
adam@374 636
adam@324 637 Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
adam@324 638 (* begin thide *)
adam@324 639 auto.
adam@324 640 Qed.
adam@324 641 (* end thide *)
adam@324 642
adam@374 643 (** Unfortunately, just the constructors of [eval] are not enough to prove theorems like the following, which depends on an arithmetic identity. *)
adam@374 644
adam@324 645 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
adam@324 646 (* begin thide *)
adam@324 647 eauto.
adam@324 648 Abort.
adam@324 649 (* end thide *)
adam@324 650
adam@374 651 (** To help prove [eval1'], we prove an alternate version of [EvalPlus] that inserts an extra equality premise. *)
adam@374 652
adam@324 653 (* begin thide *)
adam@324 654 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1
adam@324 655 -> eval var e2 n2
adam@324 656 -> n1 + n2 = n
adam@324 657 -> eval var (Plus e1 e2) n.
adam@324 658 crush.
adam@324 659 Qed.
adam@324 660
adam@324 661 Hint Resolve EvalPlus'.
adam@324 662
adam@374 663 (** 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 664
adam@324 665 Hint Extern 1 (_ = _) => abstract omega.
adam@324 666 (* end thide *)
adam@324 667
adam@374 668 (** Now we can return to [eval1'] and prove it automatically. *)
adam@374 669
adam@324 670 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
adam@324 671 (* begin thide *)
adam@324 672 eauto.
adam@324 673 Qed.
adam@324 674 (* end thide *)
adam@324 675
adam@430 676 (* begin hide *)
adam@430 677 Definition e1s := eval1'_subproof.
adam@430 678 (* end hide *)
adam@430 679
adam@324 680 Print eval1'.
adam@374 681 (** %\vspace{-.15in}%[[
adam@374 682 eval1' =
adam@374 683 fun var : nat =>
adam@374 684 EvalPlus' (EvalVar var) (EvalPlus (EvalConst var 8) (EvalVar var))
adam@374 685 (eval1'_subproof var)
adam@374 686 : forall var : nat,
adam@374 687 eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8)
adam@374 688 ]]
adam@374 689 *)
adam@374 690
adam@374 691 (** The lemma [eval1'_subproof] was generated by [abstract omega].
adam@374 692
adam@374 693 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 694
adam@324 695 Example synthesize1 : exists e, forall var, eval var e (var + 7).
adam@324 696 (* begin thide *)
adam@324 697 eauto.
adam@324 698 Qed.
adam@324 699 (* end thide *)
adam@324 700
adam@324 701 Print synthesize1.
adam@374 702 (** %\vspace{-.15in}%[[
adam@374 703 synthesize1 =
adam@374 704 ex_intro (fun e : exp => forall var : nat, eval var e (var + 7))
adam@374 705 (Plus Var (Const 7))
adam@374 706 (fun var : nat => EvalPlus (EvalVar var) (EvalConst var 7))
adam@374 707 ]]
adam@374 708 *)
adam@374 709
adam@374 710 (** Here are two more examples showing off our program synthesis abilities. *)
adam@324 711
adam@324 712 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
adam@324 713 (* begin thide *)
adam@324 714 eauto.
adam@324 715 Qed.
adam@324 716 (* end thide *)
adam@324 717
adam@374 718 (* begin hide *)
adam@324 719 Print synthesize2.
adam@374 720 (* end hide *)
adam@324 721
adam@324 722 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
adam@324 723 (* begin thide *)
adam@324 724 eauto.
adam@324 725 Qed.
adam@324 726 (* end thide *)
adam@324 727
adam@374 728 (* begin hide *)
adam@324 729 Print synthesize3.
adam@374 730 (* end hide *)
adam@374 731
adam@374 732 (** 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 733
adam@374 734 We prove a series of lemmas and add them as hints. We have alternate [eval] constructor lemmas and some facts about arithmetic. *)
adam@324 735
adam@324 736 (* begin thide *)
adam@324 737 Theorem EvalConst' : forall var n m, n = m
adam@324 738 -> eval var (Const n) m.
adam@324 739 crush.
adam@324 740 Qed.
adam@324 741
adam@324 742 Hint Resolve EvalConst'.
adam@324 743
adam@324 744 Theorem zero_times : forall n m r,
adam@324 745 r = m
adam@324 746 -> r = 0 * n + m.
adam@324 747 crush.
adam@324 748 Qed.
adam@324 749
adam@324 750 Hint Resolve zero_times.
adam@324 751
adam@324 752 Theorem EvalVar' : forall var n,
adam@324 753 var = n
adam@324 754 -> eval var Var n.
adam@324 755 crush.
adam@324 756 Qed.
adam@324 757
adam@324 758 Hint Resolve EvalVar'.
adam@324 759
adam@324 760 Theorem plus_0 : forall n r,
adam@324 761 r = n
adam@324 762 -> r = n + 0.
adam@324 763 crush.
adam@324 764 Qed.
adam@324 765
adam@324 766 Theorem times_1 : forall n, n = 1 * n.
adam@324 767 crush.
adam@324 768 Qed.
adam@324 769
adam@324 770 Hint Resolve plus_0 times_1.
adam@324 771
adam@398 772 (** 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 ring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *)
adam@374 773
adam@324 774 Require Import Arith Ring.
adam@324 775
adam@324 776 Theorem combine : forall x k1 k2 n1 n2,
adam@324 777 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).
adam@324 778 intros; ring.
adam@324 779 Qed.
adam@324 780
adam@324 781 Hint Resolve combine.
adam@324 782
adam@374 783 (** 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 784
adam@324 785 Theorem linear : forall e, exists k, exists n,
adam@324 786 forall var, eval var e (k * var + n).
adam@324 787 induction e; crush; eauto.
adam@324 788 Qed.
adam@324 789
adam@374 790 (* begin hide *)
adam@324 791 Print linear.
adam@374 792 (* end hide *)
adam@324 793 (* end thide *)
adam@324 794
adam@374 795 (** 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 796
adam@324 797
adam@324 798 (** * More on [auto] Hints *)
adam@324 799
adam@430 800 (** 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 801
adam@375 802 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]. 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 803
adam@375 804 All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern]. A few more examples of [Hint Extern] should illustrate more of the possibilities. *)
adam@324 805
adam@324 806 Theorem bool_neq : true <> false.
adam@324 807 (* begin thide *)
adam@324 808 auto.
adam@324 809
adam@410 810 (** A call to [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
adam@324 811
adam@324 812 Abort.
adam@324 813
adam@430 814 (* begin hide *)
adam@430 815 Definition boool := bool.
adam@430 816 (* end hide *)
adam@430 817
adam@375 818 (** 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 819
adam@324 820 Hint Extern 1 (_ <> _) => congruence.
adam@324 821
adam@324 822 Theorem bool_neq : true <> false.
adam@324 823 auto.
adam@324 824 Qed.
adam@324 825 (* end thide *)
adam@324 826
adam@410 827 (** A [Hint Extern] may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
adam@324 828
adam@324 829 Section forall_and.
adam@324 830 Variable A : Set.
adam@324 831 Variables P Q : A -> Prop.
adam@324 832
adam@324 833 Hypothesis both : forall x, P x /\ Q x.
adam@324 834
adam@324 835 Theorem forall_and : forall z, P z.
adam@324 836 (* begin thide *)
adam@324 837 crush.
adam@324 838
adam@375 839 (** 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 840
adam@324 841 Hint Extern 1 (P ?X) =>
adam@324 842 match goal with
adam@324 843 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@324 844 end.
adam@324 845
adam@324 846 auto.
adam@324 847 Qed.
adam@324 848 (* end thide *)
adam@324 849
adam@375 850 (** 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 [R] from a proof of [R /\ S]. *)
adam@324 851
adam@324 852 End forall_and.
adam@324 853
adam@430 854 (* begin hide *)
adam@430 855 Definition noot := (not, @eq).
adam@430 856 (* end hide *)
adam@430 857
adam@324 858 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
adam@324 859 [[
adam@430 860 Hint Extern 1 (?P ?X) =>
adam@430 861 match goal with
adam@430 862 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@430 863 end.
adam@375 864 ]]
adam@375 865 <<
adam@375 866 User error: Bound head variable
adam@375 867 >>
adam@324 868
adam@410 869 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 870
adam@375 871 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 872
adam@375 873 Hint Extern 1 =>
adam@375 874 match goal with
adam@375 875 | [ H : forall x, ?P x /\ _ |- ?P ?X ] => apply (proj1 (H X))
adam@375 876 end.
adam@375 877
adam@398 878 (** 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 879
adam@324 880
adam@324 881 (** * Rewrite Hints *)
adam@324 882
adam@375 883 (** 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 884
adam@375 885 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 886
adam@324 887 Section autorewrite.
adam@324 888 Variable A : Set.
adam@324 889 Variable f : A -> A.
adam@324 890
adam@324 891 Hypothesis f_f : forall x, f (f x) = f x.
adam@324 892
adam@375 893 Hint Rewrite f_f.
adam@324 894
adam@324 895 Lemma f_f_f : forall x, f (f (f x)) = f x.
adam@375 896 intros; autorewrite with core; reflexivity.
adam@324 897 Qed.
adam@324 898
adam@430 899 (** 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 900
adam@324 901 Section garden_path.
adam@324 902 Variable g : A -> A.
adam@324 903 Hypothesis f_g : forall x, f x = g x.
adam@375 904 Hint Rewrite f_g.
adam@324 905
adam@324 906 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@375 907 intros; autorewrite with core.
adam@324 908 (** [[
adam@324 909 ============================
adam@324 910 g (g (g x)) = g x
adam@324 911 ]]
adam@324 912 *)
adam@324 913
adam@324 914 Abort.
adam@324 915
adam@430 916 (** 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 917
adam@324 918 Reset garden_path.
adam@324 919
adam@375 920 (** The [autorewrite] tactic also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
adam@324 921
adam@324 922 Section garden_path.
adam@324 923 Variable P : A -> Prop.
adam@324 924 Variable g : A -> A.
adam@324 925 Hypothesis f_g : forall x, P x -> f x = g x.
adam@375 926 Hint Rewrite f_g.
adam@324 927
adam@324 928 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@375 929 intros; autorewrite with core.
adam@324 930 (** [[
adam@324 931
adam@324 932 ============================
adam@324 933 g (g (g x)) = g x
adam@324 934
adam@324 935 subgoal 2 is:
adam@324 936 P x
adam@324 937 subgoal 3 is:
adam@324 938 P (f x)
adam@324 939 subgoal 4 is:
adam@324 940 P (f x)
adam@324 941 ]]
adam@324 942 *)
adam@324 943
adam@324 944 Abort.
adam@324 945
adam@324 946 (** 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 947
adam@324 948 Reset garden_path.
adam@324 949
adam@324 950 (** 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 951
adam@324 952 Section garden_path.
adam@324 953 Variable P : A -> Prop.
adam@324 954 Variable g : A -> A.
adam@324 955 Hypothesis f_g : forall x, P x -> f x = g x.
adam@324 956 (* begin thide *)
adam@375 957 Hint Rewrite f_g using assumption.
adam@324 958 (* end thide *)
adam@324 959
adam@324 960 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 961 (* begin thide *)
adam@375 962 intros; autorewrite with core; reflexivity.
adam@324 963 Qed.
adam@324 964 (* end thide *)
adam@324 965
adam@375 966 (** We may still use [autorewrite] to apply [f_g] when the generated premise is among our assumptions. *)
adam@324 967
adam@324 968 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
adam@324 969 (* begin thide *)
adam@375 970 intros; autorewrite with core; reflexivity.
adam@324 971 (* end thide *)
adam@324 972 Qed.
adam@324 973 End garden_path.
adam@324 974
adam@375 975 (** 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 976
adam@324 977 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
adam@324 978 -> f x = f (f (f y)).
adam@324 979 (* begin thide *)
adam@375 980 intros; autorewrite with core in *; assumption.
adam@324 981 (* end thide *)
adam@324 982 Qed.
adam@324 983
adam@324 984 End autorewrite.
adam@375 985
adam@375 986 (** Many proofs can be automated in pleasantly modular ways with deft combination of [auto] and [autorewrite]. *)