diff options
Diffstat (limited to 'theories/Relations/Newman.v')
| -rwxr-xr-x | theories/Relations/Newman.v | 134 |
1 files changed, 71 insertions, 63 deletions
diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index 57e93240a..7de49f62f 100755 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v @@ -8,108 +8,116 @@ (*i $Id$ i*) -Require Rstar. +Require Import Rstar. Section Newman. -Variable A: Type. -Variable R: A->A->Prop. +Variable A : Type. +Variable R : A -> A -> Prop. -Local Rstar := (Rstar A R). -Local Rstar_reflexive := (Rstar_reflexive A R). -Local Rstar_transitive := (Rstar_transitive A R). -Local Rstar_Rstar' := (Rstar_Rstar' A R). +Let Rstar := Rstar A R. +Let Rstar_reflexive := Rstar_reflexive A R. +Let Rstar_transitive := Rstar_transitive A R. +Let Rstar_Rstar' := Rstar_Rstar' A R. -Definition coherence := [x:A][y:A] (exT2 ? (Rstar x) (Rstar y)). +Definition coherence (x y:A) := ex2 (Rstar x) (Rstar y). -Theorem coherence_intro : (x:A)(y:A)(z:A)(Rstar x z)->(Rstar y z)->(coherence x y). -Proof [x:A][y:A][z:A][h1:(Rstar x z)][h2:(Rstar y z)] - (exT_intro2 A (Rstar x) (Rstar y) z h1 h2). +Theorem coherence_intro : + forall x y z:A, Rstar x z -> Rstar y z -> coherence x y. +Proof + fun (x y z:A) (h1:Rstar x z) (h2:Rstar y z) => + ex_intro2 (Rstar x) (Rstar y) z h1 h2. (** A very simple case of coherence : *) -Lemma Rstar_coherence : (x:A)(y:A)(Rstar x y)->(coherence x y). - Proof [x:A][y:A][h:(Rstar x y)](coherence_intro x y y h (Rstar_reflexive y)). +Lemma Rstar_coherence : forall x y:A, Rstar x y -> coherence x y. + Proof + fun (x y:A) (h:Rstar x y) => coherence_intro x y y h (Rstar_reflexive y). (** coherence is symmetric *) -Lemma coherence_sym: (x:A)(y:A)(coherence x y)->(coherence y x). - Proof [x:A][y:A][h:(coherence x y)] - (exT2_ind A (Rstar x) (Rstar y) (coherence y x) - [w:A][h1:(Rstar x w)][h2:(Rstar y w)] - (coherence_intro y x w h2 h1) h). - -Definition confluence := - [x:A](y:A)(z:A)(Rstar x y)->(Rstar x z)->(coherence y z). +Lemma coherence_sym : forall x y:A, coherence x y -> coherence y x. + Proof + fun (x y:A) (h:coherence x y) => + ex2_ind + (fun (w:A) (h1:Rstar x w) (h2:Rstar y w) => + coherence_intro y x w h2 h1) h. + +Definition confluence (x:A) := + forall y z:A, Rstar x y -> Rstar x z -> coherence y z. -Definition local_confluence := - [x:A](y:A)(z:A)(R x y)->(R x z)->(coherence y z). +Definition local_confluence (x:A) := + forall y z:A, R x y -> R x z -> coherence y z. Definition noetherian := - (x:A)(P:A->Prop)((y:A)((z:A)(R y z)->(P z))->(P y))->(P x). + forall (x:A) (P:A -> Prop), + (forall y:A, (forall z:A, R y z -> P z) -> P y) -> P x. Section Newman_section. (** The general hypotheses of the theorem *) -Hypothesis Hyp1:noetherian. -Hypothesis Hyp2:(x:A)(local_confluence x). +Hypothesis Hyp1 : noetherian. +Hypothesis Hyp2 : forall x:A, local_confluence x. (** The induction hypothesis *) Section Induct. - Variable x:A. - Hypothesis hyp_ind:(u:A)(R x u)->(confluence u). + Variable x : A. + Hypothesis hyp_ind : forall u:A, R x u -> confluence u. (** Confluence in [x] *) - Variables y,z:A. - Hypothesis h1:(Rstar x y). - Hypothesis h2:(Rstar x z). + Variables y z : A. + Hypothesis h1 : Rstar x y. + Hypothesis h2 : Rstar x z. (** particular case [x->u] and [u->*y] *) Section Newman_. - Variable u:A. - Hypothesis t1:(R x u). - Hypothesis t2:(Rstar u y). + Variable u : A. + Hypothesis t1 : R x u. + Hypothesis t2 : Rstar u y. (** In the usual diagram, we assume also [x->v] and [v->*z] *) -Theorem Diagram : (v:A)(u1:(R x v))(u2:(Rstar v z))(coherence y z). - -Proof (* We draw the diagram ! *) - [v:A][u1:(R x v)][u2:(Rstar v z)] - (exT2_ind A (Rstar u) (Rstar v) (* local confluence in x for u,v *) - (coherence y z) (* gives w, u->*w and v->*w *) - ([w:A][s1:(Rstar u w)][s2:(Rstar v w)] - (exT2_ind A (Rstar y) (Rstar w) (* confluence in u => coherence(y,w) *) - (coherence y z) (* gives a, y->*a and z->*a *) - ([a:A][v1:(Rstar y a)][v2:(Rstar w a)] - (exT2_ind A (Rstar a) (Rstar z) (* confluence in v => coherence(a,z) *) - (coherence y z) (* gives b, a->*b and z->*b *) - ([b:A][w1:(Rstar a b)][w2:(Rstar z b)] - (coherence_intro y z b (Rstar_transitive y a b v1 w1) w2)) - (hyp_ind v u1 a z (Rstar_transitive v w a s2 v2) u2))) - (hyp_ind u t1 y w t2 s1))) - (Hyp2 x u v t1 u1)). +Theorem Diagram : forall (v:A) (u1:R x v) (u2:Rstar v z), coherence y z. + +Proof + (* We draw the diagram ! *) + fun (v:A) (u1:R x v) (u2:Rstar v z) => + ex2_ind + (* local confluence in x for u,v *) + (* gives w, u->*w and v->*w *) + (fun (w:A) (s1:Rstar u w) (s2:Rstar v w) => + ex2_ind + (* confluence in u => coherence(y,w) *) + (* gives a, y->*a and z->*a *) + (fun (a:A) (v1:Rstar y a) (v2:Rstar w a) => + ex2_ind + (* confluence in v => coherence(a,z) *) + (* gives b, a->*b and z->*b *) + (fun (b:A) (w1:Rstar a b) (w2:Rstar z b) => + coherence_intro y z b (Rstar_transitive y a b v1 w1) w2) + (hyp_ind v u1 a z (Rstar_transitive v w a s2 v2) u2)) + (hyp_ind u t1 y w t2 s1)) (Hyp2 x u v t1 u1). -Theorem caseRxy : (coherence y z). -Proof (Rstar_Rstar' x z h2 - ([v:A][w:A](coherence y w)) - (coherence_sym x y (Rstar_coherence x y h1)) (*i case x=z i*) - Diagram). (*i case x->v->*z i*) +Theorem caseRxy : coherence y z. +Proof + Rstar_Rstar' x z h2 (fun v w:A => coherence y w) + (coherence_sym x y (Rstar_coherence x y h1)) (*i case x=z i*) + Diagram. (*i case x->v->*z i*) End Newman_. -Theorem Ind_proof : (coherence y z). -Proof (Rstar_Rstar' x y h1 ([u:A][v:A](coherence v z)) - (Rstar_coherence x z h2) (*i case x=y i*) - caseRxy). (*i case x->u->*z i*) +Theorem Ind_proof : coherence y z. +Proof + Rstar_Rstar' x y h1 (fun u v:A => coherence v z) + (Rstar_coherence x z h2) (*i case x=y i*) + caseRxy. (*i case x->u->*z i*) End Induct. -Theorem Newman : (x:A)(confluence x). -Proof [x:A](Hyp1 x confluence Ind_proof). +Theorem Newman : forall x:A, confluence x. +Proof fun x:A => Hyp1 x confluence Ind_proof. End Newman_section. End Newman. - |