diff options
Diffstat (limited to 'theories7/Sets/Relations_3_facts.v')
| -rwxr-xr-x | theories7/Sets/Relations_3_facts.v | 157 |
1 files changed, 157 insertions, 0 deletions
diff --git a/theories7/Sets/Relations_3_facts.v b/theories7/Sets/Relations_3_facts.v new file mode 100755 index 00000000..822f550a --- /dev/null +++ b/theories7/Sets/Relations_3_facts.v @@ -0,0 +1,157 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) +(****************************************************************************) +(* *) +(* Naive Set Theory in Coq *) +(* *) +(* INRIA INRIA *) +(* Rocquencourt Sophia-Antipolis *) +(* *) +(* Coq V6.1 *) +(* *) +(* Gilles Kahn *) +(* Gerard Huet *) +(* *) +(* *) +(* *) +(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks *) +(* to the Newton Institute for providing an exceptional work environment *) +(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) +(****************************************************************************) + +(*i $Id: Relations_3_facts.v,v 1.1.2.1 2004/07/16 19:31:40 herbelin Exp $ i*) + +Require Export Relations_1. +Require Export Relations_1_facts. +Require Export Relations_2. +Require Export Relations_2_facts. +Require Export Relations_3. + +Theorem Rstar_imp_coherent : + (U: Type) (R: (Relation U)) (x: U) (y: U) (Rstar U R x y) -> + (coherent U R x y). +Proof. +Intros U R x y H'; Red. +Exists y; Auto with sets. +Qed. +Hints Resolve Rstar_imp_coherent. + +Theorem coherent_symmetric : + (U: Type) (R: (Relation U)) (Symmetric U (coherent U R)). +Proof. +Unfold 1 coherent. +Intros U R; Red. +Intros x y H'; Elim H'. +Intros z H'0; Exists z; Tauto. +Qed. + +Theorem Strong_confluence : + (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R). +Proof. +Intros U R H'; Red. +Intro x; Red; Intros a b H'0. +Unfold 1 coherent. +Generalize b; Clear b. +Elim H'0; Clear H'0. +Intros x0 b H'1; Exists b; Auto with sets. +Intros x0 y z H'1 H'2 H'3 b H'4. +Generalize (Lemma1 U R); Intro h; LApply h; + [Intro H'0; Generalize (H'0 x0 b); Intro h0; LApply h0; + [Intro H'5; Generalize (H'5 y); Intro h1; LApply h1; + [Intro h2; Elim h2; Intros z0 h3; Elim h3; Intros H'6 H'7; + Clear h h0 h1 h2 h3 | Clear h h0 h1] | Clear h h0] | Clear h]; Auto with sets. +Generalize (H'3 z0); Intro h; LApply h; + [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h h0 h1 | + Clear h]; Auto with sets. +Exists z1; Split; Auto with sets. +Apply Rstar_n with z0; Auto with sets. +Qed. + +Theorem Strong_confluence_direct : + (U: Type) (R: (Relation U)) (Strongly_confluent U R) -> (Confluent U R). +Proof. +Intros U R H'; Red. +Intro x; Red; Intros a b H'0. +Unfold 1 coherent. +Generalize b; Clear b. +Elim H'0; Clear H'0. +Intros x0 b H'1; Exists b; Auto with sets. +Intros x0 y z H'1 H'2 H'3 b H'4. +Cut (exT U [t: U] (Rstar U R y t) /\ (R b t)). +Intro h; Elim h; Intros t h0; Elim h0; Intros H'0 H'5; Clear h h0. +Generalize (H'3 t); Intro h; LApply h; + [Intro h0; Elim h0; Intros z0 h1; Elim h1; Intros H'6 H'7; Clear h h0 h1 | + Clear h]; Auto with sets. +Exists z0; Split; [Assumption | Idtac]. +Apply Rstar_n with t; Auto with sets. +Generalize H'1; Generalize y; Clear H'1. +Elim H'4. +Intros x1 y0 H'0; Exists y0; Auto with sets. +Intros x1 y0 z0 H'0 H'1 H'5 y1 H'6. +Red in H'. +Generalize (H' x1 y0 y1); Intro h; LApply h; + [Intro H'7; LApply H'7; + [Intro h0; Elim h0; Intros z1 h1; Elim h1; Intros H'8 H'9; Clear h H'7 h0 h1 | + Clear h] | Clear h]; Auto with sets. +Generalize (H'5 z1); Intro h; LApply h; + [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'7 H'10; Clear h h0 h1 | + Clear h]; Auto with sets. +Exists t; Split; Auto with sets. +Apply Rstar_n with z1; Auto with sets. +Qed. + +Theorem Noetherian_contains_Noetherian : + (U: Type) (R, R': (Relation U)) (Noetherian U R) -> (contains U R R') -> + (Noetherian U R'). +Proof. +Unfold 2 Noetherian. +Intros U R R' H' H'0 x. +Elim (H' x); Auto with sets. +Qed. + +Theorem Newman : + (U: Type) (R: (Relation U)) (Noetherian U R) -> (Locally_confluent U R) -> + (Confluent U R). +Proof. +Intros U R H' H'0; Red; Intro x. +Elim (H' x); Unfold confluent. +Intros x0 H'1 H'2 y z H'3 H'4. +Generalize (Rstar_cases U R x0 y); Intro h; LApply h; + [Intro h0; Elim h0; + [Clear h h0; Intro h1 | + Intro h1; Elim h1; Intros u h2; Elim h2; Intros H'5 H'6; Clear h h0 h1 h2] | + Clear h]; Auto with sets. +Elim h1; Auto with sets. +Generalize (Rstar_cases U R x0 z); Intro h; LApply h; + [Intro h0; Elim h0; + [Clear h h0; Intro h1 | + Intro h1; Elim h1; Intros v h2; Elim h2; Intros H'7 H'8; Clear h h0 h1 h2] | + Clear h]; Auto with sets. +Elim h1; Generalize coherent_symmetric; Intro t; Red in t; Auto with sets. +Unfold Locally_confluent locally_confluent coherent in H'0. +Generalize (H'0 x0 u v); Intro h; LApply h; + [Intro H'9; LApply H'9; + [Intro h0; Elim h0; Intros t h1; Elim h1; Intros H'10 H'11; + Clear h H'9 h0 h1 | Clear h] | Clear h]; Auto with sets. +Clear H'0. +Unfold 1 coherent in H'2. +Generalize (H'2 u); Intro h; LApply h; + [Intro H'0; Generalize (H'0 y t); Intro h0; LApply h0; + [Intro H'9; LApply H'9; + [Intro h1; Elim h1; Intros y1 h2; Elim h2; Intros H'12 H'13; + Clear h h0 H'9 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets. +Generalize Rstar_transitive; Intro T; Red in T. +Generalize (H'2 v); Intro h; LApply h; + [Intro H'9; Generalize (H'9 y1 z); Intro h0; LApply h0; + [Intro H'14; LApply H'14; + [Intro h1; Elim h1; Intros z1 h2; Elim h2; Intros H'15 H'16; + Clear h h0 H'14 h1 h2 | Clear h h0] | Clear h h0] | Clear h]; Auto with sets. +Red; (Exists z1; Split); Auto with sets. +Apply T with y1; Auto with sets. +Apply T with t; Auto with sets. +Qed. |