Library HistoricalExamples.Newman

Require Import Rstar.

Section Newman.

Variable A : Type.
Variable R : A → A → Prop.

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 y:A) := ex2 (Rstar x) (Rstar y).

Theorem coherence_intro :
∀ 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 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 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) :=
  ∀ y z:A, Rstar x y → Rstar x z → coherence y z.

Definition local_confluence (x:A) :=
  ∀ 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.

Section Newman_section.

The general hypotheses of the theorem

Hypothesis Hyp1 : noetherian.
Hypothesis Hyp2 : ∀ x:A, local_confluence x.

The induction hypothesis

Section Induct.
Variable x : A.
Hypothesis hyp_ind : ∀ u:A, R x u → confluence u.

Confluence in x

  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.

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

  fun (v:A) (u1:R x v) (u2:Rstar v z) ⇒
    ex2_ind


      (fun (w:A) (s1:Rstar u w) (s2:Rstar v w) ⇒
         ex2_ind


           (fun (a:A) (v1:Rstar y a) (v2:Rstar w a) ⇒
              ex2_ind


                (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 (fun v w:A ⇒ coherence y w)
    (coherence_sym x y (Rstar_coherence x y h1))
    Diagram. End Newman_.

Theorem Ind_proof : coherence y z.
Proof
  Rstar_Rstar' x y h1 (fun u v:A ⇒ coherence v z)
    (Rstar_coherence x z h2)
    caseRxy. End Induct.

Theorem Newman : ∀ x:A, confluence x.
Proof fun x:A ⇒ Hyp1 x confluence Ind_proof.

End Newman_section.

End Newman.

Navigation