Mercurial > cpdt > repo
comparison src/LogicProg.v @ 437:8077352044b2
A pass over all formatting, after big pile of coqdoc changes
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 27 Jul 2012 16:47:28 -0400 |
| parents | 610568369aee |
| children | 0650420c127b |
comparison
equal
deleted
inserted
replaced
| 436:5d5e44f905c7 | 437:8077352044b2 |
|---|---|
| 75 reflexivity. | 75 reflexivity. |
| 76 Qed. | 76 Qed. |
| 77 (* end thide *) | 77 (* end thide *) |
| 78 | 78 |
| 79 (* begin hide *) | 79 (* begin hide *) |
| 80 (* begin thide *) | |
| 80 Definition er := @eq_refl. | 81 Definition er := @eq_refl. |
| 82 (* end thide *) | |
| 81 (* end hide *) | 83 (* end hide *) |
| 82 | 84 |
| 83 Print four_plus_three. | 85 Print four_plus_three. |
| 84 (** %\vspace{-.15in}%[[ | 86 (** %\vspace{-.15in}%[[ |
| 85 four_plus_three = eq_refl | 87 four_plus_three = eq_refl |
| 353 Finished transaction in 2. secs (1.92012u,0.044003s) | 355 Finished transaction in 2. secs (1.92012u,0.044003s) |
| 354 >> | 356 >> |
| 355 *) | 357 *) |
| 356 | 358 |
| 357 (** 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. *) | 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. *) |
| 360 | |
| 361 (* begin hide *) | |
| 362 (* begin thide *) | |
| 363 Definition syms := (eq_sym, plus_n_O, eq_add_S, f_equal2). | |
| 364 (* end thide *) | |
| 365 (* end hide *) | |
| 358 | 366 |
| 359 debug eauto 3. | 367 debug eauto 3. |
| 360 (** [[ | 368 (** [[ |
| 361 1 depth=3 | 369 1 depth=3 |
| 362 1.1 depth=2 eapply ex_intro | 370 1.1 depth=2 eapply ex_intro |
| 401 This [eauto] fails to prove the goal, but it least it takes substantially less than the 2 seconds required above! *) | 409 This [eauto] fails to prove the goal, but it least it takes substantially less than the 2 seconds required above! *) |
| 402 | 410 |
| 403 Abort. | 411 Abort. |
| 404 (* end thide *) | 412 (* end thide *) |
| 405 | 413 |
| 406 (** One simple example from before runs in the same amount of time, avoiding pollution by transivity. *) | 414 (** One simple example from before runs in the same amount of time, avoiding pollution by transitivity. *) |
| 407 | 415 |
| 408 Example seven_minus_three_again : exists x, x + 3 = 7. | 416 Example seven_minus_three_again : exists x, x + 3 = 7. |
| 409 (* begin thide *) | 417 (* begin thide *) |
| 410 Time eauto 6. | 418 Time eauto 6. |
| 411 (** %\vspace{-.15in}% | 419 (** %\vspace{-.15in}% |
| 508 (* end thide *) | 516 (* end thide *) |
| 509 | 517 |
| 510 (** 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. *) | 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. *) |
| 511 | 519 |
| 512 (* begin hide *) | 520 (* begin hide *) |
| 521 (* begin thide *) | |
| 513 Definition Forall_c := (@Forall_nil, @Forall_cons). | 522 Definition Forall_c := (@Forall_nil, @Forall_cons). |
| 523 (* end thide *) | |
| 514 (* end hide *) | 524 (* end hide *) |
| 515 | 525 |
| 516 Print Forall. | 526 Print Forall. |
| 517 (** %\vspace{-.15in}%[[ | 527 (** %\vspace{-.15in}%[[ |
| 518 Inductive Forall (A : Type) (P : A -> Prop) : list A -> Prop := | 528 Inductive Forall (A : Type) (P : A -> Prop) : list A -> Prop := |
| 530 (* end thide *) | 540 (* end thide *) |
| 531 | 541 |
| 532 (** We can see which list [eauto] found by printing the proof term. *) | 542 (** We can see which list [eauto] found by printing the proof term. *) |
| 533 | 543 |
| 534 (* begin hide *) | 544 (* begin hide *) |
| 545 (* begin thide *) | |
| 535 Definition conj' := (conj, le_n). | 546 Definition conj' := (conj, le_n). |
| 547 (* end thide *) | |
| 536 (* end hide *) | 548 (* end hide *) |
| 537 | 549 |
| 538 Print length_is_2. | 550 Print length_is_2. |
| 539 (** %\vspace{-.15in}%[[ | 551 (** %\vspace{-.15in}%[[ |
| 540 length_is_2 = | 552 length_is_2 = |
| 672 eauto. | 684 eauto. |
| 673 Qed. | 685 Qed. |
| 674 (* end thide *) | 686 (* end thide *) |
| 675 | 687 |
| 676 (* begin hide *) | 688 (* begin hide *) |
| 689 (* begin thide *) | |
| 677 Definition e1s := eval1'_subproof. | 690 Definition e1s := eval1'_subproof. |
| 691 (* end thide *) | |
| 678 (* end hide *) | 692 (* end hide *) |
| 679 | 693 |
| 680 Print eval1'. | 694 Print eval1'. |
| 681 (** %\vspace{-.15in}%[[ | 695 (** %\vspace{-.15in}%[[ |
| 682 eval1' = | 696 eval1' = |
| 810 (** A call to [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *) | 824 (** A call to [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *) |
| 811 | 825 |
| 812 Abort. | 826 Abort. |
| 813 | 827 |
| 814 (* begin hide *) | 828 (* begin hide *) |
| 829 (* begin thide *) | |
| 815 Definition boool := bool. | 830 Definition boool := bool. |
| 831 (* end thide *) | |
| 816 (* end hide *) | 832 (* end hide *) |
| 817 | 833 |
| 818 (** 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. *) | 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. *) |
| 819 | 835 |
| 820 Hint Extern 1 (_ <> _) => congruence. | 836 Hint Extern 1 (_ <> _) => congruence. |
| 850 (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic. The function [proj1] is from the standard library, for extracting a proof of [R] from a proof of [R /\ S]. *) | 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 [R] from a proof of [R /\ S]. *) |
| 851 | 867 |
| 852 End forall_and. | 868 End forall_and. |
| 853 | 869 |
| 854 (* begin hide *) | 870 (* begin hide *) |
| 871 (* begin thide *) | |
| 855 Definition noot := (not, @eq). | 872 Definition noot := (not, @eq). |
| 873 (* end thide *) | |
| 856 (* end hide *) | 874 (* end hide *) |
| 857 | 875 |
| 858 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P]. | 876 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P]. |
| 859 [[ | 877 [[ |
| 860 Hint Extern 1 (?P ?X) => | 878 Hint Extern 1 (?P ?X) => |