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
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
|
Require Import Coq.Strings.String.
From stdpp Require Import base gmap relations tactics.
From mininix Require Import
binop expr interpreter maptools matching relations sem.
Lemma strong_value_stuck sv : ¬ ∃ e, expr_from_strong_value sv --> e.
Proof.
intros []. destruct sv; inv H; inv H1;
simplify_option_eq; (try inv H2); inv H.
Qed.
Lemma strong_value_stuck_rtc sv e:
expr_from_strong_value sv -->* e →
e = expr_from_strong_value sv.
Proof.
intros. inv H.
- reflexivity.
- exfalso. apply strong_value_stuck with (sv := sv). by exists y.
Qed.
Lemma force__strong_value (e : expr) (v : value) :
X_Force e -->* v →
∃ sv, v = value_from_strong_value sv.
Proof.
intros [n Hsteps] % rtc_nsteps.
revert e v Hsteps.
induction n; intros e v Hsteps; inv Hsteps.
inv H0. inv H2; simplify_eq/=.
- inv H3.
exists sv.
apply rtc_nsteps_2 in H1.
apply strong_value_stuck_rtc in H1.
unfold expr_from_strong_value, compose in H1.
congruence.
- inv H0.
destruct (IHn _ _ H1) as [sv Hsv].
by exists sv.
Qed.
Lemma forall2_force__strong_values es (vs : gmap string value) :
map_Forall2 (λ e v', X_Force e -->* X_V v') es vs →
∃ svs, vs = value_from_strong_value <$> svs.
Proof.
revert vs.
induction es using map_ind; intros vs HForall2.
- apply map_Forall2_empty_l_L in HForall2. by exists ∅.
- destruct (map_Forall2_destruct _ _ _ _ _ HForall2)
as [v [m2' [Him2' Heqvs]]]. simplify_eq/=.
apply map_Forall2_insert_inv_strict in HForall2
as [Hstep HForall2]; try done.
apply IHes in HForall2 as [svs Hsvs]. simplify_eq/=.
apply force__strong_value in Hstep as [sv Hsv]. simplify_eq/=.
exists (<[i := sv]>svs). by rewrite fmap_insert.
Qed.
Lemma force_strong_value_forall2_impl es (svs : gmap string strong_value) :
map_Forall2 (λ e v', X_Force e -->* X_V v')
es (value_from_strong_value <$> svs) →
map_Forall2 (λ e sv', X_Force e -->* expr_from_strong_value sv') es svs.
Proof. apply map_Forall2_fmap_r_L. Qed.
Lemma force_map_fmap_union_insert (sws : gmap string strong_value) es k e sv :
X_Force e -->* expr_from_strong_value sv →
X_Force (X_V (V_Attrset (<[k := e]>es ∪
(expr_from_strong_value <$> sws)))) -->*
X_Force (X_V (V_Attrset (<[k := expr_from_strong_value sv]>es ∪
(expr_from_strong_value <$> sws)))).
Proof.
intros [n Hsteps] % rtc_nsteps.
revert sws es k e Hsteps.
induction n; intros sws es k e Hsteps.
- inv Hsteps.
- inv Hsteps.
inv H0.
inv H2.
+ inv H3. inv H1.
* simplify_option_eq. unfold expr_from_strong_value, compose.
by rewrite H4.
* edestruct strong_value_stuck. exists y. done.
+ inv H0. simplify_option_eq.
apply rtc_transitive
with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪
(expr_from_strong_value <$> sws))))).
* do 2 rewrite <-insert_union_l.
apply rtc_once.
eapply E_Ctx
with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪
(expr_from_strong_value <$> sws)))))).
-- eapply IsCtx_Compose.
++ constructor.
++ eapply IsCtx_Compose
with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪
(expr_from_strong_value <$> sws)))))).
** constructor.
** done.
-- done.
* by apply IHn.
Qed.
Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x
(m1 : gmap string B) (m2 : gmap string A) :
m1 !! i = None →
<[i := f x]>m1 ∪ (f <$> m2) = m1 ∪ (f <$> <[i := x]>m2).
Proof.
intros Him1.
rewrite fmap_insert.
rewrite <-insert_union_l.
by rewrite <-insert_union_r.
Qed.
Lemma fmap_insert_union__fmap_union_insert {A B} (f : A → B) i x
(m1 : gmap string A) (m2 : gmap string A) :
m1 !! i = None →
f <$> <[i := x]>m1 ∪ m2 = f <$> m1 ∪ <[i := x]>m2.
Proof.
intros Him1.
do 2 rewrite map_fmap_union.
rewrite 2 fmap_insert.
rewrite <-insert_union_l.
rewrite <-insert_union_r; try done.
rewrite lookup_fmap.
by rewrite Him1.
Qed.
Lemma force_map_fmap_union (sws svs : gmap string strong_value) es :
map_Forall2 (λ e sv, X_Force e -->* expr_from_strong_value sv) es svs →
X_Force (X_V (V_Attrset (es ∪ (expr_from_strong_value <$> sws)))) -->*
X_Force (X_V (V_Attrset (expr_from_strong_value <$> svs ∪ sws))).
Proof.
revert sws svs.
induction es using map_ind; intros sws svs HForall2.
- apply map_Forall2_empty_l_L in HForall2.
subst. by do 2 rewrite map_empty_union.
- apply map_Forall2_destruct in HForall2 as HForall2'.
destruct HForall2' as [sv [svs' [Him2' Heqm2']]]. subst.
apply map_Forall2_insert_inv_strict
in HForall2 as [HForall21 HForall22]; try done.
apply rtc_transitive with (X_Force
(X_V (V_Attrset (<[i := expr_from_strong_value sv]> m ∪
(expr_from_strong_value <$> sws))))).
+ by apply force_map_fmap_union_insert.
+ rewrite insert_union_fmap__union_fmap_insert by done.
rewrite fmap_insert_union__fmap_union_insert by done.
by apply IHes.
Qed.
(* See 194+2024-0525-2305 for proof sketch *)
Lemma force_map_fmap (svs : gmap string strong_value) (es : gmap string expr) :
map_Forall2 (λ e sv, X_Force e -->* expr_from_strong_value sv) es svs →
X_Force (X_V (V_Attrset es)) -->*
X_Force (X_V (V_Attrset (expr_from_strong_value <$> svs))).
Proof.
pose proof (force_map_fmap_union ∅ svs es).
rewrite fmap_empty in H. by do 2 rewrite map_union_empty in H.
Qed.
Lemma id_compose_l {A B} (f : A → B) : id ∘ f = f.
Proof. done. Qed.
Lemma is_ctx_trans uf_ext uf_aux uf_int E1 E2 :
is_ctx uf_ext uf_aux E1 →
is_ctx uf_aux uf_int E2 →
is_ctx uf_ext uf_int (E1 ∘ E2).
Proof.
intros.
induction H.
- induction H0.
+ apply IsCtx_Id.
+ rewrite id_compose_l.
by apply IsCtx_Compose with uf_aux.
- apply IHis_ctx in H0.
replace (E1 ∘ E0 ∘ E2) with (E1 ∘ (E0 ∘ E2)) by done.
by apply IsCtx_Compose with uf_aux.
Qed.
Lemma ctx_mstep e e' E :
e -->* e' → is_ctx false false E → E e -->* E e'.
Proof.
intros.
induction H.
- apply rtc_refl.
- inv H.
pose proof (is_ctx_trans false false uf_int E E0 H0 H2).
eapply rtc_l.
+ replace (E (E0 e1)) with ((E ∘ E0) e1) by done.
eapply E_Ctx; [apply H | apply H3].
+ assumption.
Qed.
Definition is_nonempty_ctx (uf_ext uf_int : bool) (E : expr → expr) :=
∃ E1 E2 uf_aux,
is_ctx_item uf_ext uf_aux E1 ∧
is_ctx uf_aux uf_int E2 ∧ E = E1 ∘ E2.
Lemma nonempty_ctx_mstep e e' uf_int E :
e -->* e' → is_nonempty_ctx false uf_int E → E e -->* E e'.
Proof.
intros Hmstep Hctx.
destruct Hctx as [E1 [E2 [uf_aux [Hctx1 [Hctx2 Hctx3]]]]].
simplify_option_eq.
induction Hmstep.
+ apply rtc_refl.
+ apply rtc_l with (y := (E1 ∘ E2) y).
* inv H.
destruct (is_ctx_uf_false_impl_true E uf_int0 H0).
+++ apply E_Ctx with (E := E1 ∘ (E2 ∘ E)) (uf_int := uf_int0).
++ eapply IsCtx_Compose.
** apply Hctx1.
** eapply is_ctx_trans.
--- apply Hctx2.
--- destruct uf_int; assumption.
++ assumption.
+++ apply E_Ctx with (E := E1 ∘ (E2 ∘ E)) (uf_int := uf_int).
++ eapply IsCtx_Compose.
** apply Hctx1.
** eapply is_ctx_trans; simplify_option_eq.
--- apply Hctx2.
--- constructor.
++ assumption.
* apply IHHmstep.
Qed.
Lemma force_strong_value (sv : strong_value) :
X_Force sv -->* sv.
Proof.
destruct sv using strong_value_ind';
apply rtc_once; eapply E_Ctx with (E := id); constructor.
Qed.
Lemma id_compose_r {A B} (f : A → B) : f ∘ id = f.
Proof. done. Qed.
Lemma force_idempotent e (v' : value) :
X_Force e -->* v' →
X_Force (X_Force e) -->* v'.
Proof.
intros H.
destruct (force__strong_value _ _ H) as [sv Hsv]. subst.
apply rtc_transitive with (y := X_Force sv).
* eapply nonempty_ctx_mstep; try assumption.
rewrite <-id_compose_r.
exists X_Force, id, true.
repeat (split || constructor || done).
* apply force_strong_value.
Qed.
(* Conditional force *)
Definition cforce (uf : bool) e := if uf then X_Force e else e.
Lemma cforce_strong_value uf (sv : strong_value) :
cforce uf sv -->* sv.
Proof. destruct uf; try done. apply force_strong_value. Qed.
Theorem eval_sound_strong n uf e v' :
eval n uf e = Some v' →
cforce uf e -->* v'.
Proof.
revert uf e v'.
induction n; intros uf e v' Heval.
- discriminate.
- destruct e; rewrite eval_S in Heval; simplify_option_eq; try done.
+ (* X_V *)
case_match; simplify_option_eq.
* (* V_Bool *)
replace (V_Bool p) with (value_from_strong_value (SV_Bool p)) by done.
apply cforce_strong_value.
* (* V_Null *)
replace V_Null with (value_from_strong_value SV_Null) by done.
apply cforce_strong_value.
* (* V_Int *)
replace (V_Int n0) with (value_from_strong_value (SV_Int n0)) by done.
apply cforce_strong_value.
* (* V_Str *)
replace (V_Str s) with (value_from_strong_value (SV_Str s)) by done.
apply cforce_strong_value.
* (* V_Fn *)
replace (V_Fn x e) with (value_from_strong_value (SV_Fn x e)) by done.
apply cforce_strong_value.
* (* V_AttrsetFn *)
replace (V_AttrsetFn m e)
with (value_from_strong_value (SV_AttrsetFn m e)) by done.
apply cforce_strong_value.
* (* V_Attrset *)
case_match; simplify_option_eq; try done.
apply map_mapM_Some_L in Heqo. simplify_option_eq.
eapply map_Forall2_impl_L in Heqo. 2: { intros a b. apply IHn. }
destruct (forall2_force__strong_values _ _ Heqo). subst.
apply force_strong_value_forall2_impl in Heqo.
rewrite <-map_fmap_compose. fold expr_from_strong_value.
apply force_map_fmap in Heqo.
apply rtc_transitive
with (y := X_Force (X_V (V_Attrset (expr_from_strong_value <$> x))));
try done.
apply rtc_once.
eapply E_Ctx with (E := id); [constructor|].
replace (X_V (V_Attrset (expr_from_strong_value <$> x)))
with (expr_from_strong_value (SV_Attrset x)) by reflexivity.
apply E_Force.
+ (* X_Attrset *)
apply IHn in Heval.
apply rtc_transitive with (y := cforce uf (V_Attrset (rec_subst bs)));
[|done].
destruct uf; simplify_eq/=.
-- eapply nonempty_ctx_mstep with (E := X_Force).
++ by eapply rtc_once, E_Ctx with (E := id).
++ by exists X_Force, id, true.
-- apply rtc_once. by eapply E_Ctx with (E := id).
+ (* X_LetBinding *)
apply IHn in Heval.
apply rtc_transitive
with (y := cforce uf (subst (closed (rec_subst bs)) e)); [|done].
destruct uf; simplify_eq/=.
-- eapply nonempty_ctx_mstep with (E := X_Force).
++ by eapply rtc_once, E_Ctx with (E := id).
++ by exists X_Force, id, true.
-- apply rtc_once. by eapply E_Ctx with (E := id).
+ (* X_Select *)
case_match. simplify_option_eq.
apply IHn in Heqo. simplify_eq/=.
apply rtc_transitive with (y := cforce uf
(X_Select (V_Attrset H0) (Ne_Cons head tail))).
-- apply ctx_mstep
with (E := cforce uf ∘ (λ e, X_Select e (Ne_Cons head tail))).
++ done.
++ destruct uf; simplify_option_eq.
** eapply IsCtx_Compose; [constructor | by apply is_ctx_once].
** apply is_ctx_once. unfold compose. by simpl.
-- case_match; apply IHn in Heval.
++ apply rtc_transitive with (y := cforce uf H); [|done].
apply rtc_once.
eapply E_Ctx.
** destruct uf; [by apply is_ctx_once | done].
** by replace H0 with (<[head := H]>H0); [|apply insert_id].
++ apply rtc_transitive
with (y := cforce uf (X_Select H (Ne_Cons s l))); [|done].
** eapply rtc_l.
--- eapply E_Ctx.
+++ destruct uf; [by apply is_ctx_once | done].
+++ replace (Ne_Cons head (s :: l))
with (nonempty_cons head (Ne_Cons s l)) by done.
apply E_MSelect.
--- eapply rtc_once.
eapply E_Ctx
with (E := cforce uf ∘ (λ e, X_Select e (Ne_Cons s l))).
+++ destruct uf.
*** eapply IsCtx_Compose; [done | by apply is_ctx_once].
*** apply is_ctx_once. unfold compose. by simpl.
+++ by replace H0
with (<[head := H]>H0); [|apply insert_id].
+ (* X_SelectOr *)
case_match. simplify_option_eq.
apply IHn in Heqo. simplify_eq/=.
apply rtc_transitive
with (y := cforce uf (X_SelectOr (V_Attrset H0) (Ne_Cons head tail) e2)).
-- apply ctx_mstep
with (E := cforce uf ∘ (λ e, X_SelectOr e (Ne_Cons head tail) e2)).
++ done.
++ destruct uf; simplify_option_eq.
** eapply IsCtx_Compose; [constructor | by apply is_ctx_once].
** apply is_ctx_once. unfold compose. by simpl.
-- case_match; try case_match; apply IHn in Heval.
++ apply rtc_transitive with (y := cforce uf e); [|done].
eapply rtc_l.
** eapply E_Ctx.
--- destruct uf; [by apply is_ctx_once | done].
--- replace (Ne_Cons head []) with (nonempty_singleton head)
by done. constructor.
** eapply rtc_l.
--- eapply E_Ctx with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
+++ destruct uf; simplify_option_eq.
*** eapply IsCtx_Compose;
[constructor | by apply is_ctx_once].
*** apply is_ctx_once. unfold compose. by simpl.
+++ by apply E_OpHasAttrTrue.
--- simplify_eq/=.
eapply rtc_l.
+++ eapply E_Ctx with (E := cforce uf).
*** destruct uf; [by apply is_ctx_once | done].
*** apply E_IfTrue.
+++ eapply rtc_once.
eapply E_Ctx with (E := cforce uf).
*** destruct uf; [by apply is_ctx_once | done].
*** by replace H0 with (<[head := e]>H0);
[|apply insert_id].
++ apply rtc_transitive
with (y := cforce uf (X_SelectOr e (Ne_Cons s l) e2)); [|done].
eapply rtc_l.
** eapply E_Ctx.
--- destruct uf; [by apply is_ctx_once | done].
--- replace (Ne_Cons head (s :: l))
with (nonempty_cons head (Ne_Cons s l)) by done.
constructor.
** eapply rtc_l.
--- eapply E_Ctx with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
+++ destruct uf; simplify_option_eq.
*** eapply IsCtx_Compose;
[constructor | by apply is_ctx_once].
*** apply is_ctx_once. unfold compose. by simpl.
+++ by apply E_OpHasAttrTrue.
--- simplify_eq/=.
eapply rtc_l.
+++ eapply E_Ctx with (E := cforce uf).
*** destruct uf; [by apply is_ctx_once | done].
*** apply E_IfTrue.
+++ eapply rtc_once.
eapply E_Ctx
with (E := cforce uf ∘ λ e1,
X_SelectOr e1 (Ne_Cons s l) e2).
*** destruct uf; simplify_option_eq.
---- eapply IsCtx_Compose;
[constructor | by apply is_ctx_once].
---- apply is_ctx_once. unfold compose. by simpl.
*** by replace H0 with (<[head := e]>H0);
[|apply insert_id].
++ apply rtc_transitive with (y := cforce uf e2); [|done].
destruct tail.
** eapply rtc_l.
--- eapply E_Ctx.
+++ destruct uf; [by apply is_ctx_once | done].
+++ replace (Ne_Cons head [])
with (nonempty_singleton head) by done.
constructor.
--- eapply rtc_l.
+++ eapply E_Ctx
with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
*** destruct uf; simplify_option_eq.
---- eapply IsCtx_Compose;
[constructor | by apply is_ctx_once].
---- apply is_ctx_once. unfold compose. by simpl.
*** by apply E_OpHasAttrFalse.
+++ simplify_eq/=.
eapply rtc_once.
eapply E_Ctx with (E := cforce uf).
*** destruct uf; [by apply is_ctx_once | done].
*** apply E_IfFalse.
** eapply rtc_l.
--- eapply E_Ctx.
+++ destruct uf; [by apply is_ctx_once | done].
+++ replace (Ne_Cons head (s :: tail))
with (nonempty_cons head (Ne_Cons s tail)) by done.
constructor.
--- eapply rtc_l.
+++ eapply E_Ctx
with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
*** destruct uf; simplify_option_eq.
---- eapply IsCtx_Compose;
[constructor | by apply is_ctx_once].
---- apply is_ctx_once. unfold compose. by simpl.
*** by apply E_OpHasAttrFalse.
+++ simplify_eq/=.
eapply rtc_once.
eapply E_Ctx with (E := cforce uf).
*** destruct uf; [by apply is_ctx_once | done].
*** apply E_IfFalse.
+ (* X_Apply *)
case_match; simplify_option_eq; apply IHn in Heqo, Heval.
* (* Basic lambda abstraction *)
apply rtc_transitive with (y := cforce uf (X_Apply (V_Fn x e) e2)).
-- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2);
[done|].
destruct uf.
++ by eapply IsCtx_Compose; [|apply is_ctx_once].
++ apply is_ctx_once. unfold compose. by simpl.
-- apply rtc_transitive
with (y := cforce uf (subst {[x := X_Closed e2]} e)); [|done].
eapply rtc_once.
eapply E_Ctx.
++ destruct uf; [by apply is_ctx_once | done].
++ by constructor.
* (* Pattern-matching function *)
apply rtc_transitive
with (y := cforce uf (X_Apply (V_AttrsetFn m e) e2)).
-- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2);
[done|].
destruct uf.
++ by eapply IsCtx_Compose; [|apply is_ctx_once].
++ apply is_ctx_once. unfold compose. by simpl.
-- apply rtc_transitive
with (y := cforce uf (X_Apply (V_AttrsetFn m e) (V_Attrset H0))).
++ apply ctx_mstep
with (E := cforce uf ∘ λ e2, X_Apply (V_AttrsetFn m e) e2).
** by apply IHn in Heqo0.
** destruct uf.
--- by eapply IsCtx_Compose; [|apply is_ctx_once].
--- apply is_ctx_once. unfold compose. by simpl.
++ apply rtc_transitive with (y := cforce uf (X_LetBinding H e));
[|done].
eapply rtc_once.
eapply E_Ctx.
** destruct uf; [by apply is_ctx_once | done].
** apply matches_sound in Heqo1. by constructor.
* (* __functor *)
apply rtc_transitive with (y := cforce uf (X_Apply (V_Attrset bs) e2)).
-- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2);
[done|].
destruct uf.
++ by eapply IsCtx_Compose; [|apply is_ctx_once].
++ apply is_ctx_once. unfold compose. by simpl.
-- apply rtc_transitive
with (y := cforce uf (X_Apply (X_Apply H (V_Attrset bs)) e2));
[|done].
eapply rtc_once.
eapply E_Ctx.
++ destruct uf; [by apply is_ctx_once | done].
++ by replace bs with (<["__functor" := H]>bs); [|apply insert_id].
+ (* X_Cond *)
simplify_option_eq.
apply IHn in Heqo, Heval.
apply rtc_transitive with (y := cforce uf (X_Cond (V_Bool H0) e2 e3)).
* apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Cond e1 e2 e3); [done|].
destruct uf.
-- by eapply IsCtx_Compose; [|apply is_ctx_once].
-- apply is_ctx_once. unfold compose. by simpl.
* destruct H0; eapply rtc_l; try done; eapply E_Ctx; try done;
by destruct uf; [apply is_ctx_once|].
+ (* X_Incl *)
apply IHn in Heqo.
apply rtc_transitive with (y := cforce uf (X_Incl H e2)).
* apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Incl e1 e2).
-- done.
-- destruct uf.
++ eapply IsCtx_Compose; [done | by apply is_ctx_once].
++ unfold compose. apply is_ctx_once. by simpl.
* destruct (decide (attrset H)).
-- destruct H; inv a. simplify_option_eq. apply IHn in Heval.
eapply rtc_l; [|done].
eapply E_Ctx.
++ destruct uf; [by apply is_ctx_once | done].
++ apply E_With.
-- destruct H;
try (eapply rtc_l;
[ eapply E_Ctx;
[ destruct uf; [by apply is_ctx_once | done]
| by apply E_WithNoAttrset ]
| by apply IHn in Heval ]).
destruct n0. by exists bs.
+ (* X_Assert *)
apply IHn in Heqo.
apply rtc_transitive with (y := cforce uf (X_Assert H e2)).
* apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Assert e1 e2); [done|].
destruct uf.
-- by eapply IsCtx_Compose; [|apply is_ctx_once].
-- unfold compose. apply is_ctx_once. by simpl.
* destruct H; try discriminate. destruct p; try discriminate.
apply IHn in Heval. eapply rtc_l; [|done].
eapply E_Ctx; [|done].
by destruct uf; [apply is_ctx_once|].
+ (* X_Binop *)
apply IHn in Heqo, Heqo0.
apply rtc_transitive with (y := cforce uf (X_Op op (X_V H) e2)).
* apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Op op e1 e2).
-- done.
-- destruct uf.
++ eapply IsCtx_Compose; [done | by apply is_ctx_once].
++ unfold compose. apply is_ctx_once. by simpl.
* apply rtc_transitive with (y := cforce uf (X_Op op (X_V H) (X_V H0))).
-- apply ctx_mstep with (E := cforce uf ∘ λ e2, X_Op op (X_V H) e2).
++ done.
++ destruct uf.
** eapply IsCtx_Compose; [done | by apply is_ctx_once].
** unfold compose. apply is_ctx_once. by simpl.
-- eapply rtc_l.
++ eapply E_Ctx with (E := cforce uf).
** destruct uf; [by apply is_ctx_once | done].
** apply E_Op. by apply binop_eval_sound.
++ by apply IHn.
+ (* X_HasAttr *)
apply IHn in Heqo.
apply rtc_transitive with (y := cforce uf (X_HasAttr H x)).
* apply ctx_mstep with (E := cforce uf ∘ λ e, X_HasAttr e x); [done|].
destruct uf.
-- by eapply IsCtx_Compose; [|apply is_ctx_once].
-- unfold compose. apply is_ctx_once. by simpl.
* destruct (decide (attrset H)).
-- case_match; inv a. simplify_option_eq.
apply rtc_transitive
with (y := cforce uf (bool_decide (is_Some (x0 !! x)))).
++ apply rtc_once. eapply E_Ctx.
** destruct uf; [by apply is_ctx_once | done].
** destruct (decide (is_Some (x0 !! x))).
--- rewrite bool_decide_true by done. by constructor.
--- rewrite bool_decide_false by done. constructor.
by apply eq_None_not_Some in n0.
++ destruct uf; [|done].
apply rtc_once. simpl.
replace (V_Bool (bool_decide (is_Some (x0 !! x))))
with (value_from_strong_value
(SV_Bool (bool_decide (is_Some (x0 !! x)))))
by done.
by eapply E_Ctx with (E := id).
-- apply rtc_transitive with (y := cforce uf false).
++ apply rtc_once. eapply E_Ctx.
** destruct uf; [by apply is_ctx_once | done].
** by constructor.
++ assert (Hforce : cforce true false -->* false).
{ apply rtc_once.
simpl.
replace (V_Bool false)
with (value_from_strong_value (SV_Bool false)) by done.
eapply E_Ctx with (E := id); done. }
destruct H; try (by destruct uf; [apply Hforce | done]).
exfalso. apply n0. by exists bs.
+ (* X_Force *)
apply IHn in Heval. clear IHn n.
destruct uf; try done. simplify_eq/=.
by apply force_idempotent.
+ (* X_Closed *)
apply IHn in Heval.
eapply rtc_l; [|done].
eapply E_Ctx; [|done].
* by destruct uf; [apply is_ctx_once|].
+ (* X_Placeholder *)
apply IHn in Heval. clear IHn n.
destruct uf; simplify_eq/=; eapply rtc_l; try done.
-- eapply E_Ctx with (E := X_Force); [by apply is_ctx_once | done].
-- by eapply E_Ctx with (E := id).
Qed.
Lemma value_stuck v : ¬ ∃ e', X_V v --> e'.
Proof.
induction v; intros [e' He']; inversion He';
subst; (inv H0; [inv H1 | inv H2]).
Qed.
Theorem eval_sound_weak e v' n : eval n false e = Some v' → is_nf_of step e v'.
Proof.
intros Heval.
pose proof (eval_sound_strong _ _ _ _ Heval).
split; [done | apply value_stuck].
Qed.
|