Minor cleanup on monPred_subjectively

theories/base_logic/na.v

@@ -213,6 +213,20 @@ Section na_props.
   Lemma own_loc_na_own_any l v q : l ↦{q} v ⊢ l ↦{q} -.
   Proof. iIntros "own". by iExists _. Qed.
 
+  Lemma own_loc_na_own_loc_prim_subjectively n q v :
+    n ↦{q} v ⊢ ∃ q' C', ▷ <subj> n p↦{q'} C'.
+  Proof.
+    rewrite own_loc_na_own_loc_prim. iDestruct 1 as (C) "En".
+    iExists q, C. iNext. by iApply monPred_subjectively_intro.
+  Qed.
+  Lemma own_loc_na_view_at_own_loc_prim_subjectively n q v V :
+    @{V} n ↦{q} v ⊢ ∃ q' C', ▷ <subj> n p↦{q'} C'.
+  Proof.
+    rewrite own_loc_na_own_loc_prim_subjectively.
+    iDestruct 1 as (q' C) "En". iExists q', C. iNext.
+    by rewrite view_at_subjectively monPred_subjectively_idemp.
+  Qed.
+
   Global Instance own_loc_fractional l : Fractional (own_loc l).
   Proof.
     unfold Fractional=>p q. iSplit.

theories/examples/queue/proof_ms_gps.v

@@ -461,12 +461,11 @@ Proof.
                   [rewrite shift_0; solve_ndisj|by rewrite shift_0|].
           iClear "#".
           iCombine "own1" "own2" as "own". rewrite -view_subjectively_sep.
-          iAssert (<subj> False)%I with "[own]" as "own".
-          { iApply (monPred_subjectively_mono with "own").
-            iIntros "[o1 o2]".
-            iPoseProof (own_loc_prim_combine with "o1 o2") as "o".
-            by iDestruct (own_loc_prim_frac_1 with "o") as %?. }
-          by iDestruct (objective_subjectively with "own") as "F". }
+          iAssert (<subj> False)%I with "[own]" as "%"; [|done].
+          iApply (monPred_subjectively_mono with "own").
+          iIntros "[o1 o2]".
+          iPoseProof (own_loc_prim_combine with "o1 o2") as "o".
+          by iDestruct (own_loc_prim_frac_1 with "o") as %?. }
         subst γt'.
 
         iMod (escrow_elim with "[] ES [$Tok']") as "Q" ; [solve_ndisj|..].

theories/examples/stack/proof_treiber_gps.v

@@ -364,15 +364,14 @@ Proof.
               with "[$PPs' $Hs1 Hn Hd P H†]");
       [solve_ndisj|done|done|solve_ndisj|solve_ndisj|by left|by left|by right|..].
   { iSplitL ""; last iSplitL ""; last iSplitL "".
-    - iIntros "!> Hs1 !>". rewrite acq_subjective own_loc_na_own_loc_prim.
-      iDestruct "Hs1" as (C) "Hs1". iExists _, _. iNext. iFrame "Hs1".
+    - iIntros "!> Hs1 !>". rewrite acq_subjective view_at_subjectively_inv.
+      iDestruct ("Hs1") as (?) "Hs1".
+      iApply (own_loc_na_view_at_own_loc_prim_subjectively with "Hs1").
     - iIntros "!> !>" (t0 [] v0 _). by iApply Head_is_comparable_loc.
     - iIntros (t0 [] _). iSplitL ""; first iSplitL ""; [|iSplitL ""|..].
       + iIntros "!>" (l' NEq) "Head". iIntros "!>".
-        iDestruct (Head_has_fraction_loc_later with "Head") as (q' v') "Hs".
-        iIntros "!>". rewrite own_loc_na_own_loc_prim.
-        iDestruct "Hs" as (C) "Hs". iExists _, _. iNext.
-        by iApply monPred_subjectively_intro.
+        iDestruct (Head_has_fraction_loc_later with "Head") as (q' v') ">Hs".
+        iIntros "!>". iApply (own_loc_na_own_loc_prim_subjectively with "Hs").
       + rewrite -bi.later_sep. iIntros "!> Head !> !>".
         by iDestruct (Head_main_dup with "Head") as "[$ $]".
       + iIntros "(HP & Hn & Hd & H†) HH".

theories/gps/middleware_PP.v

@@ -561,28 +561,22 @@ Section PP.
               Pr P Q Q1 Q2 R _ _ _ E E (λ _, E)
               with "[$R $Inv $Pr HPr $Comp VS $P] Post"); [done..|].
     iSplitL "HPr".
-    - iIntros "!> Pr". iMod ("HPr" with "Pr") as (qr vr) "Pr".
-      iIntros "!>". iExists qr.
-      iPoseProof (own_loc_na_own_loc_prim with "Pr") as (Cr) "Pr".
-      iExists Cr. by iApply monPred_subjectively_intro.
+    - iIntros "!> Pr". iMod ("HPr" with "Pr") as (qr vr) ">Pr".
+      iIntros "!>". iApply (own_loc_na_own_loc_prim_subjectively with "Pr").
     - case decide => ?.
       + iIntros (t' s') "Le'". iSpecialize ("VS" $! t' s' with "Le'").
         iSplit; [rewrite bi.and_elim_l|by rewrite bi.and_elim_r].
         iDestruct "VS" as "[VS $]".
         iIntros "!>" (l') "NEq F !>". rewrite monPred_objectively_elim.
-        iMod ("VS" with "NEq F") as (q' v') "Hq'".
-        iIntros "!>". iExists q'.
-        iPoseProof (own_loc_na_own_loc_prim with "Hq'") as (C') "Hq'".
-        iExists C'. iNext. by iApply monPred_subjectively_intro.
+        iMod ("VS" with "NEq F") as (q' v') ">Hq'".
+        iIntros "!>". iApply (own_loc_na_own_loc_prim_subjectively with "Hq'").
       + iApply (rel_mono with "VS").
         iIntros "VS" (t' s') "Le'". iSpecialize ("VS" $! t' s' with "Le'").
         iSplit; [rewrite bi.and_elim_l|by rewrite bi.and_elim_r].
         iDestruct "VS" as "[VS $]".
         iIntros "!>" (l') "NEq F !>". rewrite monPred_objectively_elim.
-        iMod ("VS" with "NEq F") as (q' v') "Hq'".
-        iIntros "!>". iExists q'.
-        iPoseProof (own_loc_na_own_loc_prim with "Hq'") as (C') "Hq'".
-        iExists C'. iNext. by iApply monPred_subjectively_intro.
+        iMod ("VS" with "NEq F") as (q' v') ">Hq'".
+        iIntros "!>". iApply (own_loc_na_own_loc_prim_subjectively with "Hq'").
   Qed.
 End PP.
 

theories/gps/middleware_SW.v

@@ -174,10 +174,8 @@ Section SingleWriter.
     GPS_SWSharedReader t s v q γ.
   Proof.
     rewrite GPS_SWReader_eq GPS_SWSharedReader_eq.
-    iIntros "Prt". rewrite monPred_subjectively_exist.
-    iDestruct 1 as (tx) "R". rewrite 2!monPred_subjectively_sep.
-    iDestruct "R" as "(_ & ex & Le)". rewrite monPred_subjectively_unfold /=.
-    iDestruct "ex" as (?) "ex". iDestruct "Le" as (?) "%".
+    iIntros "Prt". iDestruct 1 as (tx) "(_ & ex & %)".
+    rewrite monPred_subjectively_unfold /=. iDestruct "ex" as (?) "ex".
     rewrite monPred_at_embed. iExists tx. by iFrame "Prt ex".
   Qed.
 
@@ -187,9 +185,8 @@ Section SingleWriter.
     GPS_SWSharedReader t1 s1 v1 (q1 + q2) γ.
   Proof.
     rewrite GPS_SWSharedReader_eq.
-    iDestruct 1 as (tx) "(Prt & ex1 & Le)". rewrite monPred_subjectively_exist.
-    iDestruct 1 as (tx') "ex". rewrite 2!monPred_subjectively_sep.
-    iDestruct "ex" as "(_&ex2&_)". rewrite monPred_subjectively_unfold /=.
+    iDestruct 1 as (tx) "(Prt & ex1 & Le)".
+    iDestruct 1 as (tx') "(_&ex2&_)". rewrite monPred_subjectively_unfold /=.
     iDestruct "ex2" as (?) "ex2". rewrite monPred_at_embed.
     iExists tx. iFrame "Prt Le".
     iDestruct (ExWrite_frac_agree with "ex1 ex2") as %?. subst tx'.
@@ -350,9 +347,7 @@ Section SingleWriter.
     rewrite GPS_SWSharedWriter_eq GPS_SWSharedReader_eq.
     iStartProof iProp. iIntros (?).
     iDestruct 1 as (ζ) "(#Seen1 & W & %MAX)".
-    iIntros (? ->). rewrite monPred_subjectively_exist.
-    iDestruct 1 as (tx') "R". rewrite 2!monPred_subjectively_sep.
-    iDestruct "R" as "(_ & ex2 & _)". iDestruct "ex2" as (?) "ex2".
+    iIntros (? ->). iDestruct 1 as (? tx') "(_ & ex2 & _)".
     iIntros (V ->) "Inv".
     set Vo := V ⊔ Vb.
     iAssert ((▷ GPS_INV IW γ) Vo)%I with "[Inv]" as "Inv".

theories/gps/surface_iPP.v

@@ -40,10 +40,9 @@ Proof.
   iAssert (<subj> ▷ GPS_PPInv IP l γ)%I with "[gpsI]" as "gpsI".
   { rewrite monPred_subjectively_unfold. by iApply monPred_in_view_elim. }
   iIntros "!>".
-  iPoseProof (monPred_subjectively_mono _ _ (GPS_PPInv_own_loc_prim _ _ true _)
-                with "gpsI") as "own".
-  rewrite monPred_subjectively_exist. setoid_rewrite monPred_subjectively_later.
-  by iFrame.
+  iDestruct (monPred_subjectively_mono _ _ (GPS_PPInv_own_loc_prim _ _ true _)
+              with "gpsI") as (?) "own".
+  rewrite -monPred_subjectively_later. by iExists _.
 Qed.
 
 Lemma GPS_iPP_agree IP l t1 t2 s1 s2 v1 v2 γ E (SUB: ↑N ⊆ E) :