From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- theories7/Wellfounded/Disjoint_Union.v | 56 --- theories7/Wellfounded/Inclusion.v | 33 -- theories7/Wellfounded/Inverse_Image.v | 58 ---- .../Wellfounded/Lexicographic_Exponentiation.v | 386 --------------------- theories7/Wellfounded/Lexicographic_Product.v | 191 ---------- theories7/Wellfounded/Transitive_Closure.v | 47 --- theories7/Wellfounded/Union.v | 74 ---- theories7/Wellfounded/Well_Ordering.v | 72 ---- theories7/Wellfounded/Wellfounded.v | 20 -- 9 files changed, 937 deletions(-) delete mode 100644 theories7/Wellfounded/Disjoint_Union.v delete mode 100644 theories7/Wellfounded/Inclusion.v delete mode 100644 theories7/Wellfounded/Inverse_Image.v delete mode 100644 theories7/Wellfounded/Lexicographic_Exponentiation.v delete mode 100644 theories7/Wellfounded/Lexicographic_Product.v delete mode 100644 theories7/Wellfounded/Transitive_Closure.v delete mode 100644 theories7/Wellfounded/Union.v delete mode 100644 theories7/Wellfounded/Well_Ordering.v delete mode 100644 theories7/Wellfounded/Wellfounded.v (limited to 'theories7/Wellfounded') 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* 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 *) -(* (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 *) -(* (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 *) -(* 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 *) -(*