diff options
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 54 | ||||
| -rw-r--r-- | theories/Wellfounded/Inclusion.v | 28 | ||||
| -rw-r--r-- | theories/Wellfounded/Inverse_Image.v | 45 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 378 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 193 | ||||
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 46 | ||||
| -rw-r--r-- | theories/Wellfounded/Union.v | 70 | ||||
| -rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 68 | ||||
| -rw-r--r-- | theories/Wellfounded/Wellfounded.v | 13 |
9 files changed, 895 insertions, 0 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v new file mode 100644 index 000000000..162a31e83 --- /dev/null +++ b/theories/Wellfounded/Disjoint_Union.v @@ -0,0 +1,54 @@ + +(* $Id$ *) + +(****************************************************************************) +(* 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. + +Syntactic Definition 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. + Induction 1;Intros. + Apply Acc_intro;Intros. + 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. + Induction 2;Intros. + Apply Acc_intro;Intros. + Inversion_clear H3;Auto with sets. + Apply acc_A_sum;Auto with sets. +Save. + + +Lemma wf_disjoint_sum: + (well_founded A leA) + -> (well_founded B leB) -> (well_founded A+B Le_AsB). +Proof. + Intros. + Unfold well_founded . + Induction a. + Intro. + Apply (acc_A_sum y). + Apply (H y). + + Intro. + Apply (acc_B_sum H y). + Apply (H0 y). +Qed. + +End Wf_Disjoint_Union. diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v new file mode 100644 index 000000000..260a539c7 --- /dev/null +++ b/theories/Wellfounded/Inclusion.v @@ -0,0 +1,28 @@ + +(* $Id$ *) + +(****************************************************************************) +(* 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. + Induction 2;Intros. + Apply Acc_intro;Auto with sets. + Save. + + 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. + Save. + +End WfInclusion. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v new file mode 100644 index 000000000..068d4903a --- /dev/null +++ b/theories/Wellfounded/Inverse_Image.v @@ -0,0 +1,45 @@ + +(* $Id$ *) + +(****************************************************************************) +(* 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). + Induction 1; Intros. + Apply Acc_intro; Intros. + Apply (H1 (f y0)); Try Trivial. + Rewrite H2; Trivial. + Save. + + Lemma Acc_inverse_image : (x:A)(Acc B R (f x)) -> (Acc A Rof x). + Intros; Apply (Acc_lemma (f x)); Trivial. + Save. + + Theorem wf_inverse_image: (well_founded B R)->(well_founded A Rof). + Red; Intros; Apply Acc_inverse_image; Auto. + Save. + +End Inverse_Image. + + + + + + + + + + + + + +(* $Id$ *) diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v new file mode 100644 index 000000000..5bf2cedaa --- /dev/null +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -0,0 +1,378 @@ + +(* $Id$ *) + +(****************************************************************************) +(* 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. + +Syntactic Definition Power := (Pow A leA). +Syntactic Definition Lex_Exp := (lex_exp A leA). +Syntactic Definition ltl := (Ltl A leA). +Syntactic Definition Descl := (Desc A leA). + +Syntactic Definition List := (list A). +Syntactic Definition Nil := (nil A). +(* useless but symmetric *) +Syntactic Definition Cons := (cons 1!A). + +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 ]. + +Hints Resolve d_one d_nil t_step. + +Syntax constr level 1: + pair_sig [<<(exist (list A) Desc $e $d)>>] -> ["<<" $e:L "," $d:L ">>"]. + + +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. + 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. + 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/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v new file mode 100644 index 000000000..5fa24e2cc --- /dev/null +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -0,0 +1,193 @@ + +(* $Id$ *) + +(****************************************************************************) +(* 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. + + +Syntactic Definition 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. + Induction 1. + Induction 4;Intros. + Apply Acc_intro. + Induction y0. + Intros. + Simple Inversion H6;Intros. + Cut (leA x2 x0);Intros. + Apply H1;Auto with sets. + Intros. + Apply H2. + Apply t_trans with x2 ;Auto with sets. + + Red in H2. + Apply H2. + Auto with sets. + + Injection H8. (*** BUG ***) + Induction 2. + Injection H9. + Induction 2;Auto with sets. + + Elim H8. + Generalize y2 y' H9 H7 . + Replace x3 with x0. + Clear H7 H8 H9 y2 y' x3 H6 y1 x2 y0. + Intros. + Apply H5. + Elim inj_pair2 with A B x0 y' x1 ;Auto with sets. + + Injection H9;Auto with sets. +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 . + Induction a;Intros. + Apply acc_A_B_lexprod;Auto with sets;Intros. + Red in wfB. + Auto with sets. +Save. + + +End WfLexicographic_Product. + + +Section Wf_Symmetric_Product. + Variable A:Set. + Variable B:Set. + Variable leA: A->A->Prop. + Variable leB: B->B->Prop. + + Syntactic Definition Symprod := (symprod A B leA leB). + +(* + 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). +Save. +*) + + Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y) + ->(Acc (A*B) Symprod (x,y)). +Proof. + Induction 1;Intros. + Elim H2;Intros. + Apply Acc_intro;Intros. + Inversion_clear H5;Auto with sets. + Apply H1;Auto with sets. + Apply Acc_intro;Auto with sets. +Save. + + +Lemma wf_symprod: (well_founded A leA)->(well_founded B leB) + ->(well_founded (A*B) Symprod). +Proof. + Red. + Induction a;Intros. + Apply Acc_symprod;Auto with sets. +Save. + +End Wf_Symmetric_Product. + + +Section Swap. + + Variable A:Set. + Variable R:A->A->Prop. + + Syntactic Definition 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. + 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. +Save. + + + Lemma Acc_swapprod: (x,y:A)(Acc A R x)->(Acc A R y) + ->(Acc A*A SwapProd (x,y)). +Proof. + Induction 1;Intros. + Cut (y0:A)(R y0 x0)->(Acc ? SwapProd (y0,y)). + Clear H1. + Elim H2;Intros. + Cut (y:A)(R y x1)->(Acc ? SwapProd (x0,y)). + Clear H3. + Intro. + Apply Acc_intro. + Induction y0;Intros. + Inversion_clear H5. + Inversion_clear H6;Auto with sets. + + Apply swap_Acc. + Inversion_clear H6;Auto with sets. + + Intros. + Apply H3;Auto with sets;Intros. + Apply Acc_inv with (y1,x1) ;Auto with sets. + Apply sp_noswap. + Apply right_sym;Auto with sets. + + Auto with sets. +Save. + + + Lemma wf_swapprod: (well_founded A R)->(well_founded A*A SwapProd). +Proof. + Red. + Induction a;Intros. + Apply Acc_swapprod;Auto with sets. +Save. + +End Swap. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v new file mode 100644 index 000000000..a97cadc27 --- /dev/null +++ b/theories/Wellfounded/Transitive_Closure.v @@ -0,0 +1,46 @@ + +(* $Id$ *) + +(****************************************************************************) +(* Bruno Barras *) +(****************************************************************************) + +Require Relation_Definitions. +Require Relation_Operators. + +Section Wf_Transitive_Closure. + Variable A: Set. + Variable R: (relation A). + + Syntactic Definition 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). + Induction 1. + Intros x0 H0 H1. + Apply Acc_intro. + Intros y H2. + Generalize H1 . + Elim H2;Auto with sets. + Intros x1 y0 z H3 H4 H5 H6 H7. + Apply Acc_inv with y0 ;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. + Induction 1;Auto with sets. + Intros x0 y0 H0 H1. + Apply Acc_inv with y0 ;Auto with sets. + 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/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v new file mode 100644 index 000000000..e58e002a4 --- /dev/null +++ b/theories/Wellfounded/Union.v @@ -0,0 +1,70 @@ + +(* $Id$ *) + +(****************************************************************************) +(* Bruno Barras *) +(****************************************************************************) + +Require Relation_Operators. +Require Relation_Definitions. +Require Transitive_Closure. + +Section WfUnion. + Variable A: Set. + Variable R1,R2: (relation A). + + Syntactic Definition 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. + Induction 2;Intros. + Elim H with y0 x0 z ;Auto with sets;Intros. + Exists x1;Auto with sets. + + Elim H2 with z0 ;Auto with sets;Intros. + Elim H4 with x1 ;Auto with sets;Intros. + Exists x2;Auto with sets. + Apply t_trans with x1 ;Auto with sets. +Save. + + + 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. + Induction 3. + Intros. + Apply Acc_intro;Intros. + Elim H4;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 H9;Intros. + Apply H7;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 H12;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. +Save. + + + 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. +Save. + +End WfUnion. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v new file mode 100644 index 000000000..ad616ecc0 --- /dev/null +++ b/theories/Wellfounded/Well_Ordering.v @@ -0,0 +1,68 @@ + +(* $Id$ *) + +(****************************************************************************) +(* 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. (*** BUG ***) + 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 . + Induction 1. + Intros. + Apply (H1 x0);Auto. +Qed. + +End Characterisation_wf_relations. diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v new file mode 100644 index 000000000..a30007e27 --- /dev/null +++ b/theories/Wellfounded/Wellfounded.v @@ -0,0 +1,13 @@ + +(* $Id$ *) + +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. + + |