diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/Wellfounded/Union.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/Wellfounded/Union.v')
-rw-r--r-- | theories/Wellfounded/Union.v | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v new file mode 100644 index 00000000..8f31ce9f --- /dev/null +++ b/theories/Wellfounded/Union.v @@ -0,0 +1,77 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Union.v,v 1.9.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +(** Author: Bruno Barras *) + +Require Import Relation_Operators. +Require Import Relation_Definitions. +Require Import Transitive_Closure. + +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. + + + 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. + + + 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. + +End WfUnion.
\ No newline at end of file |