Mercurial > cpdt > repo
comparison src/Predicates.v @ 375:d1276004eec9
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 26 Mar 2012 16:55:59 -0400 |
| parents | 549d604c3d16 |
| children | cc8d0503619f |
comparison
equal
deleted
inserted
replaced
| 374:f3146d40c2a1 | 375:d1276004eec9 |
|---|---|
| 362 (* begin thide *) | 362 (* begin thide *) |
| 363 Theorem arith_comm' : forall ls1 ls2 : list nat, | 363 Theorem arith_comm' : forall ls1 ls2 : list nat, |
| 364 length ls1 = length ls2 \/ length ls1 + length ls2 = 6 | 364 length ls1 = length ls2 \/ length ls1 + length ls2 = 6 |
| 365 -> length (ls1 ++ ls2) = 6 \/ length ls1 = length ls2. | 365 -> length (ls1 ++ ls2) = 6 \/ length ls1 = length ls2. |
| 366 (* begin hide *) | 366 (* begin hide *) |
| 367 Hint Rewrite app_length : cpdt. | 367 Hint Rewrite app_length. |
| 368 (* end hide *) | 368 (* end hide *) |
| 369 (** %\hspace{.075in}%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [app_length : cpdt.] *) | 369 (** %\hspace{.075in}%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [app_length.] *) |
| 370 | 370 |
| 371 crush. | 371 crush. |
| 372 Qed. | 372 Qed. |
| 373 (* end thide *) | 373 (* end thide *) |
| 374 | 374 |
| 635 (** %\coqdockw{%#<tt>#constructor#</tt>#%}%[; ]%\coqdockw{%#<tt>#constructor#</tt>#%}%[; ]%\coqdockw{%#<tt>#constructor#</tt>#%}%[.]%\vspace{-.075in}% *) | 635 (** %\coqdockw{%#<tt>#constructor#</tt>#%}%[; ]%\coqdockw{%#<tt>#constructor#</tt>#%}%[; ]%\coqdockw{%#<tt>#constructor#</tt>#%}%[.]%\vspace{-.075in}% *) |
| 636 | 636 |
| 637 (* end thide *) | 637 (* end thide *) |
| 638 Qed. | 638 Qed. |
| 639 | 639 |
| 640 (** It is not hard to see that sequences of constructor applications like the above can get tedious. We can avoid them using Coq's hint facility, with a new [Hint] variant that asks to consider all constructors of an inductive type during proof search. Note that this sort of hint may be placed in a default database, such that a command has no equivalent to the [: cpdt] from our earlier rewrite hints.%\index{Hint Constructirs}% The tactic %\index{tactics!auto}%[auto] performs exhaustive proof search up to a fixed depth, considering only the proof steps we have registered as hints. *) | 640 (** It is not hard to see that sequences of constructor applications like the above can get tedious. We can avoid them using Coq's hint facility, with a new [Hint] variant that asks to consider all constructors of an inductive type during proof search. The tactic %\index{tactics!auto}%[auto] performs exhaustive proof search up to a fixed depth, considering only the proof steps we have registered as hints. *) |
| 641 | 641 |
| 642 (* begin thide *) | 642 (* begin thide *) |
| 643 (* begin hide *) | 643 (* begin hide *) |
| 644 Hint Constructors even. | 644 Hint Constructors even. |
| 645 (* end hide *) | 645 (* end hide *) |
| 870 Restart. | 870 Restart. |
| 871 (* end hide *) | 871 (* end hide *) |
| 872 (** %\hspace{-.075in}\coqdockw{%#<tt>#Restart#</tt>#%}%[.] *) | 872 (** %\hspace{-.075in}\coqdockw{%#<tt>#Restart#</tt>#%}%[.] *) |
| 873 | 873 |
| 874 (* begin hide *) | 874 (* begin hide *) |
| 875 Hint Rewrite <- plus_n_Sm : cpdt. | 875 Hint Rewrite <- plus_n_Sm. |
| 876 (* end hide *) | 876 (* end hide *) |
| 877 (** %\hspace{-.075in}%[Hint] %\noindent\coqdockw{%#<tt>#Rewrite#</tt>#%}% [<- plus_n_sm : cpdt.] *) | 877 (** %\hspace{-.075in}%[Hint] %\noindent\coqdockw{%#<tt>#Rewrite#</tt>#%}% [<- plus_n_sm.] *) |
| 878 | 878 |
| 879 induction 1; crush; | 879 induction 1; crush; |
| 880 match goal with | 880 match goal with |
| 881 | [ H : S ?N = ?N0 + ?N0 |- _ ] => destruct N; destruct N0 | 881 | [ H : S ?N = ?N0 + ?N0 |- _ ] => destruct N; destruct N0 |
| 882 end; crush; eauto. | 882 end; crush; eauto. |