summaryrefslogtreecommitdiff
path: root/theories7/Wellfounded
diff options
context:
space:
mode:
Diffstat (limited to 'theories7/Wellfounded')
-rw-r--r--theories7/Wellfounded/Disjoint_Union.v56
-rw-r--r--theories7/Wellfounded/Inclusion.v33
-rw-r--r--theories7/Wellfounded/Inverse_Image.v58
-rw-r--r--theories7/Wellfounded/Lexicographic_Exponentiation.v386
-rw-r--r--theories7/Wellfounded/Lexicographic_Product.v191
-rw-r--r--theories7/Wellfounded/Transitive_Closure.v47
-rw-r--r--theories7/Wellfounded/Union.v74
-rw-r--r--theories7/Wellfounded/Well_Ordering.v72
-rw-r--r--theories7/Wellfounded/Wellfounded.v20
9 files changed, 0 insertions, 937 deletions
diff --git a/theories7/Wellfounded/Disjoint_Union.v b/theories7/Wellfounded/Disjoint_Union.v
deleted file mode 100644
index 04930170..00000000
--- a/theories7/Wellfounded/Disjoint_Union.v
+++ /dev/null
@@ -1,56 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:41 herbelin Exp $ 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
deleted file mode 100644
index 6a515333..00000000
--- a/theories7/Wellfounded/Inclusion.v
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:41 herbelin Exp $ 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
deleted file mode 100644
index 6c9c3e65..00000000
--- a/theories7/Wellfounded/Inverse_Image.v
+++ /dev/null
@@ -1,58 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:41 herbelin Exp $ 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
deleted file mode 100644
index 17f6d650..00000000
--- a/theories7/Wellfounded/Lexicographic_Exponentiation.v
+++ /dev/null
@@ -1,386 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:41 herbelin Exp $ 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
deleted file mode 100644
index f31d8c3f..00000000
--- a/theories7/Wellfounded/Lexicographic_Product.v
+++ /dev/null
@@ -1,191 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:42 herbelin Exp $ 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
deleted file mode 100644
index 4d6cbe28..00000000
--- a/theories7/Wellfounded/Transitive_Closure.v
+++ /dev/null
@@ -1,47 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:42 herbelin Exp $ 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
deleted file mode 100644
index 9b31f72d..00000000
--- a/theories7/Wellfounded/Union.v
+++ /dev/null
@@ -1,74 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:42 herbelin Exp $ 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
deleted file mode 100644
index 5c2b2405..00000000
--- a/theories7/Wellfounded/Well_Ordering.v
+++ /dev/null
@@ -1,72 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:42 herbelin Exp $ 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
deleted file mode 100644
index d1a8dd01..00000000
--- a/theories7/Wellfounded/Wellfounded.v
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(* 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.1.2.1 2004/07/16 19:31:42 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.
-
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 12:06:31 +0000