Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

9 files changed, 371 insertions, 117 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 56dc7e95..e5e6fd23 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Datatypes.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Datatypes.v 11073 2008-06-08 20:24:51Z herbelin $ i*)
 
 Set Implicit Arguments.
 
@@ -26,6 +26,52 @@ Inductive bool : Set :=
 
 Add Printing If bool.
 
+Delimit Scope bool_scope with bool.
+
+Bind Scope bool_scope with bool.
+
+(** Basic boolean operators *)
+
+Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
+
+Definition orb (b1 b2:bool) : bool := if b1 then true else b2.
+
+Definition implb (b1 b2:bool) : bool := if b1 then b2 else true.
+
+Definition xorb (b1 b2:bool) : bool :=
+  match b1, b2 with
+    | true, true => false
+    | true, false => true
+    | false, true => true
+    | false, false => false
+  end.
+
+Definition negb (b:bool) := if b then false else true.
+
+Infix "||" := orb : bool_scope.
+Infix "&&" := andb : bool_scope.
+
+(*******************************)
+(** * Properties of [andb]     *)
+(*******************************)
+
+Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
+Proof.
+  destruct a; destruct b; intros; split; try (reflexivity || discriminate).
+Qed.
+Hint Resolve andb_prop: bool v62.
+
+Lemma andb_true_intro :
+  forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
+Proof.
+  destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
+Qed.
+Hint Resolve andb_true_intro: bool v62.
+
+(** Interpretation of booleans as propositions *)
+
+Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
+
 (** [nat] is the datatype of natural numbers built from [O] and successor [S];
     note that the constructor name is the letter O.
     Numbers in [nat] can be denoted using a decimal notation; 
@@ -70,7 +116,7 @@ Definition option_map (A B:Type) (f:A->B) o :=
   end.
 
 (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *)
-(* Syntax defined in Specif.v *)
+
 Inductive sum (A B:Type) : Type :=
   | inl : A -> sum A B
   | inr : B -> sum A B.
@@ -82,6 +128,7 @@ Notation "x + y" := (sum x y) : type_scope.
 
 Inductive prod (A B:Type) : Type :=
   pair : A -> B -> prod A B.
+
 Add Printing Let prod.
 
 Notation "x * y" := (prod x y) : type_scope.
@@ -135,6 +182,13 @@ Definition CompOpp (r:comparison) :=
     | Gt => Lt
   end.
 
+(** Identity *)
+
+Definition ID := forall A:Type, A -> A.
+Definition id : ID := fun A x => x.
+
+(* begin hide *)
+
 (* Compatibility *)
 
 Notation prodT := prod (only parsing).
@@ -146,3 +200,5 @@ Notation fstT := fst (only parsing).
 Notation sndT := snd (only parsing).
 Notation prodT_uncurry := prod_uncurry (only parsing).
 Notation prodT_curry := prod_curry (only parsing).
+
+(* end hide *)
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 8b487432..6a636ccc 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Logic.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Logic.v 10304 2007-11-08 17:06:32Z emakarov $ i*)
 
 Set Implicit Arguments.
 
@@ -16,10 +16,10 @@ Require Import Notations.
 
 (** [True] is the always true proposition *)
 Inductive True : Prop :=
-  I : True. 
+  I : True.
 
 (** [False] is the always false proposition *)
-Inductive False : Prop :=. 
+Inductive False : Prop :=.
 
 (** [not A], written [~A], is the negation of [A] *)
 Definition not (A:Prop) := A -> False.
@@ -30,14 +30,14 @@ Hint Unfold not: core.
 
   (** [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 
+      [conj p q] is a proof of [A /\ B] as soon as
       [p] is a proof of [A] and [q] a proof of [B]
 
       [proj1] and [proj2] are first and second projections of a conjunction *)
 
 Inductive and (A B:Prop) : Prop :=
-  conj : A -> B -> A /\ B 
-  
+  conj : A -> B -> A /\ B
+
 where "A /\ B" := (and A B) : type_scope.
 
 Section Conjunction.
@@ -60,7 +60,7 @@ End Conjunction.
 
 Inductive or (A B:Prop) : Prop :=
   | or_introl : A -> A \/ B
-  | or_intror : B -> A \/ B 
+  | or_intror : B -> A \/ B
 
 where "A \/ B" := (or A B) : type_scope.
 
@@ -89,6 +89,67 @@ Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A).
 
 End Equivalence.
 
+Hint Unfold iff: extcore.
+
+(** Some equivalences *)
+
+Theorem neg_false : forall A : Prop, ~ A <-> (A <-> False).
+Proof.
+intro A; unfold not; split.
+intro H; split; [exact H | intro H1; elim H1].
+intros [H _]; exact H.
+Qed.
+
+Theorem and_cancel_l : forall A B C : Prop,
+  (B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem and_cancel_r : forall A B C : Prop,
+  (B -> A) -> (C -> A) -> ((B /\ A <-> C /\ A) <-> (B <-> C)).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_cancel_l : forall A B C : Prop,
+  (B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_cancel_r : forall A B C : Prop,
+  (B -> ~ A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)).
+Proof.
+intros; tauto.
+Qed.
+
+(** Backward direction of the equivalences above does not need assumptions *)
+
+Theorem and_iff_compat_l : forall A B C : Prop,
+  (B <-> C) -> (A /\ B <-> A /\ C).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem and_iff_compat_r : forall A B C : Prop,
+  (B <-> C) -> (B /\ A <-> C /\ A).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_iff_compat_l : forall A B C : Prop,
+  (B <-> C) -> (A \/ B <-> A \/ C).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_iff_compat_r : forall A B C : Prop,
+  (B <-> C) -> (B \/ A <-> C \/ A).
+Proof.
+intros; tauto.
+Qed.
+
 (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
     either [P] and [Q], or [~P] and [Q] *)
 
@@ -103,7 +164,7 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
     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 
+    [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].
 
@@ -123,14 +184,14 @@ Inductive ex (A:Type) (P:A -> Prop) : Prop :=
 Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
   ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
 
-Definition all (A:Type) (P:A -> Prop) := forall x:A, P x. 
+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, right associativity) : type_scope.
 Notation "'exists' x : t , p" := (ex (fun x:t => p))
-  (at level 200, x ident, right associativity, 
+  (at level 200, x ident, right associativity,
     format "'[' 'exists'  '/  ' x  :  t ,  '/  ' p ']'")
   : type_scope.
 
@@ -165,14 +226,14 @@ End universal_quantification.
 (** [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 
+    The others properties (symmetry, transitivity, replacement of
     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 
+    refl_equal : x = x :>A
 
 where "x = y :> A" := (@eq A x y) : type_scope.
 
@@ -222,7 +283,7 @@ Section Logic_lemmas.
     Proof.
       red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
     Qed.
-    
+
     Definition sym_equal := sym_eq.
     Definition sym_not_equal := sym_not_eq.
     Definition trans_equal := trans_eq.
@@ -233,12 +294,12 @@ Section Logic_lemmas.
     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.
   Defined.
-  
+
   Definition eq_rec_r :
     forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
     intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
   Defined.
-  
+
   Definition eq_rect_r :
     forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
     intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
@@ -246,14 +307,14 @@ Section Logic_lemmas.
 End Logic_lemmas.
 
 Theorem f_equal2 :
-  forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1) 
+  forall (A1 A2 B:Type) (f:A1 -> A2 -> B) (x1 y1:A1)
     (x2 y2:A2), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2.
 Proof.
   destruct 1; destruct 1; reflexivity.
 Qed.
 
 Theorem f_equal3 :
-  forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) 
+  forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1)
     (x2 y2:A2) (x3 y3:A3),
     x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
 Proof.
@@ -261,7 +322,7 @@ Proof.
 Qed.
 
 Theorem f_equal4 :
-  forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B) 
+  forall (A1 A2 A3 A4 B:Type) (f:A1 -> A2 -> A3 -> A4 -> B)
     (x1 y1:A1) (x2 y2:A2) (x3 y3:A3) (x4 y4:A4),
     x1 = y1 -> x2 = y2 -> x3 = y3 -> x4 = y4 -> f x1 x2 x3 x4 = f y1 y2 y3 y4.
 Proof.
@@ -295,7 +356,7 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y.
 Notation "'exists' ! x , P" := (ex (unique (fun x => P)))
   (at level 200, x ident, right associativity,
     format "'[' 'exists' !  '/  ' x ,  '/  ' P ']'") : type_scope.
-Notation "'exists' ! x : A , P" := 
+Notation "'exists' ! x : A , P" :=
   (ex (unique (fun x:A => P)))
   (at level 200, x ident, right associativity,
     format "'[' 'exists' !  '/  ' x  :  A ,  '/  ' P ']'") : type_scope.
@@ -305,15 +366,47 @@ Lemma unique_existence : forall (A:Type) (P:A->Prop),
 Proof.
   intros A P; split.
   intros ((x,Hx),Huni); exists x; red; auto.
-  intros (x,(Hx,Huni)); split. 
+  intros (x,(Hx,Huni)); split.
   exists x; assumption.
   intros x' x'' Hx' Hx''; transitivity x.
   symmetry; auto.
   auto.
 Qed.
 
-(** Being inhabited *)
+(** * Being inhabited *)
+
+(** The predicate [inhabited] can be used in different contexts. If [A] is
+    thought as a type, [inhabited A] states that [A] is inhabited. If [A] is
+    thought as a computationally relevant proposition, then
+    [inhabited A] weakens [A] so as to hide its computational meaning.
+    The so-weakened proof remains computationally relevant but only in
+    a propositional context.
+*)
 
 Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.
 
 Hint Resolve inhabits: core.
+
+Lemma exists_inhabited : forall (A:Type) (P:A->Prop),
+  (exists x, P x) -> inhabited A.
+Proof.
+  destruct 1; auto.
+Qed.
+
+(** Declaration of stepl and stepr for eq and iff *)
+
+Lemma eq_stepl : forall (A : Type) (x y z : A), x = y -> x = z -> z = y.
+Proof.
+intros A x y z H1 H2. rewrite <- H2; exact H1.
+Qed.
+
+Declare Left Step eq_stepl.
+Declare Right Step trans_eq.
+
+Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
+Proof.
+intros; tauto.
+Qed.
+
+Declare Left Step iff_stepl.
+Declare Right Step iff_trans.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index dbe944b0..c4e5f6c7 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Logic_Type.v 8866 2006-05-28 16:21:04Z herbelin $ i*)
+(*i $Id: Logic_Type.v 10840 2008-04-23 21:29:34Z herbelin $ i*)
 
 (** This module defines type constructors for types in [Type]
     ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *)
@@ -32,17 +32,17 @@ Section identity_is_a_congruence.
  Lemma sym_id : identity x y -> identity y x.
  Proof.
   destruct 1; trivial.
- Qed.
+ Defined.
 
  Lemma trans_id : identity x y -> identity y z -> identity x z.
  Proof.
   destruct 2; trivial.
- Qed.
+ Defined.
 
  Lemma congr_id : identity x y -> identity (f x) (f y).
  Proof.
   destruct 1; trivial.
- Qed.
+ Defined.
 
  Lemma sym_not_id : notT (identity x y) -> notT (identity y x).
  Proof.
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 416647b4..3dc6385d 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 8866 2006-05-28 16:21:04Z herbelin $ i*)
+(*i $Id: Notations.v 11073 2008-06-08 20:24:51Z herbelin $ i*)
 
 (** These are the notations whose level and associativity are imposed by Coq *)
 
@@ -19,13 +19,13 @@ Reserved Notation "~ x" (at level 75, right associativity).
 
 (** Notations for equality and inequalities *)
 
-Reserved Notation "x = y  :> T"
+Reserved Notation "x = y  :>  T"
 (at level 70, y at next level, no associativity).
 Reserved Notation "x = y" (at level 70, no associativity).
 Reserved Notation "x = y = z"
 (at level 70, no associativity, y at next level).
 
-Reserved Notation "x <> y  :> T"
+Reserved Notation "x <> y  :>  T"
 (at level 70, y at next level, no associativity).
 Reserved Notation "x <> y" (at level 70, no associativity).
 
@@ -49,6 +49,11 @@ Reserved Notation "- x" (at level 35, right associativity).
 Reserved Notation "/ x" (at level 35, right associativity).
 Reserved Notation "x ^ y" (at level 30, right associativity).
 
+(** Notations for booleans *)
+
+Reserved Notation "x || y" (at level 50, left associativity).
+Reserved Notation "x && y" (at level 40, left associativity).
+
 (** Notations for pairs *)
 
 Reserved Notation "( x , y , .. , z )" (at level 0).
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 3df2b566..9ef63cc8 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Peano.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Peano.v 11115 2008-06-12 16:03:32Z werner $ i*)
 
 (** The type [nat] of Peano natural numbers (built from [O] and [S])
     is defined in [Datatypes.v] *)
@@ -40,7 +40,7 @@ Hint Resolve (f_equal (A:=nat)): core.
 (** The predecessor function *)
 
 Definition pred (n:nat) : nat := match n with
-                                 | O => 0
+                                 | O => n
                                  | S u => u
                                  end.
 Hint Resolve (f_equal pred): v62.
@@ -123,6 +123,11 @@ Proof.
   auto.
 Qed.
 
+(** Standard associated names *)
+
+Notation plus_0_r_reverse := plus_n_O (only parsing).
+Notation plus_succ_r_reverse := plus_n_Sm (only parsing).
+
 (** Multiplication *)
 
 Fixpoint mult (n m:nat) {struct n} : nat :=
@@ -149,12 +154,21 @@ Proof.
 Qed.
 Hint Resolve mult_n_Sm: core v62.
 
+(** Standard associated names *)
+
+Notation mult_0_r_reverse := mult_n_O (only parsing).
+Notation mult_succ_r_reverse := mult_n_Sm (only parsing).
+
 (** 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
+  | O, _ => n
+  | S k, O => n
+(*=======
+
+  | O, _ => n
+  | S k, O => S k *)
   | S k, S l => k - l
   end
 
@@ -211,5 +225,3 @@ Proof.
   induction n; auto.
   destruct m as [| n0]; auto.
 Qed.
-
-(** Notations *)
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 5f6f1eab..6492c948 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -6,12 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Prelude.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Prelude.v 10064 2007-08-08 15:32:36Z msozeau $ i*)
 
 Require Export Notations.
 Require Export Logic.
 Require Export Datatypes.
 Require Export Specif.
 Require Export Peano.
-Require Export Wf.
-Require Export Tactics.
+Require Export Coq.Init.Wf.
+Require Export Coq.Init.Tactics.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index dd2f7697..c0f5c42a 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Specif.v 8866 2006-05-28 16:21:04Z herbelin $ i*)
+(*i $Id: Specif.v 10923 2008-05-12 18:25:06Z herbelin $ i*)
 
 (** Basic specifications : sets that may contain logical information *)
 
@@ -46,12 +46,12 @@ Arguments Scope sigT [type_scope type_scope].
 Arguments Scope sigT2 [type_scope type_scope type_scope].
 
 Notation "{ x  |  P }" := (sig (fun x => P)) : type_scope.
-Notation "{ x  |  P  &  Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
+Notation "{ x  |  P  & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
 Notation "{ x : A  |  P }" := (sig (fun x:A => P)) : type_scope.
-Notation "{ x : A  |  P  &  Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
+Notation "{ x : A  |  P  & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
   type_scope.
-Notation "{ x : A  &  P }" := (sigT (fun x:A => P)) : type_scope.
-Notation "{ x : A  &  P  &  Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) :
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+Notation "{ x : A  & P  & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) :
   type_scope.
 
 Add Printing Let sig.
@@ -107,6 +107,16 @@ Section Projections.
 
 End Projections.
 
+(** [sigT] of a predicate is equivalent to [sig] *)
+
+Lemma sig_of_sigT : forall (A:Type) (P:A->Prop), sigT P -> sig P.
+Proof. destruct 1 as (x,H); exists x; trivial. Defined.
+
+Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P.
+Proof. destruct 1 as (x,H); exists x; trivial. Defined.
+
+Coercion sigT_of_sig : sig >-> sigT.
+Coercion sig_of_sigT : sigT >-> sig.
 
 (** [sumbool] is a boolean type equipped with the justification of
     their value *)
@@ -201,6 +211,7 @@ Proof.
 Qed.
 
 Hint Resolve left right inleft inright: core v62.
+Hint Resolve exist exist2 existT existT2: core.
 
 (* Compatibility *)
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index ba210dd6..afe8297e 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -6,59 +6,143 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Tactics.v 9268 2006-10-24 12:56:16Z herbelin $ i*)
+(*i $Id: Tactics.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
 
 Require Import Notations.
 Require Import Logic.
 
-(** Useful tactics *)
+(** * Useful tactics *)
+
+(** A tactic for proof by contradiction. With contradict H, 
+    -   H:~A |-  B    gives       |-  A
+    -   H:~A |- ~B    gives  H: B |-  A
+    -   H: A |-  B    gives       |- ~A
+    -   H: A |- ~B    gives  H: B |- ~A
+    -   H:False leads to a resolved subgoal.
+   Moreover, negations may be in unfolded forms, 
+   and A or B may live in Type *)
+
+Ltac contradict H :=
+  let save tac H := let x:=fresh in intro x; tac H; rename x into H
+  in 
+  let negpos H := case H; clear H 
+  in 
+  let negneg H := save negpos H
+  in
+  let pospos H := 
+    let A := type of H in (elimtype False; revert H; try fold (~A))
+  in
+  let posneg H := save pospos H
+  in 
+  let neg H := match goal with 
+   | |- (~_) => negneg H
+   | |- (_->False) => negneg H
+   | |- _ => negpos H
+  end in 
+  let pos H := match goal with 
+   | |- (~_) => posneg H
+   | |- (_->False) => posneg H
+   | |- _ => pospos H
+  end in
+  match type of H with 
+   | (~_) => neg H
+   | (_->False) => neg H
+   | _ => (elim H;fail) || pos H
+  end.
 
-(* A shorter name for generalize + clear, can be seen as an anti-intro *)
+(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
 
-Tactic Notation "revert" ne_hyp_list(l) := generalize l; clear l.
+Ltac swap H := 
+  idtac "swap is OBSOLETE: use contradict instead.";
+  intro; apply H; clear H.
 
-(* to contradict an hypothesis without copying its type. *)
+(* To contradict an hypothesis without copying its type. *)
 
-Ltac absurd_hyp h := 
-  let T := type of h in 
+Ltac absurd_hyp H := 
+  idtac "absurd_hyp is OBSOLETE: use contradict instead.";
+  let T := type of H in 
   absurd T.
 
-(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
+(* A useful complement to contradict. Here H:A while G allows to conclude ~A *)
 
-Ltac swap H := intro; apply H; clear H.
+Ltac false_hyp H G := 
+  let T := type of H in absurd T; [ apply G | assumption ].
 
 (* 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 several times everywhere *)
 
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.
 Tactic Notation "rewrite_all" "<-" constr(eq) := repeat rewrite <- eq in *.
 
-(* Keeping a copy of an expression *)
-
-Ltac remembertac x a :=
-  let x := fresh x in
-  let H := fresh "Heq" x in
-  (set (x:=a) in *; assert (H: x=a) by reflexivity; clearbody x).
-
-Tactic Notation "remember" constr(c) "as" ident(x) := remembertac x c.
+(** Tactics for applying equivalences.
+
+The following code provides tactics "apply -> t", "apply <- t",
+"apply -> t in H" and "apply <- t in H". Here t is a term whose type
+consists of nested dependent and nondependent products with an
+equivalence A <-> B as the conclusion. The tactics with "->" in their
+names apply A -> B while those with "<-" in the name apply B -> A. *)
+
+(* The idea of the tactics is to first provide a term in the context
+whose type is the implication (in one of the directions), and then
+apply it. The first idea is to produce a statement "forall ..., A ->
+B" (call this type T) and then do "assert (H : T)" for a fresh H.
+Thus, T can be proved from the original equivalence and then used to
+perform the application. However, currently in Ltac it is difficult
+to produce such T from the original formula.
+
+Therefore, we first pose the original equivalence as H. If the type of
+H is a dependent product, we create an existential variable and apply
+H to this variable. If the type of H has the form C -> D, then we do a
+cut on C. Once we eliminate all products, we split (i.e., destruct)
+the conjunction into two parts and apply the relevant one. *)
+
+Ltac find_equiv H :=
+let T := type of H in
+lazymatch T with
+| ?A -> ?B =>
+  let H1 := fresh in
+  let H2 := fresh in
+  cut A;
+  [intro H1; pose proof (H H1) as H2; clear H H1;
+   rename H2 into H; find_equiv H |
+   clear H]
+| forall x : ?t, _ =>
+  let a := fresh "a" with
+      H1 := fresh "H" in
+    evar (a : t); pose proof (H a) as H1; unfold a in H1;
+    clear a; clear H; rename H1 into H; find_equiv H
+| ?A <-> ?B => idtac
+| _ => fail "The given statement does not seem to end with an equivalence"
+end.
+
+Ltac bapply lemma todo :=
+let H := fresh in
+  pose proof lemma as H;
+  find_equiv H; [todo H; clear H | .. ].
+
+Tactic Notation "apply" "->" constr(lemma) :=
+bapply lemma ltac:(fun H => destruct H as [H _]; apply H).
+
+Tactic Notation "apply" "<-" constr(lemma) :=
+bapply lemma ltac:(fun H => destruct H as [_ H]; apply H).
+
+Tactic Notation "apply" "->" constr(lemma) "in" ident(J) :=
+bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J).
+
+Tactic Notation "apply" "<-" constr(lemma) "in" ident(J) :=
+bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
+
+(** A tactic simpler than auto that is useful for ending proofs "in one step" *)
+Tactic Notation "now" tactic(t) :=
+t;
+match goal with
+| H : _ |- _ => solve [inversion H]
+| _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split]
+| _ => fail 1 "Cannot solve this goal"
+end.
+
+(** A tactic to document or check what is proved at some point of a script *)
+Ltac now_show c := change c.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 4e0f3745..f46b2b11 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -6,12 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Wf.v 8988 2006-06-25 22:15:32Z letouzey $ i*)
+(*i $Id: Wf.v 10712 2008-03-23 11:38:38Z herbelin $ i*)
 
-(** This module proves the validity of
-    - well-founded recursion (also called course of values)
+(** * This module proves the validity of
+    - well-founded recursion (also known as course of values)
     - well-founded induction
-
     from a well-founded ordering on a given set *)
 
 Set Implicit Arguments.
@@ -40,6 +39,7 @@ Section Well_founded.
      [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.
@@ -51,17 +51,6 @@ Section Well_founded.
 
  Definition Acc_rec (P:A -> Set) := Acc_rect P.
 
- (** A simplified version of [Acc_rect] *)
-
- Section AccIter.
-  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 (Acc_inv a h)).
-
- End AccIter.
-
  (** A relation is well-founded if every element is accessible *)
 
  Definition well_founded := forall a:A, Acc a.
@@ -74,7 +63,7 @@ Section Well_founded.
   forall P:A -> Type,
     (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
  Proof.
-  intros; apply (Acc_iter P); auto.
+  intros; apply Acc_rect; auto.
  Defined.
 
  Theorem well_founded_induction :
@@ -91,16 +80,26 @@ Section Well_founded.
   exact (fun P:A -> Prop => well_founded_induction_type P).
  Defined.
 
-(** Building fixpoints  *) 
+(** Well-founded fixpoints *) 
 
  Section FixPoint.
 
   Variable P : A -> Type.
   Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
 
-  Notation Fix_F := (Acc_iter P F) (only parsing). (* alias *)
+  Fixpoint Fix_F (x:A) (a:Acc x) {struct a} : P x :=
+    F (fun (y:A) (h:R y x) => Fix_F (Acc_inv a h)).
+
+  Scheme Acc_inv_dep := Induction for Acc Sort Prop.
+
+  Lemma Fix_F_eq :
+   forall (x:A) (r:Acc x),
+     F (fun (y:A) (p:R y x) => Fix_F (x:=y) (Acc_inv r p)) = Fix_F (x:=x) r.
+  Proof. 
+   destruct r using Acc_inv_dep; auto.
+  Qed.
 
-  Definition Fix (x:A) := Acc_iter P F (Rwf x).
+  Definition Fix (x:A) := Fix_F (Rwf x).
 
   (** Proof that [well_founded_induction] satisfies the fixpoint equation. 
       It requires an extra property of the functional *)
@@ -110,16 +109,7 @@ Section Well_founded.
       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.
 
-  Scheme Acc_inv_dep := Induction for Acc Sort Prop.
-
-  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.
+  Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F r = Fix_F s.
   Proof.
    intro x; induction (Rwf x); intros.
    rewrite <- (Fix_F_eq r); rewrite <- (Fix_F_eq s); intros.
@@ -129,7 +119,7 @@ Section Well_founded.
   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)).
+   rewrite <- Fix_F_eq.
    apply F_ext; intros.
    apply Fix_F_inv.
   Qed.
@@ -138,27 +128,29 @@ Section Well_founded.
 
 End Well_founded. 
 
-(** A recursor over pairs *)
+(** Well-founded fixpoints over pairs *)
 
 Section Well_founded_2.
 
-  Variables A B : Set.
+  Variables A B : Type.
   Variable R : A * B -> A * B -> Prop.
 
   Variable P : A -> B -> Type. 
 
-  Section Acc_iter_2.
+  Section FixPoint_2.
+
   Variable
     F :
       forall (x:A) (x':B),
         (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x'.
 
-  Fixpoint Acc_iter_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} : 
+  Fixpoint Fix_F_2 (x:A) (x':B) (a:Acc R (x, x')) {struct a} : 
    P x x' :=
     F
       (fun (y:A) (y':B) (h:R (y, y') (x, x')) =>
-         Acc_iter_2 (x:=y) (x':=y') (Acc_inv a (y, y') h)).
-  End Acc_iter_2.
+         Fix_F_2 (x:=y) (x':=y') (Acc_inv a (y,y') h)).
+
+  End FixPoint_2.
 
   Hypothesis Rwf : well_founded R.
 
@@ -167,9 +159,10 @@ Section Well_founded_2.
       (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x') ->
    forall (a:A) (b:B), P a b.
   Proof.
-   intros; apply Acc_iter_2; auto.
+   intros; apply Fix_F_2; auto.
   Defined.
 
 End Well_founded_2.
 
-Notation Fix_F := Acc_iter (only parsing). (* compatibility *)
+Notation Acc_iter   := Fix_F   (only parsing). (* compatibility *)
+Notation Acc_iter_2 := Fix_F_2 (only parsing). (* compatibility *)