# Library HistoricalExamples.Newman

Require Import Rstar.

Section Newman.

Variable A : Type.
Variable R : AAProp.

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 zRstar y zcoherence 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 ycoherence 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 ycoherence 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 yRstar x zcoherence y z.

Definition local_confluence (x:A) :=
y z:A, R x yR x zcoherence y z.

Definition noetherian :=
(x:A) (P:AProp),
( y:A, ( z:A, R y zP 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 uconfluence u.

Confluence in x

Variables y z : A.
Hypothesis h1 : Rstar x y.
Hypothesis h2 : Rstar x z.

particular case xu 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 xv 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:Acoherence 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:Acoherence v z)
(Rstar_coherence x z h2)
caseRxy. End Induct.

Theorem Newman : x:A, confluence x.
Proof fun x:AHyp1 x confluence Ind_proof.

End Newman_section.

End Newman.