Validity and update lemmas for owning multiple ghosts.

heap_lang/lib/spin_lock.v

@@ -32,7 +32,7 @@ Section proof.
   Definition locked (γ : gname): iProp Σ := own γ (Excl ()).
 
   Lemma locked_exclusive (γ : gname) : locked γ ★ locked γ ⊢ False.
-  Proof. rewrite /locked -own_op own_valid. by iIntros (?). Qed.
+  Proof. rewrite /locked own_valid_2. by iIntros (?). Qed.
 
   Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
   Proof. solve_proper. Qed.

program_logic/boxes.v

@@ -57,7 +57,7 @@ Proof. apply _. Qed.
 Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2.
 Proof.
-  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
+  rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_l.
   by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
 Qed.
 
@@ -74,7 +74,7 @@ Qed.
 Lemma box_own_agree γ Q1 Q2 :
   (box_own_prop γ Q1 ★ box_own_prop γ Q2) ⊢ ▷ (Q1 ≡ Q2).
 Proof.
-  rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
+  rewrite /box_own_prop own_valid_2 prod_validI /= and_elim_r.
   rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
   iIntros "#HQ !>". rewrite -{2}(iProp_fold_unfold Q1).
   iRewrite "HQ". by rewrite iProp_fold_unfold.

program_logic/cancelable_invariants.v

@@ -39,7 +39,7 @@ Section proofs.
   Proof. by rewrite cinv_own_op Qp_div_2. Qed.
 
   Lemma cinv_own_valid γ q1 q2 : cinv_own γ q1 ★ cinv_own γ q2 ⊢ ✓ (q1 + q2)%Qp.
-  Proof. rewrite /cinv_own -own_op own_valid. by iIntros "% !%". Qed.
+  Proof. rewrite /cinv_own own_valid_2. by iIntros "% !%". Qed.
 
   Lemma cinv_own_1_l γ q : cinv_own γ 1 ★ cinv_own γ q ⊢ False.
   Proof. rewrite cinv_own_valid. by iIntros (?%(exclusive_l 1%Qp)). Qed.

program_logic/ghost_ownership.v

@@ -52,6 +52,7 @@ Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ★ own γ a2.
 Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
 Global Instance own_mono γ : Proper (flip (≼) ==> (⊢)) (@own Σ A _ γ).
 Proof. move=>a b [c ->]. rewrite own_op. eauto with I. Qed.
+
 Lemma own_valid γ a : own γ a ⊢ ✓ a.
 Proof.
   rewrite !own_eq /own_def ownM_valid /iRes_singleton.
@@ -60,10 +61,16 @@ Proof.
   (* implicit arguments differ a bit *)
   by trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
 Qed.
+Lemma own_valid_2 γ a1 a2 : own γ a1 ★ own γ a2 ⊢ ✓ (a1 ⋅ a2).
+Proof. by rewrite -own_op own_valid. Qed.
+Lemma own_valid_3 γ a1 a2 a3 : own γ a1 ★ own γ a2 ★ own γ a3 ⊢ ✓ (a1 ⋅ a2 ⋅ a3).
+Proof. by rewrite -!own_op assoc own_valid. Qed.
+
 Lemma own_valid_r γ a : own γ a ⊢ own γ a ★ ✓ a.
 Proof. apply: uPred.always_entails_r. apply own_valid. Qed.
 Lemma own_valid_l γ a : own γ a ⊢ ✓ a ★ own γ a.
 Proof. by rewrite comm -own_valid_r. Qed.
+
 Global Instance own_timeless γ a : Timeless a → TimelessP (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
 Global Instance own_core_persistent γ a : Persistent a → PersistentP (own γ a).
@@ -107,13 +114,23 @@ Proof.
   intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP.
   by apply rvs_mono, exist_elim=> a''; apply pure_elim_l=> ->.
 Qed.
+Lemma own_update_2 γ a1 a2 a' :
+  a1 ⋅ a2 ~~> a' → own γ a1 ★ own γ a2 =r=> own γ a'.
+Proof. intros. rewrite -own_op. by apply own_update. Qed.
+Lemma own_update_3 γ a1 a2 a3 a' :
+  a1 ⋅ a2 ⋅ a3 ~~> a' → own γ a1 ★ own γ a2 ★ own γ a3 =r=> own γ a'.
+Proof. intros. rewrite -!own_op assoc. by apply own_update. Qed.
 End global.
 
 Arguments own_valid {_ _} [_] _ _.
+Arguments own_valid_2 {_ _} [_] _ _ _.
+Arguments own_valid_3 {_ _} [_] _ _ _ _.
 Arguments own_valid_l {_ _} [_] _ _.
 Arguments own_valid_r {_ _} [_] _ _.
 Arguments own_updateP {_ _} [_] _ _ _ _.
 Arguments own_update {_ _} [_] _ _ _ _.
+Arguments own_update_2 {_ _} [_] _ _ _ _ _.
+Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 
 Lemma own_empty `{inG Σ (A:ucmraT)} γ : True =r=> own γ ∅.
 Proof.

program_logic/ownership.v

@@ -56,13 +56,13 @@ Qed.
 
 (* Physical state *)
 Lemma ownP_twice σ1 σ2 : ownP σ1 ★ ownP σ2 ⊢ False.
-Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
+Proof. rewrite /ownP own_valid_2. by iIntros (?). Qed.
 Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ _ σ).
 Proof. rewrite /ownP; apply _. Qed.
 
 Lemma ownP_agree σ1 σ2 : ownP_auth σ1 ★ ownP σ2 ⊢ σ1 = σ2.
 Proof.
-  rewrite /ownP /ownP_auth -own_op own_valid -auth_both_op.
+  rewrite /ownP /ownP_auth own_valid_2 -auth_both_op.
   by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
 Qed.
 Lemma ownP_update σ1 σ2 : ownP_auth σ1 ★ ownP σ1 =r=> ownP_auth σ2 ★ ownP σ2.
@@ -85,7 +85,7 @@ Proof. by rewrite (own_empty (A:=coPset_disjUR) enabled_name). Qed.
 Lemma ownE_op E1 E2 : E1 ⊥ E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ★ ownE E2.
 Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
 Lemma ownE_disjoint E1 E2 : ownE E1 ★ ownE E2 ⊢ E1 ⊥ E2.
-Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed.
+Proof. rewrite /ownE own_valid_2. by iIntros (?%coPset_disj_valid_op). Qed.
 Lemma ownE_op' E1 E2 : E1 ⊥ E2 ∧ ownE (E1 ∪ E2) ⊣⊢ ownE E1 ★ ownE E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
@@ -100,7 +100,7 @@ Proof. by rewrite (own_empty (A:=gset_disjUR _) disabled_name). Qed.
 Lemma ownD_op E1 E2 : E1 ⊥ E2 → ownD (E1 ∪ E2) ⊣⊢ ownD E1 ★ ownD E2.
 Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
 Lemma ownD_disjoint E1 E2 : ownD E1 ★ ownD E2 ⊢ E1 ⊥ E2.
-Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
+Proof. rewrite /ownD own_valid_2. by iIntros (?%gset_disj_valid_op). Qed.
 Lemma ownD_op' E1 E2 : E1 ⊥ E2 ∧ ownD (E1 ∪ E2) ⊣⊢ ownD E1 ★ ownD E2.
 Proof.
   iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
@@ -115,7 +115,7 @@ Lemma invariant_lookup `{irisG Λ Σ} (I : gmap positive (iProp Σ)) i P :
   own invariant_name (◯ {[i := invariant_unfold P]}) ⊢
   ∃ Q, I !! i = Some Q ★ ▷ (Q ≡ P).
 Proof.
-  rewrite -own_op own_valid auth_validI /=. iIntros "[#HI #HvI]".
+  rewrite own_valid_2 auth_validI /=. iIntros "[#HI #HvI]".
   iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
   iSpecialize ("HI" $! i). iSpecialize ("HvI" $! i).
   rewrite left_id_L lookup_fmap lookup_op lookup_singleton uPred.option_equivI.

program_logic/saved_prop.v

@@ -35,7 +35,7 @@ Section saved_prop.
   Lemma saved_prop_agree γ x y :
     saved_prop_own γ x ★ saved_prop_own γ y ⊢ ▷ (x ≡ y).
   Proof.
-    rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
+    rewrite own_valid_2 agree_validI agree_equivI later_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.