### changeset 392:4b1242b277b2

Typo fixes
author Adam Chlipala Fri, 20 Apr 2012 12:49:47 -0400 fd3f1057685c d40b05266306 src/Coinductive.v src/InductiveTypes.v src/Subset.v src/Universes.v 4 files changed, 11 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/src/Coinductive.v	Thu Apr 12 18:46:55 2012 -0400
+++ b/src/Coinductive.v	Fri Apr 20 12:49:47 2012 -0400
@@ -362,7 +362,7 @@

%\medskip%

-   Must we always be cautious with automation in proofs by co-induction?  Induction seems to have dual versions the same pitfalls inherent in it, and yet we avoid those pitfalls by encapsulating safe Curry-Howard recursion schemes inside named induction principles.  It turns out that we can usually do the same with %\index{co-induction principles}\emph{%#<i>#co-induction principles#</i>#%}%.  Let us take that tack here, so that we can arrive at an [induction x; crush]-style proof for [ones_eq'].
+   Must we always be cautious with automation in proofs by co-induction?  Induction seems to have dual versions of the same pitfalls inherent in it, and yet we avoid those pitfalls by encapsulating safe Curry-Howard recursion schemes inside named induction principles.  It turns out that we can usually do the same with %\index{co-induction principles}\emph{%#<i>#co-induction principles#</i>#%}%.  Let us take that tack here, so that we can arrive at an [induction x; crush]-style proof for [ones_eq'].

An induction principle is parameterized over a predicate characterizing what we mean to prove, %\emph{%#<i>#as a function of the inductive fact that we already know#</i>#%}%.  Dually, a co-induction principle ought to be parameterized over a predicate characterizing what we mean to prove, %\emph{%#<i>#as a function of the arguments to the co-inductive predicate that we are trying to prove#</i>#%}%.

@@ -378,13 +378,14 @@
Section stream_eq_coind.
Variable A : Type.
Variable R : stream A -> stream A -> Prop.
-  (** This relation generalizes the theorem we want to prove, characterizinge exactly which two arguments to [stream_eq] we want to consider. *)
+  (** This relation generalizes the theorem we want to prove, characterizing exactly which two arguments to [stream_eq] we want to consider. *)

Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2.
Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2).
-  (** Two hypotheses characterize what makes a good choice of [R]: it enforces equality of stream heads, and it is %%#<i>#hereditary#</i>#%''% in the sense that a [R] stream pair passes on %%#"#[R]-ness#"#%''% to its tails.  An established technical term for such a relation is %\index{bisimulation}\emph{%#<i>#bisimulation#</i>#%}%. *)
+  (** Two hypotheses characterize what makes a good choice of [R]: it enforces equality of stream heads, and it is %%#<i>#hereditary#</i>#%''% in the sense that an [R] stream pair passes on %%#"#[R]-ness#"#%''% to its tails.  An established technical term for such a relation is %\index{bisimulation}\emph{%#<i>#bisimulation#</i>#%}%. *)

(** Now it is straightforward to prove the principle, which says that any stream pair in [R] is equal.  The reader may wish to step through the proof script to see what is going on. *)
+
Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2.
cofix; destruct s1; destruct s2; intro.
generalize (Cons_case_hd H); intro Heq; simpl in Heq; rewrite Heq.
@@ -395,6 +396,7 @@
End stream_eq_coind.

(** To see why this proof is guarded, we can print it and verify that the one co-recursive call is an immediate argument to a constructor. *)
+
Print stream_eq_coind.

(** We omit the output and proceed to proving [ones_eq''] again.  The only bit of ingenuity is in choosing [R], and in this case the most restrictive predicate works. *)
--- a/src/InductiveTypes.v	Thu Apr 12 18:46:55 2012 -0400
+++ b/src/InductiveTypes.v	Fri Apr 20 12:49:47 2012 -0400
@@ -233,7 +233,7 @@

(** That is, to prove that a property describes all [bool]s, prove that it describes both [true] and [false].

-There is no interesting Curry-Howard analogue of [bool].  Of course, we can define such a type by replacing [Set] by [Prop] above, but the proposition we arrive it is not very useful.  It is logically equivalent to [True], but it provides two indistinguishable primitive proofs, [true] and [false].   In the rest of the chapter, we will skip commenting on Curry-Howard versions of inductive definitions where such versions are not interesting. *)
+There is no interesting Curry-Howard analogue of [bool].  Of course, we can define such a type by replacing [Set] by [Prop] above, but the proposition we arrive at is not very useful.  It is logically equivalent to [True], but it provides two indistinguishable primitive proofs, [true] and [false].   In the rest of the chapter, we will skip commenting on Curry-Howard versions of inductive definitions where such versions are not interesting. *)

(** * Simple Recursive Types *)
@@ -660,7 +660,7 @@
end.

-(** This is a just a warm-up that does not use reflexive types, the new feature we mean to introduce.  When we set our sights on first-order logic instead, it becomes very handy to give constructors recursive arguments that are functions. *)
+(** This is just a warm-up that does not use reflexive types, the new feature we mean to introduce.  When we set our sights on first-order logic instead, it becomes very handy to give constructors recursive arguments that are functions. *)

Inductive formula : Set :=
| Eq : nat -> nat -> formula
--- a/src/Subset.v	Thu Apr 12 18:46:55 2012 -0400
+++ b/src/Subset.v	Fri Apr 20 12:49:47 2012 -0400
@@ -651,7 +651,7 @@
Defined.
(* end thide *)

-(** We can build a [sumor] version of the %%#"#bind#"#%''% notation and use it to write a similarly straightforward version of this function. *)
+(** We can build a [sumor] version of the %%#"#bind#"#%''% notation and use it to write a similarly straightforward version of this function.  %The operator rendered here as $\longleftarrow$ is noted in the source as a less-than character followed by two hyphens.% *)

(** printing <-- $\longleftarrow$ *)

@@ -676,6 +676,8 @@
Defined.
(* end thide *)

+(** This example demonstrates how judicious selection of notations can hide complexities in the rich types of programs. *)
+

(** * A Type-Checking Example *)

--- a/src/Universes.v	Thu Apr 12 18:46:55 2012 -0400
+++ b/src/Universes.v	Fri Apr 20 12:49:47 2012 -0400
@@ -627,7 +627,7 @@

(** This kind of %%#"#axiomatic presentation#"#%''% of a theory is very common outside of higher-order logic.  However, in Coq, it is almost always preferable to stick to defining your objects, functions, and predicates via inductive definitions and functional programming.

-   In general, there is a significant burden associated with any use of axioms.  It is easy to assert a set of axioms that together is %\index{inconsistent axioms}\textit{%#<i>#inconsistent#</i>#%}%.   That is, a set of axioms may imply [False], which allows any theorem to proved, which defeats the purpose of a proof assistant.  For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *)
+   In general, there is a significant burden associated with any use of axioms.  It is easy to assert a set of axioms that together is %\index{inconsistent axioms}\textit{%#<i>#inconsistent#</i>#%}%.   That is, a set of axioms may imply [False], which allows any theorem to be proved, which defeats the purpose of a proof assistant.  For example, we could assert the following axiom, which is consistent by itself but inconsistent when combined with [classic]. *)

Axiom not_classic : ~ forall P : Prop, P \/ ~ P.