diff options
Diffstat (limited to 'theories/Sets/Relations_3_facts.v')
| -rwxr-xr-x | theories/Sets/Relations_3_facts.v | 216 |
1 files changed, 115 insertions, 101 deletions
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index a57487d1e..5b1ce9e31 100755 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -33,125 +33,139 @@ 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). + forall (U:Type) (R:Relation U) (x 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. +intros U R x y H'; red in |- *. +exists y; auto with sets. Qed. -Hints Resolve Rstar_imp_coherent. +Hint Resolve Rstar_imp_coherent. Theorem coherent_symmetric : - (U: Type) (R: (Relation U)) (Symmetric U (coherent U R)). + forall (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. +unfold coherent at 1 in |- *. +intros U R; red in |- *. +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). + forall (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. +intros U R H'; red in |- *. +intro x; red in |- *; intros a b H'0. +unfold coherent at 1 in |- *. +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). + forall (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. +intros U R H'; red in |- *. +intro x; red in |- *; intros a b H'0. +unfold coherent at 1 in |- *. +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 (ex (fun 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'). + forall (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. +unfold Noetherian at 2 in |- *. +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). + forall (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. +intros U R H' H'0; red in |- *; intro x. +elim (H' x); unfold confluent in |- *. +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 coherent at 1 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 in |- *; (exists z1; split); auto with sets. +apply T with y1; auto with sets. +apply T with t; auto with sets. +Qed.
\ No newline at end of file |