Mercurial > cpdt > repo

annotate src/LogicProg.v @ 564:5504235ea06d

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