aboutsummaryrefslogtreecommitdiffstats
path: root/sound.v
diff options
context:
space:
mode:
Diffstat (limited to 'sound.v')
-rw-r--r--sound.v630
1 files changed, 630 insertions, 0 deletions
diff --git a/sound.v b/sound.v
new file mode 100644
index 0000000..761d7ad
--- /dev/null
+++ b/sound.v
@@ -0,0 +1,630 @@
1Require Import Coq.Strings.String.
2From stdpp Require Import base gmap relations tactics.
3From mininix Require Import
4 binop expr interpreter maptools matching relations sem.
5
6Lemma strong_value_stuck sv : ¬ ∃ e, expr_from_strong_value sv --> e.
7Proof.
8 intros []. destruct sv; inv H; inv H1;
9 simplify_option_eq; (try inv H2); inv H.
10Qed.
11
12Lemma strong_value_stuck_rtc sv e:
13 expr_from_strong_value sv -->* e →
14 e = expr_from_strong_value sv.
15Proof.
16 intros. inv H.
17 - reflexivity.
18 - exfalso. apply strong_value_stuck with (sv := sv). by exists y.
19Qed.
20
21Lemma force__strong_value (e : expr) (v : value) :
22 X_Force e -->* v →
23 ∃ sv, v = value_from_strong_value sv.
24Proof.
25 intros [n Hsteps] % rtc_nsteps.
26 revert e v Hsteps.
27 induction n; intros e v Hsteps; inv Hsteps.
28 inv H0. inv H2; simplify_eq/=.
29 - inv H3.
30 exists sv.
31 apply rtc_nsteps_2 in H1.
32 apply strong_value_stuck_rtc in H1.
33 unfold expr_from_strong_value, compose in H1.
34 congruence.
35 - inv H0.
36 destruct (IHn _ _ H1) as [sv Hsv].
37 by exists sv.
38Qed.
39
40Lemma forall2_force__strong_values es (vs : gmap string value) :
41 map_Forall2 (λ e v', X_Force e -->* X_V v') es vs →
42 ∃ svs, vs = value_from_strong_value <$> svs.
43Proof.
44 revert vs.
45 induction es using map_ind; intros vs HForall2.
46 - apply map_Forall2_empty_l_L in HForall2. by exists ∅.
47 - destruct (map_Forall2_destruct _ _ _ _ _ HForall2)
48 as [v [m2' [Him2' Heqvs]]]. simplify_eq/=.
49 apply map_Forall2_insert_inv_strict in HForall2
50 as [Hstep HForall2]; try done.
51 apply IHes in HForall2 as [svs Hsvs]. simplify_eq/=.
52 apply force__strong_value in Hstep as [sv Hsv]. simplify_eq/=.
53 exists (<[i := sv]>svs). by rewrite fmap_insert.
54Qed.
55
56Lemma force_strong_value_forall2_impl es (svs : gmap string strong_value) :
57 map_Forall2 (λ e v', X_Force e -->* X_V v')
58 es (value_from_strong_value <$> svs) →
59 map_Forall2 (λ e sv', X_Force e -->* expr_from_strong_value sv') es svs.
60Proof. apply map_Forall2_fmap_r_L. Qed.
61
62Lemma force_map_fmap_union_insert (sws : gmap string strong_value) es k e sv :
63 X_Force e -->* expr_from_strong_value sv →
64 X_Force (X_V (V_Attrset (<[k := e]>es ∪
65 (expr_from_strong_value <$> sws)))) -->*
66 X_Force (X_V (V_Attrset (<[k := expr_from_strong_value sv]>es ∪
67 (expr_from_strong_value <$> sws)))).
68Proof.
69 intros [n Hsteps] % rtc_nsteps.
70 revert sws es k e Hsteps.
71 induction n; intros sws es k e Hsteps.
72 - inv Hsteps.
73 - inv Hsteps.
74 inv H0.
75 inv H2.
76 + inv H3. inv H1.
77 * simplify_option_eq. unfold expr_from_strong_value, compose.
78 by rewrite H4.
79 * edestruct strong_value_stuck. exists y. done.
80 + inv H0. simplify_option_eq.
81 apply rtc_transitive
82 with (y := X_Force (X_V (V_Attrset (<[k:=E2 e2]> es ∪
83 (expr_from_strong_value <$> sws))))).
84 * do 2 rewrite <-insert_union_l.
85 apply rtc_once.
86 eapply E_Ctx
87 with (E := λ e, X_Force (X_V (V_Attrset (<[k := E2 e]>(es ∪
88 (expr_from_strong_value <$> sws)))))).
89 -- eapply IsCtx_Compose.
90 ++ constructor.
91 ++ eapply IsCtx_Compose
92 with (E1 := (λ e, X_V (V_Attrset (<[k := e]>(es ∪
93 (expr_from_strong_value <$> sws)))))).
94 ** constructor.
95 ** done.
96 -- done.
97 * by apply IHn.
98Qed.
99
100Lemma insert_union_fmap__union_fmap_insert {A B} (f : A → B) i x
101 (m1 : gmap string B) (m2 : gmap string A) :
102 m1 !! i = None →
103 <[i := f x]>m1 ∪ (f <$> m2) = m1 ∪ (f <$> <[i := x]>m2).
104Proof.
105 intros Him1.
106 rewrite fmap_insert.
107 rewrite <-insert_union_l.
108 by rewrite <-insert_union_r.
109Qed.
110
111Lemma fmap_insert_union__fmap_union_insert {A B} (f : A → B) i x
112 (m1 : gmap string A) (m2 : gmap string A) :
113 m1 !! i = None →
114 f <$> <[i := x]>m1 ∪ m2 = f <$> m1 ∪ <[i := x]>m2.
115Proof.
116 intros Him1.
117 do 2 rewrite map_fmap_union.
118 rewrite 2 fmap_insert.
119 rewrite <-insert_union_l.
120 rewrite <-insert_union_r; try done.
121 rewrite lookup_fmap.
122 by rewrite Him1.
123Qed.
124
125Lemma force_map_fmap_union (sws svs : gmap string strong_value) es :
126 map_Forall2 (λ e sv, X_Force e -->* expr_from_strong_value sv) es svs →
127 X_Force (X_V (V_Attrset (es ∪ (expr_from_strong_value <$> sws)))) -->*
128 X_Force (X_V (V_Attrset (expr_from_strong_value <$> svs ∪ sws))).
129Proof.
130 revert sws svs.
131 induction es using map_ind; intros sws svs HForall2.
132 - apply map_Forall2_empty_l_L in HForall2.
133 subst. by do 2 rewrite map_empty_union.
134 - apply map_Forall2_destruct in HForall2 as HForall2'.
135 destruct HForall2' as [sv [svs' [Him2' Heqm2']]]. subst.
136 apply map_Forall2_insert_inv_strict
137 in HForall2 as [HForall21 HForall22]; try done.
138 apply rtc_transitive with (X_Force
139 (X_V (V_Attrset (<[i := expr_from_strong_value sv]> m ∪
140 (expr_from_strong_value <$> sws))))).
141 + by apply force_map_fmap_union_insert.
142 + rewrite insert_union_fmap__union_fmap_insert by done.
143 rewrite fmap_insert_union__fmap_union_insert by done.
144 by apply IHes.
145Qed.
146
147(* See 194+2024-0525-2305 for proof sketch *)
148Lemma force_map_fmap (svs : gmap string strong_value) (es : gmap string expr) :
149 map_Forall2 (λ e sv, X_Force e -->* expr_from_strong_value sv) es svs →
150 X_Force (X_V (V_Attrset es)) -->*
151 X_Force (X_V (V_Attrset (expr_from_strong_value <$> svs))).
152Proof.
153 pose proof (force_map_fmap_union ∅ svs es).
154 rewrite fmap_empty in H. by do 2 rewrite map_union_empty in H.
155Qed.
156
157Lemma id_compose_l {A B} (f : A → B) : id ∘ f = f.
158Proof. done. Qed.
159
160Lemma is_ctx_trans uf_ext uf_aux uf_int E1 E2 :
161 is_ctx uf_ext uf_aux E1 →
162 is_ctx uf_aux uf_int E2 →
163 is_ctx uf_ext uf_int (E1 ∘ E2).
164Proof.
165 intros.
166 induction H.
167 - induction H0.
168 + apply IsCtx_Id.
169 + rewrite id_compose_l.
170 by apply IsCtx_Compose with uf_aux.
171 - apply IHis_ctx in H0.
172 replace (E1 ∘ E0 ∘ E2) with (E1 ∘ (E0 ∘ E2)) by done.
173 by apply IsCtx_Compose with uf_aux.
174Qed.
175
176Lemma ctx_mstep e e' E :
177 e -->* e' → is_ctx false false E → E e -->* E e'.
178Proof.
179 intros.
180 induction H.
181 - apply rtc_refl.
182 - inv H.
183 pose proof (is_ctx_trans false false uf_int E E0 H0 H2).
184 eapply rtc_l.
185 + replace (E (E0 e1)) with ((E ∘ E0) e1) by done.
186 eapply E_Ctx; [apply H | apply H3].
187 + assumption.
188Qed.
189
190Definition is_nonempty_ctx (uf_ext uf_int : bool) (E : expr → expr) :=
191 ∃ E1 E2 uf_aux,
192 is_ctx_item uf_ext uf_aux E1 ∧
193 is_ctx uf_aux uf_int E2 ∧ E = E1 ∘ E2.
194
195Lemma nonempty_ctx_mstep e e' uf_int E :
196 e -->* e' → is_nonempty_ctx false uf_int E → E e -->* E e'.
197Proof.
198 intros Hmstep Hctx.
199 destruct Hctx as [E1 [E2 [uf_aux [Hctx1 [Hctx2 Hctx3]]]]].
200 simplify_option_eq.
201 induction Hmstep.
202 + apply rtc_refl.
203 + apply rtc_l with (y := (E1 ∘ E2) y).
204 * inv H.
205 destruct (is_ctx_uf_false_impl_true E uf_int0 H0).
206 +++ apply E_Ctx with (E := E1 ∘ (E2 ∘ E)) (uf_int := uf_int0).
207 ++ eapply IsCtx_Compose.
208 ** apply Hctx1.
209 ** eapply is_ctx_trans.
210 --- apply Hctx2.
211 --- destruct uf_int; assumption.
212 ++ assumption.
213 +++ apply E_Ctx with (E := E1 ∘ (E2 ∘ E)) (uf_int := uf_int).
214 ++ eapply IsCtx_Compose.
215 ** apply Hctx1.
216 ** eapply is_ctx_trans; simplify_option_eq.
217 --- apply Hctx2.
218 --- constructor.
219 ++ assumption.
220 * apply IHHmstep.
221Qed.
222
223Lemma force_strong_value (sv : strong_value) :
224 X_Force sv -->* sv.
225Proof.
226 destruct sv using strong_value_ind';
227 apply rtc_once; eapply E_Ctx with (E := id); constructor.
228Qed.
229
230Lemma id_compose_r {A B} (f : A → B) : f ∘ id = f.
231Proof. done. Qed.
232
233Lemma force_idempotent e (v' : value) :
234 X_Force e -->* v' →
235 X_Force (X_Force e) -->* v'.
236Proof.
237 intros H.
238 destruct (force__strong_value _ _ H) as [sv Hsv]. subst.
239 apply rtc_transitive with (y := X_Force sv).
240 * eapply nonempty_ctx_mstep; try assumption.
241 rewrite <-id_compose_r.
242 exists X_Force, id, true.
243 repeat (split || constructor || done).
244 * apply force_strong_value.
245Qed.
246
247(* Conditional force *)
248Definition cforce (uf : bool) e := if uf then X_Force e else e.
249
250Lemma cforce_strong_value uf (sv : strong_value) :
251 cforce uf sv -->* sv.
252Proof. destruct uf; try done. apply force_strong_value. Qed.
253
254Theorem eval_sound_strong n uf e v' :
255 eval n uf e = Some v' →
256 cforce uf e -->* v'.
257Proof.
258 revert uf e v'.
259 induction n; intros uf e v' Heval.
260 - discriminate.
261 - destruct e; rewrite eval_S in Heval; simplify_option_eq; try done.
262 + (* X_V *)
263 case_match; simplify_option_eq.
264 * (* V_Bool *)
265 replace (V_Bool p) with (value_from_strong_value (SV_Bool p)) by done.
266 apply cforce_strong_value.
267 * (* V_Null *)
268 replace V_Null with (value_from_strong_value SV_Null) by done.
269 apply cforce_strong_value.
270 * (* V_Int *)
271 replace (V_Int n0) with (value_from_strong_value (SV_Int n0)) by done.
272 apply cforce_strong_value.
273 * (* V_Str *)
274 replace (V_Str s) with (value_from_strong_value (SV_Str s)) by done.
275 apply cforce_strong_value.
276 * (* V_Fn *)
277 replace (V_Fn x e) with (value_from_strong_value (SV_Fn x e)) by done.
278 apply cforce_strong_value.
279 * (* V_AttrsetFn *)
280 replace (V_AttrsetFn m e)
281 with (value_from_strong_value (SV_AttrsetFn m e)) by done.
282 apply cforce_strong_value.
283 * (* V_Attrset *)
284 case_match; simplify_option_eq; try done.
285 apply map_mapM_Some_L in Heqo. simplify_option_eq.
286 eapply map_Forall2_impl_L in Heqo. 2: { intros a b. apply IHn. }
287 destruct (forall2_force__strong_values _ _ Heqo). subst.
288 apply force_strong_value_forall2_impl in Heqo.
289 rewrite <-map_fmap_compose. fold expr_from_strong_value.
290 apply force_map_fmap in Heqo.
291 apply rtc_transitive
292 with (y := X_Force (X_V (V_Attrset (expr_from_strong_value <$> x))));
293 try done.
294 apply rtc_once.
295 eapply E_Ctx with (E := id); [constructor|].
296 replace (X_V (V_Attrset (expr_from_strong_value <$> x)))
297 with (expr_from_strong_value (SV_Attrset x)) by reflexivity.
298 apply E_Force.
299 + (* X_Attrset *)
300 apply IHn in Heval.
301 apply rtc_transitive with (y := cforce uf (V_Attrset (rec_subst bs)));
302 [|done].
303 destruct uf; simplify_eq/=.
304 -- eapply nonempty_ctx_mstep with (E := X_Force).
305 ++ by eapply rtc_once, E_Ctx with (E := id).
306 ++ by exists X_Force, id, true.
307 -- apply rtc_once. by eapply E_Ctx with (E := id).
308 + (* X_LetBinding *)
309 apply IHn in Heval.
310 apply rtc_transitive
311 with (y := cforce uf (subst (closed (rec_subst bs)) e)); [|done].
312 destruct uf; simplify_eq/=.
313 -- eapply nonempty_ctx_mstep with (E := X_Force).
314 ++ by eapply rtc_once, E_Ctx with (E := id).
315 ++ by exists X_Force, id, true.
316 -- apply rtc_once. by eapply E_Ctx with (E := id).
317 + (* X_Select *)
318 case_match. simplify_option_eq.
319 apply IHn in Heqo. simplify_eq/=.
320 apply rtc_transitive with (y := cforce uf
321 (X_Select (V_Attrset H0) (Ne_Cons head tail))).
322 -- apply ctx_mstep
323 with (E := cforce uf ∘ (λ e, X_Select e (Ne_Cons head tail))).
324 ++ done.
325 ++ destruct uf; simplify_option_eq.
326 ** eapply IsCtx_Compose; [constructor | by apply is_ctx_once].
327 ** apply is_ctx_once. unfold compose. by simpl.
328 -- case_match; apply IHn in Heval.
329 ++ apply rtc_transitive with (y := cforce uf H); [|done].
330 apply rtc_once.
331 eapply E_Ctx.
332 ** destruct uf; [by apply is_ctx_once | done].
333 ** by replace H0 with (<[head := H]>H0); [|apply insert_id].
334 ++ apply rtc_transitive
335 with (y := cforce uf (X_Select H (Ne_Cons s l))); [|done].
336 ** eapply rtc_l.
337 --- eapply E_Ctx.
338 +++ destruct uf; [by apply is_ctx_once | done].
339 +++ replace (Ne_Cons head (s :: l))
340 with (nonempty_cons head (Ne_Cons s l)) by done.
341 apply E_MSelect.
342 --- eapply rtc_once.
343 eapply E_Ctx
344 with (E := cforce uf ∘ (λ e, X_Select e (Ne_Cons s l))).
345 +++ destruct uf.
346 *** eapply IsCtx_Compose; [done | by apply is_ctx_once].
347 *** apply is_ctx_once. unfold compose. by simpl.
348 +++ by replace H0
349 with (<[head := H]>H0); [|apply insert_id].
350 + (* X_SelectOr *)
351 case_match. simplify_option_eq.
352 apply IHn in Heqo. simplify_eq/=.
353 apply rtc_transitive
354 with (y := cforce uf (X_SelectOr (V_Attrset H0) (Ne_Cons head tail) e2)).
355 -- apply ctx_mstep
356 with (E := cforce uf ∘ (λ e, X_SelectOr e (Ne_Cons head tail) e2)).
357 ++ done.
358 ++ destruct uf; simplify_option_eq.
359 ** eapply IsCtx_Compose; [constructor | by apply is_ctx_once].
360 ** apply is_ctx_once. unfold compose. by simpl.
361 -- case_match; try case_match; apply IHn in Heval.
362 ++ apply rtc_transitive with (y := cforce uf e); [|done].
363 eapply rtc_l.
364 ** eapply E_Ctx.
365 --- destruct uf; [by apply is_ctx_once | done].
366 --- replace (Ne_Cons head []) with (nonempty_singleton head)
367 by done. constructor.
368 ** eapply rtc_l.
369 --- eapply E_Ctx with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
370 +++ destruct uf; simplify_option_eq.
371 *** eapply IsCtx_Compose;
372 [constructor | by apply is_ctx_once].
373 *** apply is_ctx_once. unfold compose. by simpl.
374 +++ by apply E_OpHasAttrTrue.
375 --- simplify_eq/=.
376 eapply rtc_l.
377 +++ eapply E_Ctx with (E := cforce uf).
378 *** destruct uf; [by apply is_ctx_once | done].
379 *** apply E_IfTrue.
380 +++ eapply rtc_once.
381 eapply E_Ctx with (E := cforce uf).
382 *** destruct uf; [by apply is_ctx_once | done].
383 *** by replace H0 with (<[head := e]>H0);
384 [|apply insert_id].
385 ++ apply rtc_transitive
386 with (y := cforce uf (X_SelectOr e (Ne_Cons s l) e2)); [|done].
387 eapply rtc_l.
388 ** eapply E_Ctx.
389 --- destruct uf; [by apply is_ctx_once | done].
390 --- replace (Ne_Cons head (s :: l))
391 with (nonempty_cons head (Ne_Cons s l)) by done.
392 constructor.
393 ** eapply rtc_l.
394 --- eapply E_Ctx with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
395 +++ destruct uf; simplify_option_eq.
396 *** eapply IsCtx_Compose;
397 [constructor | by apply is_ctx_once].
398 *** apply is_ctx_once. unfold compose. by simpl.
399 +++ by apply E_OpHasAttrTrue.
400 --- simplify_eq/=.
401 eapply rtc_l.
402 +++ eapply E_Ctx with (E := cforce uf).
403 *** destruct uf; [by apply is_ctx_once | done].
404 *** apply E_IfTrue.
405 +++ eapply rtc_once.
406 eapply E_Ctx
407 with (E := cforce uf ∘ λ e1,
408 X_SelectOr e1 (Ne_Cons s l) e2).
409 *** destruct uf; simplify_option_eq.
410 ---- eapply IsCtx_Compose;
411 [constructor | by apply is_ctx_once].
412 ---- apply is_ctx_once. unfold compose. by simpl.
413 *** by replace H0 with (<[head := e]>H0);
414 [|apply insert_id].
415 ++ apply rtc_transitive with (y := cforce uf e2); [|done].
416 destruct tail.
417 ** eapply rtc_l.
418 --- eapply E_Ctx.
419 +++ destruct uf; [by apply is_ctx_once | done].
420 +++ replace (Ne_Cons head [])
421 with (nonempty_singleton head) by done.
422 constructor.
423 --- eapply rtc_l.
424 +++ eapply E_Ctx
425 with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
426 *** destruct uf; simplify_option_eq.
427 ---- eapply IsCtx_Compose;
428 [constructor | by apply is_ctx_once].
429 ---- apply is_ctx_once. unfold compose. by simpl.
430 *** by apply E_OpHasAttrFalse.
431 +++ simplify_eq/=.
432 eapply rtc_once.
433 eapply E_Ctx with (E := cforce uf).
434 *** destruct uf; [by apply is_ctx_once | done].
435 *** apply E_IfFalse.
436 ** eapply rtc_l.
437 --- eapply E_Ctx.
438 +++ destruct uf; [by apply is_ctx_once | done].
439 +++ replace (Ne_Cons head (s :: tail))
440 with (nonempty_cons head (Ne_Cons s tail)) by done.
441 constructor.
442 --- eapply rtc_l.
443 +++ eapply E_Ctx
444 with (E := cforce uf ∘ (λ e1, X_Cond e1 _ _)).
445 *** destruct uf; simplify_option_eq.
446 ---- eapply IsCtx_Compose;
447 [constructor | by apply is_ctx_once].
448 ---- apply is_ctx_once. unfold compose. by simpl.
449 *** by apply E_OpHasAttrFalse.
450 +++ simplify_eq/=.
451 eapply rtc_once.
452 eapply E_Ctx with (E := cforce uf).
453 *** destruct uf; [by apply is_ctx_once | done].
454 *** apply E_IfFalse.
455 + (* X_Apply *)
456 case_match; simplify_option_eq; apply IHn in Heqo, Heval.
457 * (* Basic lambda abstraction *)
458 apply rtc_transitive with (y := cforce uf (X_Apply (V_Fn x e) e2)).
459 -- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2);
460 [done|].
461 destruct uf.
462 ++ by eapply IsCtx_Compose; [|apply is_ctx_once].
463 ++ apply is_ctx_once. unfold compose. by simpl.
464 -- apply rtc_transitive
465 with (y := cforce uf (subst {[x := X_Closed e2]} e)); [|done].
466 eapply rtc_once.
467 eapply E_Ctx.
468 ++ destruct uf; [by apply is_ctx_once | done].
469 ++ by constructor.
470 * (* Pattern-matching function *)
471 apply rtc_transitive
472 with (y := cforce uf (X_Apply (V_AttrsetFn m e) e2)).
473 -- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2);
474 [done|].
475 destruct uf.
476 ++ by eapply IsCtx_Compose; [|apply is_ctx_once].
477 ++ apply is_ctx_once. unfold compose. by simpl.
478 -- apply rtc_transitive
479 with (y := cforce uf (X_Apply (V_AttrsetFn m e) (V_Attrset H0))).
480 ++ apply ctx_mstep
481 with (E := cforce uf ∘ λ e2, X_Apply (V_AttrsetFn m e) e2).
482 ** by apply IHn in Heqo0.
483 ** destruct uf.
484 --- by eapply IsCtx_Compose; [|apply is_ctx_once].
485 --- apply is_ctx_once. unfold compose. by simpl.
486 ++ apply rtc_transitive with (y := cforce uf (X_LetBinding H e));
487 [|done].
488 eapply rtc_once.
489 eapply E_Ctx.
490 ** destruct uf; [by apply is_ctx_once | done].
491 ** apply matches_sound in Heqo1. by constructor.
492 * (* __functor *)
493 apply rtc_transitive with (y := cforce uf (X_Apply (V_Attrset bs) e2)).
494 -- apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Apply e1 e2);
495 [done|].
496 destruct uf.
497 ++ by eapply IsCtx_Compose; [|apply is_ctx_once].
498 ++ apply is_ctx_once. unfold compose. by simpl.
499 -- apply rtc_transitive
500 with (y := cforce uf (X_Apply (X_Apply H (V_Attrset bs)) e2));
501 [|done].
502 eapply rtc_once.
503 eapply E_Ctx.
504 ++ destruct uf; [by apply is_ctx_once | done].
505 ++ by replace bs with (<["__functor" := H]>bs); [|apply insert_id].
506 + (* X_Cond *)
507 simplify_option_eq.
508 apply IHn in Heqo, Heval.
509 apply rtc_transitive with (y := cforce uf (X_Cond (V_Bool H0) e2 e3)).
510 * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Cond e1 e2 e3); [done|].
511 destruct uf.
512 -- by eapply IsCtx_Compose; [|apply is_ctx_once].
513 -- apply is_ctx_once. unfold compose. by simpl.
514 * destruct H0; eapply rtc_l; try done; eapply E_Ctx; try done;
515 by destruct uf; [apply is_ctx_once|].
516 + (* X_Incl *)
517 apply IHn in Heqo.
518 apply rtc_transitive with (y := cforce uf (X_Incl H e2)).
519 * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Incl e1 e2).
520 -- done.
521 -- destruct uf.
522 ++ eapply IsCtx_Compose; [done | by apply is_ctx_once].
523 ++ unfold compose. apply is_ctx_once. by simpl.
524 * destruct (decide (attrset H)).
525 -- destruct H; inv a. simplify_option_eq. apply IHn in Heval.
526 eapply rtc_l; [|done].
527 eapply E_Ctx.
528 ++ destruct uf; [by apply is_ctx_once | done].
529 ++ apply E_With.
530 -- destruct H;
531 try (eapply rtc_l;
532 [ eapply E_Ctx;
533 [ destruct uf; [by apply is_ctx_once | done]
534 | by apply E_WithNoAttrset ]
535 | by apply IHn in Heval ]).
536 destruct n0. by exists bs.
537 + (* X_Assert *)
538 apply IHn in Heqo.
539 apply rtc_transitive with (y := cforce uf (X_Assert H e2)).
540 * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Assert e1 e2); [done|].
541 destruct uf.
542 -- by eapply IsCtx_Compose; [|apply is_ctx_once].
543 -- unfold compose. apply is_ctx_once. by simpl.
544 * destruct H; try discriminate. destruct p; try discriminate.
545 apply IHn in Heval. eapply rtc_l; [|done].
546 eapply E_Ctx; [|done].
547 by destruct uf; [apply is_ctx_once|].
548 + (* X_Binop *)
549 apply IHn in Heqo, Heqo0.
550 apply rtc_transitive with (y := cforce uf (X_Op op (X_V H) e2)).
551 * apply ctx_mstep with (E := cforce uf ∘ λ e1, X_Op op e1 e2).
552 -- done.
553 -- destruct uf.
554 ++ eapply IsCtx_Compose; [done | by apply is_ctx_once].
555 ++ unfold compose. apply is_ctx_once. by simpl.
556 * apply rtc_transitive with (y := cforce uf (X_Op op (X_V H) (X_V H0))).
557 -- apply ctx_mstep with (E := cforce uf ∘ λ e2, X_Op op (X_V H) e2).
558 ++ done.
559 ++ destruct uf.
560 ** eapply IsCtx_Compose; [done | by apply is_ctx_once].
561 ** unfold compose. apply is_ctx_once. by simpl.
562 -- eapply rtc_l.
563 ++ eapply E_Ctx with (E := cforce uf).
564 ** destruct uf; [by apply is_ctx_once | done].
565 ** apply E_Op. by apply binop_eval_sound.
566 ++ by apply IHn.
567 + (* X_HasAttr *)
568 apply IHn in Heqo.
569 apply rtc_transitive with (y := cforce uf (X_HasAttr H x)).
570 * apply ctx_mstep with (E := cforce uf ∘ λ e, X_HasAttr e x); [done|].
571 destruct uf.
572 -- by eapply IsCtx_Compose; [|apply is_ctx_once].
573 -- unfold compose. apply is_ctx_once. by simpl.
574 * destruct (decide (attrset H)).
575 -- case_match; inv a. simplify_option_eq.
576 apply rtc_transitive
577 with (y := cforce uf (bool_decide (is_Some (x0 !! x)))).
578 ++ apply rtc_once. eapply E_Ctx.
579 ** destruct uf; [by apply is_ctx_once | done].
580 ** destruct (decide (is_Some (x0 !! x))).
581 --- rewrite bool_decide_true by done. by constructor.
582 --- rewrite bool_decide_false by done. constructor.
583 by apply eq_None_not_Some in n0.
584 ++ destruct uf; [|done].
585 apply rtc_once. simpl.
586 replace (V_Bool (bool_decide (is_Some (x0 !! x))))
587 with (value_from_strong_value
588 (SV_Bool (bool_decide (is_Some (x0 !! x)))))
589 by done.
590 by eapply E_Ctx with (E := id).
591 -- apply rtc_transitive with (y := cforce uf false).
592 ++ apply rtc_once. eapply E_Ctx.
593 ** destruct uf; [by apply is_ctx_once | done].
594 ** by constructor.
595 ++ assert (Hforce : cforce true false -->* false).
596 { apply rtc_once.
597 simpl.
598 replace (V_Bool false)
599 with (value_from_strong_value (SV_Bool false)) by done.
600 eapply E_Ctx with (E := id); done. }
601 destruct H; try (by destruct uf; [apply Hforce | done]).
602 exfalso. apply n0. by exists bs.
603 + (* X_Force *)
604 apply IHn in Heval. clear IHn n.
605 destruct uf; try done. simplify_eq/=.
606 by apply force_idempotent.
607 + (* X_Closed *)
608 apply IHn in Heval.
609 eapply rtc_l; [|done].
610 eapply E_Ctx; [|done].
611 * by destruct uf; [apply is_ctx_once|].
612 + (* X_Placeholder *)
613 apply IHn in Heval. clear IHn n.
614 destruct uf; simplify_eq/=; eapply rtc_l; try done.
615 -- eapply E_Ctx with (E := X_Force); [by apply is_ctx_once | done].
616 -- by eapply E_Ctx with (E := id).
617Qed.
618
619Lemma value_stuck v : ¬ ∃ e', X_V v --> e'.
620Proof.
621 induction v; intros [e' He']; inversion He';
622 subst; (inv H0; [inv H1 | inv H2]).
623Qed.
624
625Theorem eval_sound_weak e v' n : eval n false e = Some v' → is_nf_of step e v'.
626Proof.
627 intros Heval.
628 pose proof (eval_sound_strong _ _ _ _ Heval).
629 split; [done | apply value_stuck].
630Qed.
generated by cgit v1.2.3 (git 2.45.2) at 2024-12-25 19:30:03 +0000