Imported Upstream version 8.0pl1upstream/8.0pl1

10 files changed, 927 insertions, 0 deletions

diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
new file mode 100644
index 00000000..a3f16888
--- /dev/null
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*  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: Disjoint_Union.v,v 1.9.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+(** Author: Cristina Cornes
+    From : Constructing Recursion Operators in Type Theory                 
+           L. Paulson  JSC (1986) 2, 325-355 *) 
+
+Require Import Relation_Operators.
+
+Section Wf_Disjoint_Union.
+Variables A B : Set.
+Variable leA : A -> A -> Prop.
+Variable leB : B -> B -> Prop.
+
+Notation Le_AsB := (le_AsB A B leA leB).
+
+Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
+Proof.
+ induction 1.
+ apply Acc_intro; intros y H2.
+ inversion_clear H2.
+ auto with sets.
+Qed.
+
+Lemma acc_B_sum :
+ well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
+Proof.
+ induction 2.
+ apply Acc_intro; intros y H3.
+ inversion_clear H3; auto with sets.
+ apply acc_A_sum; auto with sets.
+Qed.
+
+
+Lemma wf_disjoint_sum :
+ well_founded leA -> well_founded leB -> well_founded Le_AsB.
+Proof.
+ intros.
+ unfold well_founded in |- *.
+ destruct a as [a| b].
+ apply (acc_A_sum a).
+ apply (H a).
+
+ apply (acc_B_sum H b).
+ apply (H0 b).
+Qed.
+
+End Wf_Disjoint_Union.
\ No newline at end of file
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
new file mode 100644
index 00000000..1677659c
--- /dev/null
+++ b/theories/Wellfounded/Inclusion.v
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*  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: Inclusion.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+(** Author: Bruno Barras *)
+
+Require Import Relation_Definitions.
+
+Section WfInclusion.
+  Variable A : Set.
+  Variables R1 R2 : A -> A -> Prop.
+
+  Lemma Acc_incl : inclusion A R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.
+  Proof.
+    induction 2.
+    apply Acc_intro; auto with sets.
+  Qed.
+
+  Hint Resolve Acc_incl.
+
+  Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
+  Proof.
+    unfold well_founded in |- *; auto with sets.
+  Qed.
+
+End WfInclusion.
\ No newline at end of file
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
new file mode 100644
index 00000000..f2cf1d2e
--- /dev/null
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*  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: Inverse_Image.v,v 1.10.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+(** Author: Bruno Barras *)
+
+Section Inverse_Image.
+
+  Variables A B : Set.
+  Variable R : B -> B -> Prop.
+  Variable f : A -> B.
+
+  Let Rof (x y:A) : Prop := R (f x) (f y).
+
+  Remark Acc_lemma : forall y:B, Acc R y -> forall x:A, y = f x -> Acc Rof x.
+    induction 1 as [y _ IHAcc]; intros x H.
+    apply Acc_intro; intros y0 H1.
+    apply (IHAcc (f y0)); try trivial.
+    rewrite H; trivial.
+  Qed.
+
+  Lemma Acc_inverse_image : forall x:A, Acc R (f x) -> Acc Rof x.
+    intros; apply (Acc_lemma (f x)); trivial.
+  Qed.
+
+  Theorem wf_inverse_image : well_founded R -> well_founded Rof.
+    red in |- *; intros; apply Acc_inverse_image; auto.
+  Qed.
+
+  Variable F : A -> B -> Prop.
+  Let RoF (x y:A) : Prop :=
+     exists2 b : B, F x b & (forall c:B, F y c -> R b c).
+
+Lemma Acc_inverse_rel : forall b:B, Acc R b -> forall x:A, F x b -> Acc RoF x.
+induction 1 as [x _ IHAcc]; intros x0 H2.
+constructor; intros y H3.
+destruct H3.
+apply (IHAcc x1); auto.
+Qed.
+
+
+Theorem wf_inverse_rel : well_founded R -> well_founded RoF.
+    red in |- *; constructor; intros.
+    case H0; intros.
+    apply (Acc_inverse_rel x); auto.
+Qed.
+
+End Inverse_Image.
+
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
new file mode 100644
index 00000000..d8a4d37c
--- /dev/null
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -0,0 +1,374 @@
+(************************************************************************)
+(*  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: Lexicographic_Exponentiation.v,v 1.10.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+(** Author: Cristina Cornes
+
+    From : Constructing Recursion Operators in Type Theory                
+           L. Paulson  JSC (1986) 2, 325-355  *)
+
+Require Import Eqdep.
+Require Import List.
+Require Import Relation_Operators.
+Require Import Transitive_Closure.
+
+Section Wf_Lexicographic_Exponentiation.
+Variable A : Set.
+Variable leA : A -> A -> Prop.
+
+Notation Power := (Pow A leA).
+Notation Lex_Exp := (lex_exp A leA).
+Notation ltl := (Ltl A leA).
+Notation Descl := (Desc A leA).
+
+Notation List := (list A).
+Notation Nil := (nil (A:=A)).
+(* useless but symmetric *)
+Notation Cons := (cons (A:=A)).
+Notation "<< x , y >>" := (exist Descl x y) (at level 0, x, y at level 100).
+
+Hint Resolve d_one d_nil t_step.
+
+Lemma left_prefix : forall x y z:List, ltl (x ++ y) z -> ltl x z.
+Proof.
+ simple induction x.
+ simple induction z.
+ simpl in |- *; intros H.
+ inversion_clear H. 
+ simpl in |- *; intros; apply (Lt_nil A leA).
+ intros a l HInd.
+ simpl in |- *.
+ intros.
+ inversion_clear H.
+ apply (Lt_hd A leA); auto with sets.
+ apply (Lt_tl A leA).
+ apply (HInd y y0); auto with sets.
+Qed.
+
+
+Lemma right_prefix :
+ forall x y z:List,
+   ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z).
+Proof.
+ intros x y; generalize x.
+ elim y; simpl in |- *.
+ right.
+ exists x0; auto with sets.
+ intros.
+ inversion H0.
+ left; apply (Lt_nil A leA).
+ left; apply (Lt_hd A leA); auto with sets.
+ generalize (H x1 z H3).
+ simple induction 1.
+ left; apply (Lt_tl A leA); auto with sets.
+ simple induction 1.
+ simple induction 1; intros.
+ rewrite H8.
+ right; exists x2; auto with sets.
+Qed.
+
+
+
+Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x.
+Proof.
+ intros.
+ inversion H.
+ generalize (app_cons_not_nil _ _ _ H1); simple induction 1. 
+ cut (x ++ Cons a Nil = Cons x0 Nil); auto with sets.
+ intro.
+ generalize (app_eq_unit _ _ H0).
+ simple induction 1; simple induction 1; intros.
+ rewrite H4; auto with sets.
+ discriminate H5.
+ generalize (app_inj_tail _ _ _ _ H0).
+ simple induction 1; intros.
+ rewrite <- H4; auto with sets.
+Qed.
+
+Lemma desc_tail :
+ forall (x:List) (a b:A),
+   Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b.
+Proof.
+ intro.
+ apply rev_ind with
+  (A := A)
+  (P := fun x:List =>
+          forall a b:A,
+            Descl (Cons b (x ++ Cons a Nil)) -> clos_trans A leA a b).
+ intros.
+
+ inversion H.
+ cut (Cons b (Cons a Nil) = (Nil ++ Cons b Nil) ++ Cons a Nil);
+  auto with sets; intro.
+ generalize H0.
+ intro.
+ generalize (app_inj_tail (l ++ Cons y Nil) (Nil ++ Cons b Nil) _ _ H4);
+  simple induction 1.
+ intros.
+
+ generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros.
+ generalize H1.
+ rewrite <- H10; rewrite <- H7; intro.
+ apply (t_step A leA); auto with sets.
+
+
+
+ intros.
+ inversion H0.
+ generalize (app_cons_not_nil _ _ _ H3); intro.
+ elim H1.
+
+ generalize H0.
+ generalize (app_comm_cons (l ++ Cons x0 Nil) (Cons a Nil) b);
+  simple induction 1.
+ intro.
+ generalize (desc_prefix (Cons b (l ++ Cons x0 Nil)) a H5); intro.
+ generalize (H x0 b H6).
+ intro.
+ apply t_trans with (A := A) (y := x0); auto with sets.
+
+ apply t_step.
+ generalize H1.
+ rewrite H4; intro.
+
+ generalize (app_inj_tail _ _ _ _ H8); simple induction 1.
+ intros.
+ generalize H2; generalize (app_comm_cons l (Cons x0 Nil) b).
+ intro.
+ generalize H10.
+ rewrite H12; intro.
+ generalize (app_inj_tail _ _ _ _ H13); simple induction 1.
+ intros.
+ rewrite <- H11; rewrite <- H16; auto with sets.
+Qed.
+
+
+Lemma dist_aux :
+ forall z:List, Descl z -> forall x y:List, z = x ++ y -> Descl x /\ Descl y.
+Proof.
+ intros z D.
+ elim D.
+ intros.
+ cut (x ++ y = Nil); auto with sets; intro.
+ generalize (app_eq_nil _ _ H0); simple induction 1.
+ intros.
+ rewrite H2; rewrite H3; split; apply d_nil.
+
+ intros.
+ cut (x0 ++ y = Cons x Nil); auto with sets.
+ intros E.
+ generalize (app_eq_unit _ _ E); simple induction 1.
+ simple induction 1; intros.
+ rewrite H2; rewrite H3; split.
+ apply d_nil.
+
+ apply d_one.
+
+ simple induction 1; intros.
+ rewrite H2; rewrite H3; split.
+ apply d_one.
+
+ apply d_nil.
+
+ do 5 intro.
+ intros Hind.
+ do 2 intro.
+ generalize x0.
+ apply rev_ind with
+  (A := A)
+  (P := fun y0:List =>
+          forall x0:List,
+            (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ y0 ->
+            Descl x0 /\ Descl y0).
+
+ intro.
+ generalize (app_nil_end x1); simple induction 1; simple induction 1.
+ split. apply d_conc; auto with sets.
+
+ apply d_nil.
+
+ do 3 intro.
+ generalize x1.
+ apply rev_ind with
+  (A := A)
+  (P := fun l0:List =>
+          forall (x1:A) (x0:List),
+            (l ++ Cons y Nil) ++ Cons x Nil = x0 ++ l0 ++ Cons x1 Nil ->
+            Descl x0 /\ Descl (l0 ++ Cons x1 Nil)).
+
+
+ simpl in |- *.
+ split.
+ generalize (app_inj_tail _ _ _ _ H2); simple induction 1.
+ simple induction 1; auto with sets.
+
+ apply d_one.
+ do 5 intro.
+ generalize (app_ass x4 (l1 ++ Cons x2 Nil) (Cons x3 Nil)).
+ simple induction 1.
+ generalize (app_ass x4 l1 (Cons x2 Nil)); simple induction 1.
+ intro E.
+ generalize (app_inj_tail _ _ _ _ E).
+ simple induction 1; intros.
+ generalize (app_inj_tail _ _ _ _ H6); simple induction 1; intros.
+ rewrite <- H7; rewrite <- H10; generalize H6.
+ generalize (app_ass x4 l1 (Cons x2 Nil)); intro E1.
+ rewrite E1.
+ intro.
+ generalize (Hind x4 (l1 ++ Cons x2 Nil) H11).
+ simple induction 1; split.
+ auto with sets.
+
+ generalize H14.
+ rewrite <- H10; intro.
+ apply d_conc; auto with sets.
+Qed.
+
+
+
+Lemma dist_Desc_concat :
+ forall x y:List, Descl (x ++ y) -> Descl x /\ Descl y.
+Proof.
+  intros.
+  apply (dist_aux (x ++ y) H x y); auto with sets.
+Qed.
+
+
+Lemma desc_end :
+ forall (a b:A) (x:List),
+   Descl (x ++ Cons a Nil) /\ ltl (x ++ Cons a Nil) (Cons b Nil) ->
+   clos_trans A leA a b. 
+
+Proof.
+ intros a b x.
+ case x.
+ simpl in |- *.
+ simple induction 1.
+ intros.
+ inversion H1; auto with sets.
+ inversion H3.
+
+ simple induction 1.
+ generalize (app_comm_cons l (Cons a Nil) a0).
+ intros E; rewrite <- E; intros.
+ generalize (desc_tail l a a0 H0); intro.
+ inversion H1.
+ apply t_trans with (y := a0); auto with sets.
+
+ inversion H4.
+Qed.
+
+
+
+
+Lemma ltl_unit :
+ forall (x:List) (a b:A),
+   Descl (x ++ Cons a Nil) ->
+   ltl (x ++ Cons a Nil) (Cons b Nil) -> ltl x (Cons b Nil).
+Proof.
+ intro.
+ case x.
+ intros; apply (Lt_nil A leA).
+
+ simpl in |- *; intros.
+ inversion_clear H0.
+ apply (Lt_hd A leA a b); auto with sets.
+ 
+ inversion_clear H1.
+Qed.
+
+
+Lemma acc_app :
+ forall (x1 x2:List) (y1:Descl (x1 ++ x2)),
+   Acc Lex_Exp << x1 ++ x2, y1 >> ->
+   forall (x:List) (y:Descl x), ltl x (x1 ++ x2) -> Acc Lex_Exp << x, y >>.
+Proof.
+ intros.
+ apply (Acc_inv (R:=Lex_Exp) (x:=<< x1 ++ x2, y1 >>)).
+ auto with sets.
+
+ unfold lex_exp in |- *; simpl in |- *; auto with sets.
+Qed.
+
+
+Theorem wf_lex_exp : well_founded leA -> well_founded Lex_Exp.
+Proof.
+ unfold well_founded at 2 in |- *.
+ simple induction a; intros x y.
+ apply Acc_intro.
+ simple induction y0.
+ unfold lex_exp at 1 in |- *; simpl in |- *.
+ apply rev_ind with
+  (A := A)
+  (P := fun x:List =>
+          forall (x0:List) (y:Descl x0), ltl x0 x -> Acc Lex_Exp << x0, y >>).
+ intros.
+ inversion_clear H0.
+
+ intro.
+ generalize (well_founded_ind (wf_clos_trans A leA H)).
+ intros GR.
+ apply GR with
+  (P := fun x0:A =>
+          forall l:List,
+            (forall (x1:List) (y:Descl x1),
+               ltl x1 l -> Acc Lex_Exp << x1, y >>) ->
+            forall (x1:List) (y:Descl x1),
+              ltl x1 (l ++ Cons x0 Nil) -> Acc Lex_Exp << x1, y >>).
+ intro; intros HInd; intros.
+ generalize (right_prefix x2 l (Cons x1 Nil) H1).
+ simple induction 1.
+ intro; apply (H0 x2 y1 H3).
+
+ simple induction 1.
+ intro; simple induction 1.
+ clear H4 H2.
+ intro; generalize y1; clear y1.
+ rewrite H2.
+ apply rev_ind with
+  (A := A)
+  (P := fun x3:List =>
+          forall y1:Descl (l ++ x3),
+            ltl x3 (Cons x1 Nil) -> Acc Lex_Exp << l ++ x3, y1 >>).
+ intros.
+ generalize (app_nil_end l); intros Heq.
+ generalize y1.
+ clear y1.
+ rewrite <- Heq.
+ intro.
+ apply Acc_intro.
+ simple induction y2.
+ unfold lex_exp at 1 in |- *.
+ simpl in |- *; intros x4 y3. intros.
+ apply (H0 x4 y3); auto with sets.
+
+ intros. 
+ generalize (dist_Desc_concat l (l0 ++ Cons x4 Nil) y1).
+ simple induction 1.
+ intros.
+ generalize (desc_end x4 x1 l0 (conj H8 H5)); intros.
+ generalize y1.
+ rewrite <- (app_ass l l0 (Cons x4 Nil)); intro.
+ generalize (HInd x4 H9 (l ++ l0)); intros HInd2.
+ generalize (ltl_unit l0 x4 x1 H8 H5); intro.
+ generalize (dist_Desc_concat (l ++ l0) (Cons x4 Nil) y2).
+ simple induction 1; intros.
+ generalize (H4 H12 H10); intro.
+ generalize (Acc_inv H14).
+ generalize (acc_app l l0 H12 H14).
+ intros f g.
+ generalize (HInd2 f); intro.
+ apply Acc_intro.
+ simple induction y3.
+ unfold lex_exp at 1 in |- *; simpl in |- *; intros.
+ apply H15; auto with sets.
+Qed.
+
+
+End Wf_Lexicographic_Exponentiation.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
new file mode 100644
index 00000000..8ac178fc
--- /dev/null
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -0,0 +1,192 @@
+(************************************************************************)
+(*  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: Lexicographic_Product.v,v 1.12.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+(** Authors: Bruno Barras, Cristina Cornes *)
+
+Require Import Eqdep.
+Require Import Relation_Operators.
+Require Import Transitive_Closure.
+
+(**  From : Constructing Recursion Operators in Type Theory            
+     L. Paulson  JSC (1986) 2, 325-355 *)
+
+Section WfLexicographic_Product.
+Variable A : Set.
+Variable B : A -> Set.
+Variable leA : A -> A -> Prop.
+Variable leB : forall x:A, B x -> B x -> Prop.
+
+Notation LexProd := (lexprod A B leA leB).
+
+Hint Resolve t_step Acc_clos_trans wf_clos_trans.
+
+Lemma acc_A_B_lexprod :
+ forall x:A,
+   Acc leA x ->
+   (forall x0:A, clos_trans A leA x0 x -> well_founded (leB x0)) ->
+   forall y:B x, Acc (leB x) y -> Acc LexProd (existS B x y).
+Proof.
+ induction 1 as [x _ IHAcc]; intros H2 y.
+ induction 1 as [x0 H IHAcc0]; intros.
+ apply Acc_intro.
+ destruct y as [x2 y1]; intro H6.
+ simple inversion H6; intro.
+ cut (leA x2 x); intros.
+ apply IHAcc; auto with sets.
+ intros.
+ apply H2.
+ apply t_trans with x2; auto with sets.
+
+ red in H2.
+ apply H2.
+ auto with sets.
+
+ injection H1.
+ destruct 2.
+ injection H3.
+ destruct 2; auto with sets.
+
+ rewrite <- H1.
+ injection H3; intros _ Hx1.
+ subst x1.
+ apply IHAcc0.
+ elim inj_pair2 with A B x y' x0; assumption.
+Qed.
+
+Theorem wf_lexprod :
+ well_founded leA ->
+ (forall x:A, well_founded (leB x)) -> well_founded LexProd.
+Proof.
+ intros wfA wfB; unfold well_founded in |- *.
+ destruct a.
+ apply acc_A_B_lexprod; auto with sets; intros.
+ red in wfB.
+ auto with sets.
+Qed.
+
+
+End WfLexicographic_Product.
+
+
+Section Wf_Symmetric_Product.
+  Variable A : Set.
+  Variable B : Set.
+  Variable leA : A -> A -> Prop.
+  Variable leB : B -> B -> Prop.
+
+  Notation Symprod := (symprod A B leA leB).
+
+(*i
+  Local sig_prod:=
+         [x:A*B]<{_:A&B}>Case x of [a:A][b:B](existS A [_:A]B a b) end.
+
+Lemma incl_sym_lexprod: (included (A*B) Symprod  
+            (R_o_f (A*B) {_:A&B} sig_prod (lexprod A [_:A]B leA [_:A]leB))).
+Proof.
+ Red.
+ Induction x.
+ (Induction y1;Intros).
+ Red.
+ Unfold sig_prod .
+ Inversion_clear H.
+ (Apply left_lex;Auto with sets).
+
+ (Apply right_lex;Auto with sets).
+Qed.
+i*)
+
+  Lemma Acc_symprod :
+   forall x:A, Acc leA x -> forall y:B, Acc leB y -> Acc Symprod (x, y).
+ Proof.
+ induction 1 as [x _ IHAcc]; intros y H2.
+ induction H2 as [x1 H3 IHAcc1].
+ apply Acc_intro; intros y H5.
+ inversion_clear H5; auto with sets.
+ apply IHAcc; auto.
+ apply Acc_intro; trivial.
+Qed.
+
+
+Lemma wf_symprod :
+ well_founded leA -> well_founded leB -> well_founded Symprod.
+Proof.
+ red in |- *.
+ destruct a.
+ apply Acc_symprod; auto with sets.
+Qed.
+
+End Wf_Symmetric_Product.
+
+
+Section Swap.
+
+  Variable A : Set.
+  Variable R : A -> A -> Prop.
+
+  Notation SwapProd := (swapprod A R).
+
+
+  Lemma swap_Acc : forall x y:A, Acc SwapProd (x, y) -> Acc SwapProd (y, x).
+Proof.
+ intros.
+ inversion_clear H.
+ apply Acc_intro.
+ destruct y0; intros.
+ inversion_clear H; inversion_clear H1; apply H0.
+ apply sp_swap.
+ apply right_sym; auto with sets.
+
+ apply sp_swap.
+ apply left_sym; auto with sets.
+
+ apply sp_noswap.
+ apply right_sym; auto with sets.
+
+ apply sp_noswap.
+ apply left_sym; auto with sets.
+Qed.
+
+
+  Lemma Acc_swapprod :
+   forall x y:A, Acc R x -> Acc R y -> Acc SwapProd (x, y).
+Proof.
+ induction 1 as [x0 _ IHAcc0]; intros H2.
+ cut (forall y0:A, R y0 x0 -> Acc SwapProd (y0, y)).
+ clear IHAcc0.
+ induction H2 as [x1 _ IHAcc1]; intros H4.
+ cut (forall y:A, R y x1 -> Acc SwapProd (x0, y)).
+ clear IHAcc1.
+ intro.
+ apply Acc_intro.
+ destruct y; intro H5.
+ inversion_clear H5.
+ inversion_clear H0; auto with sets.
+
+ apply swap_Acc.
+ inversion_clear H0; auto with sets.
+
+ intros.
+ apply IHAcc1; auto with sets; intros.
+ apply Acc_inv with (y0, x1); auto with sets.
+ apply sp_noswap.
+ apply right_sym; auto with sets.
+
+ auto with sets.
+Qed.
+
+
+  Lemma wf_swapprod : well_founded R -> well_founded SwapProd.
+Proof.
+ red in |- *.
+ destruct a; intros.
+ apply Acc_swapprod; auto with sets.
+Qed.
+
+End Swap.
\ No newline at end of file
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
new file mode 100644
index 00000000..2e9d497b
--- /dev/null
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -0,0 +1,47 @@
+(************************************************************************)
+(*  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: Transitive_Closure.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+(** Author: Bruno Barras *)
+
+Require Import Relation_Definitions.
+Require Import Relation_Operators.
+
+Section Wf_Transitive_Closure.
+  Variable A : Set.
+  Variable R : relation A.
+
+  Notation trans_clos := (clos_trans A R).
+ 
+  Lemma incl_clos_trans : inclusion A R trans_clos.
+    red in |- *; auto with sets.
+  Qed.
+
+  Lemma Acc_clos_trans : forall x:A, Acc R x -> Acc trans_clos x.
+    induction 1 as [x0 _ H1].
+    apply Acc_intro.
+    intros y H2.
+    induction H2; auto with sets.
+    apply Acc_inv with y; auto with sets.
+  Qed.
+
+  Hint Resolve Acc_clos_trans.
+
+  Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y.
+  Proof.
+    induction 1 as [| x y]; auto with sets.
+    intro; apply Acc_inv with y; assumption.
+  Qed.
+
+  Theorem wf_clos_trans : well_founded R -> well_founded trans_clos.
+  Proof.
+    unfold well_founded in |- *; auto with sets.
+  Qed.
+
+End Wf_Transitive_Closure.
\ No newline at end of file
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
new file mode 100644
index 00000000..8f31ce9f
--- /dev/null
+++ b/theories/Wellfounded/Union.v
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  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: Union.v,v 1.9.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+(** Author: Bruno Barras *)
+
+Require Import Relation_Operators.
+Require Import Relation_Definitions.
+Require Import Transitive_Closure.
+
+Section WfUnion.
+  Variable A : Set.
+  Variables R1 R2 : relation A.
+  
+ Notation Union := (union A R1 R2).
+
+ Hint Resolve Acc_clos_trans wf_clos_trans.
+
+Remark strip_commut :
+ commut A R1 R2 ->
+ forall x y:A,
+   clos_trans A R1 y x ->
+   forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & clos_trans A R1 z y'.
+Proof.
+ induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros.
+ elim H with y x z; auto with sets; intros x0 H2 H3.
+ exists x0; auto with sets.
+
+ elim IH1 with z0; auto with sets; intros.
+ elim IH2 with x0; auto with sets; intros.
+ exists x1; auto with sets.
+ apply t_trans with x0; auto with sets.
+Qed.
+
+
+  Lemma Acc_union :
+   commut A R1 R2 ->
+   (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a.
+Proof.
+ induction 3 as [x H1 H2].
+ apply Acc_intro; intros.
+ elim H3; intros; auto with sets.
+ cut (clos_trans A R1 y x); auto with sets.
+ elimtype (Acc (clos_trans A R1) y); intros.
+ apply Acc_intro; intros.
+ elim H8; intros.
+ apply H6; auto with sets.
+ apply t_trans with x0; auto with sets.
+
+ elim strip_commut with x x0 y0; auto with sets; intros.
+ apply Acc_inv_trans with x1; auto with sets.
+ unfold union in |- *.
+ elim H11; auto with sets; intros.
+ apply t_trans with y1; auto with sets.
+
+ apply (Acc_clos_trans A).
+ apply Acc_inv with x; auto with sets.
+ apply H0.
+ apply Acc_intro; auto with sets.
+Qed.
+
+
+  Theorem wf_union :
+   commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
+Proof.
+ unfold well_founded in |- *.
+ intros.
+ apply Acc_union; auto with sets.
+Qed.
+
+End WfUnion.
\ No newline at end of file
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
new file mode 100644
index 00000000..4a20c518
--- /dev/null
+++ b/theories/Wellfounded/Well_Ordering.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: Well_Ordering.v,v 1.7.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+(** Author: Cristina Cornes.
+    From: Constructing Recursion Operators in Type Theory
+    L. Paulson  JSC (1986) 2, 325-355 *)
+
+Require Import Eqdep.
+
+Section WellOrdering.
+Variable A : Set.
+Variable B : A -> Set. 
+
+Inductive WO : Set :=
+    sup : forall (a:A) (f:B a -> WO), WO.
+
+
+Inductive le_WO : WO -> WO -> Prop :=
+    le_sup : forall (a:A) (f:B a -> WO) (v:B a), le_WO (f v) (sup a f).
+ 
+
+Theorem wf_WO : well_founded le_WO.
+Proof.
+ unfold well_founded in |- *; intro.
+ apply Acc_intro.
+ elim a.
+ intros.
+ inversion H0.
+ apply Acc_intro.
+ generalize H4; generalize H1; generalize f0; generalize v.
+ rewrite H3.
+ intros.
+ apply (H v0 y0).
+ cut (f = f1).
+ intros E; rewrite E; auto.
+ symmetry  in |- *.
+ apply (inj_pair2 A (fun a0:A => B a0 -> WO) a0 f1 f H5).
+Qed.
+
+End WellOrdering.
+
+
+Section Characterisation_wf_relations.
+
+(** Wellfounded relations are the inverse image of wellordering types *)
+(*  in course of development                                          *)
+
+
+Variable A : Set.
+Variable leA : A -> A -> Prop.
+
+Definition B (a:A) := {x : A | leA x a}.
+
+Definition wof : well_founded leA -> A -> WO A B.
+Proof.
+ intros.
+ apply (well_founded_induction H (fun a:A => WO A B)); auto.
+ intros.
+ apply (sup A B x).
+ unfold B at 1 in |- *.
+ destruct 1 as [x0].
+ apply (H1 x0); auto.
+Qed.
+
+End Characterisation_wf_relations.
\ No newline at end of file
diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v
new file mode 100644
index 00000000..87c00b47
--- /dev/null
+++ b/theories/Wellfounded/Wellfounded.v
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  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: Wellfounded.v,v 1.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*)
+
+Require Export Disjoint_Union.
+Require Export Inclusion.
+Require Export Inverse_Image.
+Require Export Lexicographic_Exponentiation.
+Require Export Lexicographic_Product.
+Require Export Transitive_Closure.
+Require Export Union.
+Require Export Well_Ordering.
+
diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex
new file mode 100755
index 00000000..126071e2
--- /dev/null
+++ b/theories/Wellfounded/intro.tex
@@ -0,0 +1,4 @@
+\section{Well-founded relations}\label{Wellfounded}
+
+This library gives definitions and results about well-founded relations.
+