Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

9 files changed, 297 insertions, 185 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 6aeabe13..f71f58c6 100755..100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,19 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Datatypes.v,v 1.26.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Datatypes.v 8642 2006-03-17 10:09:02Z notin $ 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
@@ -61,7 +63,13 @@ Inductive option (A:Set) : Set :=
 
 Implicit Arguments None [A].
 
-(** [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
+Definition option_map (A B:Set) (f:A->B) o :=
+  match o with
+  | Some a => Some (f a)
+  | None => None
+  end.
+
+(** [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 bae8d4a1..cbf8d7a7 100755..100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,13 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Logic.v,v 1.29.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Logic.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Set Implicit Arguments.
 
 Require Import Notations.
 
-(** * Propositional connectives *)
+(** *** Propositional connectives *)
 
 (** [True] is the always true proposition *)
 Inductive True : Prop :=
@@ -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] *)
 
@@ -94,20 +95,28 @@ End Equivalence.
 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.
+  (at level 200, right associativity) : type_scope.
+
+(** *** 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.
 
@@ -119,19 +128,19 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x.
 (* Rule order is important to give printing priority to fully typed exists *)
 
 Notation "'exists' x , p" := (ex (fun x => p))
-  (at level 200, x ident) : type_scope.
+  (at level 200, x ident, right associativity) : type_scope.
 Notation "'exists' x : t , p" := (ex (fun x:t => p))
-  (at level 200, x ident, format "'exists'  '/  ' x  :  t ,  '/  ' p")
+  (at level 200, x ident, right associativity, 
+   format "'[' 'exists'  '/  ' x  :  t ,  '/  ' p ']'")
   : type_scope.
 
 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
-  (at level 200, x ident, p at level 200) : type_scope.
+  (at level 200, x ident, p at level 200, right associativity) : type_scope.
 Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
-  (at level 200, x ident, t at level 200, p at level 200,
-   format "'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']'")
+  (at level 200, x ident, t at level 200, p at level 200, right associativity,
+   format "'[' 'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 
-
 (** Derived rules for universal quantification *)
 
 Section universal_quantification.
@@ -151,18 +160,21 @@ Section universal_quantification.
 
 End universal_quantification.
 
-(** * Equality *)
+(** *** 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.
@@ -217,16 +229,6 @@ Section Logic_lemmas.
 
   End equality.
 
-(* Is now a primitive principle 
-  Theorem eq_rect: (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
-  Proof.
-   Intros.
-   Cut (identity A x y).
-   NewDestruct 1; Auto.
-   NewDestruct H; Auto.
-  Qed.
-*)
-
   Definition eq_ind_r :
     forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
@@ -277,3 +279,14 @@ Proof.
 Qed.
 
 Hint Immediate sym_eq sym_not_eq: core v62.
+
+(** Other notations *)
+
+Notation "'exists' ! x , P" := 
+  (exists x',  (fun x => P) x' /\ forall x'', (fun x => P) x'' -> x' = x'')
+  (at level 200, x ident, right associativity,
+   format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
+Notation "'exists' ! x : A , P" := 
+  (exists x' : A,  (fun x => P) x' /\ forall x'':A, (fun x => P) x'' -> x' = x'')
+  (at level 200, x ident, right associativity,
+   format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 0e62e842..857ffe94 100755..100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -6,18 +6,48 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Logic_Type.v,v 1.19.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Logic_Type.v 8642 2006-03-17 10:09:02Z notin $ 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/Notations.v b/theories/Init/Notations.v
index e0a18747..3ca93067 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Notations.v,v 1.24.2.2 2004/08/01 09:36:44 herbelin Exp $ i*)
+(*i $Id: Notations.v 6410 2004-12-06 11:34:35Z herbelin $ i*)
 
 (** These are the notations whose level and associativity are imposed by Coq *)
 
@@ -54,15 +54,12 @@ Reserved Notation "x ^ y" (at level 30, right associativity).
 Reserved Notation "( x , y , .. , z )" (at level 0).
 
 (** Notation "{ x }" is reserved and has a special status as component
-    of other notations; it is at level 0 to factor with {x:A|P} etc *)
+    of other notations such as "{ A } + { B }" and "A + { B }" (which
+    are at the same level than "x + y");
+    "{ x }" is at level 0 to factor with "{ x : A | P }" *)
 
 Reserved Notation "{ x }" (at level 0, x at level 99).
 
-(** Notations for sum-types *)
-
-Reserved Notation "{ A } + { B }" (at level 50, left associativity).
-Reserved Notation "A + { B }" (at level 50, left associativity).
-
 (** Notations for sigma-types or subsets *)
 
 Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 789a020f..c0416b63 100755..100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -6,9 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Peano.v,v 1.23.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Peano.v 8642 2006-03-17 10:09:02Z notin $ 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,13 +20,15 @@
     - 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.
 Require Import Logic.
+Unset Boxed Definitions.
 
 Open Scope nat_scope.
 
@@ -47,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.
@@ -54,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.
@@ -88,13 +92,14 @@ Hint Resolve n_Sn: core v62.
 Fixpoint plus (n m:nat) {struct n} : nat :=
   match n with
   | O => m
-  | S p => S (plus p m)
-  end.
+  | S p => S (p + m)
+  end
+
+where "n + m" := (plus n m) : nat_scope.
+
 Hint Resolve (f_equal2 plus): v62.
 Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
 
-Infix "+" := plus : nat_scope.
-
 Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
   induction n; simpl in |- *; auto.
@@ -122,11 +127,12 @@ Qed.
 Fixpoint mult (n m:nat) {struct n} : nat :=
   match n with
   | O => 0
-  | S p => m + mult p m
-  end.
-Hint Resolve (f_equal2 mult): core v62.
+  | S p => m + p * m
+  end
 
-Infix "*" := mult : nat_scope.
+where "n * m" := (mult n m) : nat_scope.
+
+Hint Resolve (f_equal2 mult): core v62.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
@@ -142,27 +148,25 @@ 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
   | O, _ => 0
   | S k, O => S k
-  | S k, S l => minus k l
-  end. 
+  | S k, S l => k - l
+  end
 
-Infix "-" := minus : nat_scope.
+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*)
@@ -187,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/Prelude.v b/theories/Init/Prelude.v
index 2fe520c4..5f6f1eab 100755..100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -6,11 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Prelude.v,v 1.11.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
+(*i $Id: Prelude.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Notations.
 Require Export Logic.
 Require Export Datatypes.
 Require Export Specif.
 Require Export Peano.
-Require Export Wf.
\ No newline at end of file
+Require Export Wf.
+Require Export Tactics.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 6855e689..e7fc1ac4 100755..100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -6,21 +6,21 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Specif.v,v 1.25.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Specif.v 8642 2006-03-17 10:09:02Z notin $ 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/Tactics.v b/theories/Init/Tactics.v
new file mode 100644
index 00000000..ce37715e
--- /dev/null
+++ b/theories/Init/Tactics.v
@@ -0,0 +1,72 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Tactics.v 8100 2006-02-27 12:10:03Z letouzey $ i*)
+
+Require Import Notations.
+Require Import Logic.
+
+(** Useful tactics *)
+
+(* A shorter name for generalize + clear, can be seen as an anti-intro *)
+
+Ltac revert H := generalize H; clear H.
+
+(* to contradict an hypothesis without copying its type. *)
+
+Ltac absurd_hyp h := 
+  let T := type of h in 
+  absurd T.
+
+(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
+
+Ltac swap H := intro; apply H; clear H.
+
+(* A case with no loss of information. *)
+
+Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
+
+(* A tactic for easing the use of lemmas f_equal, f_equal2, ... *)
+
+Ltac f_equal := 
+  let cg := try congruence in
+  let r := try reflexivity in 
+  match goal with 
+   | |- ?f ?a = ?f' ?a' => cut (a=a'); [cg|r]
+   | |- ?f ?a ?b = ?f' ?a' ?b' => 
+      cut (b=b');[cut (a=a');[cg|r]|r]
+   | |- ?f ?a ?b ?c = ?f' ?a' ?b' ?c'=> 
+      cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]
+   | |- ?f ?a ?b ?c ?d= ?f' ?a' ?b' ?c' ?d'=> 
+      cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]
+  | |- ?f ?a ?b ?c ?d ?e= ?f' ?a' ?b' ?c' ?d' ?e'=> 
+      cut (e=e');[cut (d=d');[cut (c=c');[cut (b=b');[cut (a=a');[cg|r]|r]|r]|r]|r]
+   | _ => idtac
+  end.
+
+(* Rewriting in all hypothesis. *)
+
+Ltac rewrite_all Eq := match type of Eq with
+  ?a = ?b =>
+     generalize Eq; clear Eq;
+     match goal with
+    | H : context [a] |- _ => intro Eq; rewrite Eq in H; rewrite_all Eq
+    | _ => intro Eq; try rewrite Eq
+    end
+ end.
+
+Ltac rewrite_all_rev Eq := match type of Eq with
+  ?a = ?b =>
+     generalize Eq; clear Eq;
+     match goal with
+    | H : context [b] |- _ => intro Eq; rewrite <- Eq in H; rewrite_all_rev Eq
+    | _ => intro Eq; try rewrite <- Eq
+    end
+ end.
+
+Tactic Notation "rewrite_all" "<-" constr(H) := rewrite_all_rev H.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 7ab3723d..fde70225 100755..100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,61 +6,59 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Set Implicit Arguments.
-
-(*i $Id: Wf.v,v 1.17.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Wf.v 8642 2006-03-17 10:09:02Z notin $ 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.
 
- Variable A : Set.
+ Variable A : Type.
  Variable R : A -> A -> Prop.
 
  (** The accessibility predicate is defined to be non-informative *)
 
- Inductive Acc : A -> Prop :=
-     Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
+ Inductive Acc (x: A) : Prop :=
+     Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
 
  Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
   destruct 1; trivial.
  Defined.
 
-  (** the informative elimination :
+  (** Informative elimination :
      [let Acc_rec F = let rec wf x = F x wf in wf] *)
 
  Section AccRecType.
   Variable P : A -> Type.
-  Variable
-    F :
-      forall x:A,
-        (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
+  Variable F : forall x:A,
+    (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
 
   Fixpoint Acc_rect (x:A) (a:Acc x) {struct a} : P x :=
-    F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (x:=y) (Acc_inv a h)).
+    F (Acc_inv a) (fun (y:A) (h:R y x) => Acc_rect (Acc_inv a h)).
 
  End AccRecType.
 
  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. 
+  Variable P : A -> Type.
   Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
 
   Fixpoint Acc_iter (x:A) (a:Acc x) {struct a} : P x :=
-    F (fun (y:A) (h:R y x) => Acc_iter (x:=y) (Acc_inv a h)).
+    F (fun (y:A) (h:R y x) => Acc_iter (Acc_inv a h)).
 
  End AccIter.
 
@@ -68,7 +66,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.
 
@@ -95,47 +93,48 @@ Section Well_founded.
 
 (** Building fixpoints  *) 
 
-Section FixPoint.
+ Section FixPoint.
 
-Variable P : A -> Set.
-Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
-
-Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
-  F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)).
+  Variable P : A -> Type.
+  Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
 
-Definition Fix (x:A) := Fix_F (Rwf x).
+  Notation Fix_F := (Acc_iter P F) (only parsing). (* alias *)
 
-(** Proof that [well_founded_induction] satisfies the fixpoint equation. 
-    It requires an extra property of the functional *)
+  Definition Fix (x:A) := Acc_iter P F (Rwf x).
 
-Hypothesis
-  F_ext :
-    forall (x:A) (f g:forall y:A, R y x -> P y),
-      (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.
+  (** Proof that [well_founded_induction] satisfies the fixpoint equation. 
+      It requires an extra property of the functional *)
 
-Scheme Acc_inv_dep := Induction for Acc Sort Prop.
+  Hypothesis
+    F_ext :
+      forall (x:A) (f g:forall y:A, R y x -> P y),
+        (forall (y:A) (p:R y x), f y p = g y p) -> F f = F g.
 
-Lemma Fix_F_eq :
- forall (x:A) (r:Acc x),
-   F (fun (y:A) (p:R y x) => Fix_F (Acc_inv r p)) = Fix_F r.
-destruct r using Acc_inv_dep; auto.
-Qed.
+  Scheme Acc_inv_dep := Induction for Acc Sort Prop.
 
-Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
-intro x; induction (Rwf x); intros.
-rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
-apply F_ext; auto.
-Qed.
+  Lemma Fix_F_eq :
+   forall (x:A) (r:Acc x),
+     F (fun (y:A) (p:R y x) => Fix_F y (Acc_inv r p)) = Fix_F x r.
+  Proof. 
+   destruct r using Acc_inv_dep; auto.
+  Qed.
 
+  Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
+  Proof.
+   intro x; induction (Rwf x); intros.
+   rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
+   apply F_ext; auto.
+  Qed.
 
-Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
-intro x; unfold Fix in |- *.
-rewrite <- (Fix_F_eq (x:=x)).
-apply F_ext; intros.
-apply Fix_F_inv.
-Qed.
+  Lemma Fix_eq : forall x:A, Fix x = F (fun (y:A) (p:R y x) => Fix y).
+  Proof.
+   intro x; unfold Fix in |- *.
+   rewrite <- (Fix_F_eq (x:=x)).
+   apply F_ext; intros.
+   apply Fix_F_inv.
+  Qed.
 
-End FixPoint.
+ End FixPoint.
 
 End Well_founded. 
 
@@ -169,3 +168,5 @@ Section Well_founded_2.
   Defined.
 
 End Well_founded_2.
+
+Notation Fix_F := Acc_iter (only parsing). (* compatibility *)