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
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
|
(* begin hide *)
Require Import Arith.
Require Import Nat.
Require Import Coq.Program.Equality. (* dependent induction *)
Require Import Lia.
(* end hide *)
Require Import L.
Require Import Evaluation.
(** * Uniform Confluence
It turns out that it doesn't matter too much what order we choose
to perform reductions on subterms. Two different choices will
always have a common ancestor downstream. This fact enables the
study of several more complicated values of the lamdba calculus.
*)
(** The uniform confluence of the one-step reduction follows from the
restrictiveness of the relation: the source can only be an
application and the evaluator only has a choice whether to reduce
the left or right hand first before performing a canonical
substitution. *)
Theorem uniform_confluence :
forall (s t1 t2: term),
one_step_reduces_to s t1 -> one_step_reduces_to s t2 ->
t1 = t2 \/ exists (u: term), one_step_reduces_to t1 u /\
one_step_reduces_to t2 u.
Proof.
intros s. induction s as [n | s1 IHs1 s2 IHs2 | x].
- intros t1 t2 Ht1.
apply must_one_step_reduce_from_application in Ht1.
inversion Ht1 as [x Hx]. inversion Hx as [y Hy].
discriminate Hy.
- intros t1 t2 Hst1 Hst2.
inversion Hst1 as [u1 v1 | u1 v1 v1' | u1 u1' v1].
+ inversion Hst2 as [u2 v2 | u2 v2 v2' | u2 u2' v2].
* assert (u1 = u2) as Hu1equ2.
{ rewrite <- H2 in H. injection H as Heq. apply Heq. }
assert (v1 = v2) as Hv1eqv2.
{ rewrite <- H3 in H0. injection H0 as Heq. apply Heq. }
left. rewrite Hu1equ2. rewrite Hv1eqv2. reflexivity.
* apply must_one_step_reduce_from_application in H2.
inversion H2. inversion H6. rewrite H7 in H. discriminate H.
* apply must_one_step_reduce_from_application in H2.
inversion H2. inversion H6. rewrite H7 in H0. discriminate H0.
+ inversion Hst2 as [u2 v2 | u2 v2 v2' | u2 u2' v2].
* apply must_one_step_reduce_from_application in H.
rewrite <- H3 in H. inversion H. inversion H6. discriminate H7.
* assert (v1 = v2 \/ exists (u: term),one_step_reduces_to v1 u /\
one_step_reduces_to v2 u) as Hs1uconf.
{ apply IHs1. apply H. apply H3. }
destruct Hs1uconf.
** left. rewrite H7. reflexivity.
** right. inversion H7 as [x Hx]. exists (app x s2). split.
*** apply one_step_appl. apply Hx.
*** apply one_step_appl. apply Hx.
* right. exists (app v1 v2). split.
** apply one_step_appr. apply H3.
** apply one_step_appl. apply H.
+ inversion Hst2 as [u2 v2 | u2 v2 v2' | u2 u2' v2].
* apply must_one_step_reduce_from_application in H.
rewrite <- H4 in H. inversion H. inversion H6. discriminate H7.
* right. exists (app v2 v1). split.
** apply one_step_appl. apply H3.
** apply one_step_appr. apply H.
* assert (v1 = v2 \/ exists (u: term),one_step_reduces_to v1 u /\
one_step_reduces_to v2 u) as Hs2uconf.
{ apply IHs2. apply H. apply H3. }
destruct Hs2uconf.
** left. rewrite H7. reflexivity.
** right. inversion H7 as [x Hx]. exists (app s1 x). split.
*** apply one_step_appr. apply Hx.
*** apply one_step_appr. apply Hx.
- intros t1 t2 Ht1. apply must_one_step_reduce_from_application in Ht1.
inversion Ht1. inversion H. discriminate H0.
Qed.
Theorem measured_uniform_confluence :
forall (s t1 t2: term) (m n: nat),
n_step_reduces_to m s t1 -> n_step_reduces_to n s t2 ->
exists (u: term) (k l: nat),
n_step_reduces_to k t1 u /\ n_step_reduces_to l t2 u /\
m + k = n + l /\ k <= n /\ l <= m.
Proof.
assert (forall (c m n: nat) (s t1 t2: term),
m <= c -> n <= c -> n_step_reduces_to m s t1 ->
n_step_reduces_to n s t2 -> exists (u: term) (k l: nat),
n_step_reduces_to k t1 u /\ n_step_reduces_to l t2 u /\
(m + k = n + l) /\ k <= n /\ l <= m) as Hequiv.
{ induction c.
- intros m n s t1 t2 Hm Hn Hst1 Hst2.
apply Nat.le_0_r in Hm. apply Nat.le_0_r in Hn.
rewrite Hm in Hst1. inversion Hst1.
rewrite Hn in Hst2. inversion Hst2.
exists s. exists 0. exists 0.
split. rewrite <- H1. apply n_step_refl.
split. rewrite <- H3. apply n_step_refl. lia.
- intros m n s t1 t2 Hm Hn Hst1 Hst2.
inversion Hst1 as [s' Hmeq Hs'eq Ht1eq |
m' s' u1 t1' Hu1onestep
Hu1nstep Hmeq Hs'eq Ht1eq].
+ exists t2. exists n. exists 0.
split. rewrite <- Ht1eq. apply Hst2. split. apply n_step_refl. lia.
+ inversion Hst2 as [s'' Hneq Hs''eq Ht2eq |
n' s'' u2 t2' Hu2onestep
Hu2nstep Hneq Hs''eq Ht2eq].
* exists t1. exists 0. exists m.
split. apply n_step_refl. split. rewrite <- Ht2eq. apply Hst1. lia.
* (* branch on c = 0 (one step reduction case) *)
destruct (1 <=? c) eqn:E.
(* c > 0 case: extend diamonds to form induction *)
{ assert (c > 0) as Hcgt0. { apply Nat.leb_le in E. lia. }
(* build top diamond with uniform confluence *)
assert (u1 = u2 \/ exists (w: term),
one_step_reduces_to u1 w /\
one_step_reduces_to u2 w) as Hw.
{ apply uniform_confluence with (s:=s).
apply Hu1onestep. apply Hu2onestep. }
destruct Hw.
- (* u1 = u2 case *)
assert (exists (u: term) (k l: nat),
n_step_reduces_to k t1 u /\ n_step_reduces_to l t2 u /\
m' + k = n' + l /\ k <= n' /\ l <= m') as Heq.
{ apply IHc with (s:=u1). lia. lia. apply Hu1nstep.
rewrite H. apply Hu2nstep. }
inversion Heq as [u Hequ]. inversion Hequ as [k Hequk].
inversion Hequk as [l Hequkl].
exists u. exists k. exists l.
split. apply Hequkl. split. apply Hequkl. lia.
- (* u1 <> u2 case: three more diamonds to form inductive diamond *)
inversion H as [w Hw].
(* left diamond: t1, w flow to r1 *)
assert (exists (r1: term) (k1 l1: nat),
n_step_reduces_to k1 t1 r1 /\ n_step_reduces_to l1 w r1 /\
m' + k1 = 1 + l1 /\ k1 <= 1 /\ l1 <= m') as Hleft.
{ apply IHc with (s:=u1). lia. lia.
apply Hu1nstep. apply n_step_incr with (u:=w). apply Hw.
apply n_step_refl. }
(* right diamond: t2, w flow to r2 *)
assert (exists (r2: term) (k2 l2: nat),
n_step_reduces_to k2 t2 r2 /\ n_step_reduces_to l2 w r2 /\
n' + k2 = 1 + l2 /\ k2 <= 1 /\ l2 <= n') as Hright.
{ apply IHc with (s:=u2). lia. lia.
apply Hu2nstep. apply n_step_incr with (u:=w). apply Hw.
apply n_step_refl. }
(* bottom diamond: r1, r2 flow from w into x. *)
inversion Hleft as [r1 Hleftr1]. inversion Hleftr1 as [k1 Hleftr1k1].
inversion Hleftr1k1 as [l1 HleftAll].
inversion Hright as [r2 Hrightr2]. inversion Hrightr2 as [k2 Hrightr2k2].
inversion Hrightr2k2 as [l2 HrightAll].
assert (exists (x: term) (p1 p2: nat),
n_step_reduces_to p1 r1 x /\ n_step_reduces_to p2 r2 x /\
l1 + p1 = l2 + p2 /\ p1 <= l2 /\ p2 <= l1) as Hbottom.
{ apply IHc with (s:=w). lia. lia. apply HleftAll. apply HrightAll. }
(* showing the four diamonds evidence x is as expected *)
inversion Hbottom as [x Hx]. inversion Hx as [p1 Hxp1].
inversion Hxp1 as [p2 HbottomAll].
exists x. exists (k1 + p1). exists (k2 + p2).
split. apply n_step_transitivity with (y:=r1).
apply HleftAll. apply HbottomAll.
split. apply n_step_transitivity with (y:=r2).
apply HrightAll. apply HbottomAll. lia. }
(* c = 0: special case of one step reductions *)
{ assert (c = 0) as Hceq0. { apply Nat.leb_gt in E. lia. }
assert (m <= 1) as Hmleq1. { lia. }
assert (m = 1) as Hmeq1.
{ apply Nat.le_1_r in Hmleq1. inversion Hmleq1.
- rewrite H in Hmeq. discriminate Hmeq.
- apply H. }
assert (n <= 1) as Hnleq1. { lia. }
assert (n = 1) as Hneq1.
{ apply Nat.le_1_r in Hnleq1. inversion Hnleq1.
- rewrite H in Hneq. discriminate Hneq.
- apply H. }
assert (m' = 0) as Hm'eq0. { lia. }
assert (n' = 0) as Hn'eq0. { lia. }
assert (one_step_reduces_to s t1) as Hleft.
{ rewrite Hm'eq0 in Hu1nstep. inversion Hu1nstep.
rewrite <- H1. apply Hu1onestep. }
assert (one_step_reduces_to s t2) as Hright.
{ rewrite Hn'eq0 in Hu2nstep. inversion Hu2nstep.
rewrite <- H1. apply Hu2onestep. }
specialize uniform_confluence with (s:=s) (t1:=t1) (t2:=t2) as Huc.
assert (t1 = t2 \/ (exists u : term, one_step_reduces_to t1 u /\
one_step_reduces_to t2 u))
as HucFinal.
{ apply Huc. apply Hleft. apply Hright. }
destruct HucFinal.
- exists t1. exists 0. exists 0.
split. apply n_step_refl. split. rewrite H. apply n_step_refl. lia.
- inversion H as [u Hu].
exists u. exists 1. exists 1.
split. apply n_step_incr with (u:=u). apply Hu. apply n_step_refl.
split. apply n_step_incr with (u:=u). apply Hu. apply n_step_refl.
lia. } }
(* now we simply rewrite in terms of the original statement *)
intros s t1 t2 m n Hst1 Hst2.
apply Hequiv with (c := m + n) (s:=s).
lia. lia. apply Hst1. apply Hst2.
Qed.
Corollary reduction_is_confluent :
forall (s t1 t2: term), reduces_to s t1 -> reduces_to s t2 ->
exists (u: term), reduces_to t1 u /\ reduces_to t2 u.
Proof.
intros s t1 t2 Hst1 Hst2.
apply reduction_is_realized in Hst1. inversion Hst1 as [m Hm].
apply reduction_is_realized in Hst2. inversion Hst2 as [n Hn].
specialize measured_uniform_confluence with (s:=s) (t1:=t1) (t2:=t2) (m:=m) (n:=n) as Huc.
apply Huc in Hm. inversion Hm as [u Hu]. inversion Hu as [k Huk]. inversion Huk as [l Hukl].
exists u. split.
apply reduction_is_realized. exists k. apply Hukl.
apply reduction_is_realized. exists l. apply Hukl.
apply Hn.
Qed.
|
