From 6b448546d61a9d8ec78f90c5fbb17b7631bd097b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 5 Nov 2020 10:49:41 +0100
Subject: [PATCH] Rename `mnat`/`mnat_auth` into `mono_nat`.

- This avoids confusion between `mnat` and `max_nat`. The `m` stands for `mono`.
- With `_mono` added, the `_auth` suffix in the algebra name no longer makes
  sense, so I removed it.
- This makes the names between the logic and the algebra-level library consistent.
- I also renamed `_frag` into `_lb` in the algebra-level library so as to make it
  consistent with the logic-level library.

Furthermore make the order of lemmas consistent and make the versions for the
fractions consistent.
---
 _CoqProject                    |   4 +-
 iris/algebra/lib/mnat_auth.v   |  89 -------------------------
 iris/algebra/lib/mono_nat.v    |  91 +++++++++++++++++++++++++
 iris/base_logic/lib/mnat.v     | 116 --------------------------------
 iris/base_logic/lib/mono_nat.v | 118 +++++++++++++++++++++++++++++++++
 5 files changed, 211 insertions(+), 207 deletions(-)
 delete mode 100644 iris/algebra/lib/mnat_auth.v
 create mode 100644 iris/algebra/lib/mono_nat.v
 delete mode 100644 iris/base_logic/lib/mnat.v
 create mode 100644 iris/base_logic/lib/mono_nat.v

diff --git a/_CoqProject b/_CoqProject
index ecff6175e..4e671b518 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -49,7 +49,7 @@ iris/algebra/lib/frac_auth.v
 iris/algebra/lib/ufrac_auth.v
 iris/algebra/lib/frac_agree.v
 iris/algebra/lib/gmap_view.v
-iris/algebra/lib/mnat_auth.v
+iris/algebra/lib/mono_nat.v
 iris/si_logic/siprop.v
 iris/si_logic/bi.v
 iris/bi/notation.v
@@ -98,7 +98,7 @@ iris/base_logic/lib/gen_inv_heap.v
 iris/base_logic/lib/fancy_updates_from_vs.v
 iris/base_logic/lib/proph_map.v
 iris/base_logic/lib/ghost_var.v
-iris/base_logic/lib/mnat.v
+iris/base_logic/lib/mono_nat.v
 iris/program_logic/adequacy.v
 iris/program_logic/lifting.v
 iris/program_logic/weakestpre.v
diff --git a/iris/algebra/lib/mnat_auth.v b/iris/algebra/lib/mnat_auth.v
deleted file mode 100644
index 351fa0a2f..000000000
--- a/iris/algebra/lib/mnat_auth.v
+++ /dev/null
@@ -1,89 +0,0 @@
-From iris.algebra Require Export auth.
-From iris.algebra Require Import numbers updates.
-From iris.prelude Require Import options.
-
-(** Authoritative CMRA for [max_nat]. The authoritative element is a
-monotonically increasing [nat], while a fragment is a lower bound. *)
-
-Definition mnat_auth   := auth max_natUR.
-Definition mnat_authR  := authR max_natUR.
-Definition mnat_authUR := authUR max_natUR.
-
-(** [mnat_auth_auth] is the authoritative element. The definition includes the
-fragment at the same value so that lemma [mnat_auth_included], which states that
-[mnat_auth_frag n ≼ mnat_auth_auth q n], does not require a frame-preserving
-update. *)
-Definition mnat_auth_auth (q : Qp) (n : nat) : mnat_auth :=
-  ●{q} MaxNat n ⋅ ◯ MaxNat n.
-Definition mnat_auth_frag (n : nat) : mnat_auth := â—¯ MaxNat n.
-
-Section mnat_auth.
-  Implicit Types (n : nat).
-
-  Global Instance mnat_auth_frag_core_id n : CoreId (mnat_auth_frag n).
-  Proof. apply _. Qed.
-
-  Lemma mnat_auth_auth_frac_op q1 q2 n :
-    mnat_auth_auth q1 n ⋅ mnat_auth_auth q2 n ≡ mnat_auth_auth (q1 + q2) n.
-  Proof.
-    rewrite /mnat_auth_auth auth_auth_frac_op.
-    rewrite (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
-    by rewrite -core_id_dup (comm _ (â—¯ _)).
-  Qed.
-
-  Lemma mnat_auth_frag_op n1 n2 :
-    mnat_auth_frag n1 â‹… mnat_auth_frag n2 = mnat_auth_frag (n1 `max` n2).
-  Proof. rewrite -auth_frag_op max_nat_op_max //. Qed.
-
-  (** rephrasing of [mnat_auth_frag_op] useful for weakening a fragment to a
-  smaller lower-bound *)
-  Lemma mnat_auth_frag_op_le_l n n' :
-    n' ≤ n →
-    mnat_auth_frag n = mnat_auth_frag n' â‹… mnat_auth_frag n.
-  Proof. intros. rewrite mnat_auth_frag_op Nat.max_r //. Qed.
-
-  Lemma mnat_auth_frac_op_valid q1 q2 n1 n2 :
-    ✓ (mnat_auth_auth q1 n1 ⋅ mnat_auth_auth q2 n2) ↔ (q1 + q2 ≤ 1)%Qp ∧ n1 = n2.
-  Proof.
-    rewrite /mnat_auth_auth (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
-    rewrite -auth_frag_op (comm _ (â—¯ _)) assoc. split.
-    - move=> /cmra_valid_op_l /auth_auth_frac_op_valid. naive_solver.
-    - intros [? ->]. rewrite -core_id_dup -auth_auth_frac_op.
-      by apply auth_both_frac_valid_discrete.
-  Qed.
-
-  Lemma mnat_auth_auth_op_valid n1 n2 :
-    ✓ (mnat_auth_auth 1 n1 ⋅ mnat_auth_auth 1 n2) ↔ False.
-  Proof. rewrite mnat_auth_frac_op_valid. naive_solver. Qed.
-
-  Lemma mnat_auth_both_frac_valid q n m :
-    ✓ (mnat_auth_auth q n ⋅ mnat_auth_frag m) ↔ (q ≤ 1)%Qp ∧ m ≤ n.
-  Proof.
-    rewrite /mnat_auth_auth /mnat_auth_frag -assoc -auth_frag_op.
-    rewrite auth_both_frac_valid_discrete max_nat_included /=.
-    naive_solver lia.
-  Qed.
-
-  Lemma mnat_auth_both_valid n m :
-    ✓ (mnat_auth_auth 1 n ⋅ mnat_auth_frag m) ↔ m ≤ n.
-  Proof. rewrite mnat_auth_both_frac_valid. naive_solver. Qed.
-
-  Lemma mnat_auth_frag_mono n1 n2 : n1 ≤ n2 → mnat_auth_frag n1 ≼ mnat_auth_frag n2.
-  Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
-
-  Lemma mnat_auth_auth_valid n : ✓ mnat_auth_auth 1 n.
-  Proof. by apply auth_both_valid. Qed.
-
-  Lemma mnat_auth_included q n : mnat_auth_frag n ≼ mnat_auth_auth q n.
-  Proof. apply cmra_included_r. Qed.
-
-  Lemma mnat_auth_update n n' :
-    n ≤ n' →
-    mnat_auth_auth 1 n ~~> mnat_auth_auth 1 n'.
-  Proof.
-    intros. rewrite /mnat_auth_auth /mnat_auth_frag.
-    by apply auth_update, max_nat_local_update.
-  Qed.
-End mnat_auth.
-
-Typeclasses Opaque mnat_auth_auth mnat_auth_frag.
diff --git a/iris/algebra/lib/mono_nat.v b/iris/algebra/lib/mono_nat.v
new file mode 100644
index 000000000..7f6332109
--- /dev/null
+++ b/iris/algebra/lib/mono_nat.v
@@ -0,0 +1,91 @@
+From iris.algebra Require Export auth.
+From iris.algebra Require Import numbers updates.
+From iris.prelude Require Import options.
+
+(** Authoritative CMRA over [max_nat]. The authoritative element is a
+monotonically increasing [nat], while a fragment is a lower bound. *)
+
+Definition mono_nat   := auth max_natUR.
+Definition mono_natR  := authR max_natUR.
+Definition mono_natUR := authUR max_natUR.
+
+(** [mono_nat_auth] is the authoritative element. The definition includes the
+fragment at the same value so that lemma [mono_nat_included], which states that
+[mono_nat_lb n ≼ mono_nat_auth q n], does not require a frame-preserving
+update. *)
+Definition mono_nat_auth (q : Qp) (n : nat) : mono_nat :=
+  ●{q} MaxNat n ⋅ ◯ MaxNat n.
+Definition mono_nat_lb (n : nat) : mono_nat := â—¯ MaxNat n.
+
+Section mono_nat.
+  Implicit Types (n : nat).
+
+  Global Instance mono_nat_lb_core_id n : CoreId (mono_nat_lb n).
+  Proof. apply _. Qed.
+
+  Lemma mono_nat_auth_frac_op q1 q2 n :
+    mono_nat_auth q1 n ⋅ mono_nat_auth q2 n ≡ mono_nat_auth (q1 + q2) n.
+  Proof.
+    rewrite /mono_nat_auth auth_auth_frac_op.
+    rewrite (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
+    by rewrite -core_id_dup (comm _ (â—¯ _)).
+  Qed.
+
+  Lemma mono_nat_lb_op n1 n2 :
+    mono_nat_lb n1 â‹… mono_nat_lb n2 = mono_nat_lb (n1 `max` n2).
+  Proof. rewrite -auth_frag_op max_nat_op_max //. Qed.
+
+  (** rephrasing of [mono_nat_lb_op] useful for weakening a fragment to a
+  smaller lower-bound *)
+  Lemma mono_nat_lb_op_le_l n n' :
+    n' ≤ n →
+    mono_nat_lb n = mono_nat_lb n' â‹… mono_nat_lb n.
+  Proof. intros. rewrite mono_nat_lb_op Nat.max_r //. Qed.
+
+  Lemma mono_nat_auth_frac_valid q n : ✓ mono_nat_auth q n ↔ (q ≤ 1)%Qp.
+  Proof.
+    rewrite /mono_nat_auth auth_both_frac_valid_discrete /=. naive_solver.
+  Qed.
+  Lemma mono_nat_auth_valid n : ✓ mono_nat_auth 1 n.
+  Proof. by apply auth_both_valid. Qed.
+
+  Lemma mono_nat_auth_frac_op_valid q1 q2 n1 n2 :
+    ✓ (mono_nat_auth q1 n1 ⋅ mono_nat_auth q2 n2) ↔ (q1 + q2 ≤ 1)%Qp ∧ n1 = n2.
+  Proof.
+    rewrite /mono_nat_auth (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite -auth_frag_op (comm _ (â—¯ _)) assoc. split.
+    - move=> /cmra_valid_op_l /auth_auth_frac_op_valid. naive_solver.
+    - intros [? ->]. rewrite -core_id_dup -auth_auth_frac_op.
+      by apply auth_both_frac_valid_discrete.
+  Qed.
+  Lemma mono_nat_auth_op_valid n1 n2 :
+    ✓ (mono_nat_auth 1 n1 ⋅ mono_nat_auth 1 n2) ↔ False.
+  Proof. rewrite mono_nat_auth_frac_op_valid. naive_solver. Qed.
+
+  Lemma mono_nat_both_frac_valid q n m :
+    ✓ (mono_nat_auth q n ⋅ mono_nat_lb m) ↔ (q ≤ 1)%Qp ∧ m ≤ n.
+  Proof.
+    rewrite /mono_nat_auth /mono_nat_lb -assoc -auth_frag_op.
+    rewrite auth_both_frac_valid_discrete max_nat_included /=.
+    naive_solver lia.
+  Qed.
+  Lemma mono_nat_both_valid n m :
+    ✓ (mono_nat_auth 1 n ⋅ mono_nat_lb m) ↔ m ≤ n.
+  Proof. rewrite mono_nat_both_frac_valid. naive_solver. Qed.
+
+  Lemma mono_nat_lb_mono n1 n2 : n1 ≤ n2 → mono_nat_lb n1 ≼ mono_nat_lb n2.
+  Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
+
+  Lemma mono_nat_included q n : mono_nat_lb n ≼ mono_nat_auth q n.
+  Proof. apply cmra_included_r. Qed.
+
+  Lemma mono_nat_update n n' :
+    n ≤ n' →
+    mono_nat_auth 1 n ~~> mono_nat_auth 1 n'.
+  Proof.
+    intros. rewrite /mono_nat_auth /mono_nat_lb.
+    by apply auth_update, max_nat_local_update.
+  Qed.
+End mono_nat.
+
+Typeclasses Opaque mono_nat_auth mono_nat_lb.
diff --git a/iris/base_logic/lib/mnat.v b/iris/base_logic/lib/mnat.v
deleted file mode 100644
index b8f554888..000000000
--- a/iris/base_logic/lib/mnat.v
+++ /dev/null
@@ -1,116 +0,0 @@
-(** Ghost state for a monotonically increasing nat, wrapping the [mnat_authR]
-RA. Provides an authoritative proposition [mnat_own_auth γ q n] for the
-underlying number [n] and a persistent proposition [mnat_own_lb γ m] witnessing that
-the authoritative nat is at least m.
-
-The key rules are [mnat_own_lb_valid], which asserts that an auth at [n] and a
-lower-bound at [m] imply that [m ≤ n], and [mnat_update], which allows to
-increase the auth element. At any time the auth nat can be "snapshotted" with
-[mnat_get_lb] to produce a persistent lower-bound proposition. *)
-
-From iris.algebra.lib Require Import mnat_auth.
-From iris.bi.lib Require Import fractional.
-From iris.proofmode Require Import tactics.
-From iris.base_logic.lib Require Export own.
-From iris.prelude Require Import options.
-
-Class mnatG Σ :=
-  MnatG { mnatG_inG :> inG Σ mnat_authR; }.
-Definition mnatΣ : gFunctors := #[ GFunctor mnat_authR ].
-Instance subG_mnatΣ Σ : subG mnatΣ Σ → mnatG Σ.
-Proof. solve_inG. Qed.
-
-Definition mnat_own_auth_def `{!mnatG Σ} (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
-  own γ (mnat_auth_auth q n).
-Definition mnat_own_auth_aux : seal (@mnat_own_auth_def). Proof. by eexists. Qed.
-Definition mnat_own_auth := mnat_own_auth_aux.(unseal).
-Definition mnat_own_auth_eq : @mnat_own_auth = @mnat_own_auth_def := mnat_own_auth_aux.(seal_eq).
-Arguments mnat_own_auth {Σ _} γ q n.
-
-Definition mnat_own_lb_def `{!mnatG Σ} (γ : gname) (n : nat): iProp Σ :=
-  own γ (mnat_auth_frag n).
-Definition mnat_own_lb_aux : seal (@mnat_own_lb_def). Proof. by eexists. Qed.
-Definition mnat_own_lb := mnat_own_lb_aux.(unseal).
-Definition mnat_own_lb_eq : @mnat_own_lb = @mnat_own_lb_def := mnat_own_lb_aux.(seal_eq).
-Arguments mnat_own_lb {Σ _} γ n.
-
-Local Ltac unseal := rewrite
-  ?mnat_own_auth_eq /mnat_own_auth_def
-  ?mnat_own_lb_eq /mnat_own_lb_def.
-
-Section mnat.
-  Context `{!mnatG Σ}.
-  Implicit Types (n m : nat).
-
-  Global Instance mnat_own_auth_timeless γ q n : Timeless (mnat_own_auth γ q n).
-  Proof. unseal. apply _. Qed.
-  Global Instance mnat_own_lb_timeless γ n : Timeless (mnat_own_lb γ n).
-  Proof. unseal. apply _. Qed.
-  Global Instance mnat_own_lb_persistent γ n : Persistent (mnat_own_lb γ n).
-  Proof. unseal. apply _. Qed.
-
-  Global Instance mnat_own_auth_fractional γ n : Fractional (λ q, mnat_own_auth γ q n).
-  Proof. unseal. intros p q. rewrite -own_op mnat_auth_auth_frac_op //. Qed.
-
-  Global Instance mnat_own_auth_as_fractional γ q n :
-    AsFractional (mnat_own_auth γ q n) (λ q, mnat_own_auth γ q n) q.
-  Proof. split; [auto|apply _]. Qed.
-
-  Lemma mnat_own_auth_agree γ q1 q2 n1 n2 :
-    mnat_own_auth γ q1 n1 -∗ mnat_own_auth γ q2 n2 -∗ ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
-  Proof.
-    unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %?%mnat_auth_frac_op_valid; done.
-  Qed.
-
-  Lemma mnat_own_auth_exclusive γ n1 n2 :
-    mnat_own_auth γ 1 n1 -∗ mnat_own_auth γ 1 n2 -∗ False.
-  Proof.
-    unseal. iIntros "H1 H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[]%mnat_auth_auth_op_valid.
-  Qed.
-
-  Lemma mnat_own_lb_valid γ q n m :
-    mnat_own_auth γ q n -∗ mnat_own_lb γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
-  Proof.
-    unseal. iIntros "Hauth Hlb".
-    iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mnat_auth_both_frac_valid.
-    auto.
-  Qed.
-
-  (** The conclusion of this lemma is persistent; the proofmode will preserve the
-  [mnat_own_auth] in the premise as long as the conclusion is introduced to the
-  persistent context, for example with [iDestruct (mnat_get_lb with
-  "Hauth") as "#Hfrag"]. *)
-  Lemma mnat_get_lb γ q n :
-    mnat_own_auth γ q n -∗ mnat_own_lb γ n.
-  Proof. unseal. apply own_mono, mnat_auth_included. Qed.
-
-  Lemma mnat_own_lb_le γ n n' :
-    n' ≤ n →
-    mnat_own_lb γ n -∗ mnat_own_lb γ n'.
-  Proof. unseal. intros. by apply own_mono, mnat_auth_frag_mono. Qed.
-
-  Lemma mnat_alloc n :
-    ⊢ |==> ∃ γ, mnat_own_auth γ 1 n ∗ mnat_own_lb γ n.
-  Proof.
-    unseal.
-    iMod (own_alloc (mnat_auth_auth 1 n ⋅ mnat_auth_frag n)) as (γ) "[??]".
-    { apply mnat_auth_both_valid; auto. }
-    auto with iFrame.
-  Qed.
-
-  Lemma mnat_update n' γ n :
-    n ≤ n' →
-    mnat_own_auth γ 1 n ==∗ mnat_own_auth γ 1 n'.
-  Proof. unseal. intros. by apply own_update, mnat_auth_update. Qed.
-
-  Lemma mnat_update_with_lb γ n n' :
-    n ≤ n' →
-    mnat_own_auth γ 1 n ==∗ mnat_own_auth γ 1 n' ∗ mnat_own_lb γ n'.
-  Proof.
-    iIntros (Hlb) "Hauth".
-    iMod (mnat_update n' with "Hauth") as "Hauth"; auto.
-    iDestruct (mnat_get_lb with "Hauth") as "#Hlb"; auto.
-  Qed.
-End mnat.
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
new file mode 100644
index 000000000..7a725a90a
--- /dev/null
+++ b/iris/base_logic/lib/mono_nat.v
@@ -0,0 +1,118 @@
+(** Ghost state for a monotonically increasing nat, wrapping the [mono_natR]
+RA. Provides an authoritative proposition [mono_nat_auth_own γ q n] for the
+underlying number [n] and a persistent proposition [mono_nat_lb_own γ m]
+witnessing that the authoritative nat is at least m.
+
+The key rules are [mono_nat_lb_own_valid], which asserts that an auth at [n] and
+a lower-bound at [m] imply that [m ≤ n], and [mono_nat_update], which allows to
+increase the auth element. At any time the auth nat can be "snapshotted" with
+[mono_nat_get_lb] to produce a persistent lower-bound proposition. *)
+From iris.proofmode Require Import tactics.
+From iris.algebra.lib Require Import mono_nat.
+From iris.bi.lib Require Import fractional.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Import options.
+
+Class mono_natG Σ :=
+  MonoNatG { mono_natG_inG :> inG Σ mono_natR; }.
+Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
+Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
+Proof. solve_inG. Qed.
+
+Definition mono_nat_auth_own_def `{!mono_natG Σ}
+    (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
+  own γ (mono_nat_auth q n).
+Definition mono_nat_auth_own_aux : seal (@mono_nat_auth_own_def). Proof. by eexists. Qed.
+Definition mono_nat_auth_own := mono_nat_auth_own_aux.(unseal).
+Definition mono_nat_auth_own_eq :
+  @mono_nat_auth_own = @mono_nat_auth_own_def := mono_nat_auth_own_aux.(seal_eq).
+Arguments mono_nat_auth_own {Σ _} γ q n.
+
+Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
+  own γ (mono_nat_lb n).
+Definition mono_nat_lb_own_aux : seal (@mono_nat_lb_own_def). Proof. by eexists. Qed.
+Definition mono_nat_lb_own := mono_nat_lb_own_aux.(unseal).
+Definition mono_nat_lb_own_eq :
+  @mono_nat_lb_own = @mono_nat_lb_own_def := mono_nat_lb_own_aux.(seal_eq).
+Arguments mono_nat_lb_own {Σ _} γ n.
+
+Local Ltac unseal := rewrite
+  ?mono_nat_auth_own_eq /mono_nat_auth_own_def
+  ?mono_nat_lb_own_eq /mono_nat_lb_own_def.
+
+Section mono_nat.
+  Context `{!mono_natG Σ}.
+  Implicit Types (n m : nat).
+
+  Global Instance mono_nat_auth_own_timeless γ q n : Timeless (mono_nat_auth_own γ q n).
+  Proof. unseal. apply _. Qed.
+  Global Instance mono_nat_lb_own_timeless γ n : Timeless (mono_nat_lb_own γ n).
+  Proof. unseal. apply _. Qed.
+  Global Instance mono_nat_lb_own_persistent γ n : Persistent (mono_nat_lb_own γ n).
+  Proof. unseal. apply _. Qed.
+
+  Global Instance mono_nat_auth_own_fractional γ n :
+    Fractional (λ q, mono_nat_auth_own γ q n).
+  Proof. unseal. intros p q. rewrite -own_op mono_nat_auth_frac_op //. Qed.
+  Global Instance mono_nat_auth_own_as_fractional γ q n :
+    AsFractional (mono_nat_auth_own γ q n) (λ q, mono_nat_auth_own γ q n) q.
+  Proof. split; [auto|apply _]. Qed.
+
+  Lemma mono_nat_auth_own_agree γ q1 q2 n1 n2 :
+    mono_nat_auth_own γ q1 n1 -∗
+    mono_nat_auth_own γ q2 n2 -∗
+    ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
+  Proof.
+    unseal. iIntros "H1 H2".
+    iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_frac_op_valid; done.
+  Qed.
+  Lemma mono_nat_auth_own_exclusive γ n1 n2 :
+    mono_nat_auth_own γ 1 n1 -∗ mono_nat_auth_own γ 1 n2 -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    by iDestruct (mono_nat_auth_own_agree with "H1 H2") as %[[] _].
+  Qed.
+
+  Lemma mono_nat_lb_own_valid γ q n m :
+    mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
+  Proof.
+    unseal. iIntros "Hauth Hlb".
+    iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mono_nat_both_frac_valid.
+    auto.
+  Qed.
+
+  (** 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 γ q n :
+    mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ n.
+  Proof. unseal. apply own_mono, mono_nat_included. Qed.
+
+  Lemma mono_nat_lb_own_le γ n n' :
+    n' ≤ n →
+    mono_nat_lb_own γ n -∗ mono_nat_lb_own γ n'.
+  Proof. unseal. intros. by apply own_mono, mono_nat_lb_mono. Qed.
+
+  Lemma mono_nat_own_alloc n :
+    ⊢ |==> ∃ γ, mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
+  Proof.
+    unseal. iMod (own_alloc (mono_nat_auth 1 n ⋅ mono_nat_lb n)) as (γ) "[??]".
+    { apply mono_nat_both_valid; auto. }
+    auto with iFrame.
+  Qed.
+
+  Lemma mono_nat_own_update n' γ n :
+    n ≤ n' →
+    mono_nat_auth_own γ 1 n ==∗ mono_nat_auth_own γ 1 n'.
+  Proof. unseal. intros. by apply own_update, mono_nat_update. Qed.
+
+  Lemma mono_nat_own_update_with_lb γ n n' :
+    n ≤ n' →
+    mono_nat_auth_own γ 1 n ==∗ mono_nat_auth_own γ 1 n' ∗ mono_nat_lb_own γ n'.
+  Proof.
+    iIntros (Hlb) "Hauth".
+    iMod (mono_nat_own_update n' with "Hauth") as "Hauth"; auto.
+    iDestruct (mono_nat_lb_own_get with "Hauth") as "#Hlb"; auto.
+  Qed.
+End mono_nat.
-- 
GitLab