Mercurial > cpdt > repo

annotate src/LogicProg.v @ 373:b13f76abc724

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prose for second LogicProg section
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:04:52 -0400
parents 3c039c72eb40
children f3146d40c2a1
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@324 603 Inductive exp : Set :=
adam@324 604 | Const : nat -> exp
adam@324 605 | Var : exp
adam@324 606 | Plus : exp -> exp -> exp.
adam@324 607
adam@324 608 Inductive eval (var : nat) : exp -> nat -> Prop :=
adam@324 609 | EvalConst : forall n, eval var (Const n) n
adam@324 610 | EvalVar : eval var Var var
adam@324 611 | EvalPlus : forall e1 e2 n1 n2, eval var e1 n1
adam@324 612 -> eval var e2 n2
adam@324 613 -> eval var (Plus e1 e2) (n1 + n2).
adam@324 614
adam@324 615 (* begin thide *)
adam@324 616 Hint Constructors eval.
adam@324 617 (* end thide *)
adam@324 618
adam@324 619 Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).
adam@324 620 (* begin thide *)
adam@324 621 auto.
adam@324 622 Qed.
adam@324 623 (* end thide *)
adam@324 624
adam@324 625 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
adam@324 626 (* begin thide *)
adam@324 627 eauto.
adam@324 628 Abort.
adam@324 629 (* end thide *)
adam@324 630
adam@324 631 (* begin thide *)
adam@324 632 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1
adam@324 633 -> eval var e2 n2
adam@324 634 -> n1 + n2 = n
adam@324 635 -> eval var (Plus e1 e2) n.
adam@324 636 crush.
adam@324 637 Qed.
adam@324 638
adam@324 639 Hint Resolve EvalPlus'.
adam@324 640
adam@324 641 Hint Extern 1 (_ = _) => abstract omega.
adam@324 642 (* end thide *)
adam@324 643
adam@324 644 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
adam@324 645 (* begin thide *)
adam@324 646 eauto.
adam@324 647 Qed.
adam@324 648 (* end thide *)
adam@324 649
adam@324 650 Print eval1'.
adam@324 651
adam@324 652 Example synthesize1 : exists e, forall var, eval var e (var + 7).
adam@324 653 (* begin thide *)
adam@324 654 eauto.
adam@324 655 Qed.
adam@324 656 (* end thide *)
adam@324 657
adam@324 658 Print synthesize1.
adam@324 659
adam@324 660 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
adam@324 661 (* begin thide *)
adam@324 662 eauto.
adam@324 663 Qed.
adam@324 664 (* end thide *)
adam@324 665
adam@324 666 Print synthesize2.
adam@324 667
adam@324 668 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
adam@324 669 (* begin thide *)
adam@324 670 eauto.
adam@324 671 Qed.
adam@324 672 (* end thide *)
adam@324 673
adam@324 674 Print synthesize3.
adam@324 675
adam@324 676 (* begin thide *)
adam@324 677 Theorem EvalConst' : forall var n m, n = m
adam@324 678 -> eval var (Const n) m.
adam@324 679 crush.
adam@324 680 Qed.
adam@324 681
adam@324 682 Hint Resolve EvalConst'.
adam@324 683
adam@324 684 Theorem zero_times : forall n m r,
adam@324 685 r = m
adam@324 686 -> r = 0 * n + m.
adam@324 687 crush.
adam@324 688 Qed.
adam@324 689
adam@324 690 Hint Resolve zero_times.
adam@324 691
adam@324 692 Theorem EvalVar' : forall var n,
adam@324 693 var = n
adam@324 694 -> eval var Var n.
adam@324 695 crush.
adam@324 696 Qed.
adam@324 697
adam@324 698 Hint Resolve EvalVar'.
adam@324 699
adam@324 700 Theorem plus_0 : forall n r,
adam@324 701 r = n
adam@324 702 -> r = n + 0.
adam@324 703 crush.
adam@324 704 Qed.
adam@324 705
adam@324 706 Theorem times_1 : forall n, n = 1 * n.
adam@324 707 crush.
adam@324 708 Qed.
adam@324 709
adam@324 710 Hint Resolve plus_0 times_1.
adam@324 711
adam@324 712 Require Import Arith Ring.
adam@324 713
adam@324 714 Theorem combine : forall x k1 k2 n1 n2,
adam@324 715 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).
adam@324 716 intros; ring.
adam@324 717 Qed.
adam@324 718
adam@324 719 Hint Resolve combine.
adam@324 720
adam@324 721 Theorem linear : forall e, exists k, exists n,
adam@324 722 forall var, eval var e (k * var + n).
adam@324 723 induction e; crush; eauto.
adam@324 724 Qed.
adam@324 725
adam@324 726 Print linear.
adam@324 727 (* end thide *)
adam@324 728
adam@324 729
adam@324 730 (** * More on [auto] Hints *)
adam@324 731
adam@324 732 (** 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 733
adam@324 734 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 735
adam@324 736 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 737
adam@324 738 Theorem bool_neq : true <> false.
adam@324 739 (* begin thide *)
adam@324 740 auto.
adam@324 741
adam@324 742 (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
adam@324 743
adam@324 744 Abort.
adam@324 745
adam@324 746 (** 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 747
adam@324 748 Hint Extern 1 (_ <> _) => congruence.
adam@324 749
adam@324 750 Theorem bool_neq : true <> false.
adam@324 751 auto.
adam@324 752 Qed.
adam@324 753 (* end thide *)
adam@324 754
adam@324 755 (** 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 756
adam@324 757 [Extern] hints may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
adam@324 758
adam@324 759 Section forall_and.
adam@324 760 Variable A : Set.
adam@324 761 Variables P Q : A -> Prop.
adam@324 762
adam@324 763 Hypothesis both : forall x, P x /\ Q x.
adam@324 764
adam@324 765 Theorem forall_and : forall z, P z.
adam@324 766 (* begin thide *)
adam@324 767 crush.
adam@324 768
adam@324 769 (** [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 770
adam@324 771 Hint Extern 1 (P ?X) =>
adam@324 772 match goal with
adam@324 773 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@324 774 end.
adam@324 775
adam@324 776 auto.
adam@324 777 Qed.
adam@324 778 (* end thide *)
adam@324 779
adam@324 780 (** 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 781
adam@324 782 End forall_and.
adam@324 783
adam@324 784 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
adam@324 785
adam@324 786 [[
adam@324 787 Hint Extern 1 (?P ?X) =>
adam@324 788 match goal with
adam@324 789 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@324 790 end.
adam@324 791
adam@324 792 User error: Bound head variable
adam@324 793
adam@324 794 ]]
adam@324 795
adam@324 796 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 797
adam@324 798 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 799
adam@324 800
adam@324 801 (** * Rewrite Hints *)
adam@324 802
adam@324 803 (** 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 804
adam@324 805 This example shows a direct use of [autorewrite]. *)
adam@324 806
adam@324 807 Section autorewrite.
adam@324 808 Variable A : Set.
adam@324 809 Variable f : A -> A.
adam@324 810
adam@324 811 Hypothesis f_f : forall x, f (f x) = f x.
adam@324 812
adam@324 813 Hint Rewrite f_f : my_db.
adam@324 814
adam@324 815 Lemma f_f_f : forall x, f (f (f x)) = f x.
adam@324 816 intros; autorewrite with my_db; reflexivity.
adam@324 817 Qed.
adam@324 818
adam@324 819 (** 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 820
adam@324 821 Section garden_path.
adam@324 822 Variable g : A -> A.
adam@324 823 Hypothesis f_g : forall x, f x = g x.
adam@324 824 Hint Rewrite f_g : my_db.
adam@324 825
adam@324 826 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 827 intros; autorewrite with my_db.
adam@324 828 (** [[
adam@324 829 ============================
adam@324 830 g (g (g x)) = g x
adam@324 831 ]]
adam@324 832 *)
adam@324 833
adam@324 834 Abort.
adam@324 835
adam@324 836 (** 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 837
adam@324 838 Reset garden_path.
adam@324 839
adam@324 840 (** [autorewrite] also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
adam@324 841
adam@324 842 Section garden_path.
adam@324 843 Variable P : A -> Prop.
adam@324 844 Variable g : A -> A.
adam@324 845 Hypothesis f_g : forall x, P x -> f x = g x.
adam@324 846 Hint Rewrite f_g : my_db.
adam@324 847
adam@324 848 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 849 intros; autorewrite with my_db.
adam@324 850 (** [[
adam@324 851
adam@324 852 ============================
adam@324 853 g (g (g x)) = g x
adam@324 854
adam@324 855 subgoal 2 is:
adam@324 856 P x
adam@324 857 subgoal 3 is:
adam@324 858 P (f x)
adam@324 859 subgoal 4 is:
adam@324 860 P (f x)
adam@324 861 ]]
adam@324 862 *)
adam@324 863
adam@324 864 Abort.
adam@324 865
adam@324 866 (** 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 867
adam@324 868 Reset garden_path.
adam@324 869
adam@324 870 (** 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 871
adam@324 872 Section garden_path.
adam@324 873 Variable P : A -> Prop.
adam@324 874 Variable g : A -> A.
adam@324 875 Hypothesis f_g : forall x, P x -> f x = g x.
adam@324 876 (* begin thide *)
adam@324 877 Hint Rewrite f_g using assumption : my_db.
adam@324 878 (* end thide *)
adam@324 879
adam@324 880 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 881 (* begin thide *)
adam@324 882 intros; autorewrite with my_db; reflexivity.
adam@324 883 Qed.
adam@324 884 (* end thide *)
adam@324 885
adam@324 886 (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *)
adam@324 887
adam@324 888 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
adam@324 889 (* begin thide *)
adam@324 890 intros; autorewrite with my_db; reflexivity.
adam@324 891 (* end thide *)
adam@324 892 Qed.
adam@324 893 End garden_path.
adam@324 894
adam@324 895 (** remove printing * *)
adam@324 896
adam@324 897 (** 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 898
adam@324 899 (** printing * $*$ *)
adam@324 900
adam@324 901 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
adam@324 902 -> f x = f (f (f y)).
adam@324 903 (* begin thide *)
adam@324 904 intros; autorewrite with my_db in *; assumption.
adam@324 905 (* end thide *)
adam@324 906 Qed.
adam@324 907
adam@324 908 End autorewrite.