Documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7042 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 129 insertions, 98 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 48f5c1497..369fd2cbd 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -8,17 +8,17 @@
 
 (*i $Id$ i*)
 
+Set Implicit Arguments.
+
 Require Import Notations.
 Require Import Logic.
 
-Set Implicit Arguments.
-
 (** [unit] is a singleton datatype with sole inhabitant [tt] *)
 
 Inductive unit : Set :=
     tt : unit.
 
-(** [bool] is the datatype of the booleans values [true] and [false] *)
+(** [bool] is the datatype of the boolean values [true] and [false] *)
 
 Inductive bool : Set :=
   | true : bool
@@ -27,7 +27,9 @@ Inductive bool : Set :=
 Add Printing If bool.
 
 (** [nat] is the datatype of natural numbers built from [O] and successor [S];
-    note that zero is the letter O, not the numeral 0 *)
+    note that the constructor name is the letter O.
+    Numbers in [nat] can be denoted using a decimal notation; 
+    e.g. [3%nat] abbreviates [S (S (S O))] *)
 
 Inductive nat : Set :=
   | O : nat
@@ -53,7 +55,7 @@ Implicit Arguments identity_ind [A].
 Implicit Arguments identity_rec [A].
 Implicit Arguments identity_rect [A].
 
-(** [option A] is the extension of A with a dummy element None *)
+(** [option A] is the extension of [A] with an extra element [None] *)
 
 Inductive option (A:Set) : Set :=
   | Some : A -> option A
@@ -67,7 +69,7 @@ Definition option_map (A B:Set) (f:A->B) o :=
   | None => None
   end.
 
-(** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
+(** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *)
 (* Syntax defined in Specif.v *)
 Inductive sum (A B:Set) : Set :=
   | inl : A -> sum A B
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index bb658c6ef..9842fa641 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -28,13 +28,6 @@ Notation "~ x" := (not x) : type_scope.
 
 Hint Unfold not: core.
 
-Inductive and (A B:Prop) : Prop :=
-    conj : A -> B -> A /\ B 
- where "A /\ B" := (and A B) : type_scope.
-
-
-Section Conjunction.
-
   (** [and A B], written [A /\ B], is the conjunction of [A] and [B]
 
       [conj p q] is a proof of [A /\ B] as soon as 
@@ -42,6 +35,13 @@ Section Conjunction.
 
       [proj1] and [proj2] are first and second projections of a conjunction *)
 
+Inductive and (A B:Prop) : Prop :=
+    conj : A -> B -> A /\ B 
+
+where "A /\ B" := (and A B) : type_scope.
+
+Section Conjunction.
+
   Variables A B : Prop.
 
   Theorem proj1 : A /\ B -> A.
@@ -61,7 +61,8 @@ End Conjunction.
 Inductive or (A B:Prop) : Prop :=
   | or_introl : A -> A \/ B
   | or_intror : B -> A \/ B 
- where "A \/ B" := (or A B) : type_scope.
+
+where "A \/ B" := (or A B) : type_scope.
 
 (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
 
@@ -96,18 +97,26 @@ Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
 Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
   (at level 200) : type_scope.
 
-(** * First-order quantifiers
-  - [ex A P], or simply [exists x, P x], expresses the existence of an 
-      [x] of type [A] which satisfies the predicate [P] ([A] is of type 
-      [Set]). This is existential quantification.
-  - [ex2 A P Q], or simply [exists2 x, P x & Q x], expresses the
-      existence of an [x] of type [A] which satisfies both the predicates
-      [P] and [Q].
-  - Universal quantification (especially first-order one) is normally 
-    written [forall x:A, P x]. For duality with existential quantification, 
-    the construction [all P] is provided too.
+(** * First-order quantifiers *)
+
+(** [ex P], or simply [exists x, P x], or also [exists x:A, P x],
+    expresses the existence of an [x] of some type [A] in [Set] which
+    satisfies the predicate [P].  This is existential quantification.
+
+    [ex2 P Q], or simply [exists2 x, P x & Q x], or also 
+    [exists2 x:A, P x & Q x], expresses the existence of an [x] of
+    type [A] which satisfies both predicates [P] and [Q].
+
+    Universal quantification is primitively written [forall x:A, Q]. By
+    symmetry with existential quantification, the construction [all P]
+    is provided too.
 *)
 
+(* Remark: [exists x, Q] denotes [ex (fun x => Q)] so that [exists x,
+   P x] is in fact equivalent to [ex (fun x => P x)] which may be not
+   convertible to [ex P] if [P] is not itself an abstraction *)
+
+
 Inductive ex (A:Type) (P:A -> Prop) : Prop :=
     ex_intro : forall x:A, P x -> ex (A:=A) P.
 
@@ -153,16 +162,19 @@ End universal_quantification.
 
 (** * Equality *)
 
-(** [eq x y], or simply [x=y], expresses the (Leibniz') equality
-    of [x] and [y]. Both [x] and [y] must belong to the same type [A].
+(** [eq x y], or simply [x=y] expresses the equality of [x] and
+    [y]. Both [x] and [y] must belong to the same type [A].
     The definition is inductive and states the reflexivity of the equality.
     The others properties (symmetry, transitivity, replacement of 
-    equals) are proved below. The type of [x] and [y] can be made explicit
-    using the notation [x = y :> A] *)
+    equals by equals) are proved below. The type of [x] and [y] can be
+    made explicit using the notation [x = y :> A]. This is Leibniz equality
+    as it expresses that [x] and [y] are equal iff every property on
+    [A] which is true of [x] is also true of [y] *)
 
 Inductive eq (A:Type) (x:A) : A -> Prop :=
     refl_equal : x = x :>A 
- where "x = y :> A" := (@eq A x y) : type_scope.
+
+where "x = y :> A" := (@eq A x y) : type_scope.
 
 Notation "x = y" := (x = y :>_) : type_scope.
 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index c8176713f..464c8071d 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -8,16 +8,46 @@
 
 (*i $Id$ i*)
 
-Set Implicit Arguments.
+(** This module defines type constructors for types in [Type]
+    ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *)
 
-(** This module defines quantification on the world [Type]
-    ([Logic.v] was defining it on the world [Set]) *)
+Set Implicit Arguments.
 
 Require Import Datatypes.
 Require Export Logic.
 
+(** Negation of a type in [Type] *)
+
 Definition notT (A:Type) := A -> False.
 
+(** Conjunction of types in [Type] *)
+
+Inductive prodT (A B:Type) : Type :=
+    pairT : A -> B -> prodT A B.
+
+Section prodT_proj.
+
+  Variables A B : Type.
+
+  Definition fstT (H:prodT A B) := match H with
+                                   | pairT x _ => x
+                                   end.
+  Definition sndT (H:prodT A B) := match H with
+                                   | pairT _ y => y
+                                   end.
+
+End prodT_proj.
+
+Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) 
+  (x:A) (y:B) : C := f (pairT x y).
+
+Definition prodT_curry (A B C:Type) (f:A -> B -> C) 
+  (p:prodT A B) : C := match p with
+                       | pairT x y => f x y
+                       end.
+
+(** Properties of [identity] *)
+
 Section identity_is_a_congruence.
 
  Variables A B : Type.
@@ -62,28 +92,4 @@ Definition identity_rect_r :
  intros A x P H y H0; case sym_id with (1 := H0); trivial.
 Defined.
 
-Inductive prodT (A B:Type) : Type :=
-    pairT : A -> B -> prodT A B.
-
-Section prodT_proj.
-
-  Variables A B : Type.
-
-  Definition fstT (H:prodT A B) := match H with
-                                   | pairT x _ => x
-                                   end.
-  Definition sndT (H:prodT A B) := match H with
-                                   | pairT _ y => y
-                                   end.
-
-End prodT_proj.
-
-Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) 
-  (x:A) (y:B) : C := f (pairT x y).
-
-Definition prodT_curry (A B C:Type) (f:A -> B -> C) 
-  (p:prodT A B) : C := match p with
-                       | pairT x y => f x y
-                       end.
-
 Hint Immediate sym_id sym_not_id: core v62.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index cd531f150..9a236b7ee 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -8,7 +8,8 @@
 
 (*i $Id$ i*)
 
-(** Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *)
+(** The type [nat] of Peano natural numbers (built from [O] and [S])
+    is defined in [Datatypes.v] *)
 
 (** This module defines the following operations on natural numbers :
     - predecessor [pred]
@@ -19,9 +20,10 @@
     - greater or equal [ge]
     - greater [gt]
 
-   This module states various lemmas and theorems about natural numbers,
-   including Peano's axioms of arithmetic (in Coq, these are in fact provable)
-   Case analysis on [nat] and induction on [nat * nat] are provided too *)
+   It states various lemmas and theorems about natural numbers,
+   including Peano's axioms of arithmetic (in Coq, these are provable).
+   Case analysis on [nat] and induction on [nat * nat] are provided too
+ *)
 
 Require Import Notations.
 Require Import Datatypes.
@@ -48,6 +50,8 @@ Proof.
   auto.
 Qed.
 
+(** Injectivity of successor *)
+
 Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
 Proof.
   intros n m H; change (pred (S n) = pred (S m)) in |- *; auto.
@@ -55,21 +59,20 @@ Qed.
 
 Hint Immediate eq_add_S: core v62.
 
-(** A consequence of the previous axioms *)
-
 Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 Proof.
   red in |- *; auto.
 Qed.
 Hint Resolve not_eq_S: core v62.
 
+(** Zero is not the successor of a number *)
+
 Definition IsSucc (n:nat) : Prop :=
   match n with
   | O => False
   | S p => True
   end.
 
-
 Theorem O_S : forall n:nat, 0 <> S n.
 Proof.
   red in |- *; intros n H.
@@ -145,7 +148,7 @@ Proof.
 Qed.
 Hint Resolve mult_n_Sm: core v62.
 
-(** Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *)
+(** Truncated subtraction: [m-n] is [0] if [n>=m] *)
 
 Fixpoint minus (n m:nat) {struct n} : nat :=
   match n, m with
@@ -159,13 +162,11 @@ where "n - m" := (minus n m) : nat_scope.
 (** Definition of the usual orders, the basic properties of [le] and [lt] 
     can be found in files Le and Lt *)
 
-(** An inductive definition to define the order *)
-
 Inductive le (n:nat) : nat -> Prop :=
-  | le_n : le n n
-  | le_S : forall m:nat, le n m -> le n (S m).
+  | le_n : n <= n
+  | le_S : forall m:nat, n <= m -> n <= S m
 
-Infix "<=" := le : nat_scope.
+where "n <= m" := (le n m) : nat_scope.
 
 Hint Constructors le: core v62.
 (*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
@@ -190,7 +191,7 @@ Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 
-(** Pattern-Matching on natural numbers *)
+(** Case analysis *)
 
 Theorem nat_case :
  forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 6df26d35d..f42749293 100755
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -8,19 +8,19 @@
 
 (*i $Id$ i*)
 
-Set Implicit Arguments.
+(** Basic specifications : sets that may contain logical information *)
 
-(** Basic specifications : Sets containing logical information *)
+Set Implicit Arguments.
 
 Require Import Notations.
 Require Import Datatypes.
 Require Import Logic.
 
-(** Subsets *)
+(** Subsets and Sigma-types *)
 
-(** [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset 
+(** [(sig A P)], or more suggestively [{x:A | P x}], denotes the subset 
     of elements of the Set [A] which satisfy the predicate [P].
-    Similarly [(sig2 A P Q)], or [{x:A | (P x) & (Q x)}], denotes the subset 
+    Similarly [(sig2 A P Q)], or [{x:A | P x & Q x}], denotes the subset 
     of elements of the Set [A] which satisfy both [P] and [Q]. *)
 
 Inductive sig (A:Set) (P:A -> Prop) : Set :=
@@ -29,8 +29,8 @@ Inductive sig (A:Set) (P:A -> Prop) : Set :=
 Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
     exist2 : forall x:A, P x -> Q x -> sig2 (A:=A) P Q.
 
-(** [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant
-    of subset where [P] is now of type [Set].
+(** [(sigS A P)], or more suggestively [{x:A & (P x)}] is a Sigma-type. 
+    It is a variant of subset where [P] is now of type [Set].
     Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
      
 Inductive sigS (A:Set) (P:A -> Set) : Set :=
@@ -57,7 +57,13 @@ Add Printing Let sigS.
 Add Printing Let sigS2.
 
 
-(** Projections of sig *)
+(** Projections of [sig]
+
+    An element [y] of a subset [{x:A & (P x)}] is the pair of an [a]
+    of type [A] and of a proof [h] that [a] satisfies [P].  Then
+    [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the
+    proof of [(P a)] *)
+
 
 Section Subset_projections.
 
@@ -76,18 +82,18 @@ Section Subset_projections.
 End Subset_projections.
 
 
-(** Projections of sigS *)
+(** Projections of [sigS]
+
+    An element [x] of a sigma-type [{y:A & P y}] is a dependent pair
+    made of an [a] of type [A] and an [h] of type [P a].  Then,
+    [(projS1 x)] is the first projection and [(projS2 x)] is the
+    second projection, the type of which depends on the [projS1]. *)
 
 Section Projections.
 
   Variable A : Set.
   Variable P : A -> Set.
 
- (** An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] of 
-     type [A] and of a proof [h] that [a] satisfies [P].
-     Then [(projS1 y)] is the witness [a]
-     and [(projS2 y)] is the proof of [(P a)] *)
-
   Definition projS1 (x:sigS P) : A := match x with
                                       | existS a _ => a
                                       end.
@@ -99,7 +105,8 @@ Section Projections.
 End Projections.
 
 
-(** Extended_booleans *)
+(** [sumbool] is a boolean type equipped with the justification of
+    their value *)
 
 Inductive sumbool (A B:Prop) : Set :=
   | left : A -> {A} + {B}
@@ -108,6 +115,9 @@ Inductive sumbool (A B:Prop) : Set :=
 
 Add Printing If sumbool.
 
+(** [sumor] is an option type equipped with the justification of why
+    it may not be a regular value *)
+
 Inductive sumor (A:Set) (B:Prop) : Set :=
   | inleft : A -> A + {B}
   | inright : B -> A + {B} 
@@ -115,12 +125,10 @@ Inductive sumor (A:Set) (B:Prop) : Set :=
 
 Add Printing If sumor.
 
-(** Choice *)
+(** Various forms of the axiom of choice for specifications *)
 
 Section Choice_lemmas.
 
-  (** The following lemmas state various forms of the axiom of choice *)
-
   Variables S S' : Set.
   Variable R : S -> S' -> Prop.
   Variable R' : S -> S' -> Set.
@@ -167,8 +175,10 @@ End Choice_lemmas.
 
  (** A result of type [(Exc A)] is either a normal value of type [A] or 
      an [error] :
-     [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)]
-     it is implemented using the option type. *) 
+
+     [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)].
+
+     It is implemented using the option type. *) 
 
 Definition Exc := option.
 Definition value := Some.
@@ -189,7 +199,7 @@ Qed.
 
 Hint Resolve left right inleft inright: core v62.
 
-(** Sigma Type at Type level [sigT] *)
+(** Sigma-type for types in [Type] *)
 
 Inductive sigT (A:Type) (P:A -> Type) : Type :=
     existT : forall x:A, P x -> sigT (A:=A) P.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 7e9f972cb..584e68657 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,21 +6,21 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Set Implicit Arguments.
-
 (*i $Id$ i*)
 
 (** This module proves the validity of
     - well-founded recursion (also called course of values)
     - well-founded induction
 
-   from a well-founded ordering on a given set *)
+    from a well-founded ordering on a given set *)
+
+Set Implicit Arguments.
 
 Require Import Notations.
 Require Import Logic.
 Require Import Datatypes.
 
-(** Well-founded induction principle on Prop *)
+(** Well-founded induction principle on [Prop] *)
 
 Section Well_founded.
 
@@ -36,7 +36,7 @@ Section Well_founded.
   destruct 1; trivial.
  Defined.
 
-  (** the informative elimination :
+  (** Informative elimination :
      [let Acc_rec F = let rec wf x = F x wf in wf] *)
 
  Section AccRecType.
@@ -53,7 +53,7 @@ Section Well_founded.
 
  Definition Acc_rec (P:A -> Set) := Acc_rect P.
 
- (** A simplified version of Acc_rec(t) *)
+ (** A simplified version of [Acc_rect] *)
 
  Section AccIter.
   Variable P : A -> Type. 
@@ -68,7 +68,7 @@ Section Well_founded.
 
  Definition well_founded := forall a:A, Acc a.
 
- (** well-founded induction on Set and Prop *)
+ (** Well-founded induction on [Set] and [Prop] *)
 
  Hypothesis Rwf : well_founded.