Mercurial > cpdt > repo

annotate src/LogicProg.v @ 372:3c039c72eb40

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prose for first LogicProg section
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 15:35:09 -0400
parents 549d604c3d16
children b13f76abc724
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@324 439 Print length.
adam@324 440
adam@324 441 Example length_1_2 : length (1 :: 2 :: nil) = 2.
adam@324 442 auto.
adam@324 443 Qed.
adam@324 444
adam@324 445 Print length_1_2.
adam@324 446
adam@324 447 (* begin thide *)
adam@324 448 Theorem length_O : forall A, length (nil (A := A)) = O.
adam@324 449 crush.
adam@324 450 Qed.
adam@324 451
adam@324 452 Theorem length_S : forall A (h : A) t n,
adam@324 453 length t = n
adam@324 454 -> length (h :: t) = S n.
adam@324 455 crush.
adam@324 456 Qed.
adam@324 457
adam@324 458 Hint Resolve length_O length_S.
adam@324 459 (* end thide *)
adam@324 460
adam@324 461 Example length_is_2 : exists ls : list nat, length ls = 2.
adam@324 462 (* begin thide *)
adam@324 463 eauto.
adam@324 464
adam@324 465 Show Proof.
adam@324 466 Abort.
adam@324 467 (* end thide *)
adam@324 468
adam@324 469 Print Forall.
adam@324 470
adam@324 471 Example length_is_2 : exists ls : list nat, length ls = 2
adam@324 472 /\ Forall (fun n => n >= 1) ls.
adam@324 473 (* begin thide *)
adam@324 474 eauto 9.
adam@324 475 Qed.
adam@324 476 (* end thide *)
adam@324 477
adam@324 478 Definition sum := fold_right plus O.
adam@324 479
adam@324 480 (* begin thide *)
adam@324 481 Lemma plusO' : forall n m,
adam@324 482 n = m
adam@324 483 -> 0 + n = m.
adam@324 484 crush.
adam@324 485 Qed.
adam@324 486
adam@324 487 Hint Resolve plusO'.
adam@324 488
adam@324 489 Hint Extern 1 (sum _ = _) => simpl.
adam@324 490 (* end thide *)
adam@324 491
adam@324 492 Example length_and_sum : exists ls : list nat, length ls = 2
adam@324 493 /\ sum ls = O.
adam@324 494 (* begin thide *)
adam@324 495 eauto 7.
adam@324 496 Qed.
adam@324 497 (* end thide *)
adam@324 498
adam@324 499 Print length_and_sum.
adam@324 500
adam@324 501 Example length_and_sum' : exists ls : list nat, length ls = 5
adam@324 502 /\ sum ls = 42.
adam@324 503 (* begin thide *)
adam@324 504 eauto 15.
adam@324 505 Qed.
adam@324 506 (* end thide *)
adam@324 507
adam@324 508 Print length_and_sum'.
adam@324 509
adam@324 510 Example length_and_sum'' : exists ls : list nat, length ls = 2
adam@324 511 /\ sum ls = 3
adam@324 512 /\ Forall (fun n => n <> 0) ls.
adam@324 513 (* begin thide *)
adam@324 514 eauto 11.
adam@324 515 Qed.
adam@324 516 (* end thide *)
adam@324 517
adam@324 518 Print length_and_sum''.
adam@324 519
adam@324 520
adam@324 521 (** * Synthesizing Programs *)
adam@324 522
adam@324 523 Inductive exp : Set :=
adam@324 524 | Const : nat -> exp
adam@324 525 | Var : exp
adam@324 526 | Plus : exp -> exp -> exp.
adam@324 527
adam@324 528 Inductive eval (var : nat) : exp -> nat -> Prop :=
adam@324 529 | EvalConst : forall n, eval var (Const n) n
adam@324 530 | EvalVar : eval var Var var
adam@324 531 | EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
adam@324 532 -> eval var e2 n2
adam@324 533 -> eval var (Plus e1 e2) (n1 + n2).
adam@324 534
adam@324 535 (* begin thide *)
adam@324 536 Hint Constructors eval.
adam@324 537 (* end thide *)
adam@324 538
adam@324 539 Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
adam@324 540 (* begin thide *)
adam@324 541 auto.
adam@324 542 Qed.
adam@324 543 (* end thide *)
adam@324 544
adam@324 545 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
adam@324 546 (* begin thide *)
adam@324 547 eauto.
adam@324 548 Abort.
adam@324 549 (* end thide *)
adam@324 550
adam@324 551 (* begin thide *)
adam@324 552 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1
adam@324 553 -> eval var e2 n2
adam@324 554 -> n1 + n2 = n
adam@324 555 -> eval var (Plus e1 e2) n.
adam@324 556 crush.
adam@324 557 Qed.
adam@324 558
adam@324 559 Hint Resolve EvalPlus'.
adam@324 560
adam@324 561 Hint Extern 1 (_ = _) => abstract omega.
adam@324 562 (* end thide *)
adam@324 563
adam@324 564 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
adam@324 565 (* begin thide *)
adam@324 566 eauto.
adam@324 567 Qed.
adam@324 568 (* end thide *)
adam@324 569
adam@324 570 Print eval1'.
adam@324 571
adam@324 572 Example synthesize1 : exists e, forall var, eval var e (var + 7).
adam@324 573 (* begin thide *)
adam@324 574 eauto.
adam@324 575 Qed.
adam@324 576 (* end thide *)
adam@324 577
adam@324 578 Print synthesize1.
adam@324 579
adam@324 580 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
adam@324 581 (* begin thide *)
adam@324 582 eauto.
adam@324 583 Qed.
adam@324 584 (* end thide *)
adam@324 585
adam@324 586 Print synthesize2.
adam@324 587
adam@324 588 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
adam@324 589 (* begin thide *)
adam@324 590 eauto.
adam@324 591 Qed.
adam@324 592 (* end thide *)
adam@324 593
adam@324 594 Print synthesize3.
adam@324 595
adam@324 596 (* begin thide *)
adam@324 597 Theorem EvalConst' : forall var n m, n = m
adam@324 598 -> eval var (Const n) m.
adam@324 599 crush.
adam@324 600 Qed.
adam@324 601
adam@324 602 Hint Resolve EvalConst'.
adam@324 603
adam@324 604 Theorem zero_times : forall n m r,
adam@324 605 r = m
adam@324 606 -> r = 0 * n + m.
adam@324 607 crush.
adam@324 608 Qed.
adam@324 609
adam@324 610 Hint Resolve zero_times.
adam@324 611
adam@324 612 Theorem EvalVar' : forall var n,
adam@324 613 var = n
adam@324 614 -> eval var Var n.
adam@324 615 crush.
adam@324 616 Qed.
adam@324 617
adam@324 618 Hint Resolve EvalVar'.
adam@324 619
adam@324 620 Theorem plus_0 : forall n r,
adam@324 621 r = n
adam@324 622 -> r = n + 0.
adam@324 623 crush.
adam@324 624 Qed.
adam@324 625
adam@324 626 Theorem times_1 : forall n, n = 1 * n.
adam@324 627 crush.
adam@324 628 Qed.
adam@324 629
adam@324 630 Hint Resolve plus_0 times_1.
adam@324 631
adam@324 632 Require Import Arith Ring.
adam@324 633
adam@324 634 Theorem combine : forall x k1 k2 n1 n2,
adam@324 635 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).
adam@324 636 intros; ring.
adam@324 637 Qed.
adam@324 638
adam@324 639 Hint Resolve combine.
adam@324 640
adam@324 641 Theorem linear : forall e, exists k, exists n,
adam@324 642 forall var, eval var e (k * var + n).
adam@324 643 induction e; crush; eauto.
adam@324 644 Qed.
adam@324 645
adam@324 646 Print linear.
adam@324 647 (* end thide *)
adam@324 648
adam@324 649
adam@324 650 (** * More on [auto] Hints *)
adam@324 651
adam@324 652 (** Another class of built-in tactics includes [auto], [eauto], and [autorewrite]. These are based on %\textit{%#<i>#hint databases#</i>#%}%, which we have seen extended in many examples so far. These tactics are important, because, in Ltac programming, we cannot create %``%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files. We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments.
adam@324 653
adam@324 654 The basic hints for [auto] and [eauto] are [Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; [Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; [Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and [Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal. Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db]. This adds the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db]. An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db]. The default depth is 5.
adam@324 655
adam@324 656 All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern]. A few examples should do best to explain how [Hint Extern] works. *)
adam@324 657
adam@324 658 Theorem bool_neq : true <> false.
adam@324 659 (* begin thide *)
adam@324 660 auto.
adam@324 661
adam@324 662 (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
adam@324 663
adam@324 664 Abort.
adam@324 665
adam@324 666 (** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove. Luckily, a simpler form suffices. *)
adam@324 667
adam@324 668 Hint Extern 1 (_ <> _) => congruence.
adam@324 669
adam@324 670 Theorem bool_neq : true <> false.
adam@324 671 auto.
adam@324 672 Qed.
adam@324 673 (* end thide *)
adam@324 674
adam@324 675 (** Our hint says: %``%#"#whenever the conclusion matches the pattern [_ <> _], try applying [congruence].#"#%''% The [1] is a cost for this rule. During proof search, whenever multiple rules apply, rules are tried in increasing cost order, so it pays to assign high costs to relatively expensive [Extern] hints.
adam@324 676
adam@324 677 [Extern] hints may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
adam@324 678
adam@324 679 Section forall_and.
adam@324 680 Variable A : Set.
adam@324 681 Variables P Q : A -> Prop.
adam@324 682
adam@324 683 Hypothesis both : forall x, P x /\ Q x.
adam@324 684
adam@324 685 Theorem forall_and : forall z, P z.
adam@324 686 (* begin thide *)
adam@324 687 crush.
adam@324 688
adam@324 689 (** [crush] makes no progress beyond what [intros] would have accomplished. [auto] will not apply the hypothesis [both] to prove the goal, because the conclusion of [both] does not unify with the conclusion of the goal. However, we can teach [auto] to handle this kind of goal. *)
adam@324 690
adam@324 691 Hint Extern 1 (P ?X) =>
adam@324 692 match goal with
adam@324 693 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@324 694 end.
adam@324 695
adam@324 696 auto.
adam@324 697 Qed.
adam@324 698 (* end thide *)
adam@324 699
adam@324 700 (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic. [proj1] is a function from the standard library for extracting a proof of [R] from a proof of [R /\ S]. *)
adam@324 701
adam@324 702 End forall_and.
adam@324 703
adam@324 704 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
adam@324 705
adam@324 706 [[
adam@324 707 Hint Extern 1 (?P ?X) =>
adam@324 708 match goal with
adam@324 709 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@324 710 end.
adam@324 711
adam@324 712 User error: Bound head variable
adam@324 713
adam@324 714 ]]
adam@324 715
adam@324 716 Coq's [auto] hint databases work as tables mapping %\textit{%#<i>#head symbols#</i>#%}% to lists of tactics to try. Because of this, the constant head of an [Extern] pattern must be determinable statically. In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P].
adam@324 717
adam@324 718 This restriction on [Extern] hints is the main limitation of the [auto] mechanism, preventing us from using it for general context simplifications that are not keyed off of the form of the conclusion. This is perhaps just as well, since we can often code more efficient tactics with specialized Ltac programs, and we will see how in the next chapter. *)
adam@324 719
adam@324 720
adam@324 721 (** * Rewrite Hints *)
adam@324 722
adam@324 723 (** We have used [Hint Rewrite] in many examples so far. [crush] uses these hints by calling [autorewrite]. Our rewrite hints have taken the form [Hint Rewrite lemma : cpdt], adding them to the [cpdt] rewrite database. This is because, in contrast to [auto], [autorewrite] has no default database. Thus, we set the convention that [crush] uses the [cpdt] database.
adam@324 724
adam@324 725 This example shows a direct use of [autorewrite]. *)
adam@324 726
adam@324 727 Section autorewrite.
adam@324 728 Variable A : Set.
adam@324 729 Variable f : A -> A.
adam@324 730
adam@324 731 Hypothesis f_f : forall x, f (f x) = f x.
adam@324 732
adam@324 733 Hint Rewrite f_f : my_db.
adam@324 734
adam@324 735 Lemma f_f_f : forall x, f (f (f x)) = f x.
adam@324 736 intros; autorewrite with my_db; reflexivity.
adam@324 737 Qed.
adam@324 738
adam@324 739 (** 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 740
adam@324 741 Section garden_path.
adam@324 742 Variable g : A -> A.
adam@324 743 Hypothesis f_g : forall x, f x = g x.
adam@324 744 Hint Rewrite f_g : my_db.
adam@324 745
adam@324 746 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 747 intros; autorewrite with my_db.
adam@324 748 (** [[
adam@324 749 ============================
adam@324 750 g (g (g x)) = g x
adam@324 751 ]]
adam@324 752 *)
adam@324 753
adam@324 754 Abort.
adam@324 755
adam@324 756 (** 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 757
adam@324 758 Reset garden_path.
adam@324 759
adam@324 760 (** [autorewrite] also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
adam@324 761
adam@324 762 Section garden_path.
adam@324 763 Variable P : A -> Prop.
adam@324 764 Variable g : A -> A.
adam@324 765 Hypothesis f_g : forall x, P x -> f x = g x.
adam@324 766 Hint Rewrite f_g : my_db.
adam@324 767
adam@324 768 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 769 intros; autorewrite with my_db.
adam@324 770 (** [[
adam@324 771
adam@324 772 ============================
adam@324 773 g (g (g x)) = g x
adam@324 774
adam@324 775 subgoal 2 is:
adam@324 776 P x
adam@324 777 subgoal 3 is:
adam@324 778 P (f x)
adam@324 779 subgoal 4 is:
adam@324 780 P (f x)
adam@324 781 ]]
adam@324 782 *)
adam@324 783
adam@324 784 Abort.
adam@324 785
adam@324 786 (** 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 787
adam@324 788 Reset garden_path.
adam@324 789
adam@324 790 (** 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 791
adam@324 792 Section garden_path.
adam@324 793 Variable P : A -> Prop.
adam@324 794 Variable g : A -> A.
adam@324 795 Hypothesis f_g : forall x, P x -> f x = g x.
adam@324 796 (* begin thide *)
adam@324 797 Hint Rewrite f_g using assumption : my_db.
adam@324 798 (* end thide *)
adam@324 799
adam@324 800 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 801 (* begin thide *)
adam@324 802 intros; autorewrite with my_db; reflexivity.
adam@324 803 Qed.
adam@324 804 (* end thide *)
adam@324 805
adam@324 806 (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *)
adam@324 807
adam@324 808 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
adam@324 809 (* begin thide *)
adam@324 810 intros; autorewrite with my_db; reflexivity.
adam@324 811 (* end thide *)
adam@324 812 Qed.
adam@324 813 End garden_path.
adam@324 814
adam@324 815 (** remove printing * *)
adam@324 816
adam@324 817 (** It can also be useful to use the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *)
adam@324 818
adam@324 819 (** printing * $*$ *)
adam@324 820
adam@324 821 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
adam@324 822 -> f x = f (f (f y)).
adam@324 823 (* begin thide *)
adam@324 824 intros; autorewrite with my_db in *; assumption.
adam@324 825 (* end thide *)
adam@324 826 Qed.
adam@324 827
adam@324 828 End autorewrite.