diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-21 14:41:16 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-21 14:41:16 +0000 |
commit | 838ffd441e80aa324ffe731f2527dbb181654308 (patch) | |
tree | a4ab1228901f2b63f0638c9a5fa627d6036af625 /theories/Wellfounded/Union.v | |
parent | 78fb07846e6ca303417699d19beaeaf1a97f96af (diff) |
ajout de theories/Wellfounded
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@900 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Wellfounded/Union.v')
-rw-r--r-- | theories/Wellfounded/Union.v | 70 |
1 files changed, 70 insertions, 0 deletions
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. |