Ajout de commentaire coqweb

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

6 files changed, 70 insertions, 33 deletions

diff --git a/theories/Zarith/Wf_Z.v b/theories/Zarith/Wf_Z.v
index 6b015c77f..6910717b4 100644
--- a/theories/Zarith/Wf_Z.v
+++ b/theories/Zarith/Wf_Z.v
@@ -7,9 +7,9 @@ Require auxiliary.
 Require Zsyntax.
 
 (* Our purpose is to write an induction shema for {0,1,2,...}
-  similar to the nat shema (Theorem Natlike_rec). For that the
+  similar to the nat schema (Theorem [Natlike_rec]). For that the
   following implications will be used :
-
+\begin{verbatim}
  (n:nat)(Q n)==(n:nat)(P (inject_nat n)) ===> (x:Z)`x > 0) -> (P x)
 
        	     /\
@@ -22,7 +22,9 @@ Require Zsyntax.
 
       	       	       	       	<=== inject_nat_complete
 
-  Then the  diagram will be closed and the theorem proved. *)
+  Then the  diagram will be closed and the theorem proved. 
+\end{verbatim}
+*)
 
 Lemma inject_nat_complete :
   (x:Z)`0 <= x` -> (EX n:nat | x=(inject_nat n)).
diff --git a/theories/Zarith/ZArith.v b/theories/Zarith/ZArith.v
index 98294aed1..4bdcca1c5 100644
--- a/theories/Zarith/ZArith.v
+++ b/theories/Zarith/ZArith.v
@@ -1,5 +1,7 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
+
+(*s Library for manipulating integers based on binary encoding *)
 
 Require Export fast_integer.
 Require Export zarith_aux.
diff --git a/theories/Zarith/ZArith_dec.v b/theories/Zarith/ZArith_dec.v
index 78fa864e9..403c95fad 100644
--- a/theories/Zarith/ZArith_dec.v
+++ b/theories/Zarith/ZArith_dec.v
@@ -1,5 +1,5 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 Require Sumbool.
 
diff --git a/theories/Zarith/Zmisc.v b/theories/Zarith/Zmisc.v
index 8b54415fe..2aa69092a 100644
--- a/theories/Zarith/Zmisc.v
+++ b/theories/Zarith/Zmisc.v
@@ -1,9 +1,9 @@
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 (********************************************************)
 (* Module Zmisc.v :           				*)
-(* Definitions et lemmes comlementaires			*)
+(* Definitions et lemmes complementaires		*)
 (* Division euclidienne					*)
 (* Patrick Loiseleur, avril 1997			*)
 (********************************************************)
@@ -19,20 +19,21 @@ Require Bool.
 
  - logic : Logic complements.
  - numbers : a few very simple lemmas for manipulating the
-   constructors POS, NEG, ZERO and xI, xO, xH
+   constructors [POS], [NEG], [ZERO] and [xI], [xO], [xH]
  - registers : defining arrays of bits and their relation with integers.
  - iter : the n-th iterate of a function is defined for n:nat and n:positive.
    The two notions are identified and an invariant conservation theorem
    is proved.
  - recursors : Here a nat-like recursor is built.
- - arith : lemmas about < <= ?= + * ...
+ - arith : lemmas about [< <= ?= + *] ...
 
 ************************************************************************)
 
 Section logic.
 
 Lemma rename : (A:Set)(P:A->Prop)(x:A) ((y:A)(x=y)->(P y)) -> (P x).
-Auto with arith. Save.
+Auto with arith. 
+Save.
 
 End logic.
 
@@ -41,7 +42,7 @@ Section numbers.
 Definition entier_of_Z := [z:Z]Case z of Nul Pos Pos end.
 Definition Z_of_entier := [x:entier]Case x of ZERO POS end.
  
-(*** Coercion Z_of_entier : entier >-> Z. ***)
+(*i Coercion Z_of_entier : entier >-> Z. i*)
 
 Lemma POS_xI : (p:positive) (POS (xI p))=`2*(POS p) + 1`.
 Intro; Apply refl_equal.
@@ -213,10 +214,10 @@ Proof.
     (Right; Compute; Exact I) Orelse (Left; Compute; Exact I)
   | Intro p; Case p; Intros; 
     (Right; Compute; Exact I) Orelse (Left; Compute; Exact I) ].
-  (*** was 
+  (*i was 
   Realizer Zeven_bool.
   Repeat Program; Compute; Trivial.
-  ***)
+  i*)
 Save.
 
 Lemma Zeven_dec : (z:Z) { (Zeven z) }+{ ~(Zeven z) }.
@@ -227,10 +228,10 @@ Proof.
     (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) 
   | Intro p; Case p; Intros; 
     (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ].
-  (*** was 
+  (*i was 
   Realizer Zeven_bool.
   Repeat Program; Compute; Trivial.
-  ***)
+  i*)
 Save.
 
 Lemma Zodd_dec : (z:Z) { (Zodd z) }+{ ~(Zodd z) }.
@@ -241,10 +242,10 @@ Proof.
     (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) 
   | Intro p; Case p; Intros; 
     (Left; Compute; Exact I) Orelse (Right; Compute; Trivial) ].
-  (*** was 
+  (*i was 
   Realizer Zodd_bool.
   Repeat Program; Compute; Trivial.
-  ***)
+  i*)
 Save.
 
 Lemma Zeven_not_Zodd : (z:Z)(Zeven z) -> ~(Zodd z).
diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v
index e77011114..c933ebedc 100644
--- a/theories/Zarith/fast_integer.v
+++ b/theories/Zarith/fast_integer.v
@@ -1,13 +1,12 @@
+
+(*i $Id$ i*)
+
 (**************************************************************************)
-(*                                                                        *)
 (*s Binary Integers                                                       *)
 (*                                                                        *)
 (* Pierre Crégut (CNET, Lannion, France)                                  *)
-(*                                                                        *)
 (**************************************************************************)
 
-(*i $Id$ i*)
-
 Require Le.
 Require Lt.
 Require Plus.
@@ -21,10 +20,14 @@ Inductive positive : Set :=
   xI : positive -> positive
 | xO : positive -> positive
 | xH : positive.
+
 Inductive Z : Set := 
   ZERO : Z | POS : positive -> Z | NEG : positive -> Z.
+
 Inductive relation : Set := 
   EGAL :relation | INFERIEUR : relation | SUPERIEUR : relation.
+
+(*s Addition *)
 Fixpoint add_un [x:positive]:positive :=
   <positive> Cases x of
                (xI x') => (xO (add_un x'))
@@ -68,6 +71,8 @@ with add_carry [x,y:positive]:positive :=
           | xH      => (xI xH)
           end
   end.
+
+(*s From positive to natural numbers *)
 Fixpoint positive_to_nat [x:positive]:nat -> nat :=
   [pow2:nat]
     <nat> Cases x of
@@ -78,12 +83,14 @@ Fixpoint positive_to_nat [x:positive]:nat -> nat :=
 
 Definition convert := [x:positive] (positive_to_nat x (S O)).
 
+(*s From natural numbers to positive *)
 Fixpoint anti_convert [n:nat]: positive :=
   <positive> Cases n of
                 O => xH
              | (S x') => (add_un (anti_convert x'))
              end.
 
+(* Correctness of addition *)
 Lemma convert_add_un :
   (x:positive)(m:nat)
     (positive_to_nat (add_un x) m) = (plus m (positive_to_nat x m)).
@@ -133,6 +140,7 @@ Proof.
 Intros x y; Exact (add_verif x y (S O)).
 Save.
 
+(*s Correctness of conversion *)
 Theorem bij1 : (m:nat) (convert (anti_convert m)) = (S m).
 Proof.
 Induction m; [
@@ -153,6 +161,7 @@ Save.
 
 Hints Resolve compare_convert_O.
 
+(*s Subtraction *)
 Fixpoint double_moins_un [x:positive]:positive :=
   <positive>Cases x of
       (xI x') => (xI (xO x'))
@@ -249,6 +258,7 @@ Induction x; [
 | Unfold convert; Simpl; Auto with arith ].
 Save.
 
+(*s Comparison of positive *)
 Fixpoint compare [x,y:positive]: relation -> relation :=
   [r:relation] <relation> Cases x of
             (xI x') => <relation>Cases y of
@@ -431,6 +441,8 @@ Theorem convert_compare_EGAL: (x:positive)(compare x x EGAL)=EGAL.
 Induction x; Auto with arith.
 Save.
 
+(*s Natural numbers coded with positive *)
+
 Inductive entier: Set := Nul : entier | Pos : positive -> entier.
 
 Definition Un_suivi_de := 
@@ -749,6 +761,7 @@ Rewrite le_plus_minus_r; [
 | Apply lt_le_weak; Exact (compare_convert_SUPERIEUR x y H)].
 Save.
 
+(*s Addition on integers *)
 Definition Zplus := [x,y:Z]
   <Z>Cases x of
       ZERO => y
@@ -776,6 +789,8 @@ Definition Zplus := [x,y:Z]
              end
     end.
 
+(*s Opposite *)
+
 Definition Zopp := [x:Z]
  <Z>Cases x of
       ZERO => ZERO
@@ -793,6 +808,7 @@ Proof.
 Induction x; Auto with arith.
 Save.
 
+(*s Addition and opposite *)
 Theorem Zero_right: (x:Z) (Zplus x ZERO) = x.
 Proof.
 Induction x; Auto with arith.
@@ -957,9 +973,9 @@ Theorem Zplus_assoc :
   (x,y,z:Z) (Zplus x (Zplus y z))= (Zplus (Zplus x y) z).
 Proof.
 Intros x y z;Case x;Case y;Case z;Auto with arith; Intros; [
-(*  Apply weak_assoc
+(*i  Apply weak_assoc
 | Apply weak_assoc 
-| *) Rewrite (Zplus_sym (NEG p0)); Rewrite weak_assoc;
+| i*) Rewrite (Zplus_sym (NEG p0)); Rewrite weak_assoc;
   Rewrite (Zplus_sym (Zplus (POS p1) (NEG p0))); Rewrite weak_assoc;
   Rewrite (Zplus_sym (POS p1)); Trivial with arith
 | Apply Zopp_intro; Do 4 Rewrite Zopp_Zplus; 
@@ -987,6 +1003,7 @@ Proof.
 Intros; Elim H; Elim H0; Auto with arith.
 Save.
 
+(*s Addition on positive numbers *)
 Fixpoint times1 [x:positive] : (positive -> positive) -> positive -> positive:=
   [f:positive -> positive][y:positive]
   <positive> Cases x of
@@ -1012,12 +1029,14 @@ Induction x; [
 | Simpl; Intros;Rewrite <- plus_n_O; Trivial with arith ].
 Save.
 
+(*s Correctness of multiplication on positive *)
 Theorem times_convert :
   (x,y:positive) (convert (times x y)) = (mult (convert x) (convert y)).
 Proof.
 Intros x y;Unfold times; Rewrite times1_convert; Trivial with arith.
 Save.
 
+(*s Multiplication on integers *)
 Definition Zmult := [x,y:Z]
   <Z>Cases x of
       ZERO => ZERO
@@ -1111,6 +1130,7 @@ Save.
 
 Hints Resolve Zero_mult_left Zero_mult_right.
 
+(* Multiplication and Opposite *)
 Theorem Zopp_Zmult:
   (x,y:Z) (Zmult (Zopp x) y) = (Zopp (Zmult x y)).
 Proof.
@@ -1159,6 +1179,7 @@ Intros x y z; Case x; [
   Apply weak_Zmult_plus_distr_r ].
 Save.
 
+(*s Comparison on integers *)
 Definition Zcompare := [x,y:Z]
   <relation>Cases x of
       ZERO => <relation>Cases y of
diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v
index 4309d2970..5b247589f 100644
--- a/theories/Zarith/zarith_aux.v
+++ b/theories/Zarith/zarith_aux.v
@@ -1,13 +1,11 @@
+(*i $Id$ i*)
+
 (**************************************************************************)
-(*                                                                        *)
-(* Binary Integers                                                        *)
+(*s Binary Integers                                                       *)
 (*                                                                        *)
 (* Pierre Crégut (CNET, Lannion, France)                                  *)
-(*                                                                        *)
 (**************************************************************************)
 
-(* $Id$ *)
-
 Require Arith.
 Require Export fast_integer.
 
@@ -17,42 +15,53 @@ Meta Definition ElimCompare com1 com2:=
        | Intro hidden_auxiliary; Elim hidden_auxiliary; 
          Clear hidden_auxiliary ] .
 
+(*s Order relations *)
 Definition Zlt := [x,y:Z](Zcompare x y) = INFERIEUR.
 Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR.
 Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR.
 Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR.
-Definition absolu := [x:Z]
+
+(*s Absolu function *)
+Definition absolu [x:Z] : nat :=
   Cases x of
      ZERO   => O
   | (POS p) => (convert p)
   | (NEG p) => (convert p)
   end.
-Definition Zabs := [z:Z]
+
+Definition Zabs [z:Z] : Z :=
   Cases z of 
      ZERO   => ZERO
   | (POS p) => (POS p)
   | (NEG p) => (POS p)
   end.
 
+(*s Properties of absolu function *)
+
 Lemma Zabs_eq : (x:Z) (Zle ZERO x) -> (Zabs x)=x.
 Destruct x; Auto with arith.
 Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith.
 Save.
 
+(*s From nat to Z *)
 Definition inject_nat := 
   [x:nat]Cases x of
            O => ZERO
          | (S y) => (POS (anti_convert y))
          end.
+
+(*s Successor and Predecessor functions on Z *)
 Definition Zs := [x:Z](Zplus x (POS xH)).
 Definition Zpred := [x:Z](Zplus x (NEG xH)).
 
+(* Properties of the order relation *)
 Theorem Zgt_Sn_n : (n:Z)(Zgt (Zs n) n).
 
 Intros n; Unfold Zgt Zs; Pattern 2 n; Rewrite <- (Zero_right n); 
 Rewrite Zcompare_Zplus_compatible;Auto with arith.
 Save.
 
+(*s Properties of the order *)
 Theorem Zle_gt_trans : (n,m,p:Z)(Zle m n)->(Zgt m p)->(Zgt n p).
 
 Unfold Zle Zgt; Intros n m p H1 H2; (ElimCompare 'm 'n); [
@@ -657,8 +666,10 @@ Intros n m; Unfold Zs; Rewrite Zmult_plus_distr_l; Rewrite Zmult_1_n;
 Trivial with arith.
 Save.
 
-(*** Just for compatibility with previous versions ***)
-(*** Use Zmult_plus_distr_r and Zmult_plus_distr_l rather than
-  their synomymous ***)
+(* 
+  Just for compatibility with previous versions 
+  Use [Zmult_plus_distr_r] and [Zmult_plus_distr_l] rather than
+  their synomymous 
+*)
 Definition Zmult_Zplus_distr := Zmult_plus_distr_r.
 Definition Zmult_plus_distr := Zmult_plus_distr_l.