phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/lib/gen_inv_heap.v *)
(* Derive a more standard accessor. *)
Lemma inv_pointsto_own_acc E l v I:
    ↑inv_heapN ⊆ E →
    inv_heap_inv L V -∗ l ↦_I v ={E, E ∖ ↑inv_heapN}=∗
      (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦_I w)).
Proof.
    iIntros (?) "#Hinv Hl".
    iMod (inv_pointsto_own_acc_strong with "Hinv") as "Hacc"; first done.
    iDestruct ("Hacc" with "Hl") as "(HI & Hl & Hclose)".
    iIntros "!> {$HI $Hl}" (w) "HI Hl".
    iMod ("Hclose" with "HI Hl") as "[$ $]".
  Qed.
(* iris/base_logic/lib/gen_inv_heap.v *)
Lemma inv_pointsto_acc l I E :
    ↑inv_heapN ⊆ E →
    inv_heap_inv L V -∗ l ↦_I □ ={E, E ∖ ↑inv_heapN}=∗
    ∃ v, ⌜I v⌝ ∗ l ↦ v ∗ (l ↦ v ={E ∖ ↑inv_heapN, E}=∗ ⌜True⌝).
Proof.
    iIntros (HN) "#Hinv Hl_inv".
    iMod (inv_acc_timeless _ inv_heapN _ with "Hinv") as "[HP Hclose]"; first done.
    iModIntro.
    iDestruct "HP" as (h) "[H● HsepM]".
    iDestruct (inv_pointsto_lookup_Some with "Hl_inv H●") as %(v&I'&?&HI').
    iDestruct (big_sepM_lookup_acc with "HsepM") as "[[#HI Hl] HsepM]"; first done.
    setoid_rewrite HI'.
    iExists _. iIntros "{$HI $Hl} Hl".
    iMod ("Hclose" with "[H● HsepM Hl]"); last done.
    iExists _. iFrame "H●". iApply ("HsepM" with "[$Hl //]").
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
(* The CMRA we need.
FIXME: This is intentionally discrete-only, but
should we support setoids via [Equiv]? *)
Class ghost_mapG Σ (K V : Type) `{Countable K}
:= GhostMapG {
  #[local] ghost_map_inG :: inG Σ (gmap_viewR K (agreeR (leibnizO V)));
}.
(* iris/base_logic/lib/ghost_map.v *)
Definition ghost_mapΣ (K V : Type) `{Countable K} : gFunctors
:=
  #[ GFunctor (gmap_viewR K (agreeR (leibnizO V))) ].
(* iris/base_logic/lib/ghost_map.v *)
Instance subG_ghost_mapΣ Σ (K V : Type) `{Countable K} :
  subG (ghost_mapΣ K V) Σ → ghost_mapG Σ K V.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Definition ghost_map_auth_def
      (γ : gname) (dq : dfrac) (m : gmap K V) : iProp Σ
:=
    own γ (gmap_view_auth (V:=agreeR $ leibnizO V) dq (to_agree <$> m)).
(* iris/base_logic/lib/ghost_map.v *)
Definition ghost_map_auth_aux : seal (@ghost_map_auth_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Definition ghost_map_auth
:= ghost_map_auth_aux.(unseal).
(* iris/base_logic/lib/ghost_map.v *)
Definition ghost_map_auth_unseal :
    @ghost_map_auth = @ghost_map_auth_def
:= ghost_map_auth_aux.(seal_eq).
(* iris/base_logic/lib/ghost_map.v *)
Definition ghost_map_elem_def
      (γ : gname) (k : K) (dq : dfrac) (v : V) : iProp Σ
:=
    own γ (gmap_view_frag (V:=agreeR $ leibnizO V) k dq (to_agree v)).
(* iris/base_logic/lib/ghost_map.v *)
Definition ghost_map_elem_aux : seal (@ghost_map_elem_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Definition ghost_map_elem
:= ghost_map_elem_aux.(unseal).
(* iris/base_logic/lib/ghost_map.v *)
Definition ghost_map_elem_unseal :
    @ghost_map_elem = @ghost_map_elem_def
:= ghost_map_elem_aux.(seal_eq).
(* iris/base_logic/lib/ghost_map.v *)
Notation "γ ↪●MAP dq m"
:= (ghost_map_auth γ dq m)
  (at level 20, dq custom dfrac at level 1,
   format "γ  ↪●MAP dq  m") : bi_scope.
(* iris/base_logic/lib/ghost_map.v *)
Notation "γ ↪◯MAP[ k ] dq v"
:= (ghost_map_elem γ k dq v)
  (at level 20, dq custom dfrac at level 1,
   format "γ  ↪◯MAP[ k ] dq  v") : bi_scope.
(* iris/base_logic/lib/ghost_map.v *)
(* Compatibility aliases. Do not use for new code.
These will eventually be deprecated and removed. *)
Notation ghost_map_auth_frac γ q m
:= (ghost_map_auth γ (DfracOwn q) m) (only parsing).
(* iris/base_logic/lib/ghost_map.v *)
Notation "k ↪[ γ ] dq v"
:= (ghost_map_elem γ k dq v)
  (at level 20, γ at level 50, dq custom dfrac at level 1,
   only parsing) : bi_scope.
(* iris/base_logic/lib/ghost_map.v *)
Ltac unseal
:= rewrite
  ?ghost_map_auth_unseal /ghost_map_auth_def
  ?ghost_map_elem_unseal /ghost_map_elem_def.
(* iris/base_logic/lib/ghost_map.v *)
(* * Lemmas about the map elements *)
Instance ghost_map_elem_timeless k γ dq v : Timeless (γ ↪◯MAP[k]{dq} v).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_elem_persistent k γ v : Persistent (γ ↪◯MAP[k]□ v).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_elem_fractional k γ v :
    Fractional (λ q, γ ↪◯MAP[k]{#q} v)%I.
Proof. unseal=> p q. rewrite -own_op -gmap_view_frag_add agree_idemp //. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_elem_as_fractional k γ q v :
    AsFractional (γ ↪◯MAP[k]{#q} v) (λ q, γ ↪◯MAP[k]{#q} v)%I q.
Proof. split; first done. apply _. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_elems_unseal γ m dq :
    ([∗ map] k ↦ v ∈ m, γ ↪◯MAP[k]{dq} v) ==∗
    own γ ([^op map] k↦v ∈ m,
      gmap_view_frag (V:=agreeR (leibnizO V)) k dq (to_agree v)).
Proof.
    unseal. destruct (decide (m = ∅)) as [->|Hne].
    - rewrite !big_opM_empty. iIntros "_". iApply own_unit.
    - rewrite big_opM_own //. iIntros "?". done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_elem_valid k γ dq v : γ ↪◯MAP[k]{dq} v -∗ ⌜✓ dq⌝.
Proof.
    unseal. iIntros "Helem".
    iDestruct (own_valid with "Helem") as %?%gmap_view_frag_valid.
    naive_solver.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_elem_valid_2 k γ dq1 dq2 v1 v2 :
    γ ↪◯MAP[k]{dq1} v1 -∗ γ ↪◯MAP[k]{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
Proof.
    unseal. iIntros "H1 H2".
    iCombine "H1 H2" gives %[? Hag]%gmap_view_frag_op_valid.
    rewrite to_agree_op_valid_L in Hag. done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_elem_agree k γ dq1 dq2 v1 v2 :
    γ ↪◯MAP[k]{dq1} v1 -∗ γ ↪◯MAP[k]{dq2} v2 -∗ ⌜v1 = v2⌝.
Proof.
    iIntros "Helem1 Helem2".
    iDestruct (ghost_map_elem_valid_2 with "Helem1 Helem2") as %[_ ?].
    done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_elem_combine_gives γ k v1 dq1 v2 dq2 :
    CombineSepGives (γ ↪◯MAP[k]{dq1} v1) (γ ↪◯MAP[k]{dq2} v2)
      ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
Proof.
    rewrite /CombineSepGives. iIntros "[H1 H2]".
    iDestruct (ghost_map_elem_valid_2 with "H1 H2") as %[H1 H2].
    eauto.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_elem_combine k γ dq1 dq2 v1 v2 :
    γ ↪◯MAP[k]{dq1} v1 -∗
    γ ↪◯MAP[k]{dq2} v2 -∗
    γ ↪◯MAP[k]{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
Proof.
    iIntros "Hl1 Hl2". iDestruct (ghost_map_elem_agree with "Hl1 Hl2") as %->.
    unseal. iCombine "Hl1 Hl2" as "Hl". rewrite agree_idemp. eauto with iFrame.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_elem_combine_as k γ dq1 dq2 v1 v2 :
    CombineSepAs (γ ↪◯MAP[k]{dq1} v1) (γ ↪◯MAP[k]{dq2} v2)
                 (γ ↪◯MAP[k]{dq1 ⋅ dq2} v1) | 60.
(* higher cost than the Fractional instance [combine_sep_fractional_bwd],
       which kicks in for #qs *)
  Proof.
    rewrite /CombineSepAs. iIntros "[H1 H2]".
    iDestruct (ghost_map_elem_combine with "H1 H2") as "[$ _]".
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_elem_frac_ne γ k1 k2 dq1 dq2 v1 v2 :
    ¬ ✓ (dq1 ⋅ dq2) → γ ↪◯MAP[k1]{dq1} v1 -∗ γ ↪◯MAP[k2]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
Proof.
    iIntros (?) "H1 H2"; iIntros (->).
    by iCombine "H1 H2" gives %[??].
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_elem_ne γ k1 k2 dq2 v1 v2 :
    γ ↪◯MAP[k1] v1 -∗ γ ↪◯MAP[k2]{dq2} v2 -∗ ⌜k1 ≠ k2⌝.
Proof. apply ghost_map_elem_frac_ne. apply: exclusive_l. Qed.
(* iris/base_logic/lib/ghost_map.v *)
(* Make an element read-only. *)
Lemma ghost_map_elem_persist k γ dq v :
    γ ↪◯MAP[k]{dq} v ==∗ γ ↪◯MAP[k]□ v.
Proof. unseal. iApply own_update. apply gmap_view_frag_persist. Qed.
(* iris/base_logic/lib/ghost_map.v *)
(* Recover fractional ownership for read-only element. *)
Lemma ghost_map_elem_unpersist k γ v :
    γ ↪◯MAP[k]□ v ==∗ ∃ q, γ ↪◯MAP[k]{#q} v.
Proof.
    unseal. iIntros "H".
    iMod (own_updateP with "H") as "H";
      first by apply gmap_view_frag_unpersist.
    iDestruct "H" as (? (q&->)) "H".
    iIntros "!>". iExists q. done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
(* * Lemmas about [ghost_map_auth] *)
Lemma ghost_map_alloc_strong P m :
    pred_infinite P →
    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ γ ↪●MAP m ∗ [∗ map] k ↦ v ∈ m, γ ↪◯MAP[k] v.
Proof.
    unseal. intros.
    iMod (own_alloc_strong
      (gmap_view_auth (V:=agreeR (leibnizO V)) (DfracOwn 1) ∅) P)
      as (γ) "[% Hauth]"; first done.
    { apply gmap_view_auth_valid. }
    iExists γ. iSplitR; first done.
    rewrite -big_opM_own_1 -own_op. iApply (own_update with "Hauth").
    etrans; first apply (gmap_view_alloc_big _ (to_agree <$> m) (DfracOwn 1)).
    - apply map_disjoint_empty_r.
    - done.
    - by apply map_Forall_fmap.
    - rewrite right_id big_opM_fmap. done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_alloc_strong_empty P :
    pred_infinite P →
    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ γ ↪●MAP (∅ : gmap K V).
Proof.
    intros. iMod (ghost_map_alloc_strong P ∅) as (γ) "(% & Hauth & _)"; eauto.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_alloc m :
    ⊢ |==> ∃ γ, γ ↪●MAP m ∗ [∗ map] k ↦ v ∈ m, γ ↪◯MAP[k] v.
Proof.
    iMod (ghost_map_alloc_strong (λ _, True) m) as (γ) "[_ Hmap]".
    - by apply pred_infinite_True.
    - eauto.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_alloc_empty :
    ⊢ |==> ∃ γ, γ ↪●MAP (∅ : gmap K V).
Proof.
    intros. iMod (ghost_map_alloc ∅) as (γ) "(Hauth & _)"; eauto.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_auth_timeless γ dq m : Timeless (γ ↪●MAP{dq} m).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_persistent γ m : Timeless (γ ↪●MAP□ m).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_auth_fractional γ m : Fractional (λ q, γ ↪●MAP{#q} m)%I.
Proof. intros p q. unseal. rewrite -own_op -gmap_view_auth_dfrac_op //. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_auth_as_fractional γ q m :
    AsFractional (γ ↪●MAP{#q} m) (λ q, γ ↪●MAP{#q} m)%I q.
Proof. split; first done. apply _. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_auth_valid γ dq m : γ ↪●MAP{dq} m -∗ ⌜✓ dq⌝%Qp.
Proof.
    unseal. iIntros "Hauth".
    iDestruct (own_valid with "Hauth") as %?%gmap_view_auth_dfrac_valid.
    done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_auth_valid_2 γ dq1 dq2 m1 m2 :
    γ ↪●MAP{dq1} m1 -∗ γ ↪●MAP{dq2} m2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ m1 = m2⌝.
Proof.
    unseal. iIntros "H1 H2".
    (* We need to explicitly specify the Inj instances instead of
    using inj _ since we need to specify [leibnizO] for [to_agree_inj]. *)
    iCombine "H1 H2" gives %[? ?%(map_fmap_equiv_inj _
      (to_agree_inj (A:=(leibnizO _))))]%gmap_view_auth_dfrac_op_valid.
    iPureIntro. split; first done. by fold_leibniz.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_auth_agree γ dq1 dq2 m1 m2 :
    γ ↪●MAP{dq1} m1 -∗ γ ↪●MAP{dq2} m2 -∗ ⌜m1 = m2⌝.
Proof.
    iIntros "H1 H2".
    iDestruct (ghost_map_auth_valid_2 with "H1 H2") as %[_ ?].
    done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_auth_persist γ dq m :
    γ ↪●MAP{dq} m ==∗ γ ↪●MAP□ m.
Proof. unseal. iApply own_update. apply gmap_view_auth_persist. Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_auth_unpersist γ m :
    γ ↪●MAP□ m ==∗ ∃ q, γ ↪●MAP{#q} m.
Proof.
    unseal. iIntros "H".
    iMod (own_updateP with "H") as "H";
      first by apply gmap_view_auth_unpersist.
    iDestruct "H" as (? (q&->)) "H".
    iIntros "!>". iExists q. done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
(* * Lemmas about the interaction of [ghost_map_auth] with the elements *)
Lemma ghost_map_lookup {γ dq m k dq' v} :
    γ ↪●MAP{dq} m -∗ γ ↪◯MAP[k]{dq'} v -∗ ⌜m !! k = Some v⌝.
Proof.
    unseal. iIntros "Hauth Hel".
    iCombine "Hauth Hel" gives
      %(av' & _ & _ & Hav' & _ & Hincl)%gmap_view_both_dfrac_valid_discrete_total.
    iPureIntro.
    apply lookup_fmap_Some in Hav' as [v' [<- Hv']].
    (* FIXME: Why do we need [(SI:=natSI) (A:=leibnizO V)]
    https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555 seems to resolve
    the problem? *)
    apply (to_agree_included_L (SI:=natSI) (A:=leibnizO V)) in Hincl.
    by rewrite Hincl.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_lookup_combine_gives_1 {γ dq m k dq' v} :
    CombineSepGives (γ ↪●MAP{dq} m) (γ ↪◯MAP[k]{dq'} v) ⌜m !! k = Some v⌝.
Proof.
    rewrite /CombineSepGives. iIntros "[H1 H2]".
    iDestruct (ghost_map_lookup with "H1 H2") as %->. eauto.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Instance ghost_map_lookup_combine_gives_2 {γ dq m k dq' v} :
    CombineSepGives (γ ↪◯MAP[k]{dq} v) (γ ↪●MAP{dq'} m) ⌜m !! k = Some v⌝.
Proof.
    rewrite /CombineSepGives comm. apply ghost_map_lookup_combine_gives_1.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_insert {γ m} k v :
    m !! k = None →
    γ ↪●MAP m ==∗ γ ↪●MAP <[k:=v]> m ∗ γ ↪◯MAP[k] v.
Proof.
    unseal. intros Hm. rewrite -own_op.
    iApply own_update. rewrite fmap_insert. apply: gmap_view_alloc; [|done..].
    rewrite lookup_fmap Hm //.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_insert_persist {γ m} k v :
    m !! k = None →
    γ ↪●MAP m ==∗ γ ↪●MAP <[k:=v]> m ∗ γ ↪◯MAP[k]□ v.
Proof.
    iIntros (?) "Hauth".
    iMod (ghost_map_insert k with "Hauth") as "[$ Helem]"; first done.
    iApply ghost_map_elem_persist. done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_delete {γ m k v} :
    γ ↪●MAP m -∗ γ ↪◯MAP[k] v ==∗ γ ↪●MAP delete k m.
Proof.
    unseal. iApply bi.wand_intro_r. rewrite -own_op.
    iApply own_update. rewrite fmap_delete. apply: gmap_view_delete.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_update {γ m k v} w :
    γ ↪●MAP m -∗ γ ↪◯MAP[k] v ==∗ γ ↪●MAP <[k:=w]> m ∗ γ ↪◯MAP[k] w.
Proof.
    unseal. iApply bi.wand_intro_r. rewrite -!own_op.
    iApply own_update. rewrite fmap_insert. apply: gmap_view_replace; done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
(* Big-op versions of above lemmas *)
Lemma ghost_map_lookup_big {γ dq m dq'} m0 :
    γ ↪●MAP{dq} m -∗
    ([∗ map] k↦v ∈ m0, γ ↪◯MAP[k]{dq'} v) -∗
    ⌜m0 ⊆ m⌝.
Proof.
    iIntros "Hauth Hfrag". rewrite map_subseteq_spec. iIntros (k v Hm0).
    iDestruct (ghost_map_lookup with "Hauth [Hfrag]") as %->.
    { rewrite big_sepM_lookup; done. }
    done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_insert_big {γ m} m' :
    m' ##ₘ m →
    γ ↪●MAP m ==∗
    γ ↪●MAP (m' ∪ m) ∗ [∗ map] k ↦ v ∈ m', γ ↪◯MAP[k] v.
Proof.
    unseal. intros ?. rewrite -big_opM_own_1 -own_op. iApply own_update.
    etrans; first apply: (gmap_view_alloc_big _ (to_agree <$> m') (DfracOwn 1)).
    - apply map_disjoint_fmap. done.
    - done.
    - by apply map_Forall_fmap.
    - rewrite map_fmap_union big_opM_fmap. done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_insert_persist_big {γ m} m' :
    m' ##ₘ m →
    γ ↪●MAP m ==∗
    γ ↪●MAP (m' ∪ m) ∗ [∗ map] k ↦ v ∈ m', γ ↪◯MAP[k]□ v.
Proof.
    iIntros (Hdisj) "Hauth".
    iMod (ghost_map_insert_big m' with "Hauth") as "[$ Helem]"; first done.
    iApply big_sepM_bupd. iApply (big_sepM_impl with "Helem").
    iIntros "!#" (k v) "_". iApply ghost_map_elem_persist.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Lemma ghost_map_delete_big {γ m} m0 :
    γ ↪●MAP m -∗
    ([∗ map] k↦v ∈ m0, γ ↪◯MAP[k] v) ==∗
    γ ↪●MAP (m ∖ m0).
Proof.
    iIntros "Hauth Hfrag". iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
    unseal. iApply (own_update_2 with "Hauth Hfrag").
    rewrite map_fmap_difference.
    etrans; last apply: gmap_view_delete_big.
    rewrite big_opM_fmap. done.
  Qed.
(* iris/base_logic/lib/ghost_map.v *)
Theorem ghost_map_update_big {γ m} m0 m1 :
    dom m0 = dom m1 →
    γ ↪●MAP m -∗
    ([∗ map] k↦v ∈ m0, γ ↪◯MAP[k] v) ==∗
    γ ↪●MAP (m1 ∪ m) ∗ [∗ map] k↦v ∈ m1, γ ↪◯MAP[k] v.
Proof.
    iIntros (?) "Hauth Hfrag".
    iMod (ghost_map_elems_unseal with "Hfrag") as "Hfrag".
    unseal. rewrite -big_opM_own_1 -own_op.
    iApply (own_update_2 with "Hauth Hfrag").
    rewrite map_fmap_union.
    rewrite -!(big_opM_fmap to_agree (λ k, gmap_view_frag k (DfracOwn 1))).
    apply: gmap_view_replace_big.
    - rewrite !dom_fmap_L. done.
    - by apply map_Forall_fmap.
  Qed.
(* iris/base_logic/lib/ghost_var.v *)
(* The CMRA we need. *)
Class ghost_varG Σ (A : Type)
:= GhostVarG {
  #[local] ghost_var_inG :: inG Σ (dfrac_agreeR $ leibnizO A);
}.
(* iris/base_logic/lib/ghost_var.v *)
Definition ghost_varΣ (A : Type) : gFunctors
:=
  #[ GFunctor (dfrac_agreeR $ leibnizO A) ].
(* iris/base_logic/lib/ghost_var.v *)
Instance subG_ghost_varΣ Σ A : subG (ghost_varΣ A) Σ → ghost_varG Σ A.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/ghost_var.v *)
Definition ghost_var_def `{!ghost_varG Σ A}
    (γ : gname) (dq : dfrac) (a : A) : iProp Σ
:=
  own γ (to_dfrac_agree (A:=leibnizO A) dq a).
(* iris/base_logic/lib/ghost_var.v *)
Definition ghost_var_aux : seal (@ghost_var_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/ghost_var.v *)
Definition ghost_var
:= ghost_var_aux.(unseal).
(* iris/base_logic/lib/ghost_var.v *)
Definition ghost_var_unseal :
  @ghost_var = @ghost_var_def
:= ghost_var_aux.(seal_eq).
(* iris/base_logic/lib/ghost_var.v *)
Ltac unseal
:= rewrite ?ghost_var_unseal /ghost_var_def.
(* iris/base_logic/lib/ghost_var.v *)
Notation "γ ↪VAR dq n"
:= (ghost_var γ dq n)
  (at level 20, dq custom dfrac at level 1,
   format "γ  ↪VAR dq  n").
(* iris/base_logic/lib/ghost_var.v *)
(* Compatibility alias. Do not use for new code.
This will eventually be deprecated and removed. *)
Notation ghost_var_frac γ q n
:= (ghost_var γ (DfracOwn q) n) (only parsing).
(* iris/base_logic/lib/ghost_var.v *)
Instance ghost_var_timeless γ dq a : Timeless (γ ↪VAR{dq} a).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/ghost_var.v *)
Instance ghost_var_persistent γ a : Persistent (γ ↪VAR□ a).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/ghost_var.v *)
Instance ghost_var_fractional γ a : Fractional (λ q, γ ↪VAR{#q} a).
Proof. intros q1 q2. unseal. rewrite -own_op -frac_agree_op //. Qed.
(* iris/base_logic/lib/ghost_var.v *)
Instance ghost_var_as_fractional γ a q :
    AsFractional (γ ↪VAR{#q} a) (λ q, γ ↪VAR{#q} a) q.
Proof. split; [done|]. apply _. Qed.
(* iris/base_logic/lib/ghost_var.v *)
Lemma ghost_var_alloc_strong a (P : gname → Prop) :
    pred_infinite P →
    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ γ ↪VAR a.
Proof. unseal. intros. iApply own_alloc_strong; done. Qed.
(* iris/base_logic/lib/ghost_var.v *)
Lemma ghost_var_alloc a :
    ⊢ |==> ∃ γ, γ ↪VAR a.
Proof. unseal. iApply own_alloc. done. Qed.
(* iris/base_logic/lib/ghost_var.v *)
Lemma ghost_var_valid_2 γ a1 dq1 a2 dq2 :
    γ ↪VAR{dq1} a1 -∗ γ ↪VAR{dq2} a2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ a1 = a2⌝.
Proof.
    unseal. iIntros "Hvar1 Hvar2".
    iCombine "Hvar1 Hvar2" gives %[Hq Ha]%dfrac_agree_op_valid.
    done.
  Qed.
(* iris/base_logic/lib/ghost_var.v *)
(* Almost all the time, this is all you really need. *)
Lemma ghost_var_agree γ a1 dq1 a2 dq2 :
    γ ↪VAR{dq1} a1 -∗ γ ↪VAR{dq2} a2 -∗ ⌜a1 = a2⌝.
Proof.
    iIntros "Hvar1 Hvar2".
    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done.
  Qed.
(* iris/base_logic/lib/ghost_var.v *)
Instance ghost_var_combine_gives γ a1 dq1 a2 dq2 :
    CombineSepGives (γ ↪VAR{dq1} a1) (γ ↪VAR{dq2} a2) ⌜✓ (dq1 ⋅ dq2) ∧ a1 = a2⌝.
Proof.
    rewrite /CombineSepGives. iIntros "[H1 H2]".
    iDestruct (ghost_var_valid_2 with "H1 H2") as %[H1 H2].
    eauto.
  Qed.
(* iris/base_logic/lib/ghost_var.v *)
Instance ghost_var_combine_as γ a1 dq1 a2 dq2 dq :
    IsOp dq dq1 dq2 →
    CombineSepAs (γ ↪VAR{dq1} a1) (γ ↪VAR{dq2} a2) (γ ↪VAR{dq} a1) | 60.
(* higher cost than the Fractional instance, which is used for a1 = a2 *)
  Proof.
    rewrite /CombineSepAs /IsOp => ->. iIntros "[H1 H2]".
    (* This can't be a single [iCombine] since the instance providing that is
    exactly what we are proving here. *)
    iCombine "H1 H2" gives %[_ ->].
    unseal. iCombine "H1 H2" as "H". rewrite dfrac_agree_op. done.
  Qed.
(* iris/base_logic/lib/ghost_var.v *)
(* This is just an instance of fractionality above, but that can be hard to find. *)
Lemma ghost_var_split γ a q1 q2 :
    γ ↪VAR{#q1 + q2} a -∗ γ ↪VAR{#q1} a ∗ γ ↪VAR{#q2} a.
Proof. iIntros "[$$]". Qed.
(* iris/base_logic/lib/ghost_var.v *)
(* Update the ghost variable to new value [b]. *)
Lemma ghost_var_update b γ a :
    γ ↪VAR a ==∗ γ ↪VAR b.
Proof.
    unseal. iApply own_update. apply cmra_update_exclusive. done.
  Qed.
(* iris/base_logic/lib/ghost_var.v *)
Lemma ghost_var_update_2 b γ a1 q1 a2 q2 :
    (q1 + q2 = 1)%Qp →
    γ ↪VAR{#q1} a1 -∗ γ ↪VAR{#q2} a2 ==∗ γ ↪VAR{#q1} b ∗ γ ↪VAR{#q2} b.
Proof.
    intros Hq. unseal. rewrite -own_op. iApply own_update_2.
    apply frac_agree_update_2. done.
  Qed.
(* iris/base_logic/lib/ghost_var.v *)
Lemma ghost_var_update_halves b γ a1 a2 :
    γ ↪VAR{#1/2} a1 -∗
    γ ↪VAR{#1/2} a2 ==∗
    γ ↪VAR{#1/2} b ∗ γ ↪VAR{#1/2} b.
Proof. iApply ghost_var_update_2. apply Qp.half_half. Qed.
(* iris/base_logic/lib/ghost_var.v *)
Lemma ghost_var_persist γ dq a :
    γ ↪VAR{dq} a ==∗ γ ↪VAR□ a.
Proof.
    unseal. iApply own_update. apply dfrac_agree_persist.
  Qed.
(* iris/base_logic/lib/ghost_var.v *)
Lemma ghost_var_unpersist γ a :
    γ ↪VAR□ a ==∗ ∃ q, γ ↪VAR{#q} a.
Proof.
    unseal. iIntros "H".
    iMod (own_updateP with "H") as "H";
      first by apply dfrac_agree_unpersist.
    iDestruct "H" as (? (q&->)) "H".
    iIntros "!>". iExists q. done.
  Qed.
(* iris/base_logic/lib/ghost_var.v *)
(* Framing support *)
Instance frame_ghost_var p γ a q1 q2 q :
    FrameFractionalQp q1 q2 q →
    Frame p (γ ↪VAR{#q1} a) (γ ↪VAR{#q2} a) (γ ↪VAR{#q} a) | 5.
Proof. apply: frame_fractional. Qed.
(* iris/base_logic/lib/gset_bij.v *)
(* The uCMRA we need. *)
Class gset_bijG Σ A B `{Countable A, Countable B}
:=
  GsetBijG { #[local] gset_bijG_inG :: inG Σ (gset_bijR A B); }.
(* iris/base_logic/lib/gset_bij.v *)
Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors
:=
  #[ GFunctor (gset_bijR A B) ].
(* iris/base_logic/lib/gset_bij.v *)
Instance subG_gset_bijΣ `{Countable A, Countable B} Σ :
  subG (gset_bijΣ A B) Σ → gset_bijG Σ A B.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/gset_bij.v *)
Definition gset_bij_own_auth_def `{gset_bijG Σ A B} (γ : gname)
    (dq : dfrac) (L : gset (A * B)) : iProp Σ
:=
  own γ (gset_bij_auth dq L).
(* iris/base_logic/lib/gset_bij.v *)
Definition gset_bij_own_auth_aux : seal (@gset_bij_own_auth_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/gset_bij.v *)
Definition gset_bij_own_auth
:= unseal gset_bij_own_auth_aux.
(* iris/base_logic/lib/gset_bij.v *)
Definition gset_bij_own_auth_eq :
  @gset_bij_own_auth = @gset_bij_own_auth_def
:= seal_eq gset_bij_own_auth_aux.
(* iris/base_logic/lib/gset_bij.v *)
Definition gset_bij_own_elem_def `{gset_bijG Σ A B} (γ : gname)
  (a : A) (b : B) : iProp Σ
:= own γ (gset_bij_elem a b).
(* iris/base_logic/lib/gset_bij.v *)
Definition gset_bij_own_elem_aux : seal (@gset_bij_own_elem_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/gset_bij.v *)
Definition gset_bij_own_elem
:= unseal gset_bij_own_elem_aux.
(* iris/base_logic/lib/gset_bij.v *)
Definition gset_bij_own_elem_eq :
  @gset_bij_own_elem = @gset_bij_own_elem_def
:= seal_eq gset_bij_own_elem_aux.
(* iris/base_logic/lib/gset_bij.v *)
Notation "γ ↪●BIJ dq L"
:= (gset_bij_own_auth γ dq L)
  (at level 20, dq custom dfrac at level 1,
   format "γ  ↪●BIJ dq  L").
(* iris/base_logic/lib/gset_bij.v *)
Notation "γ ↪◯BIJ ⟨ a , b ⟩"
:= (gset_bij_own_elem γ a b)
  (at level 20, format "γ  ↪◯BIJ  ⟨ a , b ⟩").
(* iris/base_logic/lib/gset_bij.v *)
Instance gset_bij_own_auth_timeless γ dq L :
    Timeless (γ ↪●BIJ{dq} L).
Proof. rewrite gset_bij_own_auth_eq. apply _. Qed.
(* iris/base_logic/lib/gset_bij.v *)
Instance gset_bij_own_auth_persistent γ L :
    Persistent (γ ↪●BIJ□ L).
Proof. rewrite gset_bij_own_auth_eq. apply _. Qed.
(* iris/base_logic/lib/gset_bij.v *)
Instance gset_bij_own_elem_timeless γ a b :
    Timeless (γ ↪◯BIJ ⟨a,b⟩).
Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
(* iris/base_logic/lib/gset_bij.v *)
Instance gset_bij_own_elem_persistent γ a b :
    Persistent (γ ↪◯BIJ ⟨a,b⟩).
Proof. rewrite gset_bij_own_elem_eq. apply _. Qed.
(* iris/base_logic/lib/gset_bij.v *)
Instance gset_bij_own_auth_fractional γ L :
    Fractional (λ q, γ ↪●BIJ{#q} L).
Proof.
    intros p q. rewrite gset_bij_own_auth_eq -own_op gset_bij_auth_dfrac_op //.
  Qed.