From 73df1945b31c0beee88cf4476df4ccd09d31403b Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Wed, 26 Jun 2024 20:50:18 +0200
Subject: Import Coq project

---
 sound.v | 630 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 630 insertions(+)
 create mode 100644 sound.v

(limited to 'sound.v')

diff --git a/sound.v b/sound.v
new file mode 100644
index 0000000..761d7ad
--- /dev/null
+++ b/sound.v
@@ -0,0 +1,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.
-- 
cgit v1.2.3