A unified `fupd_logrel` rule and better instances.

Now with one rule primitive we can prove several instances that allows
us to eliminate
- Fancy updates
- Basic updates
- Laters

theories/examples/counter.v

@@ -157,9 +157,8 @@ Section CG_Counter.
     iMod "H" as (n) "[Hx [HR Hrev]]".  iModIntro.
     iExists #n. iFrame. iNext. iIntros "Hx".
     iDestruct "Hrev" as "[Hrev _]".
-    iApply fupd_logrel.
-    iMod ("Hrev" with "[HR Hx]").
-    { iExists _. iFrame. } iModIntro. simpl.
+    iMod ("Hrev" with "[HR Hx]") as "_".
+    { iExists _. iFrame. } simpl.
     rel_rec_l.
     rel_op_l.
     rel_cas_l_atomic.
@@ -286,7 +285,7 @@ Section CG_Counter.
 
     iApply (bin_log_related_pair _ with "[]").
     - rel_rec_l.
-      unfold CG_increment. unlock.
+      unlock CG_increment.
       rel_rec_r.
       rel_rec_r.
       replace (λ: <>, acquire # l ;; #cnt' <- #1 + (! #cnt');; release # l)%E

theories/examples/generative.v

@@ -68,13 +68,11 @@ Section namegen_refinement.
     iIntros (Δ).
     unlock nameGenTy nameGen1 nameGen2.
     rel_alloc_r as c "Hc". rel_let_r.
-    iApply fupd_logrel'.
     iMod alloc_empty_bij as (γ) "HB".
     pose (N:=logrelN.@"ng").
     iMod (inv_alloc N _ (ng_Inv γ c) with "[-]") as "#Hinv".
     { iNext. iExists 0, ∅. iFrame.
       by rewrite big_sepS_empty. }
-    iModIntro.
     iApply (bin_log_related_pack _ (ngR γ)).
     iApply bin_log_related_pair.
     - (* New name *)
@@ -101,7 +99,6 @@ Section namegen_refinement.
       { iIntros (Hx). destruct Hx as [x Hy].
         rewrite (big_sepS_elem_of _ L (x,S n) Hy).
         iDestruct "HL" as "[_ %]". omega. }
-      iApply fupd_logrel.
       iMod (bij_alloc_alt _ _ γ _ l' (S n) with "HB") as "[HB #Hl'n]"; auto.
       iMod ("Hcl" with "[-]").
       { iNext. iExists _,_; iFrame.
@@ -109,7 +106,6 @@ Section namegen_refinement.
         iFrame. iSplit; eauto.
         iApply (big_sepS_mono _ _ L L with "HL"); first reflexivity.
         intros [l x] Hlx. apply uPred.sep_mono_r, uPred.pure_mono. eauto. }
-      iModIntro.
       rel_vals. iModIntro. iAlways.
       iExists _, _; eauto.
     - (* Name comparison *)

theories/examples/stack/helping.v

@@ -305,8 +305,7 @@ Section refinement.
     iModIntro. iExists _; iFrame. iNext. iIntros "Hst1".
     rewrite stackRel_unfold.
     iDestruct "Hrel" as (w1 w2) "[[% %] #Hrel]"; simplify_eq/=.
-    iApply fupd_logrel'.
-    iDestruct "Hrel" as "[>[% %] | Hrel]"; simplify_eq; iModIntro; rel_fold_l.
+    iDestruct "Hrel" as "[>[% %] | Hrel]"; simplify_eq; rel_fold_l.
     - rel_case_l.
       rel_seq_l.
       rel_apply_r (CG_pop_fail_r with "Hst2 Hl").
@@ -317,9 +316,7 @@ Section refinement.
         rewrite stackRel_unfold.
         iExists _,_; iSplit; eauto. }
       rel_vals. iLeft. iModIntro. iExists (_,_). eauto.
-    - iApply fupd_logrel'.
-      iDestruct "Hrel" as (n t1 t2) "(>% & >% & Hrel)". simplify_eq/=.
-      iModIntro.
+    - iDestruct "Hrel" as (n t1 t2) "(>% & >% & Hrel)". simplify_eq/=.
       rel_case_l.
       rel_let_l.
       iMod ("Hcl" with "[-IH]").
@@ -339,11 +336,9 @@ Section refinement.
         iIntros (?). iNext. iIntros "Hst1".
         rel_if_true_l.
         rewrite stackRel_unfold.
-        iApply fupd_logrel'.
         iDestruct "Hrel" as (??) "[[% %] Hrel]"; simplify_eq/=.
         iDestruct "Hrel" as "[>[% %] | Hrel]"; simplify_eq.
         iDestruct "Hrel" as (???) "(>% & >% & Hrel)"; simplify_eq/=.
-        iModIntro.
         rel_apply_r (CG_pop_suc_r with "Hst2 Hl").
         { solve_ndisj. }
         iIntros "Hst' Hl".
@@ -382,7 +377,6 @@ Section refinement.
     unlock push_st. rel_rec_l. rel_let_l.
     unlock CG_locked_pop. rel_rec_r. rel_let_r.
     unlock CG_locked_push. rel_rec_r. rel_let_r.
-    iApply fupd_logrel.
     iMod (own_alloc (● to_offer_reg ∅ : authR offerRegR)) as (γo) "Hor".
     { apply auth_auth_valid. apply to_offer_reg_valid. }
     iMod (inv_alloc stackN _ (stackInv γo st st' mb l') with "[-]") as "#Hinv".
@@ -391,7 +385,6 @@ Section refinement.
       iSplit; eauto. iApply stackRel_empty.
       iSplitL; first eauto.
       iApply offerInv_empty. }
-    iModIntro.
     iApply bin_log_related_pair; last first.
   (* * Push refinement *)
   { iApply bin_log_related_arrow_val; eauto.
@@ -421,9 +414,7 @@ Section refinement.
     rel_rec_l.
     unlock revoke_offer. rel_rec_l.
     iDestruct (offerInv_excl with "HN Ho") as %Hbaz.
-    iApply fupd_logrel'.
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-    iModIntro.
     rewrite {2}bin_log_related_eq /bin_log_related_def.
     iIntros (vvs ρ) "#Hs #HΓ".
     iIntros (j K) "Hj". cbn[snd fst].
@@ -582,7 +573,7 @@ Section refinement.
          apply bin_log_related_spec_ctx.
          iDestruct 1 as (ρ') "#Hspec".
          tp_rec j.
-         iApply fupd_logrel'.
+         iApply fupd_logrel.
          tp_cas_suc j. simpl.
          repeat (tp_pure j _). simpl.
          unlock CG_push.

theories/examples/stack/refinement.v

@@ -61,9 +61,7 @@ Section Stack_refinement.
       rel_apply_r (CG_push_r with "Hst' Hl").
       { solve_ndisj. }
       iIntros "Hst' Hl".
-      iApply fupd_logrel'. (* TODO iMod should pick this up on its own *)
       iMod (stack_owns_alloc with "[$Hoe $Hnstk]") as "[Hoe Hnstk]".
-      iModIntro.
       iMod ("Hclose" with "[Hst Hoe Hst' Hl HLK Hnstk]").
       { iNext. rewrite {2}/sinv. iExists _,_,_.
         iFrame "Hoe Hst' Hst Hl".
@@ -335,7 +333,6 @@ Section Full_refinement.
     simpl.
     rel_rec_l.
 
-    iApply fupd_logrel.
     iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done.
     set (istkG := StackG _ _ γ).
     change γ with (@stack_name _ istkG).
@@ -353,7 +350,6 @@ Section Full_refinement.
     { iExists _, _, _. by iFrame. }
     iMod (inv_alloc stackN with "[Hinv]") as "#Hinv".
     { iNext. iExact "Hinv". }
-    iModIntro.
     unlock FG_stack_body.
     unlock FG_push.
     repeat rel_rec_l.

theories/examples/symbol.v

@@ -279,11 +279,9 @@ Section proof.
     rel_alloc_r as size2 "[Hs2 Hs2']"; rel_let_r.
     rel_alloc_l as tbl1 "[Htbl1 Htbl1']"; rel_let_l.
     rel_alloc_r as tbl2 "[Htbl2 Htbl2']"; rel_let_r.
-    iApply fupd_logrel'.
     iMod (own_alloc (● (0 : mnat))) as (γ) "Ha"; first done.
     iMod (inv_alloc sizeN _ (table_inv γ size1 size2 tbl1 tbl2) with "[Hs1 Hs2 Htbl1 Htbl2 Ha]") as "#Hinv".
     { iNext. iExists _,_. iFrame. iApply LIST_interp_nil. }
-    iModIntro.
     rel_apply_r bin_log_related_newlock_r; first done.
     iIntros (l2) "Hl2". rel_let_r.
     pose (N:=(logrelN.@"lock1")).
@@ -320,11 +318,9 @@ Section proof.
       rel_store_r.
       rel_let_r.
       (* Before we close the lock, we need to gather some evidence *)
-      iApply fupd_logrel'.
       iMod (conjure_0 γ) as "Hf".
       iMod (same_size with "[$Ha $Hf]") as "[Ha #Hf]".
       iMod (inc_size with "Ha") as "Ha".
-      iModIntro.
       iDestruct "Hs2" as "[Hs2 Hs2']".
       rewrite Nat.add_1_r.
       iMod ("Hcl" with "[Ha Hs1 Hs2 Htbl1 Htbl2]") as "_".

theories/examples/ticket_lock.v

@@ -133,11 +133,9 @@ Section refinement.
   Proof.
     iIntros (Δ).
     pose (N:=logrelN.@"locked").
-    iApply fupd_logrel'.
     iMod (own_alloc (● (∅ : lockPoolR))) as (γp) "HP"; first done.
     iMod (inv_alloc N _ (moduleInv γp) with "[HP]") as "#Hinv".
     { iNext. iExists ∅. iFrame. by rewrite /lockPoolInv big_sepS_empty. }
-    iModIntro.
     iApply (bin_log_related_pack _ (lockInt γp)).
     repeat iApply bin_log_related_pair.
     - (* Allocating a new lock *)
@@ -151,14 +149,12 @@ Section refinement.
       iInv N as (P) "[>HP Hpool]" "Hcl".
       iModIntro. iNext.
       iIntros (ln) "Hln".
-      iApply fupd_logrel'.
       iMod (own_alloc (● (GSet ∅) ⋅ ◯ (GSet ∅))) as (γ) "[Hγ Hγ']".
       { by rewrite -auth_both_op. }
       iMod (own_update with "HP") as "[HP Hls]".
       { eapply auth_update_alloc.
         eapply (gset_local_update _ _ ({[(lo, ln, γ, l')]} ∪ P)).
         apply union_subseteq_r. }
-      iModIntro.
       iDestruct (lockPool_excl _ lo ln γ l' with "Hpool Hlo") as %Hnew.
       iMod ("Hcl" with "[-Hls]") as "_".
       { iNext. iExists _; iFrame.
@@ -203,12 +199,10 @@ Section refinement.
           iApply "Hpool". iExists _,_,_; by iFrame. }
         iApply "IH".
       + simplify_eq.
-        iApply fupd_logrel'.
         iMod (own_update with "Hseq") as "[Hseq Hticket]".
         { eapply auth_update_alloc.
           eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
           apply (seq_set_S_disjoint 0). }
-        iModIntro.
         rewrite -(seq_set_S_union_L 0).
         rewrite Nat.add_1_r.
         iMod ("Hcl" with "[-Hticket]") as "_".

theories/examples/various.v

@@ -74,20 +74,16 @@ Section refinement.
     rel_alloc_l as x "Hx".
     rel_alloc_r as y "Hy".
     rel_let_l; rel_let_r.
-    iApply fupd_logrel.
-    iMod new_pending as (γ) "Ht". (*TODO typeclasses for this?*)
-    iModIntro.
+    iMod new_pending as (γ) "Ht".
     iMod (inv_alloc shootN _ ((x ↦ᵢ #0 ∗ pending γ ∨ x ↦ᵢ #1 ∗ shot γ) ∗ y ↦ₛ #1)%I with "[Hx Ht $Hy]") as "#Hinv".
     { iNext. iLeft. iFrame. }
     iApply bin_log_related_arrow; auto.
-    iIntros "!#" (f1 f2) "Hf".
+    iIntros "!#" (f1 f2) "#Hf".
     rel_let_l. rel_let_r.
     rel_store_l_atomic.
     iInv shootN as "[[[Hx Hp] | [Hx #Hs]] Hy]" "Hcl";
       iModIntro; iExists _; iFrame "Hx"; iNext; iIntros "Hx"; rel_rec_l.
-    - iApply fupd_logrel'.
-      iMod (shoot γ with "Hp") as "#Hs".
-      iModIntro.
+    - iMod (shoot γ with "Hp") as "#Hs".
       iMod ("Hcl" with "[$Hy Hx]") as "_".
       { iNext. iRight. by iFrame. }
       iApply (bin_log_related_seq with "[Hf]"); auto.
@@ -448,11 +444,9 @@ Section refinement.
     iDestruct "Hc2" as "[(Hc2 & Hp) | (Hc2 & Hs & Ht'2 & %)]"; last first.
     { iDestruct (own_valid_2 with "Ht Ht'2") as %Hfoo.
       inversion Hfoo. }
-    iApply fupd_logrel.
     iMod (shoot γ with "Hp") as "#Hs".
     iMod ("Hcl" with "[-]") as "_".
     { iNext. iExists m. iRight. iFrame. done. }
-    iModIntro.
     iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
     { iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hg]").
       iApply (related_ret ⊤). iApply interp_ret; eauto using to_of_val.
@@ -503,10 +497,8 @@ Section refinement.
     rel_let_l. rel_let_r.
     rel_alloc_l as c1 "Hc1".
     rel_alloc_r as c2 "Hc2".
-    iApply fupd_logrel.
-    iMod new_pending as (γ) "Ht". (*TODO typeclasses for this?*)
+    iMod new_pending as (γ) "Ht".
     iMod (own_alloc (Excl ())) as (γ') "Ht'"; first done.
-    iModIntro.
     iMod (inv_alloc shootN _ (i6 c1 c2 γ γ') with "[Hc1 Hc2 Ht]") as "#Hinv".
     { iNext. iExists 0. iLeft. iFrame. }
     rel_let_l. rel_let_r.

theories/logrel/fundamental_binary.v

@@ -318,16 +318,13 @@ Section masked.
     rel_op_l.
     rel_op_r.
     destruct (decide (l1 = l1')) as [->|?].
-    - iApply fupd_logrel.
-      iMod (interp_ref_funct _ _ _ l1' l2 l2' with "[Hl Hl']") as %->.
+    - iMod (interp_ref_funct _ _ _ l1' l2 l2' with "[Hl Hl']") as %->.
       { solve_ndisj. }
       { iSplit; iExists (_,_); eauto. }
       rewrite decide_left.
-      iModIntro.
       value_case.
     - destruct (decide (l2 = l2')) as [->|?].
-      + iApply fupd_logrel.
-        iMod (interp_ref_inj _ _ _ l2' l1 l1' with "[Hl Hl']") as %->.
+      + iMod (interp_ref_inj _ _ _ l2' l1 l1' with "[Hl Hl']") as %->.
         { solve_ndisj. }
         { iSplit; iExists (_,_); eauto. }
         congruence.
@@ -580,20 +577,16 @@ Section masked.
     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 ">%".
+      iAssert (⌜v2 = v2'⌝)%I with "[IH2]" as %->.
       { rewrite ?interp_EqType_agree; trivial. }
-      iModIntro.
       rel_cas_suc_r.
       iMod ("Hclose" with "[-]").
       { iNext; iExists (_, _); by iFrame. }
       rel_vals; eauto.
     - iSplitL; last by (iIntros (?); congruence).
       iIntros (?). iNext. iIntros "Hv1".
-      iApply fupd_logrel'.
-      iAssert (▷ ⌜v' ≠ v2'⌝)%I as ">%".
+      iAssert (⌜v' ≠ v2'⌝)%I as "%".
       { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
-      iModIntro.
       rel_cas_fail_r.
       iMod ("Hclose" with "[-]").
       { iNext; iExists (_, _); by iFrame. }

theories/logrel/logrel_binary.v

@@ -167,47 +167,45 @@ Section related_facts.
   Implicit Types Δ : listC D.
 
   (* We need this to be able to open and closed invariants in front of logrels *)
-  Lemma fupd_logrel E1 E2 Δ Γ e e' τ :
-    ((|={E1,E2}=> ({E2;Δ;Γ} ⊨ e ≤log≤ e' : τ))
-     -∗ {E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I.
+  Lemma fupd_logrel E1 E2 E3 Δ Γ e e' τ :
+    ((|={E1,E2}=> ({E2,E3;Δ;Γ} ⊨ e ≤log≤ e' : τ))
+     -∗ {E1,E3;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I.
   Proof.
-    rewrite bin_log_related_eq.
-    iIntros "H".
-    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    iMod "H".
-    iSpecialize ("H" with "Hs [HΓ] Hj"); eauto.
-  Qed.
-
-  Lemma fupd_logrel' E1 E2 Δ Γ e e' τ :
-    ((|={E1}=> ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ))
-     -∗ {E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ)%I.
-  Proof.
-    rewrite bin_log_related_eq.
+    rewrite bin_log_related_eq /bin_log_related_def.
     iIntros "H".
     iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
-    iMod "H".
+    iMod "H" as "H".
     iSpecialize ("H" with "Hs [HΓ] Hj"); eauto.
   Qed.
 
-  Global Instance elim_modal_logrel E1 E2 Δ Γ e e' P τ :
+  Global Instance elim_fupd_logrel E1 E2 E3 Δ Γ e e' P τ :
    ElimModal (|={E1,E2}=> P) P
-     ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) | 10.
+     ({E1,E3;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E2,E3;Δ;Γ} ⊨ e ≤log≤ e' : τ).
   Proof.
     rewrite /ElimModal.
     iIntros "[HP HI]". iApply fupd_logrel.
     iMod "HP". iApply ("HI" with "HP").
   Qed.
 
-  Global Instance elim_modal_logrel' E1 E2 Δ Γ e e' P τ :
-   ElimModal (|={E1}=> P) P
-     ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) | 0.
+  Global Instance elim_bupd_logrel E1 E2 Δ Γ e e' P τ :
+   ElimModal (|==> P) P
+     ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ) ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ).
   Proof.
-    rewrite /ElimModal.
-    iIntros "[HP HI]". iApply fupd_logrel'.
-    iMod "HP". iApply ("HI" with "HP").
+    rewrite /ElimModal (bupd_fupd E1).
+    apply: elim_fupd_logrel.
+  Qed.
+
+  (* This + elim_modal_timless_bupd' is useful for stripping off laters of timeless propositions. *)
+  Global Instance is_except_0_logrel E1 E2 Δ Γ e e' τ :
+    IsExcept0 ({E1,E2;Δ;Γ} ⊨ e ≤log≤ e' : τ).
+  Proof.
+    rewrite /IsExcept0.
+    iIntros "HL".
+    iApply fupd_logrel.
+    by iMod "HL".
   Qed.
 
-  Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 τ :
+  Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 (τ : type) :
     {Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗
     {τi::Δ;⤉Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)].
   Proof.