Mercurial > cpdt > repo
changeset 459:9fbf3b4dac29
Proofreading pass through Chapter 13
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 29 Aug 2012 14:11:26 -0400 |
parents | b750ec0a8edb |
children | 38549f152568 |
files | src/LogicProg.v |
diffstat | 1 files changed, 6 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/src/LogicProg.v Tue Aug 28 16:53:16 2012 -0400 +++ b/src/LogicProg.v Wed Aug 29 14:11:26 2012 -0400 @@ -126,7 +126,7 @@ apply PlusS. apply PlusO. -(** 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. *) +(** 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 %\index{Vernacular commands!Hint Constructors}%[Hint Constructors] to register the two candidate proof steps as hints. *) Restart. auto. @@ -149,7 +149,7 @@ auto 6. -(** 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.) *) +(** 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].) *) Restart. info auto 6. @@ -191,7 +191,7 @@ Example seven_minus_three' : exists x, plusR x 3 7. (* begin thide *) -(** 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}% _unification variables_ standing in for those parameters we wish to postpone guessing. *) +(** 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. *) eapply ex_intro. (** [[ @@ -392,7 +392,7 @@ Abort. End slow. -(** 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 segragate hints into different groups that may be called on as needed. Here we put [eq_trans] into the database [slow]. *) +(** 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]. *) (* begin thide *) Hint Resolve eq_trans : slow. @@ -559,7 +559,7 @@ ]] *) -(** 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. *) +(** 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. *) Definition sum := fold_right plus O. @@ -863,7 +863,7 @@ Qed. (* end thide *) - (** 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]. *) + (** 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]. *) End forall_and.