diff options
Diffstat (limited to 'theories7/Sets/Relations_3_facts.v')
| -rwxr-xr-x | theories7/Sets/Relations_3_facts.v | 157 |
1 files changed, 0 insertions, 157 deletions
diff --git a/theories7/Sets/Relations_3_facts.v b/theories7/Sets/Relations_3_facts.v deleted file mode 100755 index 822f550a..00000000 --- a/theories7/Sets/Relations_3_facts.v +++ /dev/null @@ -1,157 +0,0 @@ -(************************************************************************) -(* 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. |