provide _big variant of gen_heap_init

theories/base_logic/lib/gen_heap.v

@@ -126,17 +126,6 @@ Local Notation "l ↦{ q } v" := (mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
 Local Notation "l ↦ v" := (mapsto l 1 v) (at level 20) : bi_scope.
 
-Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
-  ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_interp σ.
-Proof.
-  iMod (own_alloc (gmap_view_auth 1 (σ : gmap L (leibnizO V)))) as (γh) "Hh".
-  { exact: gmap_view_auth_valid. }
-  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L gnameO))) as (γm) "Hm".
-  { exact: gmap_view_auth_valid. }
-  iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
-  iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.
-Qed.
-
 Section gen_heap.
   Context {L V} `{Countable L, !gen_heapG L V Σ}.
   Implicit Types P Q : iProp Σ.
@@ -300,3 +289,26 @@ Section gen_heap.
     rewrite dom_insert_L. set_solver.
   Qed.
 End gen_heap.
+
+(** This lemma drops ownership of the initial [σ] on the floor; see
+[gen_heap_init_big] for a version of the lemma that preserves this ownership. *)
+Lemma gen_heap_init `{Countable L, !gen_heapPreG L V Σ} σ :
+  ⊢ |==> ∃ _ : gen_heapG L V Σ, gen_heap_interp σ.
+Proof.
+  iMod (own_alloc (gmap_view_auth 1 (σ : gmap L (leibnizO V)))) as (γh) "Hh".
+  { exact: gmap_view_auth_valid. }
+  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L gnameO))) as (γm) "Hm".
+  { exact: gmap_view_auth_valid. }
+  iModIntro. iExists (GenHeapG L V Σ _ _ _ _ _ γh γm).
+  iExists ∅; simpl. iFrame "Hh Hm". by rewrite dom_empty_L.
+Qed.
+
+Lemma gen_heap_init_big `{Countable L, !gen_heapPreG L V Σ} σ :
+  ⊢ |==> ∃ _ : gen_heapG L V Σ,
+    gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
+Proof.
+  iMod (gen_heap_init ∅) as (gen_heap) "Hinterp". iExists gen_heap.
+  iMod (gen_heap_alloc_big with "Hinterp") as "(Hinterp & $ & $)".
+  { apply map_disjoint_empty_r. }
+  rewrite right_id. done.
+Qed.