diff options
Diffstat (limited to 'theories/Wellfounded/Union.v')
| -rw-r--r-- | theories/Wellfounded/Union.v | 98 |
1 files changed, 48 insertions, 50 deletions
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index 269cfd9d..634576ad 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Union.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Union.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Author: Bruno Barras *) @@ -18,60 +18,58 @@ Section WfUnion. Variable A : Set. Variables R1 R2 : relation A. - Notation Union := (union A R1 R2). - - Hint Resolve Acc_clos_trans wf_clos_trans. - -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. - 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. -Qed. + Notation Union := (union A R1 R2). + + 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. + 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. + Qed. 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. - 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 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. -Qed. + commut A R1 R2 -> + (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a. + Proof. + 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 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. + Qed. + Theorem wf_union : - commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union. -Proof. - unfold well_founded in |- *. - intros. - apply Acc_union; auto with sets. -Qed. + commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union. + Proof. + unfold well_founded in |- *. + intros. + apply Acc_union; auto with sets. + Qed. End WfUnion.
\ No newline at end of file |