### annotate src/LogicProg.v @ 506:05c0f872a129

Pass through Chapter 13
rev   line source
adam@324 10 (* begin hide *)
adam@324 18 (* end hide *)
adam@324 22 \chapter{Proof Search by Logic Programming}% *)
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@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 29 (** * Introducing Logic Programming *)
adam@372 31 (** Recall the definition of addition from the standard library. *)
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 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 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@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@324 52 (* begin thide *)
adam@324 54 (* end thide *)
adam@324 56 Theorem plus_plusR : forall n m,
adam@324 57 plusR n m (n + m).
adam@324 58 (* begin thide *)
adam@324 61 (* end thide *)
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 69 (* end thide *)
adam@372 71 (** With the functional definition of [plus], simple equalities about arithmetic follow by computation. *)
adam@324 73 Example four_plus_three : 4 + 3 = 7.
adam@324 74 (* begin thide *)
adam@324 77 (* end thide *)
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@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@324 93 Example four_plus_three' : plusR 4 3 7.
adam@324 94 (* begin thide *)
adam@372 100 Error: Impossible to unify "plusR 0 ?24 ?24" with "plusR 4 3 7".
adam@372 108 Error: Impossible to unify "plusR 0 ?25 ?25" with "plusR 3 3 6".
adam@372 116 Error: Impossible to unify "plusR 0 ?26 ?26" with "plusR 2 3 5".
adam@372 124 Error: Impossible to unify "plusR 0 ?27 ?27" with "plusR 1 3 4".
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@324 134 (* end thide *)
adam@372 138 four_plus_three' = PlusS (PlusS (PlusS (PlusS (PlusO 3))))
adam@372 142 (** Let us try the same approach on a slightly more complex goal. *)
adam@372 144 Example five_plus_three : plusR 5 3 8.
adam@324 145 (* begin thide *)
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@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 157 == apply PlusS; apply PlusS; apply PlusS; apply PlusS;
adam@372 158 apply PlusS; apply PlusO.
adam@324 162 (* end thide *)
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 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 170 apply ex_intro with 0.
adam@372 176 Error: Impossible to unify "7" with "0 + 3".
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 183 apply ex_intro with 4.
adam@324 186 (* end thide *)
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 190 Next we demonstrate unification, which will be easier when we switch to the relational formulation of addition. *)
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 201 plusR ?70 3 7
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 209 plusR ?71 3 6
adam@372 212 apply PlusS. apply PlusS. apply PlusS.
adam@372 215 plusR ?74 3 3
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 225 == eapply ex_intro; apply PlusS; apply PlusS;
adam@372 226 apply PlusS; apply PlusS; apply PlusO.
adam@324 230 (* end thide *)
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@324 234 Example seven_minus_four' : exists x, plusR 4 x 7.
adam@324 235 (* begin thide *)
adam@324 238 (* end thide *)
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@324 242 (* begin thide *)
adam@324 243 SearchRewrite (O + _).
adam@372 245 plus_O_n: forall n : nat, 0 + n = n
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@372 252 (** The counterpart to [PlusS] we will prove ourselves. *)
adam@324 254 Lemma plusS : forall n m r,
adam@324 255 n + m = r
adam@324 256 -> S n + m = S r.
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@324 263 (* end thide *)
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 267 Example seven_minus_three'' : exists x, x + 3 = 7.
adam@324 268 (* begin thide *)
adam@324 271 (* end thide *)
adam@324 273 Example seven_minus_four : exists x, 4 + x = 7.
adam@324 274 (* begin thide *)
adam@324 277 (* end thide *)
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 281 Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
adam@324 282 (* begin thide *)
adam@324 285 (* end thide *)
adam@324 289 (* begin thide *)
adam@324 290 Lemma plusO : forall n m,
adam@324 292 -> n + 0 = m.
adam@324 297 (* end thide *)
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@324 301 Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
adam@324 302 (* begin thide *)
adam@324 305 (* end thide *)
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 312 : forall (A : Type) (x y z : A), x = y -> y = z -> x = z
adam@372 316 (** Hints are scoped over sections, so let us enter a section to contain the effects of an unfortunate hint choice. *)
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@484 323 Example zero_minus_one : exists x, 1 + x = 0.
adam@372 327 Finished transaction in 0. secs (0.u,0.s)
adam@372 334 Finished transaction in 0. secs (0.u,0.s)
adam@372 341 Finished transaction in 0. secs (0.008u,0.s)
adam@372 348 Finished transaction in 0. secs (0.068005u,0.004s)
adam@372 355 Finished transaction in 2. secs (1.92012u,0.044003s)
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@437 361 (* begin hide *)
adam@437 362 (* begin thide *)
adam@437 364 (* end thide *)
adam@437 365 (* end hide *)
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 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@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@324 397 (* begin thide *)
adam@324 398 Hint Resolve eq_trans : slow.
adam@324 399 (* end thide *)
adam@324 401 Example three_minus_four_zero : exists x, 1 + x = 0.
adam@324 402 (* begin thide *)
adam@372 406 Finished transaction in 0. secs (0.004u,0.s)
adam@469 409 This [eauto] fails to prove the goal, but at least it takes substantially less than the 2 seconds required above! *)
adam@324 412 (* end thide *)
adam@437 414 (** One simple example from before runs in the same amount of time, avoiding pollution by transitivity. *)
adam@324 416 Example seven_minus_three_again : exists x, x + 3 = 7.
adam@324 417 (* begin thide *)
adam@372 421 Finished transaction in 0. secs (0.004001u,0.s)
adam@324 426 (* end thide *)
adam@398 428 (** When we _do_ need transitivity, we ask for it explicitly. *)
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 436 == intro x; intro y; intro H; intro H0; simple eapply ex_intro;
adam@372 437 apply plusS; simple eapply eq_trans.
adam@324 444 (* end thide *)
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@324 449 (** * Searching for Underconstrained Values *)
adam@373 451 (** Recall the definition of the list length function. *)
adam@373 456 fun A : Type =>
adam@373 457 fix length (l : list A) : nat :=
adam@373 459 | nil => 0
adam@373 460 | _ :: l' => S (length l')
adam@373 464 This function is easy to reason about in the forward direction, computing output from input. *)
adam@324 466 Example length_1_2 : length (1 :: 2 :: nil) = 2.
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 477 (* begin thide *)
adam@324 478 Theorem length_O : forall A, length (nil (A := A)) = O.
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 488 Hint Resolve length_O length_S.
adam@324 489 (* end thide *)
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@324 493 Example length_is_2 : exists ls : list nat, length ls = 2.
adam@324 494 (* begin thide *)
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@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 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@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@324 516 (* end thide *)
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@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@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@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 540 (* end thide *)
adam@373 542 (** We can see which list [eauto] found by printing the proof term. *)
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@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@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@324 564 Definition sum := fold_right plus O.
adam@373 566 (** Another basic lemma will be helpful to guide proof search. *)
adam@324 568 (* begin thide *)
adam@324 569 Lemma plusO' : forall n m,
adam@324 571 -> 0 + n = m.
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@324 579 Hint Extern 1 (sum _ = _) => simpl.
adam@324 580 (* end thide *)
adam@373 582 (** Now we can find a length-2 list whose sum is 0. *)
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 589 (* end thide *)
adam@373 591 (* begin hide *)
adam@373 593 (* end hide *)
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 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 602 (* end thide *)
adam@373 604 (* begin hide *)
adam@373 606 (* end hide *)
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 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 616 (* end thide *)
adam@373 618 (* begin hide *)
adam@373 620 (* end hide *)
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 625 (** * Synthesizing Programs *)
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@324 629 Inductive exp : Set :=
adam@324 630 | Const : nat -> exp
adam@324 631 | Var : exp
adam@324 632 | Plus : exp -> exp -> exp.
adam@374 634 (** An inductive relation specifies the semantics of an expression, relating a variable value and an expression to the expression value. *)
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 643 (* begin thide *)
adam@324 645 (* end thide *)
adam@374 647 (** We can use [auto] to execute the semantics for specific expressions. *)
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 653 (* end thide *)
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@324 657 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).
adam@324 658 (* begin thide *)
adam@324 661 (* end thide *)
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@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@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@324 677 Hint Extern 1 (_ = _) => abstract omega.
adam@324 678 (* end thide *)
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 686 (* end thide *)
adam@430 688 (* begin hide *)
adam@437 689 (* begin thide *)
adam@430 690 Definition e1s := eval1'_subproof.
adam@437 691 (* end thide *)
adam@430 692 (* end hide *)
adam@374 697 fun var : nat =>
adam@374 698 EvalPlus' (EvalVar var) (EvalPlus (EvalConst var 8) (EvalVar var))
adam@374 700 : forall var : nat,
adam@374 701 eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8)
adam@374 705 (** The lemma [eval1'_subproof] was generated by [abstract omega].
adam@374 707 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 709 Example synthesize1 : exists e, forall var, eval var e (var + 7).
adam@324 710 (* begin thide *)
adam@324 713 (* end thide *)
adam@374 718 ex_intro (fun e : exp => forall var : nat, eval var e (var + 7))
adam@374 719 (Plus Var (Const 7))
adam@374 720 (fun var : nat => EvalPlus (EvalVar var) (EvalConst var 7))
adam@374 724 (** Here are two more examples showing off our program synthesis abilities. *)
adam@324 726 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).
adam@324 727 (* begin thide *)
adam@324 730 (* end thide *)
adam@374 732 (* begin hide *)
adam@374 734 (* end hide *)
adam@324 736 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).
adam@324 737 (* begin thide *)
adam@324 740 (* end thide *)
adam@374 742 (* begin hide *)
adam@374 744 (* end hide *)
adam@374 746 (** 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 748 We prove a series of lemmas and add them as hints. We have alternate [eval] constructor lemmas and some facts about arithmetic. *)
adam@324 750 (* begin thide *)
adam@324 751 Theorem EvalConst' : forall var n m, n = m
adam@324 752 -> eval var (Const n) m.
adam@324 758 Theorem zero_times : forall n m r,
adam@324 760 -> r = 0 * n + m.
adam@324 766 Theorem EvalVar' : forall var n,
adam@324 768 -> eval var Var n.
adam@324 774 Theorem plus_0 : forall n r,
adam@324 776 -> r = n + 0.
adam@324 780 Theorem times_1 : forall n, n = 1 * n.
adam@324 784 Hint Resolve plus_0 times_1.
adam@398 786 (** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the _ring_ algebraic structure, so, since the naturals form a ring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *)
adam@324 788 Require Import Arith Ring.
adam@324 790 Theorem combine : forall x k1 k2 n1 n2,
adam@324 791 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).
adam@374 797 (** 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@324 799 Theorem linear : forall e, exists k, exists n,
adam@324 800 forall var, eval var e (k * var + n).
adam@324 801 induction e; crush; eauto.
adam@374 804 (* begin hide *)
adam@374 806 (* end hide *)
adam@324 807 (* end thide *)
adam@374 809 (** By printing the proof term, it is possible to see the procedure that is used to choose the constants for each input term. *)
adam@324 812 (** * More on [auto] Hints *)
adam@430 814 (** 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@506 816 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@484 818 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 820 Theorem bool_neq : true <> false.
adam@324 821 (* begin thide *)
adam@410 824 (** A call to [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
adam@430 828 (* begin hide *)
adam@437 829 (* begin thide *)
adam@430 830 Definition boool := bool.
adam@437 831 (* end thide *)
adam@430 832 (* end hide *)
adam@375 834 (** 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 836 Hint Extern 1 (_ <> _) => congruence.
adam@324 838 Theorem bool_neq : true <> false.
adam@324 841 (* end thide *)
adam@410 843 (** A [Hint Extern] may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *)
adam@324 846 Variable A : Set.
adam@324 847 Variables P Q : A -> Prop.
adam@324 849 Hypothesis both : forall x, P x /\ Q x.
adam@324 851 Theorem forall_and : forall z, P z.
adam@324 852 (* begin thide *)
adam@375 855 (** 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 857 Hint Extern 1 (P ?X) =>
adam@324 859 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@324 864 (* end thide *)
adam@459 866 (** 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@430 870 (* begin hide *)
adam@437 871 (* begin thide *)
adam@430 872 Definition noot := (not, @eq).
adam@437 873 (* end thide *)
adam@430 874 (* end hide *)
adam@324 876 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
adam@430 878 Hint Extern 1 (?P ?X) =>
adam@430 880 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
adam@410 887 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@375 889 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@375 891 Hint Extern 1 =>
adam@375 893 | [ H : forall x, ?P x /\ _ |- ?P ?X ] => apply (proj1 (H X))
adam@398 896 (** 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 899 (** * Rewrite Hints *)
adam@375 901 (** 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@375 903 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 906 Variable A : Set.
adam@324 907 Variable f : A -> A.
adam@324 909 Hypothesis f_f : forall x, f (f x) = f x.
adam@324 913 Lemma f_f_f : forall x, f (f (f x)) = f x.
adam@375 914 intros; autorewrite with core; reflexivity.
adam@430 917 (** 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 920 Variable g : A -> A.
adam@324 921 Hypothesis f_g : forall x, f x = g x.
adam@324 924 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@375 925 intros; autorewrite with core.
adam@324 928 g (g (g x)) = g x
adam@430 934 (** 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@375 938 (** The [autorewrite] tactic also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)
adam@324 941 Variable P : A -> Prop.
adam@324 942 Variable g : A -> A.
adam@324 943 Hypothesis f_g : forall x, P x -> f x = g x.
adam@324 946 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@375 947 intros; autorewrite with core.
adam@324 950 g (g (g x)) = g x
adam@324 963 (** 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 967 (** 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 970 Variable P : A -> Prop.
adam@324 971 Variable g : A -> A.
adam@324 972 Hypothesis f_g : forall x, P x -> f x = g x.
adam@324 973 (* begin thide *)
adam@375 974 Hint Rewrite f_g using assumption.
adam@324 975 (* end thide *)
adam@324 977 Lemma f_f_f' : forall x, f (f (f x)) = f x.
adam@324 978 (* begin thide *)
adam@375 979 intros; autorewrite with core; reflexivity.
adam@324 981 (* end thide *)
adam@375 983 (** We may still use [autorewrite] to apply [f_g] when the generated premise is among our assumptions. *)
adam@324 985 Lemma f_f_f_g : forall x, P x -> f (f x) = g x.
adam@324 986 (* begin thide *)
adam@375 987 intros; autorewrite with core; reflexivity.
adam@324 988 (* end thide *)