blob: c53db971ed0433cce30b3c95c5f5a0c071905e20 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id: Newman.v,v 1.1.2.1 2004/07/16 19:31:37 herbelin Exp $ i*)
Require Rstar.
Section Newman.
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).
Definition coherence := [x:A][y:A] (exT2 ? (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).
(** 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)).
(** 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).
Definition local_confluence :=
[x:A](y:A)(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 (* 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 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*)
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*)
End Induct.
Theorem Newman : (x:A)(confluence x).
Proof [x:A](Hyp1 x confluence Ind_proof).
End Newman_section.
End Newman.
|
