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

comparison src/LogicProg.v @ 410:b4c37245502e

Typesetting pass over LogicProg

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 08 Jun 2012 15:09:11 -0400
parents	05efde66559d
children	610568369aee

comparison

equal deleted inserted replaced

-:934945edc6b5
+:b4c37245502e
 (** 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. *)
+(** 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.) *)
 Restart.
 info auto 6.
 (** %\vspace{-.15in}%[[
 == apply PlusS; apply PlusS; apply PlusS; apply PlusS;
 ]]
 *)
 Qed.
 (* end thide *)
-(** The two key components of logic programming are %\index{backtracking}%_backtracking_ and %\index{unification}%_unification_.  To see these techniques in action, consider this further silly example.  Here our candidate proof steps will be reflexivity and quantifier instantiation. *)
+(** The two key components of logic programming are%\index{backtracking}% _backtracking_ and%\index{unification}% _unification_.  To see these techniques in action, consider this further silly example.  Here our candidate proof steps will be reflexivity and quantifier instantiation. *)
 Example seven_minus_three : exists x, x + 3 = 7.
 (* begin thide *)
 (** For explanatory purposes, let us simulate a user with minimal understanding of arithmetic.  We start by choosing an instantiation for the quantifier.  Recall that [ex_intro] is the constructor for existentially quantified formulas. *)
 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] instead, 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 segragate 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 *)
 Theorem bool_neq : true <> false.
 (* begin thide *)
 auto.
-(** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
+(** A call to [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
 Abort.
 (** 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. *)
 Theorem bool_neq : true <> false.
 auto.
 Qed.
 (* end thide *)
-(** [Extern] hints may be implemented with the full Ltac language.  This example shows a case where a hint uses a [match]. *)
+(** A [Hint Extern] may be implemented with the full Ltac language.  This example shows a case where a hint uses a [match]. *)
 Section forall_and.
 Variable A : Set.
 Variables P Q : A -> Prop.
 ]]
 <<
 User error: Bound head variable
 >>
-Coq's [auto] hint databases work as tables mapping %\index{head symbol}%_head symbols_ to lists of tactics to try.  Because of this, the constant head of an [Extern] pattern must be determinable statically.  In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P].
+Coq's [auto] hint databases work as tables mapping%\index{head symbol}% _head symbols_ to lists of tactics to try.  Because of this, the constant head of an [Extern] pattern must be determinable statically.  In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P].
 Fortunately, a more basic form of [Hint Extern] also applies.  We may simply leave out the pattern to the left of the [=>], incorporating the corresponding logic into the Ltac script. *)
 Hint Extern 1 =>
 match goal with
 intros; autorewrite with core; reflexivity.
 (* end thide *)
 Qed.
 End garden_path.
-(** remove printing * *)
 (** It can also be useful to apply the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *)
-(** printing * $*$ *)
 Lemma in_star : forall x y, f (f (f (f x))) = f (f y)
 -> f x = f (f (f y)).
 (* begin thide *)
 intros; autorewrite with core in *; assumption.

Mercurial > cpdt > repo

comparison src/LogicProg.v @ 410:b4c37245502e