## Mercurial > cpdt > repo

### diff src/LogicProg.v @ 484:5025a401ad9e

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Last round of feedback from class at Penn

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Sun, 06 Jan 2013 16:23:26 -0500 |

parents | 1fd4109f7b31 |

children | 05c0f872a129 |

line wrap: on

line diff

--- a/src/LogicProg.v Sun Jan 06 15:19:01 2013 -0500 +++ b/src/LogicProg.v Sun Jan 06 16:23:26 2013 -0500 @@ -320,7 +320,7 @@ (** 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. *) - Example three_minus_four_zero : exists x, 1 + x = 0. + Example zero_minus_one : exists x, 1 + x = 0. Time eauto 1. (** %\vspace{-.15in}% << @@ -488,7 +488,7 @@ Hint Resolve length_O length_S. (* end thide *) -(** Let us apply these hints to prove that a [list nat] of length 2 exists. *) +(** 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.) *) Example length_is_2 : exists ls : list nat, length ls = 2. (* begin thide *) @@ -660,7 +660,7 @@ Abort. (* end thide *) -(** To help prove [eval1'], we prove an alternate version of [EvalPlus] that inserts an extra equality premise. *) +(** 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. *) (* begin thide *) Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1 @@ -815,7 +815,7 @@ 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]. 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. -All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern]. A few more examples of [Hint Extern] should illustrate more of the possibilities. *) +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. *) Theorem bool_neq : true <> false. (* begin thide *)