diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /theories/Wellfounded/Union.v | |
parent | 9058fb97426307536f56c3e7447be2f70798e081 (diff) |
Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Wellfounded/Union.v')
-rw-r--r-- | theories/Wellfounded/Union.v | 87 |
1 files changed, 45 insertions, 42 deletions
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index ee45a9476..d7f241dd0 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -10,65 +10,68 @@ (** Author: Bruno Barras *) -Require Relation_Operators. -Require Relation_Definitions. -Require Transitive_Closure. +Require Import Relation_Operators. +Require Import Relation_Definitions. +Require Import Transitive_Closure. Section WfUnion. - Variable A: Set. - Variable R1,R2: (relation A). + Variable A : Set. + Variables R1 R2 : relation A. Notation Union := (union A R1 R2). - Hints Resolve Acc_clos_trans wf_clos_trans. + Hint 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')). +Remark strip_commut : + commut A R1 R2 -> + forall x y:A, + clos_trans A R1 y x -> + forall z:A, R2 z y -> exists2 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. + induction 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. + 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). + Lemma Acc_union : + commut A R1 R2 -> + (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc 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. + induction 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 (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. + elim strip_commut with x x0 y0; auto with sets; intros. + apply Acc_inv_trans with x1; auto with sets. + unfold union in |- *. + 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. + 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). + Theorem wf_union : + commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union. Proof. - Unfold well_founded . - Intros. - Apply Acc_union;Auto with sets. + unfold well_founded in |- *. + intros. + apply Acc_union; auto with sets. Qed. -End WfUnion. +End WfUnion.
\ No newline at end of file |