Add an ElimModal instance for the relational interpretation

F_mu_ref_conc/examples/counter.v

@@ -122,7 +122,6 @@ Section CG_Counter.
       iApply (steps_CG_increment E with "Hspec Hx"); auto. }
     Unshelve. all: trivial.
   Qed.
-
   
   Lemma bin_log_related_CG_locked_increment Γ K E1 E2 t τ x n l :
     nclose specN ⊆ E1 →
@@ -337,10 +336,9 @@ Section CG_Counter.
       iApply (bin_log_related_load_r _ [] with "[Hcnt']"); auto.
         { solve_ndisj. } { by compute. }
       iIntros "Hcnt'".
-      iApply fupd_logrel.
       iMod ("Hclose" with "[Hl Hcnt Hcnt']").
       { iNext. iExists _. by iFrame. }
-      simpl. iModIntro.
+      simpl. 
       iPoseProof (bin_log_related_nat [TArrow TUnit TNat; TUnit] ⊤ n) as "H". iFrame "H". (* TODO: iApply does not work in this case *)
    - Transparent CG_locked_increment.
      unfold CG_locked_increment.
@@ -363,7 +361,6 @@ Section CG_Counter.
      iInv counterN as (n) "[>Hl [Hcnt >Hcnt']]" "Hclose". iModIntro.
      iExists (#nv n). iSplit; eauto. iFrame "Hcnt".
      iIntros "Hcnt". simpl.
-     iApply fupd_logrel.
      iMod ("Hclose" with "[Hl Hcnt Hcnt']").
      { iNext. iExists _. iFrame "Hl Hcnt Hcnt'". }
      iApply (bin_log_related_rec_l _ []); auto. iNext. asimpl.
@@ -381,7 +378,6 @@ Section CG_Counter.
        iApply (bin_log_related_CG_locked_increment _ [] with "Hcnt' Hl");
          auto. solve_ndisj.
        iIntros "Hcnt' Hl". 
-       iApply fupd_logrel.
        iMod ("Hclose" with "[Hl Hcnt Hcnt']").
        { iNext. iExists (S m). iFrame. }
        iApply (bin_log_related_if_true_l _ []); auto.
@@ -391,7 +387,6 @@ Section CG_Counter.
        iSplitL; eauto; last first.
        { iDestruct 1 as %Hfoo. injection Hfoo. intro. by exfalso. }
        iIntros "_ Hcnt". simpl.
-       iApply fupd_logrel.
        iMod ("Hclose" with "[Hl Hcnt Hcnt']").
        { iNext. iExists m. iFrame. }
        iApply (bin_log_related_if_false_l [] []); auto.

F_mu_ref_conc/relational_properties.v

@@ -26,6 +26,14 @@ Section properties.
     iApply ("H" with "* Hs [HΓ] * Hj"); auto.
   Qed.
 
+  Global Instance elim_modal_logrel E1 E2 Γ e e' P τ :
+   ElimModal (|={E1,E2}=> P) P
+     ({E1,E2;Γ} ⊨ e ≤log≤ e' : τ) ({E2,E2;Γ} ⊨ e ≤log≤ e' : τ) | 0.
+  Proof. 
+    iIntros "[HP HI]". iApply fupd_logrel.
+    iMod "HP". iApply ("HI" with "HP").
+  Qed.
+  
   Lemma bin_log_related_val Γ τ e e' v v'
     (Hclosed : ∀ f, e.[f] = e)
     (Hclosed' : ∀ f, e'.[f] = e') :
@@ -355,11 +363,10 @@ Section properties.
     -∗ {E1,E1;Γ} ⊨ fill K (Alloc e) ≤log≤ t : τ.
   Proof.
     iIntros "Hlog".
-    iApply fupd_logrel. 
     pose (Φ:=(fun (_ : unit) w => ∃ l, ⌜w = LocV l⌝ ∗ l ↦ᵢ v)%I).
     iApply (bin_log_related_step_atomic_l Φ); auto.
     { rewrite_closed. }
-    iMod "Hlog" as "Hlog". iModIntro. 
+    iMod "Hlog". iModIntro. 
     iExists ().
     iSplitR "Hlog".
     - iApply (wp_alloc _ _ v); auto. iNext. iIntros (l) "Hl".      
@@ -387,7 +394,6 @@ Section properties.
     -∗ {E1,E1;Γ} ⊨ fill K (Load (Loc l)) ≤log≤ t : τ.
   Proof.
     iIntros "Hlog".
-    iApply fupd_logrel. 
     pose (Φ:=(fun v' w => ⌜w = v'⌝ ∗ l ↦ᵢ v')%I).
     iApply (bin_log_related_step_atomic_l Φ); auto.
     iMod "Hlog" as (v') "[% [Hl Hlog]]". iModIntro.
@@ -423,7 +429,6 @@ Section properties.
     -∗ {E1,E1;Γ} ⊨ fill K (Store (Loc l) e) ≤log≤ t : τ.
   Proof.
     iIntros (?) "Hlog".
-    iApply fupd_logrel. 
     pose (Φ:=(fun (_ : unit) w => ⌜w = UnitV⌝ ∗ l ↦ᵢ v')%I).
     iApply (bin_log_related_step_atomic_l Φ); auto.
     { rewrite_closed. }
@@ -462,7 +467,6 @@ Section properties.
     -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ.
   Proof.
     iIntros (??) "Hlog".
-    iApply fupd_logrel. 
     pose (Φ:=(fun v' w => (⌜v' <> v1⌝ -∗ ⌜w = BoolV false⌝ ∗ l ↦ᵢ v') ∗
                         (⌜v' = v1⌝ -∗ ⌜w = BoolV true⌝ ∗ l ↦ᵢ v2))%I).
     iApply (bin_log_related_step_atomic_l Φ); auto.
@@ -505,7 +509,6 @@ Section properties.
     -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ.
   Proof.
     iIntros (??) "Hlog".
-    iApply fupd_logrel. 
     pose (Φ:=(fun v' w => ⌜w = BoolV false⌝ ∗ l ↦ᵢ v')%I).
     iApply (bin_log_related_step_atomic_l Φ); auto.
     { rewrite_closed. }
@@ -546,7 +549,6 @@ Section properties.
     -∗ {E1,E1;Γ} ⊨ fill K (CAS (Loc l) e1 e2) ≤log≤ t : τ.
   Proof.  
     iIntros (??) "Hlog".
-    iApply fupd_logrel. 
     pose (Φ:=(fun (_ : unit) w => ⌜w = BoolV true⌝ ∗ l ↦ᵢ v2)%I).
     iApply (bin_log_related_step_atomic_l Φ); auto.
     { rewrite_closed. }
@@ -807,4 +809,7 @@ Section properties.
     done.
   Qed.
 
+  (* To prevent accidental unfolding by iMod or other tactics *)
+  Typeclasses Opaque bin_log_related.
+
 End properties.