Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7

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

9 files changed, 937 insertions, 0 deletions

diff --git a/theories7/Wellfounded/Disjoint_Union.v b/theories7/Wellfounded/Disjoint_Union.v
new file mode 100644
index 000000000..44c2f8661
--- /dev/null
+++ b/theories7/Wellfounded/Disjoint_Union.v
@@ -0,0 +1,56 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Author: Cristina Cornes
+    From : Constructing Recursion Operators in Type Theory                 
+           L. Paulson  JSC (1986) 2, 325-355 *) 
+
+Require Relation_Operators.
+
+Section Wf_Disjoint_Union.
+Variable 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: (x:A)(Acc A leA x)->(Acc A+B Le_AsB (inl A B x)).
+Proof.
+ NewInduction 1.
+ Apply Acc_intro;Intros y H2.
+ Inversion_clear H2.
+ Auto with sets.
+Qed.
+
+Lemma acc_B_sum: (well_founded A leA) ->(x:B)(Acc B leB x)
+                        ->(Acc A+B Le_AsB (inr A B x)).
+Proof.
+ NewInduction 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 A leA) 
+    -> (well_founded B leB) -> (well_founded A+B Le_AsB).
+Proof.
+ Intros.
+ Unfold well_founded .
+ NewDestruct 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.
diff --git a/theories7/Wellfounded/Inclusion.v b/theories7/Wellfounded/Inclusion.v
new file mode 100644
index 000000000..2038b34bf
--- /dev/null
+++ b/theories7/Wellfounded/Inclusion.v
@@ -0,0 +1,33 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Author: Bruno Barras *)
+
+Require Relation_Definitions.
+
+Section WfInclusion.
+  Variable A:Set.
+  Variable R1,R2:A->A->Prop.
+
+  Lemma Acc_incl: (inclusion A R1 R2)->(z:A)(Acc A R2 z)->(Acc A R1 z).
+  Proof.
+    NewInduction 2.
+    Apply Acc_intro;Auto with sets.
+  Qed.
+
+  Hints Resolve Acc_incl.
+
+  Theorem wf_incl: 
+         (inclusion A R1 R2)->(well_founded A R2)->(well_founded A R1).
+  Proof.
+    Unfold well_founded ;Auto with sets.
+  Qed.
+
+End WfInclusion.
diff --git a/theories7/Wellfounded/Inverse_Image.v b/theories7/Wellfounded/Inverse_Image.v
new file mode 100644
index 000000000..ac828ac1a
--- /dev/null
+++ b/theories7/Wellfounded/Inverse_Image.v
@@ -0,0 +1,58 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Author: Bruno Barras *)
+
+Section Inverse_Image.
+
+  Variables A,B:Set.
+  Variable R : B->B->Prop.
+  Variable f:A->B.
+
+  Local Rof : A->A->Prop := [x,y:A](R (f x) (f y)).
+
+  Remark Acc_lemma : (y:B)(Acc B R y)->(x:A)(y=(f x))->(Acc A Rof x).
+    NewInduction 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 : (x:A)(Acc B R (f x)) -> (Acc A Rof x).
+    Intros; Apply (Acc_lemma (f x)); Trivial.
+  Qed.
+
+  Theorem wf_inverse_image: (well_founded B R)->(well_founded A Rof).
+    Red; Intros; Apply Acc_inverse_image; Auto.
+  Qed.
+
+  Variable F : A -> B -> Prop.
+  Local RoF : A -> A -> Prop := [x,y]
+    (EX b : B | (F x b) & (c:B)(F y c)->(R b c)).
+
+Lemma Acc_inverse_rel :
+   (b:B)(Acc B R b)->(x:A)(F x b)->(Acc A RoF x).
+NewInduction 1 as [x _ IHAcc]; Intros x0 H2.
+Constructor; Intros y H3.
+NewDestruct H3.
+Apply (IHAcc x1); Auto.
+Save.
+
+
+Theorem wf_inverse_rel : 
+   (well_founded B R)->(well_founded A RoF).
+    Red; Constructor; Intros.
+    Case H0; Intros.
+    Apply (Acc_inverse_rel x); Auto.
+Save.
+
+End Inverse_Image.
+
+
diff --git a/theories7/Wellfounded/Lexicographic_Exponentiation.v b/theories7/Wellfounded/Lexicographic_Exponentiation.v
new file mode 100644
index 000000000..8efa124c3
--- /dev/null
+++ b/theories7/Wellfounded/Lexicographic_Exponentiation.v
@@ -0,0 +1,386 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Author: Cristina Cornes
+
+    From : Constructing Recursion Operators in Type Theory                
+           L. Paulson  JSC (1986) 2, 325-355  *)
+
+Require Eqdep.
+Require PolyList.
+Require PolyListSyntax.
+Require Relation_Operators.
+Require 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).
+(* useless but symmetric *)
+Notation Cons := (cons 1!A).
+Notation "<< x , y >>" := (exist List Descl x y) (at level 0)
+  V8only (at level 0, x,y at level 100).
+
+V7only[
+Syntax constr
+  level 1:
+    List [ (list A) ] -> ["List"]
+  | Nil  [ (nil A) ] -> ["Nil"]
+  | Cons [ (cons A) ] -> ["Cons"]
+  ;
+  level 10:
+    Cons2 [ (cons A $e $l) ] -> ["Cons " $e:L " " $l:L ].
+
+Syntax constr
+  level 1:
+  pair_sig [ (exist (list A) Desc $e $d) ] -> ["<<" $e:L "," $d:L ">>"].
+].
+Hints Resolve d_one d_nil  t_step.
+
+Lemma left_prefix : (x,y,z:List)(ltl x^y z)-> (ltl x z).
+Proof.
+ Induction x.
+ Induction z.
+ Simpl;Intros H.
+ Inversion_clear H. 
+ Simpl;Intros;Apply (Lt_nil A leA).
+ Intros a l HInd.
+ Simpl.
+ 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 : 
+  (x,y,z:List)(ltl x y^z)-> (ltl x y) \/ (EX y':List | x=(y^y') /\ (ltl y' z)).
+Proof.
+ Intros x y;Generalize x.
+ Elim y;Simpl.
+ 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) .
+ Induction 1.
+ Left;Apply (Lt_tl A leA);Auto with sets.
+ Induction 1.
+ Induction 1;Intros.
+ Rewrite -> H8.
+ Right;Exists x2 ;Auto with sets.
+Qed.
+
+
+
+Lemma desc_prefix: (x:List)(a:A)(Descl x^(Cons a Nil))->(Descl x).
+Proof.
+ Intros.
+ Inversion H.
+ Generalize (app_cons_not_nil H1); Induction 1. 
+ Cut (x^(Cons a Nil))=(Cons x0 Nil); Auto with sets.
+ Intro.
+ Generalize (app_eq_unit H0) .
+ Induction 1; Induction 1; Intros.
+ Rewrite -> H4; Auto with sets.
+ Discriminate H5.
+ Generalize (app_inj_tail H0) .
+ Induction 1; Intros.
+ Rewrite <- H4; Auto with sets.
+Qed.
+
+Lemma desc_tail: (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:=[x:List](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 2!(l^(Cons y Nil)) 3!(Nil^(Cons b Nil)) H4);
+ Induction 1.
+ Intros.
+
+ Generalize (app_inj_tail H6); 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); 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); 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); Induction 1.
+ Intros.
+ Rewrite <- H11; Rewrite <- H16; Auto with sets.
+Qed.
+
+
+Lemma dist_aux : (z:List)(Descl z)->(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) ; 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); Induction 1.
+ Induction 1;Intros.
+ Rewrite -> H2;Rewrite -> H3; Split.
+ Apply d_nil.
+
+ Apply d_one.
+
+ 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:=[y0:List]
+          (x0:List)
+          ((l^(Cons y Nil))^(Cons x Nil))=(x0^y0)->(Descl x0)/\(Descl y0).
+
+ Intro.
+ Generalize (app_nil_end x1) ; Induction 1; Induction 1.
+ Split. Apply d_conc; Auto with sets.
+
+ Apply d_nil.
+
+ Do 3 Intro.
+ Generalize x1 .
+ Apply rev_ind with 
+  A:=A 
+  P:=[l0:List]
+     (x1:A)
+      (x0:List)
+       ((l^(Cons y Nil))^(Cons x Nil))=(x0^(l0^(Cons x1 Nil)))
+         ->(Descl x0)/\(Descl (l0^(Cons x1 Nil))).
+
+
+ Simpl.
+ Split.
+ Generalize (app_inj_tail H2) ;Induction 1.
+ Induction 1;Auto with sets.
+
+ Apply d_one.
+ Do 5 Intro.
+ Generalize (app_ass x4 (l1^(Cons x2 Nil)) (Cons x3 Nil)) .
+ Induction 1.
+ Generalize (app_ass x4 l1 (Cons x2 Nil)) ;Induction 1.
+ Intro E.
+ Generalize (app_inj_tail E) .
+ Induction 1;Intros.
+ Generalize (app_inj_tail H6) ;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) .
+ Induction 1;Split.
+ Auto with sets.
+
+ Generalize H14.
+ Rewrite <- H10; Intro.
+ Apply d_conc;Auto with sets.
+Qed.
+
+
+
+Lemma dist_Desc_concat : (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:(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.
+ Induction 1.
+ Intros.
+ Inversion H1;Auto with sets.
+ Inversion H3.
+
+ 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: (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;Intros.
+ Inversion_clear H0.
+ Apply (Lt_hd A leA  a b);Auto with sets.
+ 
+ Inversion_clear H1.
+Qed.
+
+
+Lemma acc_app: 
+    (x1,x2:List)(y1:(Descl x1^x2))
+     (Acc Power Lex_Exp (exist List Descl (x1^x2)  y1))
+     ->(x:List)
+        (y:(Descl x))
+         (ltl x (x1^x2))->(Acc Power Lex_Exp (exist List Descl x y)).
+Proof.
+ Intros.
+ Apply (Acc_inv Power Lex_Exp (exist List Descl (x1^x2) y1)).
+ Auto with sets.
+
+ Unfold lex_exp ;Simpl;Auto with sets.
+Qed.
+
+
+Theorem wf_lex_exp :
+  (well_founded A leA)->(well_founded Power Lex_Exp).
+Proof.
+ Unfold 2 well_founded .
+ Induction a;Intros x y.
+ Apply Acc_intro.
+ Induction y0.
+ Unfold 1 lex_exp ;Simpl.
+ Apply rev_ind with A:=A P:=[x:List]
+                            (x0:List)
+                             (y:(Descl x0))
+                              (ltl x0 x)
+                               ->(Acc Power Lex_Exp (exist List Descl x0 y)) .
+ Intros.
+ Inversion_clear H0.
+
+ Intro.
+ Generalize (well_founded_ind A (clos_trans A leA) (wf_clos_trans A leA H)).
+ Intros GR.
+ Apply GR with P:=[x0:A]
+                  (l:List)
+                   ((x1:List)
+                     (y:(Descl x1))
+                      (ltl x1 l)
+                       ->(Acc Power Lex_Exp (exist List Descl x1 y)))
+                    ->(x1:List)
+                       (y:(Descl x1))
+                        (ltl x1 (l^(Cons x0 Nil)))
+                         ->(Acc Power Lex_Exp (exist List Descl x1 y)) .
+ Intro;Intros HInd; Intros.
+ Generalize (right_prefix x2 l (Cons x1 Nil) H1) .
+ Induction 1.
+ Intro; Apply (H0 x2 y1 H3).
+
+ Induction 1.
+ Intro;Induction 1.
+ Clear  H4  H2.
+ Intro;Generalize y1 ;Clear  y1.
+ Rewrite -> H2.
+ Apply rev_ind with A:=A P:=[x3:List]
+                            (y1:(Descl (l^x3)))
+                             (ltl x3 (Cons x1 Nil))
+                              ->(Acc Power Lex_Exp
+                                  (exist List Descl (l^x3) y1)) .
+ Intros.
+ Generalize (app_nil_end l) ;Intros Heq.
+ Generalize y1 .
+ Clear  y1.
+ Rewrite <- Heq.
+ Intro.
+ Apply Acc_intro.
+ Induction y2.
+ Unfold 1 lex_exp .
+ Simpl;Intros x4 y3. Intros.
+ Apply (H0 x4 y3);Auto with sets.
+
+ Intros. 
+ Generalize (dist_Desc_concat l (l0^(Cons x4 Nil)) y1) .
+ 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) .
+ Induction 1;Intros.
+ Generalize (H4 H12 H10); Intro.
+ Generalize (Acc_inv Power Lex_Exp (exist List Descl (l^l0) H12) H14) .
+ Generalize (acc_app l l0 H12 H14).
+ Intros f g.
+ Generalize (HInd2 f);Intro.
+ Apply Acc_intro.
+ Induction y3.
+ Unfold 1 lex_exp ;Simpl; Intros.
+ Apply H15;Auto with sets.
+Qed.
+
+
+End Wf_Lexicographic_Exponentiation.
diff --git a/theories7/Wellfounded/Lexicographic_Product.v b/theories7/Wellfounded/Lexicographic_Product.v
new file mode 100644
index 000000000..b8f74c9ff
--- /dev/null
+++ b/theories7/Wellfounded/Lexicographic_Product.v
@@ -0,0 +1,191 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Authors: Bruno Barras, Cristina Cornes *)
+
+Require Eqdep.
+Require Relation_Operators.
+Require 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: (x:A)(B x)->(B x)->Prop.
+
+Notation LexProd := (lexprod A B leA leB).
+
+Hints Resolve t_step Acc_clos_trans wf_clos_trans.
+
+Lemma acc_A_B_lexprod : (x:A)(Acc A leA x)
+        ->((x0:A)(clos_trans A leA x0 x)->(well_founded (B x0) (leB x0)))
+                ->(y:(B x))(Acc (B x) (leB x) y)
+                        ->(Acc (sigS A B) LexProd (existS A B x y)).
+Proof.
+ NewInduction 1 as [x _ IHAcc]; Intros H2 y.
+ NewInduction 1 as [x0 H IHAcc0];Intros.
+ Apply Acc_intro.
+ NewDestruct 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.
+ NewDestruct 2.
+ Injection H3.
+ NewDestruct 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 A leA) ->((x:A) (well_founded (B x) (leB x))) 
+             -> (well_founded (sigS A B) LexProd).
+Proof.
+ Intros wfA wfB;Unfold well_founded .
+ NewDestruct 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: (x:A)(Acc A leA x)->(y:B)(Acc B leB y)
+                        ->(Acc (A*B) Symprod (x,y)).
+ Proof.
+ NewInduction 1 as [x _ IHAcc]; Intros y H2.
+ NewInduction 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 A leA)->(well_founded B leB)
+                        ->(well_founded (A*B) Symprod).
+Proof.
+ Red.
+ NewDestruct 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: (x,y:A)(Acc A*A SwapProd (x,y))->(Acc A*A SwapProd (y,x)).
+Proof.
+ Intros.
+ Inversion_clear H.
+ Apply Acc_intro.
+ NewDestruct 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: (x,y:A)(Acc A R x)->(Acc A R y)
+                                ->(Acc A*A SwapProd (x,y)).
+Proof.
+ NewInduction 1 as [x0 _ IHAcc0];Intros H2.
+ Cut (y0:A)(R y0 x0)->(Acc ? SwapProd (y0,y)).
+ Clear  IHAcc0.
+ NewInduction H2 as [x1 _ IHAcc1]; Intros H4.
+ Cut (y:A)(R y x1)->(Acc ? SwapProd (x0,y)).
+ Clear  IHAcc1.
+ Intro.
+ Apply Acc_intro.
+ NewDestruct 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 A R)->(well_founded A*A SwapProd).
+Proof.
+ Red.
+ NewDestruct a;Intros.
+ Apply Acc_swapprod;Auto with sets.
+Qed.
+
+End Swap.
diff --git a/theories7/Wellfounded/Transitive_Closure.v b/theories7/Wellfounded/Transitive_Closure.v
new file mode 100644
index 000000000..c650d4675
--- /dev/null
+++ b/theories7/Wellfounded/Transitive_Closure.v
@@ -0,0 +1,47 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Author: Bruno Barras *)
+
+Require Relation_Definitions.
+Require 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;Auto with sets.
+  Qed.
+
+  Lemma Acc_clos_trans: (x:A)(Acc A R x)->(Acc A trans_clos x).
+    NewInduction 1 as [x0 _ H1].
+    Apply Acc_intro.
+    Intros y H2.
+    NewInduction H2;Auto with sets.
+    Apply Acc_inv with y ;Auto with sets.
+  Qed.
+
+  Hints Resolve Acc_clos_trans.
+
+  Lemma Acc_inv_trans: (x,y:A)(trans_clos y x)->(Acc A R x)->(Acc A R y).
+  Proof.
+    NewInduction 1 as [|x y];Auto with sets.
+    Intro; Apply Acc_inv with y; Assumption.
+  Qed.
+
+  Theorem wf_clos_trans: (well_founded A R)  ->(well_founded A trans_clos).
+  Proof.
+    Unfold well_founded;Auto with sets.
+  Qed.
+
+End Wf_Transitive_Closure.
diff --git a/theories7/Wellfounded/Union.v b/theories7/Wellfounded/Union.v
new file mode 100644
index 000000000..ee45a9476
--- /dev/null
+++ b/theories7/Wellfounded/Union.v
@@ -0,0 +1,74 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Author: Bruno Barras *)
+
+Require Relation_Operators.
+Require Relation_Definitions.
+Require Transitive_Closure.
+
+Section WfUnion.
+  Variable A: Set.
+  Variable R1,R2: (relation A).
+  
+ Notation Union := (union A R1 R2).
+
+ Hints Resolve Acc_clos_trans wf_clos_trans.
+
+Remark strip_commut: 
+      (commut A R1 R2)->(x,y:A)(clos_trans A R1 y x)->(z:A)(R2 z y)
+            ->(EX y':A | (R2 y' x) & (clos_trans A R1 z y')).
+Proof.
+ NewInduction 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)->((x:A)(Acc A R2 x)->(Acc A R1 x))
+                         ->(a:A)(Acc A R2 a)->(Acc A Union a).
+Proof.
+ NewInduction 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 A (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 .
+ 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 A R1)->(well_founded A R2)
+                  ->(well_founded A Union).
+Proof.
+ Unfold well_founded .
+ Intros.
+ Apply Acc_union;Auto with sets.
+Qed.
+
+End WfUnion.
diff --git a/theories7/Wellfounded/Well_Ordering.v b/theories7/Wellfounded/Well_Ordering.v
new file mode 100644
index 000000000..49595dd2b
--- /dev/null
+++ b/theories7/Wellfounded/Well_Ordering.v
@@ -0,0 +1,72 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(** Author: Cristina Cornes.
+    From: Constructing Recursion Operators in Type Theory
+    L. Paulson  JSC (1986) 2, 325-355 *)
+
+Require Eqdep.
+
+Section WellOrdering.
+Variable A:Set.
+Variable B:A->Set. 
+
+Inductive WO : Set :=
+   sup : (a:A)(f:(B a)->WO)WO.
+
+
+Inductive le_WO  : WO->WO->Prop :=
+  le_sup : (a:A)(f:(B a)->WO)(v:(B a)) (le_WO  (f v) (sup a f)).
+ 
+
+Theorem wf_WO : (well_founded WO le_WO ).
+Proof.
+ Unfold well_founded ;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 (eq ? f f1).
+ Intros E;Rewrite -> E;Auto.
+ Symmetry.
+ Apply (inj_pair2 A [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 A leA)-> A-> (WO A B).
+Proof.
+ Intros.
+ Apply (well_founded_induction A leA H [a:A](WO A B));Auto.
+ Intros.
+ Apply (sup A B x).
+ Unfold 1 B .
+ NewDestruct 1 as [x0].
+ Apply (H1 x0);Auto.
+Qed.
+
+End Characterisation_wf_relations.
diff --git a/theories7/Wellfounded/Wellfounded.v b/theories7/Wellfounded/Wellfounded.v
new file mode 100644
index 000000000..10fca099c
--- /dev/null
+++ b/theories7/Wellfounded/Wellfounded.v
@@ -0,0 +1,20 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ 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.
+
+