Remove the persistence requirements from the exists interpretation

theories/logrel/fundamental_binary.v

@@ -367,12 +367,11 @@ Section fundamental.
   Qed.
 
   Lemma bin_log_related_tapp (τi : D) Δ Γ e e' τ :
-    (∀ ww, Persistent (τi ww)) →
     {Δ;Γ} ⊨ e ≤log≤ e' : TForall τ -∗
     {τi::Δ;⤉Γ} ⊨ TApp e ≤log≤ TApp e' : τ.
   Proof.
     rewrite bin_log_related_eq.
-    iIntros (?) "IH".
+    iIntros "IH".
     iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
     wp_bind (env_subst _ e).
     tp_bind j (env_subst _ e').
@@ -417,18 +416,16 @@ Section fundamental.
     rel_bind_ap e e' "IH" v v' "#IH".
     value_case.
     iExists (v, v'). iModIntro. simpl; iSplit; eauto.
-    iExists (⟦ τ' ⟧ Δ).
-    iSplit; eauto. iPureIntro. apply _.
+    iExists (⟦ τ' ⟧ Δ).    
     by rewrite interp_subst.
   Qed.
 
   Lemma bin_log_related_pack (τi : D) Δ Γ e e' τ :
-    (∀ ww, Persistent (τi ww)) →
     {τi::Δ;⤉Γ} ⊨ e ≤log≤ e' : τ -∗
     {Δ;Γ} ⊨ Pack e ≤log≤ Pack e' : TExists τ.
   Proof.
     rewrite bin_log_related_eq.
-    iIntros (?) "IH".
+    iIntros "IH".
     iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
     wp_bind (env_subst _ e).
     tp_bind j (env_subst _ e').
@@ -444,7 +441,7 @@ Section fundamental.
 
   Lemma bin_log_related_unpack Δ Γ e1 e1' e2 e2' τ τ2 :
     {Δ;Γ} ⊨ e1 ≤log≤ e1' : TExists τ -∗
-    (∀ τi : D, ⌜∀ ww, Persistent (τi ww)⌝ →
+    (∀ τi : D,
       {τi::Δ;⤉Γ} ⊨
         e2 ≤log≤ e2' : TArrow τ (asubst (ren (+1)) τ2)) -∗
     {Δ;Γ} ⊨ Unpack e1 e2 ≤log≤ Unpack e1' e2' : τ2.
@@ -454,11 +451,11 @@ Section fundamental.
     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/=.
+    iDestruct "Hτi" as (τi) "#Hτi"; simplify_eq/=.
     wp_unpack.
     iApply fupd_wp.
     tp_pack j; eauto. iModIntro.
-    iSpecialize ("IH2" $! τi with "[] Hs [HΓ]"); auto.
+    iSpecialize ("IH2" $! τi with "Hs [HΓ]"); auto.
     { by rewrite interp_env_ren. }
     tp_bind j (env_subst (snd <$> vvs) e2').
     iMod ("IH2" with "Hj") as "IH2". simpl.

theories/logrel/semtypes.v

@@ -77,8 +77,6 @@ Section semtypes.
   Program Definition interp_forall (E : coPset)
       (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
     (□ ∀ τi,
-          (* □ (∀ ww, (τi ww -∗ □ (τi ww))) → *)
-          (* ⌜∀ ww, Persistent (τi ww)⌝ → *)
           interp_expr E
             interp (τi :: Δ) (TApp (of_val (ww.1)), TApp (of_val (ww.2))))%I.
   Solve Obligations with solve_proper.
@@ -86,7 +84,7 @@ Section semtypes.
   Program Definition interp_exists
       (interp : listC D -n> D) : listC D -n> D := λne Δ ww,
     (∃ vv, ⌜ww = (PackV (vv.1), PackV (vv.2))⌝
-     ∧ ∃ τi : D, ⌜∀ ww, Persistent (τi ww)⌝ ∧ interp (τi :: Δ) vv)%I.
+     ∧ ∃ τi : D, interp (τi :: Δ) vv)%I.
   Solve Obligations with solve_proper.
 
   Program Definition interp_rec1