From iris_logrel.F_mu_ref_conc Require Export logrel_binary.
From iris.proofmode Require Import tactics.
From iris_logrel.F_mu_ref_conc Require Import lang rules_binary tactics.
From iris.base_logic Require Export big_op.
From iris.program_logic Require Import ectx_lifting.

Section fundamental.
Context `{logrelG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types e : expr.
Implicit Types Δ : listC D.
Hint Resolve to_of_val.

Section masked.
  Variable (E : coPset).

  Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]; repeat iModIntro.

  Local Tactic Notation "smart_bind" ident(j) uconstr(e) uconstr(e') constr(IH) ident(v) ident(w) constr(Hv):=
    try (iModIntro);
    wp_bind e;
    tp_bind j e';
    iSpecialize (IH with "Hs [HΓ] Hj"); eauto;
    iApply fupd_wp; iApply (fupd_mask_mono _); auto;
    iMod IH as IH; iModIntro;
    iApply (wp_wand with IH);
    iIntros (v);
    let vh := iFresh in
    iIntros vh;
    try (iMod vh);
    iDestruct vh as (w) (String.append "[Hj " (String.append Hv " ]")); simpl.

  Lemma bin_log_related_var Δ Γ x τ :
    Γ !! x = Some τ →
    {E,E;Δ;Γ} ⊨ Var x ≤log≤ Var x : τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (? vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
    iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[Hvv' ?]"; first done.
    iDestruct "Hvv'" as %Hvv'.
    cbn-[env_subst].
    rewrite (env_subst_lookup (snd <$> vvs) x v'); last first.
    { rewrite lookup_fmap. by rewrite Hvv'. } 
    rewrite (env_subst_lookup _ x v); last first.
    { rewrite lookup_fmap. by rewrite Hvv'. } 
    iModIntro. value_case; eauto.
  Qed.

  Lemma bin_log_related_unit Δ Γ : {E,E;Δ;Γ} ⊨ Unit ≤log≤ Unit : TUnit.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
    value_case. 
    iExists UnitV; eauto.
  Qed.

  Lemma bin_log_related_nat Δ Γ n : {E,E;Δ;Γ} ⊨ #n n ≤log≤ #n n : TNat.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
    value_case.
    iExists (#nv _); eauto.
  Qed.

  Lemma bin_log_related_bool Δ Γ b : {E,E;Δ;Γ} ⊨ #♭ b ≤log≤ #♭ b : TBool.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
    value_case.
    iExists (#♭v _); eauto.
  Qed.

  Lemma bin_log_related_pair Δ Γ e1 e2 e1' e2' τ1 τ2 :
      {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗
      {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗
      {E,E;Δ;Γ} ⊨ Pair e1 e2 ≤log≤ Pair e1' e2' : TProd τ1 τ2.
  Proof.
    rewrite bin_log_related_eq.
    iIntros "IH1 IH2". iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    cbn.
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v1 w1 "IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" v2 w2 "IH2".
    value_case.
    iExists (PairV w1 w2); iFrame. 
    iExists _, _; eauto.
    iSplit; simpl; eauto.  auto. 
  Qed.

  Lemma bin_log_related_fst Δ Γ e e' τ1 τ2 :
    ↑ specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TProd τ1 τ2 -∗
    {E,E;Δ;Γ} ⊨ Fst e ≤log≤ Fst e' : τ1.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    cbn.
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".    
    iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]".
    simplify_eq/=.
    iApply wp_fst; eauto. iNext.
    iExists v2.
    tp_fst j; eauto. 
  Qed.

  Lemma bin_log_related_snd Δ Γ e e' τ1 τ2 :
    ↑ specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TProd τ1 τ2 -∗
    {E,E;Δ;Γ} ⊨ Snd e ≤log≤ Snd e' : τ2.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    cbn.
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
    iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]".
    simplify_eq.
    iApply wp_snd; eauto. iNext. 
    iExists w2.
    tp_snd j; eauto. 
  Qed.

  Lemma bin_log_related_app Δ Γ e1 e2 e1' e2' τ1 τ2 :
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow τ1 τ2 -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ1 -∗
    {E,E;Δ;Γ} ⊨ App e1 e2 ≤log≤ App e1' e2' :  τ2.
  Proof.
    rewrite bin_log_related_eq.
    iIntros "IH1 IH2".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" f f' "#IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" v v' "IH2".
    iSpecialize ("IH1" with "IH2 Hj").    
    by iMod "IH1". 
  Qed.
    
  Lemma bin_log_related_rec Δ (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
    Closed (x :b: f :b: dom _ Γ) e →
    Closed (x :b: f :b: dom _ Γ) e' →
    □ ({E,E;Δ;<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ)} ⊨ e ≤log≤ e' : τ2) -∗
    {E,E;Δ;Γ} ⊨ Rec f x e ≤log≤ Rec f x e' : TArrow τ1 τ2.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (??) "#Ht".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". cbn.
    iDestruct (interp_env_dom with "HΓ") as %Hdom.    
    (* TODO: how to get rid of/ simplify those proofs? *)
    assert (Closed (x :b: f :b: ∅)
              (env_subst (delete f (delete x (fst <$> vvs))) e)).
    { eapply subst_p_closes; eauto.
      rewrite ?dom_delete_binder Hdom.
      rewrite dom_fmap.
      destruct x as [|x], f as [|f]; cbn-[union difference].
      + set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union_id. 
        set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union_id. 
        set_solver.
      + rewrite ?(right_id ∅ union).
        rewrite (comm union {[x]} {[f]}) !assoc.
        rewrite difference_union_id. 
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
        rewrite difference_union_id. 
        set_solver.
    } 
    assert (Closed (x :b: f :b: ∅)
              (env_subst (delete f (delete x (snd <$> vvs))) e')).
    { eapply subst_p_closes; eauto.
      rewrite ?dom_delete_binder Hdom.
      rewrite dom_fmap.
      destruct x as [|x], f as [|f]; cbn-[union difference].
      + set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union_id. 
        set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union_id. 
        set_solver.
      + rewrite ?(right_id ∅ union).
        rewrite (comm union {[x]} {[f]}) !assoc.
        rewrite difference_union_id. 
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
        rewrite difference_union_id. 
        set_solver.
    }
    iModIntro. value_case; eauto. rewrite decide_left; eauto.
    iExists (RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e')). iIntros "{$Hj} !#".
    iLöb as "IH". iIntros ([v v']) "#Hiv". simpl. iIntros (j' K') "Hj".
    iModIntro. simpl.
    iApply (wp_rec _ f x (subst_p _ e)); eauto 2 using to_of_val. iNext.
    iApply fupd_wp.
    tp_rec j'; auto.
    pose (vvs':=(<[x:=(v,v')]>(<[f:=(RecV f x (subst_p (delete f (delete x (fst <$> vvs))) e), RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e'))]>vvs))).
    iAssert (interp_env (<[x:=τ1]> (<[f:=TArrow τ1 τ2]> Γ)) ⊤ ⊤ Δ vvs') as "#HΓ'".
    { unfold vvs'. destruct f as [|f], x as [|x]; cbn; eauto;
      rewrite -?interp_env_cons -?Hdom; eauto. }
    iSpecialize ("Ht" with "Hs [HΓ']"); eauto.
    iSpecialize ("Ht" $! j' K').
    rewrite {2}/vvs' /env_subst.
    rewrite !fmap_insert' /=.
    rewrite subst_p_insert.
    rewrite !subst_p_insert /=.
    unfold env_subst in *.
    erewrite !subst_p_delete; auto. (* TODO: [auto] solve the [Closed] goal, but [solve_closed] does not *)
    rewrite !(delete_commute_binder _ x f).
    iApply (fupd_mask_mono E); auto.
    iApply ("Ht" with "Hj").
  Qed.

  Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 :
    ↑ specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ1 -∗
    {E,E;Δ;Γ} ⊨ InjL e ≤log≤ InjL e' : (TSum τ1 τ2).
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
    value_case.
    iExists (InjLV w); iFrame.
    iLeft. iExists (_,_); eauto 10.
  Qed.
    
  Lemma bin_log_related_injr Δ Γ e e' τ1 τ2 :
    ↑ specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ2 -∗
    {E,E;Δ;Γ} ⊨ InjR e ≤log≤ InjR e' : TSum τ1 τ2.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v w "IH".
    value_case.
    iExists (InjRV w); iFrame.
    iRight. iExists (_,_); eauto 10.
  Qed.

  Lemma bin_log_related_case Δ Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
    ↑ specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e0 ≤log≤ e0' : TSum τ1 τ2 -∗
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow τ1 τ3 -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow τ2 τ3 -∗ 
    {E,E;Δ;Γ} ⊨ Case e0 e1 e2 ≤log≤ Case e0' e1' e2' : τ3.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH1 IH2 IH3".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
    iDestruct "IH1" as "[Hiv|Hiv]";
    iDestruct "Hiv" as ([w w']) "[% #Hw]"; simplify_eq; iApply fupd_wp.
    - tp_case_inl j; eauto. 
      iApply wp_case_inl; eauto using to_of_val. fold of_val. 
      iSpecialize ("IH2" with "Hs [HΓ]"); auto.
      tp_bind j (env_subst (snd <$> vvs) e1').
      iApply (fupd_mask_mono _); eauto.
      iMod ("IH2" with "Hj") as "IH2". iModIntro. iNext. simpl.
      wp_bind (env_subst (fst <$> vvs) e1).
      iApply (wp_wand with "IH2").
      iIntros (v). iDestruct 1 as (v') "[Hj #Ht]".
      iSpecialize ("Ht" $! (w, w') with "Hw Hj"). cbn.
      by iApply fupd_wp. 
    - tp_case_inr j; eauto. 
      iApply wp_case_inr; eauto using to_of_val. fold of_val. 
      iSpecialize ("IH3" with "Hs [HΓ]"); auto.
      tp_bind j (env_subst (snd <$> vvs) e2').
      iApply (fupd_mask_mono _); eauto.
      iMod ("IH3" with "Hj") as "IH3". iModIntro. iNext. simpl.
      wp_bind (env_subst (fst <$> vvs) e2).
      iApply (wp_wand with "IH3").
      iIntros (v). iDestruct 1 as (v') "[Hj #Ht]".
      iSpecialize ("Ht" $! (w, w') with "Hw Hj"). cbn.
      by iApply fupd_wp.
  Qed.

  Lemma bin_log_related_if Δ Γ e0 e1 e2 e0' e1' e2' τ :
    ↑specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e0 ≤log≤ e0' : TBool -∗
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : τ -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ -∗ 
    {E,E;Δ;Γ} ⊨ If e0 e1 e2 ≤log≤ If e0' e1' e2' : τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH1 IH2 IH3".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e0) (env_subst _ e0') "IH1" v v' "IH1".
    iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=; iApply fupd_wp.
    - tp_if_true j; eauto. iModIntro.
      iApply wp_if_true. iNext. iApply fupd_wp.
      smart_bind j (env_subst _ e1) (env_subst _ e1') "IH2" v v' "?".
    - tp_if_false j; eauto. iModIntro.
      iApply wp_if_false. iNext. iApply fupd_wp.
      smart_bind j (env_subst _ e2) (env_subst _ e2') "IH3" v v' "?".
  Qed.

  Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' :
    ↑specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TNat -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TNat -∗
    {E,E;Δ;Γ} ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : binop_res_type op.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH1 IH2".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "IH2".
    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
    iApply fupd_wp.
    tp_nat_binop j; eauto; tp_normalise j.
    iApply wp_nat_binop. iModIntro. iExists _; iSplitL; eauto.
    repeat iModIntro.
    destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
      try destruct lt_dec; eauto.
  Qed.

  Lemma bin_log_related_tlam Δ Γ e e' τ :
    Closed (dom _ Γ) e →
    Closed (dom _ Γ) e' →
    ↑ specN ⊆ E →
    (∀ (τi : D), ⌜∀ ww, PersistentP (τi ww)⌝ → □ ({E,E;(τi::Δ);Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨ e ≤log≤ e' : τ)) -∗
    {E,E;Δ;Γ} ⊨ TLam e ≤log≤ TLam e' : TForall τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (???) "#IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    iDestruct (interp_env_dom with "HΓ") as %Hdom.
    assert (Closed ∅ (env_subst (fst <$> vvs) e)).
    { eapply subst_p_closes; eauto. rewrite dom_fmap Hdom. rewrite right_id. reflexivity. }
    assert (Closed ∅ (env_subst (snd <$> vvs) e')).
    { eapply subst_p_closes; eauto. rewrite dom_fmap Hdom. rewrite right_id. reflexivity. }
    value_case. rewrite decide_left; eauto. 
    iExists (TLamV (env_subst (snd <$> vvs) e')). cbn.
    iFrame "Hj". iAlways.
    iIntros (τi ? j' K') "Hv /=".
    iApply wp_tlam; eauto. iModIntro; iNext; iApply fupd_wp.
    tp_tlam j'; eauto.
    iSpecialize ("IH" $! τi with "[] Hs [HΓ]"); auto.
    { by rewrite interp_env_ren. }
    iSpecialize ("IH" with "Hv").
    iApply (fupd_mask_mono E); eauto.
  Qed.

  Lemma bin_log_related_tapp' Δ Γ e e' τ τ' :
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TForall τ -∗
    {E,E;Δ;Γ} ⊨ TApp e ≤log≤ TApp e' : τ.[τ'/].
  Proof.
    rewrite bin_log_related_eq.
    iIntros "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
    iSpecialize ("IH" $! (interp ⊤ ⊤ τ' Δ) with "[#]"); [iPureIntro; apply _|].
    iApply wp_wand_r; iSplitL.
    iSpecialize ("IH" with "Hj").
    iApply fupd_wp. iApply "IH". 
    iIntros (w).
    iDestruct 1 as (w') "[Hw Hiw]".
    iExists _; rewrite -interp_subst; eauto. 
  Qed.

  Lemma bin_log_related_tapp (τi : D) Δ Γ e e' τ :
    (∀ ww, PersistentP (τi ww)) →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TForall τ -∗
    {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨ TApp e ≤log≤ TApp e' : τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    wp_bind (env_subst _ e).
    tp_bind j (env_subst _ e').
    iSpecialize ("IH" with "Hs [HΓ] Hj").
    { by rewrite interp_env_ren. }
    iMod "IH" as "IH /=". iModIntro.
    iApply (wp_wand with "IH").
    iIntros (v). iDestruct 1 as (v') "[Hj #IH]".
    iSpecialize ("IH" $! τi with "[]"); auto.
    unfold interp_expr.
    iMod ("IH" with "Hj") as "IH /=".
    done.
  Qed.

  Lemma bin_log_related_fold Δ Γ e e' τ :
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ.[(TRec τ)/] -∗
    {E,E;Δ;Γ} ⊨ Fold e ≤log≤ Fold e' : TRec τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
    value_case. 
    iExists (FoldV v'); iFrame "Hj".
    rewrite fixpoint_unfold /= -interp_subst.
    iExists (_, _); eauto.
  Qed.

  Lemma bin_log_related_unfold Δ Γ e e' τ :
    ↑specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TRec τ -∗
    {E,E;Δ;Γ} ⊨ Unfold e ≤log≤ Unfold e' : τ.[(TRec τ)/].
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
    rewrite /= fixpoint_unfold /=.
    change (fixpoint _) with (interp ⊤ ⊤ (TRec τ) Δ).
    iDestruct "IH" as ([w w']) "#[% Hiz]"; simplify_eq/=.
    iApply fupd_wp.
    tp_fold j; eauto.
    iApply wp_fold; cbn; auto.
    iModIntro; iNext. iExists _; iFrame. by rewrite -interp_subst. 
  Qed.

  Lemma bin_log_related_pack' Δ Γ e e' τ τ' :
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ.[τ'/] -∗
    {E,E;Δ;Γ} ⊨ Pack e ≤log≤ Pack e' : TExists τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "#IH".
    value_case. 
    iExists (PackV v'). simpl. iFrame.
    iExists (v, v'). simpl; iSplit; eauto.
    iAlways. rewrite -interp_subst. iExists (interp _ _ τ' Δ).
    iSplit; eauto. iPureIntro. apply _.
  Qed.

  Lemma bin_log_related_pack (τi : D) Δ Γ e e' τ :
    (∀ ww, PersistentP (τi ww)) →
    {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨ e ≤log≤ e' : τ -∗
    {E,E;Δ;Γ} ⊨ Pack e ≤log≤ Pack e' : TExists τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    wp_bind (env_subst _ e).
    tp_bind j (env_subst _ e').
    iSpecialize ("IH" with "Hs [HΓ] Hj").
    { by rewrite interp_env_ren. }
    iMod "IH" as "IH /=". iModIntro.
    iApply (wp_wand with "IH").
    iIntros (v). iDestruct 1 as (v') "[Hj #IH]".
    value_case.
    iExists (PackV v'). simpl. iFrame.
    iExists (v, v'). simpl; iSplit; eauto.
  Qed.

  Lemma bin_log_related_unpack Δ Γ e1 e1' e2 e2' τ τ2
    (Hmasked : ↑specN ⊆ E) :
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TExists τ -∗
    (∀ (τi : D), ⌜∀ ww, PersistentP (τi ww)⌝ → {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨ e2 ≤log≤ e2' : TArrow τ (Autosubst_Classes.subst (ren (+1)) τ2)) -∗
    {E,E;Δ;Γ} ⊨ Unpack e1 e2 ≤log≤ Unpack e1' e2' : τ2.
  Proof.
    rewrite bin_log_related_eq.
    iIntros "IH1 IH2".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
    iDestruct "IH1" as ([w w']) "[% #Hτi]"; simplify_eq/=.
    iDestruct "Hτi" as (τi) "[% #Hτi]"; simplify_eq/=.
    iApply wp_pack; eauto. iNext.
    iApply fupd_wp. 
    tp_pack j; eauto. iModIntro.
    iSpecialize ("IH2" $! τi with "[] Hs [HΓ]"); auto.
    { by rewrite interp_env_ren. }
    tp_bind j (env_subst (snd <$> vvs) e2').
    iApply fupd_wp. iApply (fupd_mask_mono E); eauto.
    iMod ("IH2" with "Hj") as "IH2". simpl.
    wp_bind (env_subst (fst <$> vvs) e2).
    iApply (wp_wand with "IH2"). iModIntro.
    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".
    iSpecialize ("Hvv'" $! (w,w') with "Hτi Hj"). simpl.
    iMod "Hvv'". 
    iApply (wp_wand with "Hvv'"). clear v v'.
    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".    
    rewrite (interp_weaken [] [τi] Δ _ _ τ2) /=.
    eauto.
  Qed.
  
  Lemma bin_log_related_fork Δ Γ e e' :
    ↑specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TUnit -∗
    {E,E;Δ;Γ} ⊨ Fork e ≤log≤ Fork e' : TUnit.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
    tp_fork j as i "Hi". fold subst_p.  iModIntro.
    iApply wp_fork. fold subst_p. iNext. iSplitL "Hj".
    - iExists UnitV; eauto.
    - iSpecialize ("IH" with "Hs HΓ"). 
      iSpecialize ("IH" $! i []). simpl.
      iSpecialize ("IH" with "Hi"). 
      iApply fupd_wp. iApply (fupd_mask_mono E); eauto.      
      iMod "IH". iApply (wp_wand with "IH"). eauto.
  Qed.

  Lemma bin_log_related_alloc Δ Γ e e' τ :
    ↑specN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ -∗
    {E,E;Δ;Γ} ⊨ Alloc e ≤log≤ Alloc e' : Tref τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
    iApply fupd_wp.
    tp_alloc j as k "Hk"; eauto.  iModIntro.
    iApply wp_atomic; eauto.
    iApply wp_alloc; eauto. iModIntro. iNext.
    iIntros (l) "Hl". 
    iMod (inv_alloc (logN .@ (l,k)) _ (∃ w : val * val,
      l ↦ᵢ w.1 ∗ k ↦ₛ w.2 ∗ interp _ _ τ Δ w)%I with "[Hl Hk IH]") as "HN"; eauto.
    { iNext. iExists (v, v'); simpl; iFrame. }
    iModIntro; iExists (LocV k).
    iFrame "Hj". iExists (l, k); eauto.
  Qed.

  Lemma bin_log_related_load Δ Γ e e' τ :
    ↑specN ⊆ E →
    ↑logN  ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : (Tref τ) -∗
    {E,E;Δ;Γ} ⊨ Load e ≤log≤ Load e' : τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (??) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e) (env_subst _ e') "IH" v v' "IH".
    iDestruct "IH" as ([l l']) "[% Hinv]"; simplify_eq/=. 
    iApply wp_atomic; eauto.
    iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
    iModIntro.
    iApply (wp_load with "Hw1").
    iNext. iIntros "Hw1".
    tp_load j.
    iMod ("Hclose" with "[Hw1 Hw2]").
    { iNext. iExists (w,w'); by iFrame. }
    iModIntro. iExists w'; by iFrame.
  Qed.

  Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
    ↑specN ⊆ E →
    ↑logN  ⊆ E →    
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : (Tref τ) -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ -∗
    {E,E;Δ;Γ} ⊨ Store e1 e2 ≤log≤ Store e1' e2' : TUnit.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (??) "IH1 IH2".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "#IH2".
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=. 
    iApply wp_atomic; eauto.
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
    iModIntro.
    iApply (wp_store with "Hv1"); auto using to_of_val. 
    iNext. iIntros "Hw2".
    tp_store j.
    iMod ("Hclose" with "[Hw2 Hv2]").
    { iNext; iExists (_, _); simpl; iFrame. iFrame "IH2". }
    iExists UnitV; iFrame; auto.
  Qed.

  Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ
    (HEqτ : EqType τ) :
    ↑specN ⊆ E →    
    ↑logN  ⊆ E →    
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref τ -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ -∗
    {E,E;Δ;Γ} ⊨ e3 ≤log≤ e3' : τ -∗
    {E,E;Δ;Γ} ⊨ CAS e1 e2 e3 ≤log≤ CAS e1' e2' e3' : TBool.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (??) "IH1 IH2 IH3".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
    smart_bind j (env_subst _ e2) (env_subst _ e2') "IH2" w w' "#IH2".
    smart_bind j (env_subst _ e3) (env_subst _ e3') "IH3" u u' "#IH3".
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
    iApply wp_atomic; eauto.
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
    iModIntro.
    iPoseProof ("Hv") as "Hv'".
    rewrite {2}[interp _ _ τ Δ (v, v')]interp_EqType_agree; trivial.
    iMod "Hv'" as %Hv'; subst.
    destruct (decide (v' = w)) as [|Hneq]; subst.
    - iAssert (▷ ⌜w' = w⌝)%I as ">%".
      { rewrite ?interp_EqType_agree; trivial. by iSimplifyEq. }
      simpl. iApply (wp_cas_suc with "Hv1"); eauto using to_of_val.
      iNext. iIntros "Hv1".
      tp_cas_suc j; subst; eauto using to_of_val. 
      iMod ("Hclose" with "[Hv1 Hv2]").
      { iNext; iExists (_, _); by iFrame. }
      iExists (#♭v true). iModIntro. eauto. 
    - iAssert (▷ ⌜v' ≠ w'⌝)%I as ">%".
      { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
      simpl. iApply (wp_cas_fail with "Hv1"); eauto.
      iNext. iIntros "Hv1". 
      tp_cas_fail j; eauto.
      iMod ("Hclose" with "[Hv1 Hv2]").
      { iNext; iExists (_, _); by iFrame. }
      iExists (#♭v false); repeat iModIntro; eauto.
  Qed.

  Theorem binary_fundamental_masked Δ Γ e τ :
    ↑specN ⊆ E →
    ↑logN ⊆ E →
    Γ ⊢ₜ e : τ → ({E,E;Δ;Γ} ⊨ e ≤log≤ e : τ)%I.
  Proof.
    intros HspecN HlogN Ht. iInduction Ht as [] "IH" forall (Δ).
    - by iApply bin_log_related_var.
    - iApply bin_log_related_unit.
    - by iApply bin_log_related_nat.
    - by iApply bin_log_related_bool.
    - by iApply (bin_log_related_nat_binop with "[]").
    - by iApply (bin_log_related_pair with "[]").
    - by iApply bin_log_related_fst.
    - by iApply bin_log_related_snd.
    - by iApply bin_log_related_injl.
    - by iApply bin_log_related_injr.
    - by iApply (bin_log_related_case with "[] []").
    - by iApply (bin_log_related_if with "[] []").
    - assert (Closed (x :b: f :b: dom (gset string) Γ) e).
      { apply typed_X_closed in Ht.
        rewrite !dom_insert_binder in Ht.
        revert Ht. destruct x,f; cbn-[union]; 
        (* TODO: why is simple rewriting is not sufficient here? *)
        erewrite ?(left_id ∅); eauto.
        all: apply _. }
      iApply (bin_log_related_rec with "[]"); eauto.
    - by iApply (bin_log_related_app with "[] []").
    - assert (Closed (dom _ Γ) e).
      { apply typed_X_closed in Ht.        
        pose (K:=(dom_fmap (Autosubst_Classes.subst (ren (+1))) Γ)). 
        fold_leibniz. by rewrite -K. }
      iApply bin_log_related_tlam; eauto.
    - by iApply bin_log_related_tapp'.
    - by iApply bin_log_related_fold.
    - by iApply bin_log_related_unfold.
    - by iApply bin_log_related_pack'.
    - iApply (bin_log_related_unpack with "[]"); eauto.
    - by iApply bin_log_related_fork.
    - by iApply bin_log_related_alloc.
    - by iApply bin_log_related_load.
    - by iApply (bin_log_related_store with "[]").
    - by iApply (bin_log_related_CAS with "[] []").
  Qed.
End masked.

Theorem binary_fundamental Γ e τ :
  Γ ⊢ₜ e : τ → (Γ ⊨ e ≤log≤ e : τ)%I.
Proof. by eapply binary_fundamental_masked. Qed.

End fundamental.