Library iris.array_lang.substitution

From iris.array_lang Require Export lang tactics.
From iris.prelude Require Import list.
Import heap_lang.

Arguments subst x es !e /.
Lemma closed_commute x1 es1 x2 es2 e:
  Closed [] es1
  Closed [] es2
  x1 x2
  subst x1 es1 (subst x2 es2 e) = subst x2 es2 (subst x1 es1 e).
Proof.
  revert x1 es1 x2 es2.
  induction e; simplify_eq /=; intros; auto; try (f_equal; eauto; done).
  - repeat (case_decide || simpl_subst); naive_solver.
  - repeat (case_decide || simpl_subst); eauto. by rewrite IHe.
  - repeat (case_decide || simpl_subst); eauto; by rewrite IHe1 // IHe2 //.
Qed.

Definition subst_map := gmap string expr.
Implicit Types S : subst_map.

Definition lsubst l e :=
  fold_right (λ p e', subst (p.1) (p.2) e') e l.
Definition msubst S e := lsubst (map_to_list S) e.

Lemma Permutation_Forall (A: Type) P (l l': list A) :
 Permutation l l' Forall P l Forall P l'.
Proof.
  induction 1; auto.
  - intros (?&?)%Forall_cons; eauto.
  - intros (?&(?&?)%Forall_cons)%Forall_cons; eauto.
Qed.
Instance Permutation_Forall' (A: Type) P: Proper (Permutation ==> iff) (@Forall A P).
Proof. intros ???. split; by apply Permutation_Forall. Qed.

Lemma exists_is_closed e: l, is_closed l e.
Proof.
  induction e;
  try ( []; eauto; done);
  try (eauto; done);
  try (destruct IHe1 as (l1&Hclo1);
        destruct IHe2 as (l2&Hclo2);
        destruct IHe3 as (l3&Hclo3);
         (l1 ++ l2 ++ l3);
        simpl; repeat (apply andb_prop_intro; split); eapply is_closed_weaken; eauto; set_solver);
  try (destruct IHe1 as (l1&Hclo1);
        destruct IHe2 as (l2&Hclo2);
         (l1 ++ l2);
        simpl; repeat (apply andb_prop_intro; split); eapply is_closed_weaken; eauto; set_solver).
  - [x]. rewrite /is_closed // ?bool_decide_spec.
    set_solver.
  - destruct IHe as (l&Hclo). l.
    simpl; eapply is_closed_weaken; eauto.
    set_solver.
Qed.

Lemma is_closed_hd x l e: is_closed l e is_closed (x :: filter (λ y, y x) l) e.
Proof.
  intros; eapply is_closed_weaken; eauto.
  set_unfoldx'. rewrite elem_of_list_filter.
  case (decide (x = x')); naive_solver.
Qed.

Definition ClosedSubst l S := map_Forall (λ x e, Closed l e) S.

Lemma ClosedSubst_subseteq l S1 S2: ClosedSubst l S2 S1 S2 ClosedSubst l S1.
Proof.
  rewrite /ClosedSubst /map_Forall map_subseteq_specHclo Hsub x e Hlook.
  by eapply Hclo, Hsub.
Qed.

Lemma ClosedSubst_map l S: ClosedSubst l S Forall (Closed l) (map_to_list S.*2).
Proof.
  rewrite /ClosedSubst map_Forall_to_list.
  remember (map_to_list S) as lS eqn:Heq.
  assert (Permutation lS (map_to_list S)) as Hperm.
  { rewrite Heq; reflexivity. }
  clear Heq. revert S Hperm. induction lS as [|(x,e) ?]. intros Heq; eauto.
  - econstructor.
  - intros S Heq. rewrite -Heq //=.
    intros (?&?)%Forall_cons. econstructor; eauto.
    efeed pose proof (map_to_list_insert_inv S).
    { rewrite -Heq; reflexivity. }
    assert (NoDup (lS.*1)).
    { apply (NoDup_cons_12 x (lS.*1)).
      replace (x :: lS.*1) with (((x, e) :: lS).*1); auto.
      rewrite Heq. apply NoDup_fst_map_to_list. }
    eapply IHlS.
    × symmetry. by apply map_to_of_list.
    × rewrite map_to_of_list; eauto.
Qed.

Lemma lsubst_app l1 l2 e:
  lsubst (l1 ++ l2) e = lsubst l1 (lsubst l2 e).
Proof. induction l1; auto. by rewrite //= IHl1. Qed.

Lemma lsubst_snoc l x es e:
  lsubst l (subst x es e) = lsubst (l ++ [(x, es)]) e.
Proof. induction l; auto. by rewrite //= IHl. Qed.

Lemma lsubst_cons l x es e:
  subst x es (lsubst l e) = lsubst ((x,es) :: l) e.
Proof. induction l; auto. Qed.

Lemma lsubst_permutation l l' e:
  Forall (Closed []) (l.*2) NoDup (l.*1) Permutation l l' lsubst l e = lsubst l' e.
Proof.
  intros Hclo Hnd Hperm. revert Hnd Hclo e.
  induction Hperm; auto.
  - inversion 1. subst=>//=. intros (?&?)%Forall_cons e. f_equal. eauto.
  - inversion 1 as [|?? Hnin]. subst=>//=. intros (?&(?&?)%Forall_cons)%Forall_cons e.
    apply closed_commute; eauto.
    intros Heq. apply Hnin; rewrite Heq; left.
  - intros. rewrite IHHperm1 //= IHHperm2 //=.
    × by rewrite -Hperm1.
    × by rewrite -Hperm1.
Qed.

Lemma lsubst_subst_commute l x es e:
  Forall (Closed []) (l.*2) NoDup (l.*1)
  Closed [] es x (l.*1)
  lsubst l (subst x es e) = subst x es (lsubst l e).
Proof.
  intros Hclo Hnd Hclo' Hnd'.
  rewrite lsubst_cons lsubst_snoc.
  symmetry. apply lsubst_permutation.
  - econstructor; eauto.
  - econstructor; eauto.
  - apply Permutation_cons_append.
Qed.

Lemma lsubst_foldl l e:
  Forall (Closed []) (l.*2) NoDup (l.*1)
  lsubst l e = fold_left (λ e' p, subst (p.1) (p.2) e') l e.
Proof.
  revert e. induction l; auto. rewrite //=. intros e (?&?)%Forall_cons (?&?)%NoDup_cons.
  simpl. rewrite -lsubst_subst_commute; auto.
Qed.

Lemma lsubst_closed lS l e:
  Closed l e
  ( x, x l x lS.*1)
  lsubst lS e = e.
Proof.
  revert l e. induction lS as [|(x, es)]; auto.
  rewrite //= ⇒ l e Hclo Hnin. rewrite IHlS.
  - eapply is_closed_subst; eauto.
    intros Hin. eapply Hnin; eauto. by left.
  - intros ???. eapply Hnin; eauto. by right.
Qed.

Lemma lsubst_closing_1 lS l2 e:
  Forall (Closed []) (lS.*2)
  Closed (lS.*1 ++ l2) e
  Closed l2 (lsubst lS e).
Proof.
  revert l2 e. induction lS as [|(x, es)] using rev_ind; auto.
  intros l2 e HcloS Hclo.
  rewrite -lsubst_snoc.
  eapply IHlS.
  - move: HcloS. rewrite fmap_app Forall_app. naive_solver.
  - apply is_closed_subst_remove; eauto.
    × move: HcloS. rewrite fmap_app Forall_app Forall_singleton.
      naive_solver.
    × eapply is_closed_perm; eauto.
      rewrite fmap_app //= app_comm_cons.
      apply Permutation_app; last reflexivity.
      symmetry. apply Permutation_cons_append.
Qed.

Lemma lsubst_closing_2 lS l1 l2 e:
  Forall (Closed []) (lS.*2)
  Closed l1 e
  ( x, x l1 x (lS.*1) x l2)
  Closed l2 (lsubst lS e).
Proof.
  intros ???.
  apply lsubst_closing_1; auto.
  eapply is_closed_weaken; eauto.
  set_solver.
Qed.

Lemma lsubst_closing_inv_1 lS l e:
  Forall (Closed []) (lS.*2)
  Closed l (lsubst lS e)
  Closed (lS.*1 ++ l) e.
Proof.
  revert l e. induction lS as [|(x, es)] ; autol2 e HcloS Hclo.
  simpl in Hclo.
  eapply is_closed_subst_inv_1 in Hclo; last by inversion HcloS.
  eapply IHlS in Hclo; last by inversion HcloS.
  eapply is_closed_perm; eauto.
  rewrite fmap_cons //=. rewrite app_comm_cons.
  symmetry; rewrite Permutation_cons_append -assoc //.
Qed.

Lemma lsubst_closing_inv_2 lS l e:
  Forall (Closed []) (lS.*2)
  Closed (lS.*1 ++ l) (lsubst lS e)
  Closed (lS.*1 ++ l) e.
Proof.
  revert l e. induction lS as [|(x, es)] ; autol2 e HcloS Hclo.
  rewrite fmap_cons //= in Hclo ×.
  eapply is_closed_subst_inv_2 in Hclo; last by inversion HcloS.
  eapply is_closed_perm in Hclo; last first.
  { rewrite app_comm_cons Permutation_cons_append -assoc //. }
  eapply IHlS in Hclo; last by inversion HcloS.
  eapply is_closed_perm; eauto.
  rewrite assoc -Permutation_cons_append app_comm_cons //.
Qed.

Lemma elem_of_dom_map_to_list S x:
  x (map_to_list S).*1 x dom (gset string) S.
Proof.
  split.
  - intros ((x'&e)&?&Helem)%elem_of_list_fmap_2.
    subst; eapply elem_of_dom_2, elem_of_map_to_list. eauto.
  - intros [e Heq]%elem_of_dom. eapply elem_of_list_fmap_1_alt; eauto.
    × apply elem_of_map_to_list; eauto.
    × eauto.
Qed.

Lemma msubst_closing_1 S l l' e:
  Closed l e
  ClosedSubst [] S
  ( x, x l x l' x dom (gset string) S)
  Closed l' (msubst S e).
Proof.
  intros Hclo HcloS Hcontains.
  rewrite /msubst. eapply lsubst_closing_2; eauto.
  - by apply ClosedSubst_map.
  - intros x [Hin_l|Hin_dom]%Hcontains; auto.
    left. by apply elem_of_dom_map_to_list.
Qed.

Lemma msubst_closing_2 S l e:
  Closed l e
  ClosedSubst [] S
  ( x, x l x dom (gset string) S)
  Closed [] (msubst S e).
Proof. intros; eapply msubst_closing_1; eauto. Qed.

Lemma msubst_weaken_1 e S1 S2 l:
  Closed l e
  ClosedSubst [] S2
  S1 S2
  ( x, x (dom (gset string) S2) (dom (gset string) S1) x l)
  msubst S1 e = msubst S2 e.
Proof.
  intros Hclo HcloS2 Hcontains Hdom.
  generalize (map_to_list_contains _ _ Hcontains)=>Hcontains_list.
  apply contains_Permutation in Hcontains_list as (lS&Heq).
  rewrite /msubst. rewrite (lsubst_permutation (map_to_list S2) (lS ++ map_to_list S1)); eauto.
  - rewrite lsubst_app.
    pose (l' := filter (λ x, x (dom (gset string) S1)) l).
    erewrite (lsubst_closed lS l'); eauto.
    × eapply (lsubst_closing_2); eauto.
      ** eapply ClosedSubst_map, ClosedSubst_subseteq; eauto.
      ** rewrite /l'x. rewrite elem_of_list_filter -elem_of_dom_map_to_list.
         intros Hin. case (decide (x (map_to_list S1).*1)); eauto.
    × rewrite /l'x. rewrite elem_of_list_filter.
      intros (?&?) HinS.
      eapply (Hdom x); auto. set_unfold.
      split; auto. rewrite -elem_of_dom_map_to_list Heq fmap_app.
      set_solver.
  - by eapply ClosedSubst_map.
  - apply NoDup_fst_map_to_list.
  - rewrite Heq. apply Permutation_app_comm.
Qed.

Lemma msubst_weaken_2 e S1 S2:
  ClosedSubst [] S2
  S1 S2
  ( l, ( x, x dom (gset string) S1 x l) is_closed l e)
  msubst S1 e = msubst S2 e.
Proof.
  intros HcloS Hsub Hclosing.
  eapply (msubst_weaken_1 _ _ _ (map_to_list S1.*1)); eauto.
  - eapply Hclosingx. rewrite elem_of_dom.
    intros (es&Hlook). apply elem_of_list_fmap.
     (x, es); split; auto. rewrite elem_of_map_to_list //.
  - set_unfold. intros x (_&Hnin).
    intros ((?&es)&?&?%elem_of_map_to_list)%elem_of_list_fmap.
    subst. eapply Hnin. apply elem_of_dom; eauto.
Qed.

Lemma msubst_closed e S:
  Closed [] e
  msubst S e = e.
Proof.
  rewrite /msubst. intros. eapply lsubst_closed; eauto.
  set_solver.
Qed.


Lemma filter_cons {A} (a: A) (l: list A) (P: A Prop) Hdec:
  P a @filter _ _ _ P Hdec (a :: l) = a :: @filter _ _ _ P Hdec l.
Proof. induction l; rewrite /filter //= =>?; case_decide; naive_solver. Qed.

Lemma filter_cons_neg {A} (a: A) (l: list A) (P: A Prop) Hdec:
  ¬ P a @filter _ _ _ P Hdec (a :: l) = @filter _ _ _ P Hdec l.
Proof. induction l; rewrite /filter //= =>?; case_decide; naive_solver. Qed.

Lemma lsubst_unfold lS e:
  lsubst lS e =
  match e with
  | Var ylsubst lS (Var y)
  | Rec f y e
     Rec f y $ (lsubst (filter (λ p, BNamed (p.1) f BNamed (p.1) y) lS) e)
  | App e1 e2App (lsubst lS e1) (lsubst lS e2)
  | Lit lLit l
  | UnOp op eUnOp op (lsubst lS e)
  | BinOp op e1 e2BinOp op (lsubst lS e1) (lsubst lS e2)
  | If e0 e1 e2If (lsubst lS e0) (lsubst lS e1) (lsubst lS e2)
  | Pair e1 e2Pair (lsubst lS e1) (lsubst lS e2)
  | Letp y z e1 e2
    Letp y z (lsubst lS e1) (lsubst (filter (λ p, BNamed (p.1) y BNamed (p.1) z) lS) e2)
  | Fst eFst (lsubst lS e)
  | Snd eSnd (lsubst lS e)
  | InjL eInjL (lsubst lS e)
  | InjR eInjR (lsubst lS e)
  | Case e0 e1 e2Case (lsubst lS e0) (lsubst lS e1) (lsubst lS e2)
  | Fork eFork (lsubst lS e)
  | Alloc e ezAlloc (lsubst lS e) (lsubst lS ez)
  | Load eLoad (lsubst lS e)
  | Store e1 e2Store (lsubst lS e1) (lsubst lS e2)
  | CAS e0 e1 e2CAS (lsubst lS e0) (lsubst lS e1) (lsubst lS e2)
  end.
Proof.
  destruct e; auto;
  try (induction lS; auto; rewrite //= IHlS; auto; done).
  - revert f x e. induction lS; auto.
    intros. simpl. rewrite IHlS. simpl.
    case_decide; f_equal.
    × rewrite filter_cons //.
    × rewrite filter_cons_neg //.
  - revert x y e1 e2. induction lS; auto.
    intros. simpl. rewrite IHlS. simpl.
    case_decide; f_equal.
    × rewrite filter_cons //.
    × rewrite filter_cons_neg //.
Qed.

Definition deleteB (x: binder) S :=
  match x with
    | BAnonS
    | BNamed x'delete x' S
  end.

Fixpoint msubst' S (e : expr) : expr :=
  match e with
  | Var y
    match S !! y with
      | NoneVar y
      | Some eses
    end
  | Rec f y e
     Rec f y $ msubst' (deleteB f (deleteB y S)) e
  | App e1 e2App (msubst' S e1) (msubst' S e2)
  | Lit lLit l
  | UnOp op eUnOp op (msubst' S e)
  | BinOp op e1 e2BinOp op (msubst' S e1) (msubst' S e2)
  | If e0 e1 e2If (msubst' S e0) (msubst' S e1) (msubst' S e2)
  | Pair e1 e2Pair (msubst' S e1) (msubst' S e2)
  | Letp y z e1 e2
    Letp y z (msubst' S e1) $ msubst' (deleteB y (deleteB z S)) e2
  | Fst eFst (msubst' S e)
  | Snd eSnd (msubst' S e)
  | InjL eInjL (msubst' S e)
  | InjR eInjR (msubst' S e)
  | Case e0 e1 e2Case (msubst' S e0) (msubst' S e1) (msubst' S e2)
  | Fork eFork (msubst' S e)
  | Alloc e ezAlloc (msubst' S e) (msubst' S ez)
  | Load eLoad (msubst' S e)
  | Store e1 e2Store (msubst' S e1) (msubst' S e2)
  | CAS e0 e1 e2CAS (msubst' S e0) (msubst' S e1) (msubst' S e2)
  end.

Lemma filter_Permutation {A: Type} P pf (l l': list A):
  Permutation l l' Permutation (@filter _ _ _ P pf l) (@filter _ _ _ P pf l').
Proof.
  induction 1; auto.
  - rewrite /filter //=. case_decide; naive_solver.
  - rewrite /filter //= /filter //=. do 2 case_decide; try econstructor; eauto.
  - etransitivity; eauto.
Qed.
Instance filter_Permutation' A P pf: Proper (Permutation ==> Permutation) (@filter A _ _ P pf).
Proof. intros ???. by apply filter_Permutation. Qed.

Lemma deleteB_insert_ne i x e m:
  BNamed i x deleteB x (<[i := e]> m) = <[i := e]> (deleteB x m).
Proof.
  destruct x; rewrite //=.
  intros Hne. rewrite delete_insert_ne //. naive_solver.
Qed.

Lemma lookup_deleteB_None x m j:
  deleteB x m !! j = None x = (BNamed j) m !! j = None.
Proof.
  destruct x; rewrite //=. naive_solver.
  rewrite lookup_delete_None; naive_solver.
Qed.

Lemma filter_deleteB x y S:
  Permutation (filter (λ p, BNamed (p.1) x BNamed (p.1) y) (map_to_list S))
              (map_to_list (deleteB x (deleteB y S))).
Proof.
  induction S using map_ind.
  - rewrite /deleteB. do 2 case_match;
    rewrite //= ?delete_empty ?map_to_list_empty //=.
  - rewrite map_to_list_insert // /filter //=.
    case_decide as Hcase.
    × rewrite deleteB_insert_ne; last naive_solver.
      rewrite deleteB_insert_ne; last naive_solver.
      rewrite map_to_list_insert; last first.
      { rewrite ?lookup_deleteB_None. naive_solver. }
      econstructor; eauto.
    × rewrite IHS. apply eq_subrelation; auto.
      f_equal.
      destruct x as [|s], y as [|s']; rewrite //=.
      ** naive_solver.
      ** rewrite not_and_l in Hcase ×. intros [[]|Hcase%dec_stable]; first congruence.
         inversion Hcase; subst.
         rewrite delete_insert // delete_notin //.
      ** rewrite not_and_l in Hcase ×. intros [Hcase%dec_stable|[]]; last congruence.
         inversion Hcase; subst.
         rewrite delete_insert // delete_notin //.
      ** rewrite not_and_l in Hcase ×. intros [Hcase%dec_stable|Hcase%dec_stable];
         inversion Hcase; subst;
         case (decide (s = s')).
         *** intros →. rewrite delete_insert // ?delete_notin //.
         *** symmetry. rewrite delete_commute delete_insert //.
             rewrite delete_commute //. f_equal.
             rewrite delete_notin //.
         *** intros →. rewrite delete_insert // ?delete_notin //.
         *** rewrite delete_commute delete_insert //.
             rewrite delete_commute //. intros. f_equal.
             rewrite delete_notin //.
Qed.

Lemma ClosedSubst_delete l S x:
  ClosedSubst l S ClosedSubst l (delete x S).
Proof.
  rewrite /ClosedSubst /map_Forall //=.
  intros Hclo i e.
  rewrite lookup_delete_Some=>?. eapply Hclo. naive_solver.
Qed.

Lemma ClosedSubst_deleteB l S x:
  ClosedSubst l S ClosedSubst l (deleteB x S).
Proof.
  destruct x as [|x]; auto.
  rewrite /ClosedSubst /map_Forall //=.
  intros Hclo i e.
  rewrite lookup_delete_Some=>?. eapply Hclo. naive_solver.
Qed.

Lemma ClosedSubst_insert l S x es:
  ClosedSubst l S Closed l es ClosedSubst l (<[x := es]>S).
Proof.
  rewrite /ClosedSubst /map_Forall //=.
  intros HcloS Hclo i e.
  case (decide (x = i)).
  - intros →. rewrite lookup_insert //. naive_solver.
  - intros ?. rewrite lookup_insert_ne //. naive_solver.
Qed.

Lemma msubst_msubst' S e:
  ClosedSubst [] S
  msubst S e = msubst' S e.
Proof.
  revert S. induction eS Hclo;
  try (rewrite /msubst lsubst_unfold //=; f_equal; eauto; done).
  - rewrite /msubst lsubst_unfold //=.
    case_match.
    × assert ( k, Permutation (map_to_list S) (k ++ [(x, e)])) as (k&Hperm).
      { setoid_rewrite Permutation_app_comm.
        apply contains_Permutation.
        rewrite -(map_to_of_list [(x, e)]).
        × apply map_to_list_contains. set_unfold.
          apply map_subseteq_spec.
          intros x' e'.
          case (decide (x = x')).
          ** intros →. rewrite lookup_insert. inversion 1; subst; auto.
          ** intros Hne. rewrite lookup_insert_ne //=.
        × eapply NoDup_singleton. }
      erewrite lsubst_permutation; eauto using ClosedSubst_map.
      ** rewrite lsubst_app //= decide_True //.
         apply (lsubst_closed _ []).
         *** naive_solver.
         *** set_solver.
      ** apply NoDup_fst_map_to_list.
    × apply (lsubst_closed _ [x]); eauto.
      ** rewrite /Closed /is_closed bool_decide_spec; set_solver.
      ** intros x'. rewrite elem_of_dom_map_to_list.
         rewrite not_elem_of_dom. set_solver.
  - rewrite /msubst lsubst_unfold //=.
    f_equal. etransitivity; last (eapply IHe; eauto).
    × symmetry. apply lsubst_permutation.
      ** apply ClosedSubst_map, ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
      ** apply NoDup_fst_map_to_list.
      ** symmetry. apply filter_deleteB.
    × apply ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
  - rewrite /msubst lsubst_unfold //=.
    f_equal; eauto. etransitivity; last (eapply IHe2; eauto).
    × symmetry. apply lsubst_permutation.
      ** apply ClosedSubst_map, ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
      ** apply NoDup_fst_map_to_list.
      ** symmetry. apply filter_deleteB.
    × apply ClosedSubst_deleteB, ClosedSubst_deleteB; eauto.
Qed.

Lemma msubst_insert_1 S x es e:
  ClosedSubst [] S
  Closed [] es
  S !! x = None
  msubst (<[x := es]>S) e = subst x es (msubst S e).
Proof.
  intros HcloS Hclo. rewrite /msubst.
  etransitivity.
  - apply lsubst_permutation.
    × eapply ClosedSubst_map, ClosedSubst_insert; eauto.
    × eapply NoDup_fst_map_to_list.
    × by rewrite map_to_list_insert.
  - auto.
Qed.

Lemma msubst_insert_2 S x es e:
  ClosedSubst [] S
  Closed [] es
  msubst (<[x := es]>S) e = subst x es (msubst (delete x S) e).
Proof.
  intros HcloS Hclo. rewrite -insert_delete.
  apply msubst_insert_1; eauto.
  - by apply ClosedSubst_delete.
  - by apply lookup_delete.
Qed.

Lemma msubst_insert_3 S x es e:
  ClosedSubst [] S
  Closed [] es
  msubst (<[x := es]>S) e = (msubst S (subst x es e)).
Proof.
  intros HcloS Hclo. rewrite /msubst.
  rewrite -insert_delete.
  etransitivity.
  - apply lsubst_permutation.
    × eapply ClosedSubst_map, ClosedSubst_insert; eauto.
      apply ClosedSubst_delete; eauto.
    × eapply NoDup_fst_map_to_list.
    × rewrite map_to_list_insert; first apply Permutation_cons_append.
      apply lookup_delete.
  - rewrite -lsubst_snoc.
    destruct (exists_is_closed e) as (l&Hclo').
    apply (is_closed_hd x) in Hclo'.
    efeed pose proof (msubst_weaken_1) as Hweak;
      try (apply is_closed_subst_remove; eauto); last first.
    { move:Hweak. rewrite /msubst. eauto. }
    × intros x'. rewrite dom_delete. set_unfold.
      intros (?&Hin).
      apply not_and_l in Hin as [?|?%dec_stable].
      ** naive_solver.
      ** subst. rewrite elem_of_list_filter. naive_solver.
    × apply delete_subseteq.
    × eauto.
Qed.

Lemma msubst_closing_inv_1 S l e:
  ClosedSubst [] S
  Closed l (msubst S e)
  Closed (map_to_list S.*1 ++ l) e.
Proof. intros; eapply lsubst_closing_inv_1; eauto using ClosedSubst_map. Qed.

Lemma msubst_closing_inv_2 S x l e:
  ClosedSubst [] S
  Closed l (msubst S e)
  Closed (x :: l) (msubst (delete x S) e).
Proof.
  intros HcloS Hclo.
  case_eq (S !! x).
  - intros es Heq. eapply (is_closed_subst_inv_1 _ _ _ es); first by eapply HcloS.
    erewrite <-msubst_insert_2; eauto.
    by rewrite insert_id.
  - intros. rewrite delete_notin //.
    eapply is_closed_weaken; eauto. set_solver.
Qed.

Lemma msubst_closing_inv_3 S x l e:
  ClosedSubst [] S
  Closed (x :: l) (msubst S e)
  Closed (x :: l) (msubst (delete x S) e).
Proof.
  intros HcloS Hclo.
  case_eq (S !! x).
  - intros es Heq. eapply (is_closed_subst_inv_2 _ _ _ es); first by eapply HcloS.
    erewrite <-msubst_insert_2; eauto.
    by rewrite insert_id.
  - intros. rewrite delete_notin //.
Qed.

Lemma msubst_unfold (S: subst_map) (e : expr):
  ClosedSubst [] S
  msubst S e =
  match e with
  | Var y
    match S !! y with
      | NoneVar y
      | Some eses
    end
  | Rec f y e
     Rec f y $ msubst (deleteB f (deleteB y S)) e
  | App e1 e2App (msubst S e1) (msubst S e2)
  | Lit lLit l
  | UnOp op eUnOp op (msubst S e)
  | BinOp op e1 e2BinOp op (msubst S e1) (msubst S e2)
  | If e0 e1 e2If (msubst S e0) (msubst S e1) (msubst S e2)
  | Pair e1 e2Pair (msubst S e1) (msubst S e2)
  | Letp y z e1 e2
    Letp y z (msubst S e1) $ msubst (deleteB y (deleteB z S)) e2
  | Fst eFst (msubst S e)
  | Snd eSnd (msubst S e)
  | InjL eInjL (msubst S e)
  | InjR eInjR (msubst S e)
  | Case e0 e1 e2Case (msubst S e0) (msubst S e1) (msubst S e2)
  | Fork eFork (msubst S e)
  | Alloc e ezAlloc (msubst S e) (msubst S ez)
  | Load eLoad (msubst S e)
  | Store e1 e2Store (msubst S e1) (msubst S e2)
  | CAS e0 e1 e2CAS (msubst S e0) (msubst S e1) (msubst S e2)
  end.
Proof.
  intros. destruct e; rewrite ?msubst_msubst' //; do 2 eapply ClosedSubst_deleteB; auto.
Qed.