Mercurial > cpdt > repo

annotate src/LogicProg.v @ 384:eb0fa506d04c

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