From dc6db28b2e3cc9cd5e519ef54d1e67c38e7e12a3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 17 Jun 2016 01:45:35 +0200
Subject: [PATCH] Improve allocation lemmas for gmap.

---
 algebra/gmap.v                  | 35 ++++++++++++++++++---------------
 algebra/updates.v               |  8 ++++----
 heap_lang/heap.v                |  2 +-
 program_logic/ghost_ownership.v |  2 +-
 4 files changed, 25 insertions(+), 22 deletions(-)

diff --git a/algebra/gmap.v b/algebra/gmap.v
index c9858eba7..948d7f97e 100644
--- a/algebra/gmap.v
+++ b/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 :
diff --git a/algebra/updates.v b/algebra/updates.v
index ab978f4e0..46dcfe7ab 100644
--- a/algebra/updates.v
+++ b/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 *)
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 2d57cc202..9ee470dfd 100644
--- a/heap_lang/heap.v
+++ b/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.
 
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 5a64e3af7..4b99d5435 100644
--- a/program_logic/ghost_ownership.v
+++ b/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.
-- 
GitLab