phanerozoic/Coq-Iris huggingface dataset:
(* iris/base_logic/lib/later_credits.v *)
Definition le_upd_pre `{!lcGS hlc Σ} (P le_upd : iProp Σ) : iProp Σ
:=
    ∀ n, lc_supply n ==∗
      (** Case 1: Generalization of except-0 [◇], needed for proving the rule
      [le_upd_keep]. There we obtain [▷^n ◇ P] for a timeless [P], and need to
      eliminate [n] laters and one except-0, which can be done by having a
      disjunct [▷^(S n) False] in the goal. *)
      ▷^(S n) False ∨
      (** Case 2: No credits are spent. *)
      (lc_supply n ∗ P) ∨
      (** Case 3: Eliminate a later by decreasing the credit supply (which
      means at least one credit needs to be spent). This case is impossible if
      later credits are disabled ([HasNoLc]), because [m < 0] is false. *)
      (∃ m, ⌜m < n⌝ ∗ lc_supply m ∗ ▷ le_upd).
(* iris/base_logic/lib/later_credits.v *)
Instance le_upd_pre_contractive `{!lcGS hlc Σ} P : Contractive (le_upd_pre P).
Proof. solve_contractive. Qed.
(* iris/base_logic/lib/later_credits.v *)
Definition le_upd_def `{!lcGS hlc Σ} (P : iProp Σ) : iProp Σ
:=
    fixpoint (le_upd_pre P).
(* iris/base_logic/lib/later_credits.v *)
Definition le_upd_aux : seal (@le_upd_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/later_credits.v *)
Definition le_upd
:= le_upd_aux.(unseal).
(* iris/base_logic/lib/later_credits.v *)
Definition le_upd_unseal : @le_upd = @le_upd_def
:= le_upd_aux.(seal_eq).
(* iris/base_logic/lib/later_credits.v *)
Notation "'|==£>' P"
:= (le_upd P)
    (at level 20, P at level 200, format "|==£>  P") : bi_scope.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_unfold `{!lcGS hlc Σ} P :
    (|==£> P) ⊣⊢
    ∀ n, lc_supply n ==∗
         ▷^(S n) False ∨ (lc_supply n ∗ P) ∨ (∃ m, ⌜m < n⌝ ∗ lc_supply m ∗ ▷ |==£> P).
Proof.
    by rewrite le_upd_unseal
      /le_upd_def {1}(fixpoint_unfold (le_upd_pre P)) {1}/le_upd_pre.
  Qed.
(* iris/base_logic/lib/later_credits.v *)
(* If later credits are disabled, this lemma shows that [le_upd] is just the
  basic update + except-0 modality, i.e., fancy updates are like Iris 3.0. *)
Lemma le_upd_unfold_no_le `{!lcGS HasNoLc Σ} P : (|==£> P) ⊣⊢ |==> ◇ P.
Proof.
    rewrite le_upd_unfold. setoid_rewrite lc_supply_no_lc. iSplit.
    - iIntros "H".
      iMod ("H" $! 0 with "[//]") as "[>[]|[[_ ?]|(%m&%Hm&_)]]"; auto with lia.
    - iIntros "H %n ->". rewrite /bi_except_0. iMod "H" as "[?|?]"; auto.
  Qed.
(* iris/base_logic/lib/later_credits.v *)
(* Rules for the later elimination update *)
Instance le_upd_ne : NonExpansive le_upd.
Proof.
      intros n; induction (lt_wf n) as [n _ IH].
      intros P1 P2 HP. rewrite (le_upd_unfold P1) (le_upd_unfold P2).
      do 10 (done || f_equiv). f_contractive. by eapply IH, dist_lt.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma bupd_le_upd P : (|==> P) ⊢ |==£> P.
Proof.
      rewrite le_upd_unfold; iIntros "HP" (n) "Hpr".
      iMod "HP" as "HP". auto with iFrame.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma except_0_le_upd P : ◇ (|==£> P) ⊢ |==£> P.
Proof.
      rewrite /bi_except_0. iIntros "[HFalse|$]".
      iApply le_upd_unfold; iIntros (n) "_ !>". iLeft. by iNext.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_bind P Q : (P -∗ |==£> Q) -∗ (|==£> P) -∗ |==£> Q.
Proof.
      iLöb as "IH". iIntros "HPQ".
      iEval (rewrite (le_upd_unfold P) (le_upd_unfold Q)).
      iIntros "HP" (n) "Hpr".
      iMod ("HP" with "Hpr") as "[?|[[Hpr HP]|HP]]"; first by auto.
      - iEval (rewrite le_upd_unfold) in "HPQ". by iApply ("HPQ" with "HP").
      - iModIntro. do 2 iRight. iDestruct "HP" as (n') "($ & $ & HP)".
        iNext. by iApply ("IH" with "HPQ HP").
    Qed.
(* iris/base_logic/lib/later_credits.v *)
(* Derived lemmas *)
Lemma le_upd_intro P : P ⊢ |==£> P.
Proof. iIntros "H". by iApply bupd_le_upd. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_mono P Q : (P ⊢ Q) → (|==£> P) ⊢ |==£> Q.
Proof.
      intros Hent. iApply le_upd_bind.
      iIntros "P"; iApply le_upd_intro; by iApply Hent.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance le_upd_mono' : Proper ((⊢) ==> (⊢)) le_upd.
Proof. intros P Q PQ; by apply le_upd_mono. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance le_upd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) le_upd.
Proof. intros P Q PQ; by apply le_upd_mono. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance le_upd_equiv_proper : Proper ((≡) ==> (≡)) le_upd.
Proof. apply ne_proper. apply _. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_trans P : (|==£> |==£> P) ⊢ |==£> P.
Proof.
      iIntros "HP". iApply le_upd_bind; eauto.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_frame_r P R : (|==£> P) ∗ R ⊢ |==£> P ∗ R.
Proof.
      iIntros "[Hupd R]". iApply (le_upd_bind with "[R]"); last done.
      iIntros "P". iApply le_upd_intro. by iFrame.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_frame_l P R : R ∗ (|==£> P) ⊢ |==£> R ∗ P.
Proof. rewrite comm le_upd_frame_r comm //. Qed.
(* iris/base_logic/lib/later_credits.v *)
(* We do not use this to build an instance, because it would conflict
       with the basic updates. *)
Lemma bi_bupd_mixin_le_upd : BiBUpdMixin (iPropI Σ) le_upd.
Proof.
      split; rewrite /bupd.
      - apply _.
      - apply le_upd_intro.
      - apply le_upd_mono.
      - apply le_upd_trans.
      - apply le_upd_frame_r.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
(* Proof mode class instances internally needed for people defining their
    [fupd] with [le_upd]. *)
Instance elim_bupd_le_upd p P Q :
      ElimModal True p false (|==> P) P (|==£> Q) (|==£> Q).
Proof.
      rewrite /ElimModal bi.intuitionistically_if_elim //=.
      rewrite bupd_le_upd. iIntros "_ [HP HPQ]".
      iApply (le_upd_bind with "HPQ HP").
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance from_assumption_le_upd p P Q :
      FromAssumption p P Q → KnownRFromAssumption p P (|==£> Q).
Proof.
      rewrite /KnownRFromAssumption /FromAssumption=>->. apply le_upd_intro.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance from_pure_le_upd a P φ :
      FromPure a P φ → FromPure a (|==£> P) φ.
Proof. rewrite /FromPure=> <-. apply le_upd_intro. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance is_except_0_le_upd P : IsExcept0 (le_upd P).
Proof. apply except_0_le_upd. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance from_modal_le_upd P :
      FromModal True modality_id (|==£> P) (|==£> P) P.
Proof. by rewrite /FromModal /= -le_upd_intro. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance elim_modal_le_upd p P Q :
      ElimModal True p false (|==£> P) P (|==£> Q) (|==£> Q).
Proof.
      by rewrite /ElimModal
        intuitionistically_if_elim le_upd_frame_r wand_elim_r le_upd_trans.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance frame_le_upd p R P Q :
      Frame p R P Q → Frame p R (|==£> P) (|==£> Q).
Proof. rewrite /Frame=><-. by rewrite le_upd_frame_l. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_le_upd_elim_later `{!lcGS HasLc Σ} P : £ 1 -∗ (▷ P) -∗ |==£> P.
Proof.
    iIntros "Hc Hl". iApply le_upd_unfold. iIntros (n) "Hs". do 2 iRight.
    iDestruct (lc_supply_bound with "Hs Hc") as "%".
    replace n with (1 + (n - 1)) by lia.
    iMod (lc_decrease_supply with "Hs Hc") as "$"; iModIntro.
    iSplit; [by eauto with lia|]. iNext. by iApply bupd_le_upd.
  Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_le_upd_add_later `{!lcGS HasLc Σ} P : £ 1 -∗ ▷ (|==£> P) -∗ |==£> P.
Proof.
    iIntros "H£ H". iApply le_upd_trans.
    by iApply (lc_le_upd_elim_later with "H£").
  Qed.
(* iris/base_logic/lib/later_credits.v *)
(* You probably do NOT want to use these lemmas; use [lc_soundness] if you
  want to actually use [le_upd]! *)
Lemma lc_alloc `{!lcGpreS Σ} n :
    ⊢ |==> ∃ _ : lcGS HasLc Σ, lc_supply n ∗ £ n.
Proof.
    rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.
    iMod (own_alloc (● n ⋅ ◯ n)) as (γLC) "[H● H◯]";
      first (apply auth_both_valid; split; done).
    iModIntro. iExists (LcGS HasLc _ _ γLC). iFrame.
  Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_alloc_no_lc `{!lcGpreS Σ} n :
    ⊢ ∃ _ : lcGS HasNoLc Σ, lc_supply 0 ∗ £ n.
Proof.
    rewrite lc_unseal /lc_def lc_supply_unseal /lc_supply_def.
    (* Use [fresh] to pick *any* ghost name (it is unused anyway). *)
    by iExists (LcGS HasNoLc _ _ (fresh (∅ : gset gname))).
  Qed.
(* iris/base_logic/lib/later_credits.v *)
(* The later-elimination finally modality [le_upd_finally] is used internally
  in the finally modality for fancy updates ([fupd_finally]). It should not be
  used directly by end-users. See the file [fancy_updates] for documentation how
  to prove soundness/adequacy results using the user-facing finally modality.

  Compared to the later-elimination modality [le_upd] itself, this modality
  only consumes the supply [lc_supply], but does not give it back. This change
  allows us to prove the rules [le_upd_finally_later], [le_upd_finally_keep],
  and [le_upd_finally_forall], which cannot be proven for [le_upd]. For instance,
  to prove [le_upd_finally_forall] the goal is [▷^m ◇ ■ ∀ x, Φ x] where we can
  just commute out the [∀]. Such a proof does not work for a corresponding lemma
  for [le_upd] because we cannot commute out the [∀].

  Due to the plain modality [■], we can perform basic updates around
  [le_upd_finally] (we have [(|==> ■ P) ⊣⊢ ■ P]). This fact is exposed by the
  rule [le_upd_le_upd_finally] combined with the rule [bupd_le_upd]. *)
Definition le_upd_finally_def `{!lcGS hlc Σ} (P : iProp Σ) : iProp Σ
:=
    ∀ m, lc_supply m -∗ ▷^m ◇ ■ P.
(* iris/base_logic/lib/later_credits.v *)
Definition le_upd_finally_aux : seal (@le_upd_finally_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/later_credits.v *)
Definition le_upd_finally
:= le_upd_finally_aux.(unseal).
(* iris/base_logic/lib/later_credits.v *)
Definition le_upd_finally_unseal :
    @le_upd_finally = @le_upd_finally_def
:= le_upd_finally_aux.(seal_eq).
(* iris/base_logic/lib/later_credits.v *)
Notation "|==£|> Q"
:= (le_upd_finally Q) (at level 20, Q at level 200,
     format "'[  ' |==£|>  '/' Q ']'") : bi_scope.
(* iris/base_logic/lib/later_credits.v *)
Instance le_upd_finally_ne : NonExpansive le_upd_finally.
Proof. rewrite le_upd_finally_unseal. solve_proper. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_finally_mono P Q : (P ⊢ Q) → (|==£|> P) ⊢ (|==£|> Q).
Proof. rewrite le_upd_finally_unseal. solve_proper. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_finally_intro P : ■ P ⊢ |==£|> P.
Proof. rewrite le_upd_finally_unseal. iIntros "#HP %m _ !> !>". done. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_le_upd_finally P : (|==£> |==£|> P) ⊢ |==£|> P.
Proof.
      rewrite le_upd_finally_unseal /le_upd_finally_def. iIntros "HP %m Hlc".
      iLöb as "IH" forall (m).
      iEval (rewrite le_upd_unfold) in "HP".
      iMod ("HP" with "Hlc") as "[HFalse|[[Hlc H]|(%m' & %Hm & Hlc & H)]]".
      { iNext. by iMod "HFalse". }
      { by iApply "H". }
      replace m with (S ((m - m' - 1) + m')) by lia. rewrite /= laterN_add.
      do 2 iNext. iApply ("IH" with "H Hlc").
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_finally_except_0 P : (|==£|> ◇ P) ⊢ |==£|> P.
Proof.
      rewrite le_upd_finally_unseal /le_upd_finally_def. iIntros "HP %m Hlc".
      iEval (rewrite -except_0_idemp except_0_plainly). by iApply "HP".
    Qed.
(* iris/base_logic/lib/later_credits.v *)
(* Commute a later out of the modality. This only works if the proposition
    below the later can be turned into an except-0 [◇]. *)
Lemma le_upd_finally_later P : ▷ (|==£|> P) ⊢ |==£|> ▷ ◇ P.
Proof.
      rewrite le_upd_finally_unseal /le_upd_finally_def. iIntros "H %m Hlc".
      iEval (rewrite -later_plainly -except_0_plainly
        -except_0_intro -laterN_later /=).
      iNext. by iApply "H".
    Qed.
(* iris/base_logic/lib/later_credits.v *)
(* Add a later credit by removing a later below the modality. This
    only works if the proposition below the later can be turned into an
    except-0 [◇]. *)
Lemma le_upd_finally_add_lc P : (£ 1 -∗ |==£|> P) ⊢ |==£|> ▷ ◇ P.
Proof.
      rewrite le_upd_finally_unseal. iIntros "H %m Hlc".
      rewrite -except_0_intro -later_plainly -except_0_plainly -laterN_later.
      destruct hlc.
      - iMod (later_credits.lc_increase_supply 1 with "Hlc") as "[Hlc H£]".
        iApply ("H" with "H£ Hlc").
      - iIntros "/= !>". iApply ("H" with "[] Hlc"). by iApply lc_no_lc.
    Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_finally_forall {A} (Φ : A → iProp Σ) :
      (∀ x, |==£|> Φ x) ⊢ |==£|> ∀ x, Φ x.
Proof.
      rewrite le_upd_finally_unseal.
      iIntros "H %m Hlc %x". iApply ("H" with "Hlc").
    Qed.
(* iris/base_logic/lib/later_credits.v *)
(* [iApply] this lemma to use your current context for proving a (timeless)
    assertion [P] *without* actually using up the context. You can then continue
    the proof in the second conjunct. *)
Lemma le_upd_keep P `{!TCOr (TCEq hlc HasNoLc) (Timeless P)} Q :
      (|==£|> P) ∧ (P -∗ |==£> Q) ⊢ |==£> Q.
Proof.
      iIntros "H". iApply le_upd_unfold; iIntros (n) "Hc".
      iAssert (▷^(S n) False ∨ ■ P)%I as "#[Hfalse|HP]"; [|by auto|].
      { iDestruct "H" as "[H _]". rewrite le_upd_finally_unseal.
        destruct select (TCOr _ _) as [->%TCEq_eq|?].
        - iDestruct (lc_supply_no_lc with "Hc") as %->; simpl.
          iApply ("H" with "Hc").
        - iApply (timeless_laterN _ (S n)). iSpecialize ("H" with "Hc").
          by iEval (rewrite except_0_into_later -laterN_later) in "H". }
      iDestruct "H" as "[_ H]". by iApply (le_upd_unfold with "(H [//])").
    Qed.
(* iris/base_logic/lib/later_credits.v *)
(* Since the modality is used only internally in the version for fancy
    updates, we do not provide instances of the proof mode classes. *)
Instance le_upd_finally_proper : Proper ((⊣⊢) ==> (⊣⊢)) le_upd_finally.
Proof. apply: ne_proper. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance le_upd_finally_mono' : Proper ((⊢) ==> (⊢)) le_upd_finally.
Proof. intros P Q. apply le_upd_finally_mono. Qed.
(* iris/base_logic/lib/later_credits.v *)
Instance le_upd_finally_flip_mono' :
      Proper (flip (⊢) ==> flip (⊢)) le_upd_finally.
Proof. intros P Q. apply le_upd_finally_mono. Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma le_upd_finally_soundness hlc `{!lcGpreS Σ} n P :
    (∀ `{!lcGS hlc Σ}, £ n ⊢ |==£|> P) → ⊢ P.
Proof.
    rewrite le_upd_finally_unseal. intros HP. destruct hlc.
    - apply (laterN_soundness _ (S n)).
      rewrite laterN_later -except_0_into_later -(plainly_elim P).
      iMod (lc_alloc n) as (Hc) "[Hlc H£]". iApply (HP with "H£ Hlc").
    - apply (laterN_soundness _ 1).
      iDestruct (lc_alloc_no_lc n) as (Hc) "[Hlc H£]".
      by iMod (HP with "H£ Hlc") as "H".
  Qed.
(* iris/base_logic/lib/later_credits.v *)
Lemma lc_soundness hlc `{!lcGpreS Σ} m (P : iProp Σ) `{!Plain P} :
    (∀ `{!lcGS hlc Σ}, £ m -∗ |==£> P) → ⊢ P.
Proof.
    intros H. apply (le_upd_finally_soundness hlc m); iIntros (?) "H£".
    iApply le_upd_le_upd_finally. iMod (H with "H£") as "HP"; iModIntro.
    iApply le_upd_finally_intro. by iApply plain_plainly.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Class mono_listG (A : Type) Σ
:=
  MonoListG { #[local] mono_list_inG :: inG Σ (mono_listR (leibnizO A)) }.
(* iris/base_logic/lib/mono_list.v *)
Definition mono_listΣ (A : Type) : gFunctors
:=
  #[GFunctor (mono_listR (leibnizO A))].
(* iris/base_logic/lib/mono_list.v *)
Instance subG_mono_listΣ {A Σ} :
  subG (mono_listΣ A) Σ → (mono_listG A) Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/mono_list.v *)
Definition mono_list_auth_own_def `{!mono_listG A Σ}
    (γ : gname) (dq : dfrac) (l : list A) : iProp Σ
:=
  own γ (●ML{dq} (l : listO (leibnizO A))).
(* iris/base_logic/lib/mono_list.v *)
Definition mono_list_auth_own_aux : seal (@mono_list_auth_own_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/mono_list.v *)
Definition mono_list_auth_own
:= mono_list_auth_own_aux.(unseal).
(* iris/base_logic/lib/mono_list.v *)
Definition mono_list_auth_own_unseal :
  @mono_list_auth_own = @mono_list_auth_own_def
:= mono_list_auth_own_aux.(seal_eq).
(* iris/base_logic/lib/mono_list.v *)
Definition mono_list_lb_own_def `{!mono_listG A Σ}
    (γ : gname) (l : list A) : iProp Σ
:=
  own γ (◯ML (l : listO (leibnizO A))).
(* iris/base_logic/lib/mono_list.v *)
Definition mono_list_lb_own_aux : seal (@mono_list_lb_own_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/mono_list.v *)
Definition mono_list_lb_own
:= mono_list_lb_own_aux.(unseal).
(* iris/base_logic/lib/mono_list.v *)
Definition mono_list_lb_own_unseal :
  @mono_list_lb_own = @mono_list_lb_own_def
:= mono_list_lb_own_aux.(seal_eq).
(* iris/base_logic/lib/mono_list.v *)
Definition mono_list_idx_own `{!mono_listG A Σ}
    (γ : gname) (i : nat) (a : A) : iProp Σ
:=
  ∃ l : list A, ⌜ l !! i = Some a ⌝ ∗ mono_list_lb_own γ l.
(* iris/base_logic/lib/mono_list.v *)
Notation "γ ↪●ML dq l"
:= (mono_list_auth_own γ dq l)
  (at level 20, dq custom dfrac at level 1,
   format "γ  ↪●ML dq  l").
(* iris/base_logic/lib/mono_list.v *)
Notation "γ ↪◯ML l"
:= (mono_list_lb_own γ l)
  (at level 20, l at level 20).
(* iris/base_logic/lib/mono_list.v *)
Notation "γ ↪◯ML[ i ] a "
:= (mono_list_idx_own γ i a)
  (at level 20, format "γ  ↪◯ML[ i ]  a") : bi_scope.
(* iris/base_logic/lib/mono_list.v *)
Ltac unseal
:= rewrite
  /mono_list_idx_own ?mono_list_auth_own_unseal /mono_list_auth_own_def
  ?mono_list_lb_own_unseal /mono_list_lb_own_def.
(* iris/base_logic/lib/mono_list.v *)
Instance mono_list_auth_own_timeless γ dq l : Timeless (γ ↪●ML{dq} l).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_list.v *)
Instance mono_list_auth_own_persistent γ l : Persistent (γ ↪●ML□ l).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_list.v *)
Instance mono_list_lb_own_timeless γ l : Timeless (γ ↪◯ML l).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_list.v *)
Instance mono_list_lb_own_persistent γ l : Persistent (γ ↪◯ML l).
Proof. unseal. apply _. Qed.
(* iris/base_logic/lib/mono_list.v *)
Instance mono_list_idx_own_timeless γ i a :
    Timeless (γ ↪◯ML[i] a)
:= _.
(* iris/base_logic/lib/mono_list.v *)
Instance mono_list_idx_own_persistent γ i a :
    Persistent (γ ↪◯ML[i] a)
:= _.
(* iris/base_logic/lib/mono_list.v *)
Instance mono_list_auth_own_fractional γ l :
    Fractional (λ q, γ ↪●ML{#q} l).
Proof. unseal. intros p q. by rewrite -own_op -mono_list_auth_dfrac_op. Qed.
(* iris/base_logic/lib/mono_list.v *)
Instance mono_list_auth_own_as_fractional γ q l :
    AsFractional (γ ↪●ML{#q} l) (λ q, γ ↪●ML{#q} l) q.
Proof. split; [auto|apply _]. Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_auth_own_agree γ dq1 dq2 l1 l2 :
    γ ↪●ML{dq1} l1 -∗ γ ↪●ML{dq2} l2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ l1 = l2⌝.
Proof.
    unseal. iIntros "H1 H2".
    by iCombine "H1 H2" gives %?%mono_list_auth_dfrac_op_valid_L.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_auth_own_exclusive γ l1 l2 :
    γ ↪●ML l1 -∗ γ ↪●ML l2 -∗ False.
Proof.
    iIntros "H1 H2".
    iDestruct (mono_list_auth_own_agree with "H1 H2") as %[]; done.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_auth_lb_own_valid γ dq l1 l2 :
    γ ↪●ML{dq} l1 -∗ γ ↪◯ML l2 -∗ ⌜✓ dq ∧ l2 `prefix_of` l1 ⌝.
Proof.
    unseal. iIntros "Hauth Hlb".
    by iCombine "Hauth Hlb" gives %?%mono_list_both_dfrac_valid_L.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_lb_own_valid γ l1 l2 :
    γ ↪◯ML l1 -∗
    γ ↪◯ML l2 -∗
    ⌜ l1 `prefix_of` l2 ∨ l2 `prefix_of` l1 ⌝.
Proof.
    unseal. iIntros "H1 H2".
    by iCombine "H1 H2" gives %?%mono_list_lb_op_valid_L.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_idx_agree γ i a1 a2 :
    γ ↪◯ML[i] a1 -∗ γ ↪◯ML[i] a2 -∗ ⌜ a1 = a2 ⌝.
Proof.
    iDestruct 1 as (l1 Hl1) "H1". iDestruct 1 as (l2 Hl2) "H2".
    iDestruct (mono_list_lb_own_valid with "H1 H2") as %Hpre.
    iPureIntro.
    destruct Hpre as [Hpre|Hpre]; eapply prefix_lookup_Some in Hpre; eauto; congruence.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_auth_idx_lookup γ dq l i a :
    γ ↪●ML{dq} l -∗ γ ↪◯ML[i] a -∗ ⌜ l !! i = Some a ⌝.
Proof.
    iIntros "Hauth". iDestruct 1 as (l1 Hl1) "Hl1".
    iDestruct (mono_list_auth_lb_own_valid with "Hauth Hl1") as %[_ Hpre].
    iPureIntro.
    eapply prefix_lookup_Some in Hpre; eauto; congruence.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_lb_own_get γ dq l :
    γ ↪●ML{dq} l ⊢ γ ↪◯ML l.
Proof. intros. unseal. by apply own_mono, mono_list_included. Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_lb_own_le {γ l} l' :
    l' `prefix_of` l →
    γ ↪◯ML l ⊢ γ ↪◯ML l'.
Proof. unseal. intros. by apply own_mono, mono_list_lb_mono. Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_lb_own_nil γ :
    ⊢ |==> γ ↪◯ML [].
Proof. unseal. iApply own_unit. Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_idx_own_get {γ l} i a :
    l !! i = Some a →
    γ ↪◯ML l -∗ γ ↪◯ML[i] a.
Proof. iIntros (Hli) "Hl". iExists l. by iFrame. Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_own_alloc l :
    ⊢ |==> ∃ γ, γ ↪●ML l ∗ γ ↪◯ML l.
Proof.
    unseal. setoid_rewrite <- own_op. by apply own_alloc, mono_list_both_valid_L.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_auth_own_update {γ l} l' :
    l `prefix_of` l' →
    γ ↪●ML l ==∗ γ ↪●ML l' ∗ γ ↪◯ML l'.
Proof.
    iIntros (?) "Hauth".
    iAssert (γ ↪●ML l') with "[> Hauth]" as "Hauth".
    { unseal. iApply (own_update with "Hauth"). by apply mono_list_update. }
    iModIntro. iSplit; [done|]. by iApply mono_list_lb_own_get.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_auth_own_update_app {γ l} l' :
    γ ↪●ML l ==∗
    γ ↪●ML (l ++ l') ∗ γ ↪◯ML (l ++ l').
Proof. by apply mono_list_auth_own_update, prefix_app_r. Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_auth_own_persist γ dq l :
    γ ↪●ML{dq} l ==∗ γ ↪●ML□ l.
Proof.
    unseal. iApply own_update. apply mono_list_auth_persist.
  Qed.
(* iris/base_logic/lib/mono_list.v *)
Lemma mono_list_auth_own_unpersist γ l :
    γ ↪●ML□ l ==∗ ∃ q, γ ↪●ML{#q} l.
Proof.
    unseal. iIntros "H".
    iMod (own_updateP with "H") as "H";
      first by apply mono_list_auth_unpersist.
    iDestruct "H" as (? (q&->)) "H".
    iIntros "!>". iExists q. done.
  Qed.
(* iris/base_logic/lib/mono_nat.v *)
Class mono_natG Σ
:=
  MonoNatG { #[local] mono_natG_inG :: inG Σ mono_natR; }.
(* iris/base_logic/lib/mono_nat.v *)
Definition mono_natΣ : gFunctors
:= #[ GFunctor mono_natR ].
(* iris/base_logic/lib/mono_nat.v *)
Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
Proof. solve_inG. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Definition mono_nat_auth_own_def `{!mono_natG Σ}
    (γ : gname) (dq : dfrac) (n : nat) : iProp Σ
:=
  own γ (●MN{dq} n).
(* iris/base_logic/lib/mono_nat.v *)
Definition mono_nat_auth_own_aux : seal (@mono_nat_auth_own_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Definition mono_nat_auth_own
:= mono_nat_auth_own_aux.(unseal).
(* iris/base_logic/lib/mono_nat.v *)
Definition mono_nat_auth_own_unseal :
  @mono_nat_auth_own = @mono_nat_auth_own_def
:= mono_nat_auth_own_aux.(seal_eq).
(* iris/base_logic/lib/mono_nat.v *)
Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ
:=
  own γ (◯MN n).
(* iris/base_logic/lib/mono_nat.v *)
Definition mono_nat_lb_own_aux : seal (@mono_nat_lb_own_def).
Proof. by eexists. Qed.
(* iris/base_logic/lib/mono_nat.v *)
Definition mono_nat_lb_own
:= mono_nat_lb_own_aux.(unseal).
(* iris/base_logic/lib/mono_nat.v *)
Definition mono_nat_lb_own_unseal :
  @mono_nat_lb_own = @mono_nat_lb_own_def
:= mono_nat_lb_own_aux.(seal_eq).
(* iris/base_logic/lib/mono_nat.v *)
Notation "γ ↪●MN dq n"
:= (mono_nat_auth_own γ dq n)
  (at level 20, dq custom dfrac at level 1,
   format "γ  ↪●MN dq  n").
(* iris/base_logic/lib/mono_nat.v *)
Notation "γ ↪◯MN n"
:= (mono_nat_lb_own γ n)
  (at level 20).
(* iris/base_logic/lib/mono_nat.v *)
(* Compatibility alias. Do not use for new code.
This will eventually be deprecated and removed. *)
Notation mono_nat_auth_own_frac γ q n
:=
  (mono_nat_auth_own γ (DfracOwn q) n) (only parsing).
(* iris/base_logic/lib/mono_nat.v *)
Ltac unseal
:= rewrite
  ?mono_nat_auth_own_unseal /mono_nat_auth_own_def
  ?mono_nat_lb_own_unseal /mono_nat_lb_own_def.