phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/lib/mono_nat.v *)
Instance mono_nat_auth_own_timeless γ dq n : Timeless (γ ↪●MN{dq} n).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Instance mono_nat_auth_own_persistent γ n : Persistent (γ ↪●MN□ n).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Instance mono_nat_lb_own_timeless γ n : Timeless (γ ↪◯MN n).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Instance mono_nat_lb_own_persistent γ n : Persistent (γ ↪◯MN n).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Instance mono_nat_auth_own_fractional γ n :
    Fractional (λ q, γ ↪●MN{#q} n).
Proof. unseal. intros p q. rewrite -own_op -mono_nat_auth_dfrac_op //. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Instance mono_nat_auth_own_as_fractional γ q n :
    AsFractional (γ ↪●MN{#q} n) (λ q, γ ↪●MN{#q} n) q.
Proof. split; [auto|apply _]. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_auth_own_agree γ dq1 dq2 n1 n2 :
    γ ↪●MN{dq1} n1 -∗
    γ ↪●MN{dq2} n2 -∗
    ⌜✓ (dq1 ⋅ dq2) ∧ n1 = n2⌝.
Proof.
    unseal. iIntros "H1 H2".
    iCombine "H1 H2" gives %?%mono_nat_auth_dfrac_op_valid; done.
  Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_auth_own_exclusive γ n1 n2 :
    γ ↪●MN n1 -∗ γ ↪●MN n2 -∗ False.
Proof.
    iIntros "H1 H2".
    by iDestruct (mono_nat_auth_own_agree with "H1 H2") as %[[] _].
  Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_auth_lb_own_valid γ dq n m :
    γ ↪●MN{dq} n -∗ γ ↪◯MN m -∗ ⌜✓ dq ∧ m ≤ n⌝.
Proof.
    unseal. iIntros "Hauth Hlb".
    iCombine "Hauth Hlb" gives %Hvalid%mono_nat_both_dfrac_valid.
    auto.
  Qed.
(* iris/base_logic/lib/mono_nat.v *)
(* The conclusion of this lemma is persistent; the proofmode will preserve
  the [mono_nat_auth_own] in the premise as long as the conclusion is introduced
  to the persistent context, for example with [iDestruct (mono_nat_lb_own_get
  with "Hauth") as "#Hfrag"]. *)
Lemma mono_nat_lb_own_get γ dq n :
    γ ↪●MN{dq} n -∗ γ ↪◯MN n.
Proof. unseal. iApply own_mono. apply mono_nat_included. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_lb_own_le {γ n} n' :
    n' ≤ n →
    γ ↪◯MN n -∗ γ ↪◯MN n'.
Proof. unseal. intros. iApply own_mono. by apply mono_nat_lb_mono. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_lb_own_0 γ :
    ⊢ |==> γ ↪◯MN 0.
Proof. unseal. iApply own_unit. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_own_alloc_strong P n :
    pred_infinite P →
    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ γ ↪●MN n ∗ γ ↪◯MN n.
Proof.
    unseal. intros.
    iMod (own_alloc_strong (●MN n ⋅ ◯MN n) P) as (γ) "[% [??]]"; first done.
    { apply mono_nat_both_valid; auto. }
    auto with iFrame.
  Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_own_alloc n :
    ⊢ |==> ∃ γ, γ ↪●MN n ∗ γ ↪◯MN n.
Proof.
    iMod (mono_nat_own_alloc_strong (λ _, True) n) as (γ) "[_ ?]".
    - by apply pred_infinite_True.
    - eauto.
  Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_own_update {γ n} n' :
    n ≤ n' →
    γ ↪●MN n ==∗ γ ↪●MN n' ∗ γ ↪◯MN n'.
Proof.
    iIntros (?) "Hauth".
    iAssert (γ ↪●MN n') with "[> Hauth]" as "Hauth".
    { unseal. iApply (own_update with "Hauth"). by apply mono_nat_update. }
    iModIntro. iSplit; [done|]. by iApply mono_nat_lb_own_get.
  Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_own_persist γ dq a :
    γ ↪●MN{dq} a ==∗ γ ↪●MN□ a.
Proof.
    unseal. iApply own_update. apply mono_nat_auth_persist.
  Qed.
(* iris/base_logic/lib/mono_nat.v *)
Lemma mono_nat_own_unpersist γ a :
    γ ↪●MN□ a ==∗ ∃ q, γ ↪●MN{#q} a.
Proof.
    unseal. iIntros "H".
    iMod (own_updateP with "H") as "H";
      first by apply mono_nat_auth_unpersist.
    iDestruct "H" as (? (q&->)) "H".
    iIntros "!>". iExists q. done.
  Qed.
(* iris/base_logic/lib/mono_Z.v *)
Class mono_ZG Σ
:=
  MonoZG { #[local] mono_ZG_natG :: mono_natG Σ; }.
(* iris/base_logic/lib/mono_Z.v *)
Definition mono_ZΣ
:= mono_natΣ.
(* iris/base_logic/lib/mono_Z.v *)
Definition mono_Z_auth_own_def `{!mono_ZG Σ}
    (γ : gname) (dq : dfrac) (n : Z) : iProp Σ
:=
  ⌜0 ≤ n⌝ ∗ γ ↪●MN{dq} (Z.to_nat n).
(* iris/base_logic/lib/mono_Z.v *)
Definition mono_Z_auth_own_aux : seal (@mono_Z_auth_own_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/mono_Z.v *)
Definition mono_Z_auth_own
:= mono_Z_auth_own_aux.(unseal).
(* iris/base_logic/lib/mono_Z.v *)
Definition mono_Z_auth_own_unseal :
  @mono_Z_auth_own = @mono_Z_auth_own_def
:= mono_Z_auth_own_aux.(seal_eq).
(* iris/base_logic/lib/mono_Z.v *)
Definition mono_Z_lb_own_def `{!mono_ZG Σ} (γ : gname) (n : Z) : iProp Σ
:=
  ⌜0 ≤ n⌝ ∗ γ ↪◯MN (Z.to_nat n).
(* iris/base_logic/lib/mono_Z.v *)
Definition mono_Z_lb_own_aux : seal (@mono_Z_lb_own_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/mono_Z.v *)
Definition mono_Z_lb_own
:= mono_Z_lb_own_aux.(unseal).
(* iris/base_logic/lib/mono_Z.v *)
Definition mono_Z_lb_own_unseal :
  @mono_Z_lb_own = @mono_Z_lb_own_def
:= mono_Z_lb_own_aux.(seal_eq).
(* iris/base_logic/lib/mono_Z.v *)
Notation "γ ↪●MZ dq n"
:= (mono_Z_auth_own γ dq n)
  (at level 20, dq custom dfrac at level 1,
   format "γ  ↪●MZ dq  n").
(* iris/base_logic/lib/mono_Z.v *)
Notation "γ ↪◯MZ n"
:= (mono_Z_lb_own γ n)
  (at level 20).
(* iris/base_logic/lib/mono_Z.v *)
(* Compatibility alias. Do not use for new code.
This will eventually be deprecated and removed. *)
Notation mono_Z_auth_own_frac γ q n
:=
  (mono_Z_auth_own γ (DfracOwn q) n) (only parsing).
(* iris/base_logic/lib/mono_Z.v *)
Ltac unseal
:= rewrite
  ?mono_Z_auth_own_unseal /mono_Z_auth_own_def
  ?mono_Z_lb_own_unseal /mono_Z_lb_own_def.
(* iris/base_logic/lib/mono_Z.v *)
Instance mono_Z_auth_own_timeless γ dq n : Timeless (γ ↪●MZ{dq} n).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_Z.v *)
Instance mono_Z_auth_own_persistent γ n : Persistent (γ ↪●MZ□ n).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_Z.v *)
Instance mono_Z_lb_own_timeless γ n : Timeless (γ ↪◯MZ n).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_Z.v *)
Instance mono_Z_lb_own_persistent γ n : Persistent (γ ↪◯MZ n).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_Z.v *)
Instance mono_Z_auth_own_fractional γ n :
    Fractional (λ q, γ ↪●MZ{#q} n).
Proof.
    unseal. intros p q. iSplit.
    - iIntros "[% [$ $]]". eauto.
    - iIntros "[[% H1] [% H2]]". iCombine "H1 H2" as "$". eauto.
  Qed.
(* iris/base_logic/lib/mono_Z.v *)
Instance mono_Z_auth_own_as_fractional γ q n :
    AsFractional (γ ↪●MZ{#q} n) (λ q, γ ↪●MZ{#q} n) q.
Proof. split; [auto|apply _]. Qed.
(* iris/base_logic/lib/mono_Z.v *)
Lemma mono_Z_auth_own_agree γ dq1 dq2 n1 n2 :
    γ ↪●MZ{dq1} n1 -∗
    γ ↪●MZ{dq2} n2 -∗
    ⌜✓ (dq1 ⋅ dq2) ∧ n1 = n2⌝.
Proof.
    unseal. iIntros "[% H1] [% H2]".
    iDestruct (mono_nat_auth_own_agree with "H1 H2") as %?.
    iPureIntro. naive_solver lia.
  Qed.
(* iris/base_logic/lib/mono_Z.v *)
Lemma mono_Z_auth_own_exclusive γ n1 n2 :
    γ ↪●MZ n1 -∗ γ ↪●MZ n2 -∗ False.
Proof.
    iIntros "H1 H2".
    by iDestruct (mono_Z_auth_own_agree with "H1 H2") as %[[] _].
  Qed.
(* iris/base_logic/lib/mono_Z.v *)
Lemma mono_Z_auth_lb_own_valid γ dq n m :
    γ ↪●MZ{dq} n -∗ γ ↪◯MZ m -∗ ⌜✓ dq ∧ m ≤ n⌝.
Proof.
    unseal. iIntros "[% Hauth] [% Hlb]".
    iDestruct (mono_nat_auth_lb_own_valid with "Hauth Hlb") as %Hvalid.
    iPureIntro. naive_solver lia.
  Qed.
(* iris/base_logic/lib/mono_Z.v *)
(* The conclusion of this lemma is persistent; the proofmode will preserve
  the [mono_Z_auth_own] in the premise as long as the conclusion is introduced
  to the persistent context, for example with [iDestruct (mono_Z_lb_own_get
  with "Hauth") as "#Hfrag"]. *)
Lemma mono_Z_lb_own_get γ dq n :
    γ ↪●MZ{dq} n -∗ γ ↪◯MZ n.
Proof. unseal. iIntros "[% ?]". iSplit; first done. by iApply mono_nat_lb_own_get. Qed.
(* iris/base_logic/lib/mono_Z.v *)
Lemma mono_Z_lb_own_le {γ n} n' :
    n' ≤ n →
    0 ≤ n' →
    γ ↪◯MZ n -∗ γ ↪◯MZ n'.
Proof.
    unseal. iIntros "% % [% ?]". iSplit; first done.
    iApply mono_nat_lb_own_le; last done. lia.
  Qed.
(* iris/base_logic/lib/mono_Z.v *)
Lemma mono_Z_lb_own_0 γ :
    ⊢ |==> γ ↪◯MZ 0.
Proof. unseal. iMod mono_nat_lb_own_0 as "$". eauto. Qed.
(* iris/base_logic/lib/mono_Z.v *)
Lemma mono_Z_own_alloc n :
    0 ≤ n →
    ⊢ |==> ∃ γ, γ ↪●MZ n ∗ γ ↪◯MZ n.
Proof.
    unseal. intros. iMod mono_nat_own_alloc as (γ) "[??]".
    iModIntro. iExists _. iFrame. eauto.
  Qed.
(* iris/base_logic/lib/mono_Z.v *)
Lemma mono_Z_own_update {γ n} n' :
    n ≤ n' →
    γ ↪●MZ n ==∗ γ ↪●MZ n' ∗ γ ↪◯MZ n'.
Proof.
    iIntros (?) "Hauth".
    iAssert (γ ↪●MZ n') with "[> Hauth]" as "Hauth".
    { unseal. iDestruct "Hauth" as "[% Hauth]".
      iMod (mono_nat_own_update with "Hauth") as "[$ _]"; auto with lia. }
    iModIntro. iSplit; [done|]. by iApply mono_Z_lb_own_get.
  Qed.
(* iris/base_logic/lib/mono_Z.v *)
Lemma mono_Z_own_persist γ dq a :
    γ ↪●MZ{dq} a ==∗ γ ↪●MZ□ a.
Proof.
    unseal. iIntros "[$ Hown]". iApply mono_nat_own_persist. done.
  Qed.
(* iris/base_logic/lib/mono_Z.v *)
Lemma mono_Z_own_unpersist γ a :
    γ ↪●MZ□ a ==∗ ∃ q, γ ↪●MZ{#q} a.
Proof.
    unseal. iIntros "[$ Hown]". iApply mono_nat_own_unpersist. done.
  Qed.
(* iris/base_logic/lib/na_invariants.v *)
(* Non-atomic ("thread-local") invariants. *)
Definition na_inv_pool_name
:= gname.
(* iris/base_logic/lib/na_invariants.v *)
Class na_invG Σ
:=
  #[local] na_inv_inG :: inG Σ (prodR coPset_disjR (gset_disjR positive)).
(* iris/base_logic/lib/na_invariants.v *)
Definition na_invΣ : gFunctors
:=
  #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
(* iris/base_logic/lib/na_invariants.v *)
Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/na_invariants.v *)
Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ
:=
    own p (CoPset E, GSet ∅).
(* iris/base_logic/lib/na_invariants.v *)
Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ
:=
    ∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧
         inv N (P ∗ own p (ε, GSet {[i]}) ∨ na_own p {[i]}).
(* iris/base_logic/lib/na_invariants.v *)
Instance : Params (@na_inv) 3
:= {}.
(* iris/base_logic/lib/na_invariants.v *)
Instance na_own_timeless p E : Timeless (na_own p E).
Proof. rewrite /na_own; apply _. Qed.
(* iris/base_logic/lib/na_invariants.v *)
Instance na_inv_contractive p N : Contractive (na_inv p N).
Proof. rewrite /na_inv. solve_contractive. Qed.
(* iris/base_logic/lib/na_invariants.v *)
Instance na_inv_ne p N : NonExpansive (na_inv p N).
Proof. rewrite /na_inv. solve_proper. Qed.
(* iris/base_logic/lib/na_invariants.v *)
Instance na_inv_proper p N : Proper ((≡) ==> (≡)) (na_inv p N).
Proof. apply (ne_proper _). Qed.
(* iris/base_logic/lib/na_invariants.v *)
Instance na_inv_persistent p N P : Persistent (na_inv p N P).
Proof. rewrite /na_inv; apply _. Qed.
(* iris/base_logic/lib/na_invariants.v *)
Instance na_own_empty_persistent p : Persistent (na_own p ∅).
Proof. rewrite /na_own; apply _. Qed.
(* iris/base_logic/lib/na_invariants.v *)
Lemma na_inv_iff p N P Q : na_inv p N P -∗ ▷ □ (P ↔ Q) -∗ na_inv p N Q.
Proof.
    rewrite /na_inv. iIntros "(%i & % & HI) #HPQ".
    iExists i. iSplit; first done. iApply (inv_iff with "HI").
    iIntros "!> !>".
    iSplit; iIntros "[[? Ho]|$]"; iLeft; iFrame "Ho"; by iApply "HPQ".
  Qed.
(* iris/base_logic/lib/na_invariants.v *)
Lemma na_alloc : ⊢ |==> ∃ p, na_own p ⊤.
Proof. by apply own_alloc. Qed.
(* iris/base_logic/lib/na_invariants.v *)
Lemma na_own_disjoint p E1 E2 : na_own p E1 -∗ na_own p E2 -∗ ⌜E1 ## E2⌝.
Proof.
    iApply wand_intro_r.
    rewrite /na_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
  Qed.
(* iris/base_logic/lib/na_invariants.v *)
Lemma na_own_union p E1 E2 :
    E1 ## E2 → na_own p (E1 ∪ E2) ⊣⊢ na_own p E1 ∗ na_own p E2.
Proof.
    intros. rewrite /na_own -own_op -pair_op. by rewrite coPset_disj_union.
  Qed.
(* iris/base_logic/lib/na_invariants.v *)
Lemma na_own_acc E2 E1 tid :
    E2 ⊆ E1 → na_own tid E1 -∗ na_own tid E2 ∗ (na_own tid E2 -∗ na_own tid E1).
Proof.
    intros HF. assert (E1 = E2 ∪ (E1 ∖ E2)) as -> by exact: union_difference_L.
    rewrite na_own_union; last by set_solver+. iIntros "[$ $]". auto.
  Qed.
(* iris/base_logic/lib/na_invariants.v *)
Lemma na_inv_alloc p E N P : ▷ P ={E}=∗ na_inv p N P.
Proof.
    iIntros "HP".
    iMod (own_unit (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
    iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
    { apply prod_updateP'.
      - apply cmra_updateP_id, (reflexivity (R:=eq)).
      - apply (gset_disj_alloc_empty_updateP_strong' (λ i, i ∈ (↑N:coPset)))=> Ef.
        apply fresh_inv_name. }
    simpl. iDestruct "Hm" as %(<- & i & -> & ?).
    rewrite /na_inv.
    iMod (inv_alloc N with "[-]"); last (iModIntro; iExists i; eauto).
    iNext. iLeft. by iFrame.
  Qed.
(* iris/base_logic/lib/na_invariants.v *)
Lemma na_inv_acc p E F N P :
    ↑N ⊆ E → ↑N ⊆ F →
    na_inv p N P -∗ na_own p F ={E}=∗ ▷ P ∗ na_own p (F∖↑N) ∗
                       (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F).
Proof.
    rewrite /na_inv. iIntros (??) "#(%i & % & Hinv) Htoks".
    rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
    rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
    iDestruct "Htoks" as "[[Htoki $] $]".
    iInv "Hinv" as "[[$ >Hdis]|>Htoki2]" "Hclose".
    - iMod ("Hclose" with "[Htoki]") as "_"; first auto.
      iIntros "!> [HP $]".
      iInv N as "[[_ >Hdis2]|>Hitok]".
      + iCombine "Hdis Hdis2" gives %[_ Hval%gset_disj_valid_op].
        set_solver.
      + iSplitR "Hitok"; last by iFrame. eauto with iFrame.
    - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
  Qed.
(* iris/base_logic/lib/na_invariants.v *)
Lemma na_own_empty p : ⊢ |==> na_own p ∅.
Proof. apply: own_unit. Qed.
(* iris/base_logic/lib/na_invariants.v *)
Instance into_inv_na p N P : IntoInv (na_inv p N P) N
:= {}.
(* iris/base_logic/lib/na_invariants.v *)
Instance into_acc_na p F E N P :
    IntoAcc (X:=unit) (na_inv p N P)
            (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) (fupd E E) (fupd E E)
            (λ _, ▷ P ∗ na_own p (F∖↑N))%I (λ _, ▷ P ∗ na_own p (F∖↑N))%I
              (λ _, Some (na_own p F))%I.
Proof.
    rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
    rewrite exist_unit -assoc /=.
    iApply (na_inv_acc with "Hinv"); done.
  Qed.
(* iris/base_logic/lib/own.v *)
(* The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
[Σ]. This class is similar to the [subG] class, but written down in terms of
individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmra)
:= InG {
  inG_id : gid Σ;
  inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
  inG_prf : A = inG_apply (iPropO Σ) _;
}.
(* iris/base_logic/lib/own.v *)
Lemma subG_inG Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPropO Σ)).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(* iris/base_logic/lib/own.v *)
(* This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
Ltac solve_inG
:=
  (* Get all assumptions *)
  intros;
  (* Unfold the top-level xΣ. We need to support this to be a function. *)
  lazymatch goal with
  | H : subG (?xΣ _ _ _ _) _ |- _ => try unfold xΣ in H
  | H : subG (?xΣ _ _ _) _ |- _ => try unfold xΣ in H
  | H : subG (?xΣ _ _) _ |- _ => try unfold xΣ in H
  | H : subG (?xΣ _) _ |- _ => try unfold xΣ in H
  | H : subG ?xΣ _ |- _ => try unfold xΣ in H
  end;
  (* Take apart subG for non-"atomic" lists *)
  repeat match goal with
         | H : subG (gFunctors.app _ _) _ |- _ => apply subG_inv in H; destruct H
         end;
  (* Try to turn singleton subG into inG; but also keep the subG for typeclass
     resolution -- to keep them, we put them onto the goal. *)
  repeat match goal with
         | H : subG _ _ |- _ => move:(H); (apply subG_inG in H || clear H)
         end;
  (* Again get all assumptions and simplify the functors *)
  intros; simpl in *;
  (* We support two kinds of goals: Things convertible to inG;
     and records with inG and typeclass fields. Try to solve the
     first case. *)
  try assumption;
  (* That didn't work, now we're in for the second case. *)
  split; (assumption || by apply _).
(* iris/base_logic/lib/own.v *)
(* * Definition of the connective [own] *)
Definition inG_unfold {Σ A} {i : inG Σ A} :
    inG_apply i (iPropO Σ) -n> inG_apply i (iPrePropO Σ)
:=
  rFunctor_map _ (iProp_fold, iProp_unfold).
(* iris/base_logic/lib/own.v *)
Definition inG_fold {Σ A} {i : inG Σ A} :
    inG_apply i (iPrePropO Σ) -n> inG_apply i (iPropO Σ)
:=
  rFunctor_map _ (iProp_unfold, iProp_fold).
(* iris/base_logic/lib/own.v *)
Definition iRes_singleton {Σ A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ
:=
  discrete_fun_singleton (inG_id i)
    {[ γ := inG_unfold (cmra_transport inG_prf a) ]}.
(* iris/base_logic/lib/own.v *)
Instance : Params (@iRes_singleton) 4
:= {}.
(* iris/base_logic/lib/own.v *)
Definition own_def `{!inG Σ A} (γ : gname) (a : A) : iProp Σ
:=
  uPred_ownM (iRes_singleton γ a).
(* iris/base_logic/lib/own.v *)
Definition own_aux : seal (@own_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/own.v *)
Definition own
:= own_aux.(unseal).
(* iris/base_logic/lib/own.v *)
Definition own_eq : @own = @own_def
:= own_aux.(seal_eq).
(* iris/base_logic/lib/own.v *)
Instance : Params (@own) 4
:= {}.
(* iris/base_logic/lib/own.v *)
(* ** Properties of [iRes_singleton] *)
Lemma inG_unfold_fold (x : inG_apply i (iPrePropO Σ)) :
  inG_unfold (inG_fold x) ≡ x.
Proof.
  rewrite /inG_unfold /inG_fold -rFunctor_map_compose -{2}[x]rFunctor_map_id.
  apply (ne_proper (rFunctor_map _)); split=> ?; apply iProp_unfold_fold.
Qed.
(* iris/base_logic/lib/own.v *)
Lemma inG_fold_unfold (x : inG_apply i (iPropO Σ)) :
  inG_fold (inG_unfold x) ≡ x.
Proof.
  rewrite /inG_unfold /inG_fold -rFunctor_map_compose -{2}[x]rFunctor_map_id.
  apply (ne_proper (rFunctor_map _)); split=> ?; apply iProp_fold_unfold.
Qed.
(* iris/base_logic/lib/own.v *)
Lemma inG_unfold_validN n (x : inG_apply i (iPropO Σ)) :
  ✓{n} (inG_unfold x) ↔ ✓{n} x.
Proof.
  split; [|apply (cmra_morphism_validN _)].
  move=> /(cmra_morphism_validN inG_fold). by rewrite inG_fold_unfold.
Qed.
(* iris/base_logic/lib/own.v *)
Instance iRes_singleton_ne γ : NonExpansive (@iRes_singleton Σ A _ γ).
Proof. by intros n a a' Ha; apply discrete_fun_singleton_ne; rewrite Ha. Qed.
(* iris/base_logic/lib/own.v *)
Lemma iRes_singleton_validI γ a : ✓ (iRes_singleton γ a) ⊢@{iPropI Σ} ✓ a.
Proof.
  sbi_unfold=> n. rewrite /iRes_singleton.
  rewrite discrete_fun_singleton_validN singleton_validN inG_unfold_validN.
  by destruct inG_prf.
Qed.
(* iris/base_logic/lib/own.v *)
Lemma iRes_singleton_op γ a1 a2 :
  iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
Proof.
  rewrite /iRes_singleton discrete_fun_singleton_op singleton_op cmra_transport_op.
  f_equiv. apply: singletonM_proper. apply (cmra_morphism_op _).
Qed.
(* iris/base_logic/lib/own.v *)
Instance iRes_singleton_discrete γ a :
  Discrete a → Discrete (iRes_singleton γ a).
Proof.
  intros ?. rewrite /iRes_singleton.
  apply discrete_fun_singleton_discrete, gmap_singleton_discrete; [apply _|].
  intros x Hx. assert (cmra_transport inG_prf a ≡ inG_fold x) as Ha.
  { apply (discrete_0 _). by rewrite -Hx inG_fold_unfold. }
  by rewrite Ha inG_unfold_fold.
Qed.
(* iris/base_logic/lib/own.v *)
Instance iRes_singleton_core_id γ a :
  CoreId a → CoreId (iRes_singleton γ a).
Proof.
  intros. apply discrete_fun_singleton_core_id, gmap_singleton_core_id.
  by rewrite /CoreId -cmra_morphism_pcore core_id.
Qed.
(* iris/base_logic/lib/own.v *)
Lemma later_internal_eq_iRes_singleton γ a r :
  ▷ (r ≡ iRes_singleton γ a) ⊢@{iPropI Σ}
  ◇ ∃ b r', r ≡ iRes_singleton γ b ⋅ r' ∧ ▷ (a ≡ b).
Proof.
  assert (NonExpansive (λ r : iResUR Σ, r (inG_id i) !! γ)).
  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id i)). }
  rewrite (f_equivI (λ r : iResUR Σ, r (inG_id i) !! γ) r).
  rewrite {1}/iRes_singleton discrete_fun_lookup_singleton lookup_singleton_eq.
  rewrite option_equivI. case Hb: (r (inG_id _) !! γ)=> [b|]; last first.
  { by rewrite /bi_except_0 -or_intro_l. }
  rewrite -except_0_intro.
  rewrite -(exist_intro (cmra_transport (eq_sym inG_prf) (inG_fold b))).
  rewrite -(exist_intro (discrete_fun_insert (inG_id _) (delete γ (r (inG_id i))) r)).
  apply and_intro.
  - apply equiv_internal_eq. rewrite /iRes_singleton.
    rewrite cmra_transport_trans eq_trans_sym_inv_l /=.
    intros i'. rewrite discrete_fun_lookup_op.
    destruct (decide (i' = inG_id i)) as [->|?].
    + rewrite discrete_fun_lookup_insert discrete_fun_lookup_singleton.
      intros γ'. rewrite lookup_op. destruct (decide (γ' = γ)) as [->|?].
      * by rewrite lookup_singleton_eq lookup_delete_eq Hb inG_unfold_fold.
      * by rewrite lookup_singleton_ne // lookup_delete_ne // left_id.
    + rewrite discrete_fun_lookup_insert_ne //.
      by rewrite discrete_fun_lookup_singleton_ne // left_id.
  - apply later_mono. rewrite (f_equivI inG_fold) inG_fold_unfold.
    apply: (internal_eq_rewrite' _ _ (λ b, a ≡ cmra_transport (eq_sym inG_prf) b)%I);
      [solve_proper|apply internal_eq_sym|].
    rewrite cmra_transport_trans eq_trans_sym_inv_r /=. apply internal_eq_refl.
Qed.
(* iris/base_logic/lib/own.v *)
(* ** Properties of [own] *)
Instance own_ne γ : NonExpansive (@own Σ A _ γ).
Proof. rewrite !own_eq. solve_proper. Qed.
(* iris/base_logic/lib/own.v *)
Instance own_proper γ :
  Proper ((≡) ==> (⊣⊢)) (@own Σ A _ γ)
:= ne_proper _.
(* iris/base_logic/lib/own.v *)
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.
(* iris/base_logic/lib/own.v *)
Lemma own_mono γ a1 a2 : a2 ≼ a1 → own γ a1 ⊢ own γ a2.
Proof. move=> [c ->]. by rewrite own_op sep_elim_l. Qed.
(* iris/base_logic/lib/own.v *)
Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (@own Σ A _ γ).
Proof. intros a1 a2. apply own_mono. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_valid γ a : own γ a ⊢ ✓ a.
Proof. by rewrite !own_eq /own_def ownM_valid iRes_singleton_validI. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_valid_2 γ a1 a2 : own γ a1 -∗ own γ a2 -∗ ✓ (a1 ⋅ a2).
Proof. apply entails_wand, wand_intro_r. by rewrite -own_op own_valid. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
Proof. apply entails_wand. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_valid_r γ a : own γ a ⊢ own γ a ∗ ✓ a.
Proof. apply: bi.persistent_entails_r. apply own_valid. Qed.
(* iris/base_logic/lib/own.v *)
Lemma own_valid_l γ a : own γ a ⊢ ✓ a ∗ own γ a.
Proof. by rewrite comm -own_valid_r. Qed.
(* iris/base_logic/lib/own.v *)
Instance own_timeless γ a : Discrete a → Timeless (own γ a).
Proof. rewrite !own_eq /own_def. apply _. Qed.
(* iris/base_logic/lib/own.v *)
Instance own_core_persistent γ a : CoreId a → Persistent (own γ a).
Proof. rewrite !own_eq /own_def; apply _. Qed.
(* iris/base_logic/lib/own.v *)
Lemma later_own γ a : ▷ own γ a ⊢ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b).
Proof.
  rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
  assert (NonExpansive (λ r : iResUR Σ, r (inG_id i) !! γ)).
  { intros n r1 r2 Hr. f_equiv. by specialize (Hr (inG_id i)). }
  rewrite internal_eq_sym later_internal_eq_iRes_singleton.
  rewrite (except_0_intro (uPred_ownM r)) -except_0_and. f_equiv.
  rewrite and_exist_l. f_equiv=> b. rewrite and_exist_l. apply exist_elim=> r'.
  rewrite assoc. apply and_mono_l.
  etrans; [|apply ownM_mono, (cmra_included_l _ r')].
  eapply (internal_eq_rewrite' _ _ uPred_ownM _ _); [apply and_elim_r|].
  apply and_elim_l.
Qed.