Improve allocation lemmas for gmap.

algebra/gmap.v

@@ -318,7 +318,7 @@ Section freshness.
     ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
   Proof. eauto using alloc_updateP. Qed.
 
-  Lemma singleton_updateP_unit (P : A → Prop) (Q : gmap K A → Prop) u i :
+  Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i :
     ✓ u → LeftId (≡) u (⋅) →
     u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
   Proof.
@@ -333,14 +333,15 @@ Section freshness.
       move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
     - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
   Qed.
-  Lemma singleton_updateP_unit' (P: A → Prop) u i :
+  Lemma alloc_unit_singleton_updateP' (P: A → Prop) u i :
     ✓ u → LeftId (≡) u (⋅) →
     u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
-  Proof. eauto using singleton_updateP_unit. Qed.
-  Lemma singleton_update_unit u i (y : A) :
+  Proof. eauto using alloc_unit_singleton_updateP. Qed.
+  Lemma alloc_unit_singleton_update u i (y : A) :
     ✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}.
   Proof.
-    rewrite !cmra_update_updateP; eauto using singleton_updateP_unit with subst.
+    rewrite !cmra_update_updateP;
+      eauto using alloc_unit_singleton_updateP with subst.
   Qed.
 End freshness.
 
@@ -361,19 +362,21 @@ Lemma singleton_local_update i x y mf :
   x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf.
 Proof. apply insert_local_update. Qed.
 
-Lemma alloc_singleton_local_update i x mf :
+Lemma alloc_singleton_local_update m i x mf :
+  (m ⋅? mf) !! i = None → ✓ x → m ~l~> <[i:=x]> m @ mf.
+Proof.
+  rewrite lookup_opM op_None=> -[Hi Hif] ?.
+  rewrite insert_singleton_op // comm. apply alloc_local_update.
+  intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
+  - intros _; rewrite !lookup_opM lookup_op !lookup_singleton Hif Hi.
+    by apply cmra_valid_validN.
+  - by rewrite !lookup_opM lookup_op !lookup_singleton_ne // right_id.
+Qed.
+
+Lemma alloc_unit_singleton_local_update i x mf :
   mf ≫= (!! i) = None → ✓ x → ∅ ~l~> {[ i := x ]} @ mf.
 Proof.
-  intros Hi. split.
-  - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
-    + intros _; rewrite !lookup_opM !lookup_insert !Some_op_opM Hi /=.
-      by apply cmra_valid_validN.
-    + by rewrite !lookup_opM !lookup_insert_ne.
-  - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
-    destruct (decide (i = j)); subst.
-    + intros _. rewrite !lookup_opM !lookup_insert !Hi !lookup_empty !left_id_L.
-      by intros <-.
-    + by rewrite !lookup_opM !lookup_insert_ne.
+  intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
 Qed.
 
 Lemma delete_local_update m i x `{!Exclusive x} mf :

algebra/updates.v

@@ -68,11 +68,11 @@ Proof.
   - intros n mz'. rewrite !cmra_opM_assoc. move=> Hv /(H1 _ (Some _) Hv) /=; auto.
 Qed.
 
-Lemma alloc_local_update x y mz : ✓ (x ⋅ y ⋅? mz) → x ~l~> x ⋅ y @ mz.
+Lemma alloc_local_update x y mz :
+  (∀ n, ✓{n} (x ⋅? mz) → ✓{n} (x ⋅ y ⋅? mz)) → x ~l~> x ⋅ y @ mz.
 Proof.
-  split.
-  - intros n _. by apply cmra_valid_validN.
-  - intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->.
+  split; first done.
+  intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc=> ->.
 Qed.
 
 (** ** Frame preserving updates *)

heap_lang/heap.v

@@ -154,7 +154,7 @@ Section heap.
     iIntros {l} "[% Hheap]". iExists {[ l := (1%Qp, DecAgree v) ]}.
     rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None.
     iFrame "Hheap". iSplit; first iPureIntro.
-    { by apply alloc_singleton_local_update; first apply of_heap_None. }
+    { by apply alloc_unit_singleton_local_update; first apply of_heap_None. }
     iIntros "Hheap". iApply "HΦ". by rewrite /heap_mapsto.
   Qed.
 

program_logic/ghost_ownership.v

@@ -86,7 +86,7 @@ Implicit Types a : A.
 Lemma own_empty γ E : True ={E}=> own γ ∅.
 Proof.
   rewrite ownG_empty /own. apply pvs_ownG_update, iprod_singleton_update_empty.
-  apply (singleton_update_unit (cmra_transport inG_prf ∅)); last done.
+  apply (alloc_unit_singleton_update (cmra_transport inG_prf ∅)); last done.
   - apply cmra_transport_valid, ucmra_unit_valid.
   - intros x; destruct inG_prf. by rewrite left_id.
 Qed.