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
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
|
Require Import Coq.Strings.String.
From stdpp Require Import gmap option tactics.
From mininix Require Import binop expr maptools matching relations sem.
Lemma ctx_item_inj E uf_ext uf_int :
is_ctx_item uf_ext uf_int E →
Inj (=) (=) E.
Proof.
intros Hctx.
destruct Hctx; intros e1' e2' Hinj; try congruence.
injection Hinj as Hinj.
by apply map_insert_rev_1_L in Hinj.
Qed.
Global Instance id_inj {A} : Inj (=) (=) (@id A).
Proof. by unfold Inj. Qed.
Lemma ctx_inj E uf_ext uf_int :
is_ctx uf_ext uf_int E →
Inj (=) (=) E.
Proof.
intros Hctx.
induction Hctx.
- apply id_inj.
- apply ctx_item_inj in H.
by apply compose_inj with (=).
Qed.
Lemma base_step_deterministic : deterministic base_step.
Proof.
unfold deterministic.
intros e0 e1 e2 H1 H2.
inv H1; inv H2; try done.
- destruct ys, ys0. by simplify_eq/=.
- destruct ys. by simplify_eq/=.
- destruct ys. by simplify_eq/=.
- apply map_insert_inv in H0. by destruct H0.
- destruct ys. by simplify_eq/=.
- destruct ys. by simplify_eq/=.
- destruct ys, ys0. by simplify_eq/=.
- exfalso. apply H3. by exists bs.
- exfalso. apply H. by exists bs.
- f_equal. by eapply matches_deterministic.
- apply map_insert_inv in H0 as [H01 H02].
by simplify_eq /=.
- f_equal. by eapply binop_deterministic.
- rewrite H4 in H. by apply is_Some_None in H.
- exfalso. apply H4. by exists bs.
- rewrite H in H4. by apply is_Some_None in H4.
- exfalso. apply H. by exists bs.
Qed.
Reserved Notation "e '-/' uf '/->' e'" (right associativity, at level 55).
Inductive fstep : bool → expr → expr → Prop :=
| F_Ctx e1 e2 E uf_ext uf_int :
is_ctx uf_ext uf_int E →
e1 -->base e2 →
E e1 -/uf_ext/-> E e2
where "e -/ uf /-> e'" := (fstep uf e e').
Hint Constructors fstep : core.
Lemma ufstep e e' : e -/false/-> e' ↔ e --> e'.
Proof. split; intros; inv H; by econstructor. Qed.
Lemma fstep_strongly_confluent_aux x uf y1 y2 :
x -/uf/-> y1 →
x -/uf/-> y2 →
y1 = y2 ∨ ∃ z, y1 -/uf/-> z ∧ y2 -/uf/-> z.
Proof.
intros Hstep1 Hstep2.
inv Hstep1 as [b11 b12 E1 uf_int uf_int1 Hctx1 Hbase1].
inv Hstep2 as [b21 b22 E2 uf_int uf_int2 Hctx2 Hbase2].
revert b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H0.
induction Hctx1 as [|E1 E0];
intros b11 b12 b21 b22 E2 Hbase1 Hbase2 Hctx2 H2; inv Hctx2.
- (* L: id, R: id *) left. by eapply base_step_deterministic.
- (* L: id, R: ∘ *) simplify_eq/=.
inv H; try inv select (_ -->base b12);
(inv select (is_ctx _ _ _);
[inv select (b21 -->base b22)
|inv select (is_ctx_item _ _ _)]).
simplify_option_eq.
destruct sv; try discriminate.
exfalso. clear uf. simplify_option_eq.
apply fmap_insert_lookup in H1. simplify_option_eq.
revert bs0 x H H1 Heqo.
induction H2; intros bs0 x H' H1 Heqo; [inv Hbase2|].
simplify_option_eq.
inv H. destruct H'; try discriminate.
inv H1. apply fmap_insert_lookup in H0. simplify_option_eq.
by eapply IHis_ctx.
- (* L: ∘, R: id *) simplify_eq/=.
inv H; try inv select (_ -->base b22);
(inv select (is_ctx _ _ _);
[inv select (b11 -->base b12)
|inv select (is_ctx_item _ _ _)]).
clear IHHctx1.
simplify_option_eq.
destruct sv; try discriminate.
exfalso. simplify_option_eq.
apply fmap_insert_lookup in H0. simplify_option_eq.
revert bs0 x H H0 Heqo.
induction H1; intros bs0 x H' H0 Heqo; [inv Hbase1|].
simplify_option_eq.
inv H. destruct H'; try discriminate.
inv H0. apply fmap_insert_lookup in H2. simplify_option_eq.
by eapply IHis_ctx.
- (* L: ∘, R: ∘ *)
simplify_option_eq.
inv H; inv H0.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_Select z xs).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e, X_Select e xs) ∘ E); try done;
by eapply IsCtx_Compose.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_SelectOr z xs e2).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e1, X_SelectOr e1 xs e2) ∘ E); try done;
by eapply IsCtx_Compose.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_Incl z e2).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e1, X_Incl e1 e2) ∘ E); try done;
by eapply IsCtx_Compose.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_Apply z e2).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e1, X_Apply e1 e2) ∘ E); try done;
by eapply IsCtx_Compose.
+ inv Hctx1; simplify_option_eq.
* inv Hbase1.
* inv H.
+ inv H1; simplify_option_eq.
* inv Hbase2.
* inv H.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H0)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_Apply (V_AttrsetFn m e1) z).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e2, X_Apply (V_AttrsetFn m e1) e2) ∘ E);
try done;
by eapply IsCtx_Compose.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_Cond z e2 e3).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e1, X_Cond e1 e2 e3) ∘ E); try done;
by eapply IsCtx_Compose.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_Assert z e2).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e1, X_Assert e1 e2) ∘ E); try done;
by eapply IsCtx_Compose.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_Op op z e2).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e1, X_Op op e1 e2) ∘ E); try done;
by eapply IsCtx_Compose.
+ inv Hctx1; simplify_option_eq.
* inv Hbase1.
* inv H0.
+ inv H1; simplify_option_eq.
* inv Hbase2.
* inv H0.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H0)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_Op op v1 z).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e2, X_Op op v1 e2) ∘ E); try done;
by eapply IsCtx_Compose.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_HasAttr z x).
split; [inv IHz1 | inv IHz2];
eapply F_Ctx with (E := (λ e, X_HasAttr e x) ∘ E); try done;
by eapply IsCtx_Compose.
+ destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H2)
as [IH | [z [IHz1 IHz2]]].
* left. congruence.
* right. exists (X_Force z).
split.
-- inv IHz1.
(* apply is_ctx_uf_false_impl_true in H0 as []. *)
eapply F_Ctx with (E := X_Force ∘ E); try done;
by eapply IsCtx_Compose.
-- inv IHz2.
eapply F_Ctx with (E := X_Force ∘ E); try done;
by eapply IsCtx_Compose.
+ destruct (decide (x0 = x)).
* simplify_option_eq.
apply map_insert_rev_L in H2 as [H21 H22].
destruct (IHHctx1 _ _ _ _ E4 Hbase1 Hbase2 H1 H21)
as [IH | [z [IHz1 IHz2]]].
-- left. rewrite IH. do 2 f_equal.
by apply map_insert_L.
-- right. exists (V_Attrset (<[x := z]>bs)).
split.
++ inv IHz1.
eapply F_Ctx
with (E := (λ e, X_V $ V_Attrset (<[x := e]>bs)) ∘ E); try done.
by eapply IsCtx_Compose.
++ inv IHz2.
rewrite (map_insert_L _ _ _ _ _ (eq_refl (E e1)) H22).
eapply F_Ctx
with (E := (λ e, X_V $ V_Attrset (<[x := e]>bs)) ∘ E); try done.
by eapply IsCtx_Compose.
* simplify_option_eq.
right. exists (V_Attrset (<[x := E0 b12]>(<[x0 := E4 b22]>bs))).
split.
-- apply map_insert_ne_inv in H2 as H3; try done.
destruct H3.
replace bs with (<[x0 := E4 b21]>bs) at 1; try by rewrite insert_id.
setoid_rewrite insert_commute; try by congruence.
eapply F_Ctx
with (E := (λ e, X_V $ V_Attrset
(<[x0 := e]>(<[x := E0 b12]> bs))) ∘ E4).
++ by eapply IsCtx_Compose.
++ done.
-- apply map_insert_ne_inv in H2 as H3; try done.
destruct H3 as [H31 [H32 H33]].
replace bs0 with (<[x := E0 b11]>bs0) at 1;
try by rewrite insert_id.
rewrite insert_commute; try by congruence.
replace (<[x:=E0 b11]> (<[x0:=E4 b22]> bs0))
with (<[x:=E0 b11]> (<[x0:=E4 b22]> bs)).
2: {
rewrite <-insert_delete_insert.
setoid_rewrite <-insert_delete_insert at 2.
rewrite delete_insert_ne by congruence.
rewrite delete_commute. rewrite <-H33.
rewrite insert_delete_insert.
rewrite <-delete_insert_ne by congruence.
by rewrite insert_delete_insert.
}
eapply F_Ctx with (E := (λ e, X_V $ V_Attrset
(<[x := e]>(<[x0 := E4 b22]>bs))) ∘ E0).
++ by eapply IsCtx_Compose.
++ done.
Qed.
Lemma step_strongly_confluent_aux x y1 y2 :
x --> y1 →
x --> y2 →
y1 = y2 ∨ ∃ z, y1 --> z ∧ y2 --> z.
Proof.
intros Hstep1 Hstep2.
apply ufstep in Hstep1, Hstep2.
destruct (fstep_strongly_confluent_aux _ _ _ _ Hstep1 Hstep2) as [|[?[]]].
- by left.
- right. exists x0. split; by apply ufstep.
Qed.
Theorem step_strongly_confluent : strongly_confluent step.
Proof.
intros x y1 y2 Hy1 Hy2.
destruct (step_strongly_confluent_aux x y1 y2 Hy1 Hy2) as [|[z [Hz1 Hz2]]].
- exists y1. by subst.
- exists z. split.
+ by apply rtc_once.
+ by apply rc_once.
Qed.
Lemma step_semi_confluent : semi_confluent step.
Proof. apply strong__semi_confluence. apply step_strongly_confluent. Qed.
Lemma step_cr : cr step.
Proof. apply semi_confluence__cr. apply step_semi_confluent. Qed.
Theorem step_confluent : confluent step.
Proof. apply confluent_alt. apply step_cr. Qed.
|
