Certified Programming with Dependent Types: src/LogicProg.v comparison

comparison src/LogicProg.v @ 459:9fbf3b4dac29

Proofreading pass through Chapter 13

author	Adam Chlipala <adam@chlipala.net>
date	Wed, 29 Aug 2012 14:11:26 -0400
parents	0650420c127b
children	b36876d4611e

comparison

equal deleted inserted replaced

-:b750ec0a8edb
+:9fbf3b4dac29
 Error: Impossible to unify "plusR 0 ?27 ?27" with "plusR 1 3 4".
 >> *)
 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.
 Qed.
 (* end thide *)
 (** 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. *)
 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.
 (** %\vspace{-.15in}%[[
 == apply PlusS; apply PlusS; apply PlusS; apply PlusS;
 Next we demonstrate unification, which will be easier when we switch to the relational formulation of addition. *)
 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.
 (** [[
 1 subgoal
 ]]
 *)
 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.
 (* end thide *)
 (Forall_cons 1 (le_n 1)
 (Forall_cons 1 (le_n 1) (Forall_nil (fun n : nat => n >= 1)))))
 ]]
 *)
-(** 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.
 (** Another basic lemma will be helpful to guide proof search. *)
 auto.
 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.
 (* begin hide *)
 (* begin thide *)

Mercurial > cpdt > repo

comparison src/LogicProg.v @ 459:9fbf3b4dac29