Prove more compatibility lemmas without unfolding the definition

F_mu_ref_conc/context_refinement.v

 From iris_logrel.F_mu_ref_conc Require Export fundamental_binary.
 From iris.proofmode Require Import tactics classes.
+From Autosubst Require Import Autosubst_Classes. (* for [subst] *)
 
 Inductive ctx_item :=
   (* λ-rec *)

F_mu_ref_conc/fundamental_binary.v

 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.
+From iris_logrel.F_mu_ref_conc.proofmode Require Export tactics rel_tactics.
 
 Section fundamental.
 Context `{logrelG Σ}.
@@ -15,7 +12,7 @@ Section masked.
   Variable (E : coPset).
 
   Local Ltac value_case :=
-    iApply related_ret;
+    iApply (related_ret ⊤);
     iApply interp_ret; [solve_to_val..|];
     simpl; eauto.
 
@@ -94,13 +91,9 @@ Section masked.
     iIntros (?) "IH".
     rel_bind_ap e e' "IH" v w "IH".
     iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]". simplify_eq/=.
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    rewrite /env_subst !Closed_subst_p_id.
-    iModIntro.
-    iApply wp_fst; eauto. iNext.
-    iExists v2.
-    tp_fst j; eauto. 
+    rel_proj_l.
+    rel_proj_r.
+    value_case.
   Qed.
 
   Lemma bin_log_related_snd Δ Γ e e' τ1 τ2 :
@@ -111,13 +104,9 @@ Section masked.
     iIntros (?) "IH".
     rel_bind_ap e e' "IH" v w "IH".
     iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]". simplify_eq/=.
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    rewrite /env_subst !Closed_subst_p_id.
-    iModIntro.
-    iApply wp_snd; eauto. iNext.
-    iExists w2.
-    tp_snd j; eauto. 
+    rel_proj_l.
+    rel_proj_r.
+    value_case.
   Qed.
 
   Lemma bin_log_related_app Δ Γ e1 e2 e1' e2' τ1 τ2 :
@@ -128,11 +117,8 @@ Section masked.
     iIntros "IH1 IH2".
     rel_bind_ap e1 e1' "IH1" f f' "Hff".
     rel_bind_ap e2 e2' "IH2" v v' "Hvv".
-    iSpecialize ("Hff" with "Hvv").
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ". iIntros (j K) "Hj /=". iModIntro.
-    rewrite /env_subst !Closed_subst_p_id.
-    by iMod ("Hff" with "Hj").
+    iSpecialize ("Hff" with "Hvv"). simpl.
+    by iApply related_ret.
   Qed.
 
   Lemma bin_log_related_rec Δ (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
@@ -241,35 +227,13 @@ Section masked.
   Proof.
     iIntros (?) "IH1 IH2 IH3".
     rel_bind_ap e0 e0' "IH1" v0 v0' "IH1".
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    iModIntro.
-    rewrite /env_subst !Closed_subst_p_id.
     iDestruct "IH1" as "[Hiv|Hiv]";
     iDestruct "Hiv" as ([w w']) "[% #Hw]"; simplify_eq/=;
-      tp_case j.
-    - iApply wp_case_inl; eauto using to_of_val. fold of_val.
-      iNext.
-      iSpecialize ("IH2" with "Hs [HΓ]"); auto.
-      tp_bind j (env_subst (snd <$> vvs) e1').
-      iApply fupd_wp. iApply (fupd_mask_mono _); eauto.
-      iMod ("IH2" with "Hj") as "IH2". iModIntro.
-      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.
-    - iApply wp_case_inr; eauto using to_of_val. fold of_val.
-      iNext.
-      iSpecialize ("IH3" with "Hs [HΓ]"); auto.
-      tp_bind j (env_subst (snd <$> vvs) e2').
-      iApply fupd_wp. iApply (fupd_mask_mono _); eauto.
-      iMod ("IH3" with "Hj") as "IH3". iModIntro.
-      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.
+      rel_case_l; rel_case_r.
+    - iApply (bin_log_related_app with "IH2").
+      value_case.
+    - iApply (bin_log_related_app with "IH3").
+      value_case.
   Qed.
 
   Lemma bin_log_related_if Δ Γ e0 e1 e2 e0' e1' e2' τ :
@@ -281,15 +245,8 @@ Section masked.
   Proof.
     iIntros (?) "IH1 IH2 IH3".
     rel_bind_ap e0 e0' "IH1" v0 v0' "IH1".
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    iModIntro. rewrite /env_subst !Closed_subst_p_id.
     iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=;
-      tp_if j.
-    - iApply wp_if_true. iNext.
-      smart_bind j (env_subst _ e1) (env_subst _ e1') "IH2" v v' "?".
-    - iApply wp_if_false. iNext.
-      smart_bind j (env_subst _ e2) (env_subst _ e2') "IH3" v v' "?".
+      rel_if_l; rel_if_r; iAssumption.
   Qed.
 
   Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' τ :
@@ -304,12 +261,10 @@ Section masked.
     rel_bind_ap e2 e2' "IH2" v2 v2' "IH2".
     iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
     iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
     destruct (binop_nat_typed_safe op n n' _ Hopτ) as [v' Hopv'].
-    tp_binop j; eauto; tp_normalise j.
-    iApply wp_nat_binop; eauto. iModIntro. iExists _; iSplitL; eauto.
-    iModIntro.
+    rel_op_l; eauto.
+    rel_op_r; eauto.
+    value_case.
     destruct op; simpl in Hopv'; simplify_eq/=; try destruct eq_nat_dec; try destruct le_dec;
       try destruct lt_dec; eauto.
   Qed.
@@ -326,11 +281,10 @@ Section masked.
     rel_bind_ap e2 e2' "IH2" v2 v2' "IH2".
     iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
     iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
     destruct (binop_bool_typed_safe op n n' _ Hopτ) as [v' Hopv'].
-    tp_binop j; eauto; tp_normalise j.
-    iApply wp_nat_binop; eauto. iModIntro. iExists _; iSplitL; eauto.
+    rel_op_l; eauto.
+    rel_op_r; eauto.
+    value_case.
     destruct op; simpl in Hopv'; simplify_eq/=; eauto.
   Qed.
 
@@ -365,17 +319,11 @@ Section masked.
     {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".
+    rel_bind_ap e 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.
+    iApply (related_ret ⊤).
+    iApply (interp_expr_subst Δ τ τ' (TApp v, TApp v')  with "IH").
   Qed.
 
   Lemma bin_log_related_tapp (τi : D) Δ Γ e e' τ :
@@ -420,27 +368,22 @@ Section masked.
     rewrite /= fixpoint_unfold /=.
     change (fixpoint _) with (interp ⊤ ⊤ (TRec τ) Δ).
     iDestruct "IH" as ([w w']) "#[% Hiz]"; simplify_eq/=.
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    rewrite /env_subst !Closed_subst_p_id.
-    tp_fold j; eauto.
-    iApply wp_fold; cbn; auto.
-    iModIntro; iNext. iExists _; iFrame. by rewrite -interp_subst.
+    rel_unfold_l.
+    rel_unfold_r.
+    value_case. 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.
+    rel_bind_ap e e' "IH" v v' "#IH".
+    value_case.
     iExists (v, v'). simpl; iSplit; eauto.
-    iAlways. rewrite -interp_subst. iExists (interp _ _ τ' Δ).
+    iAlways. iExists (⟦ τ' ⟧ Δ).
     iSplit; eauto. iPureIntro. apply _.
+    by rewrite interp_subst.
   Qed.
 
   Lemma bin_log_related_pack (τi : D) Δ Γ e e' τ :
@@ -519,18 +462,13 @@ Section masked.
   Proof.
     iIntros (?) "IH".
     rel_bind_ap e e' "IH" v v' "IH".
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    rewrite /env_subst !Closed_subst_p_id.
-    tp_alloc j as k "Hk"; eauto. iModIntro.
-    iApply wp_atomic; eauto.
-    iApply wp_alloc; eauto. iModIntro. iNext.
-    iIntros (l) "Hl".
+    rel_alloc_l as l "Hl".
+    rel_alloc_r as k "Hk".
     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.
+    rel_vals.
+    iExists (l, k). eauto.
   Qed.
 
   Lemma bin_log_related_load Δ Γ e e' τ :
@@ -541,18 +479,14 @@ Section masked.
     iIntros (?) "IH".
     rel_bind_ap e e' "IH" v v' "IH".
     iDestruct "IH" as ([l l']) "[% Hinv]"; simplify_eq/=.
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    iModIntro.
-    iApply wp_atomic; eauto.
+    rel_load_l_atomic.
     iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
-    iModIntro.
-    iApply (wp_load with "Hw1").
+    iModIntro. iExists _; iFrame "Hw1".
     iNext. iIntros "Hw1".
-    tp_load j.
+    rel_load_r.
     iMod ("Hclose" with "[Hw1 Hw2]").
     { iNext. iExists (w,w'); by iFrame. }
-    iModIntro. iExists w'; by iFrame.
+    rel_vals; eauto.
   Qed.
 
   Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
@@ -565,19 +499,14 @@ Section masked.
     rel_bind_ap e1 e1' "IH1" v v' "IH1".
     iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
     rel_bind_ap e2 e2' "IH2" w w' "IH2".
-    rewrite bin_log_related_eq.
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    iModIntro.
-    rewrite /env_subst !Closed_subst_p_id.
-    iApply wp_atomic; eauto.
+    rel_store_l_atomic.
     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 IH2]").
+    iModIntro. iExists _; iFrame "Hv1".
+    iNext. iIntros "Hw1".
+    rel_store_r.
+    iMod ("Hclose" with "[Hw1 Hv2 IH2]").
     { iNext; iExists (_, _); simpl; iFrame. }
-    iExists (LitV ()); iFrame; auto.
+    by rel_vals.
   Qed.
 
   Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ
@@ -588,36 +517,38 @@ Section masked.
     {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".
+    rel_bind_ap e1 e1' "IH1" v1 v1' "#IH1".
+    rel_bind_ap e2 e2' "IH2" v2 v2' "#IH2".
+    rel_bind_ap e3 e3' "IH3" v3 v3' "#IH3".
     iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
-    iApply wp_atomic; eauto.
+    rel_cas_l_atomic.
     iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
-    iModIntro.
-    iPoseProof ("Hv") as "Hv'".
+    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]").
+    iModIntro. iExists _; iFrame. simpl.
+    destruct (decide (v' = v2)) as [|Hneq]; subst.
+    - iSplitR; first by (iIntros (?); contradiction).
+      iIntros (?). iNext. iIntros "Hv1".
+      iApply fupd_logrel'.
+      iAssert (▷ ⌜v2 = v2'⌝)%I with "[IH2]" as ">%".
+      { rewrite ?interp_EqType_agree; trivial. }
+      iModIntro.
+      rel_cas_suc_r.
+      iMod ("Hclose" with "[-]").
       { iNext; iExists (_, _); by iFrame. }
-      iExists (#♭v true). iModIntro. eauto.
-    - iAssert (▷ ⌜v' ≠ w'⌝)%I as ">%".
+      rel_vals; eauto.
+    - iSplitL; last by (iIntros (?); congruence).
+      iIntros (?). iNext. iIntros "Hv1".
+      iApply fupd_logrel'.
+      iAssert (▷ ⌜v' ≠ v2'⌝)%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]").
+      iModIntro.
+      rel_cas_fail_r.
+      iMod ("Hclose" with "[-]").
       { iNext; iExists (_, _); by iFrame. }
-      iExists (#♭v false); repeat iModIntro; eauto.
+      rel_vals; eauto.
   Qed.
 
   Theorem binary_fundamental_masked Δ Γ e τ :

F_mu_ref_conc/logrel_binary.v

@@ -155,6 +155,7 @@ Section logrel.
     | Tref τ' => interp_ref (interp E1 E2 τ')
     end.
   Notation "⟦ τ ⟧" := (interp ⊤ ⊤ τ).
+  Notation "⟦ τ ⟧ₑ" := (interp_expr ⊤ ⊤ ⟦ τ ⟧).
 
   Definition interp_env (Γ : stringmap type) (E1 E2 : coPset)
       (Δ : listC D) (vvs : stringmap (val * val)) : iProp Σ :=
@@ -218,9 +219,17 @@ Section logrel.
   Qed.
 
   Lemma interp_subst Δ2 τ τ' :
-    interp ⊤ ⊤ τ ((interp ⊤ ⊤ τ' Δ2) :: Δ2) ≡ interp ⊤ ⊤ (τ.[τ'/]) Δ2.
+    ⟦ τ ⟧ ((⟦ τ' ⟧ Δ2) :: Δ2) ≡ ⟦ τ.[τ'/] ⟧ Δ2.
   Proof. apply (interp_subst_up []). Qed.
 
+  Lemma interp_expr_subst Δ2 τ τ' ww :
+    ⟦ τ ⟧ₑ ((⟦ τ' ⟧ Δ2) :: Δ2) ww ≡ ⟦ τ.[τ'/] ⟧ₑ Δ2 ww.
+  Proof.
+    unfold interp_expr.
+    properness; auto.
+    apply interp_subst.
+  Qed.
+
   Lemma interp_env_dom Δ Γ E1 E2 vvs : interp_env Γ E1 E2 Δ vvs ⊢ ⌜dom _ Γ = dom _ vvs⌝.
   Proof. by iIntros "[% ?]". Qed.
 
@@ -398,16 +407,19 @@ Notation "Γ ⊨ e '≤log≤' e' : τ" :=
 Section monadic.
   Context `{logrelG Σ}.
 
-  Lemma related_ret τ Δ e1 e2 Γ `{Closed ∅ e1} `{Closed ∅ e2} E :
-    interp_expr E E ⟦ τ ⟧ Δ (e1,e2) -∗ {E,E;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ%I.
+  Lemma related_ret E1 E2 Δ Γ e1 e2 τ `{Closed ∅ e1} `{Closed ∅ e2} :
+    interp_expr E1 E1 ⟦ τ ⟧ Δ (e1,e2) -∗ {E2,E2;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ%I.
   Proof.
     iIntros "Hτ".
     rewrite bin_log_related_eq /bin_log_related_def.
     iIntros (vvs ρ) "#Hs #HΓ".
-    by rewrite /env_subst !Closed_subst_p_id.
+    rewrite /env_subst !Closed_subst_p_id.
+    iIntros (j K) "Hj /=". iModIntro.
+    iApply fupd_wp. iApply (fupd_mask_mono E1); auto.
+    by iMod ("Hτ" with "Hj") as "Hτ".
   Qed.
 
-  Lemma interp_ret τ Δ e1 e2 v1 v2 E :
+  Lemma interp_ret E τ Δ e1 e2 v1 v2 :
     to_val e1 = Some v1 →
     to_val e2 = Some v2 →
     ⟦ τ ⟧ Δ (v1,v2) -∗ interp_expr E E ⟦ τ ⟧ Δ (e1,e2).
@@ -419,7 +431,7 @@ Section monadic.
     iApply wp_value; eauto.
   Qed.
 
-  Lemma related_bind Δ Γ (e1 e2 : expr) (τ τ' : type) (K K' : list ectx_item) E :
+  Lemma related_bind E Δ Γ (e1 e2 : expr) (τ τ' : type) (K K' : list ectx_item) :
     ({E,E;Δ;Γ} ⊨ e1 ≤log≤ e2 : τ) -∗
     (∀ vv, ⟦ τ ⟧ Δ vv -∗ {E,E;Δ;Γ} ⊨ fill K (of_val (vv.1)) ≤log≤ fill K' (of_val (vv.2)) : τ') -∗
     ({E,E;Δ;Γ} ⊨ fill K e1 ≤log≤ fill K' e2 : τ').