Merge branch 'robbert/mnat_tweaks' into 'master'

Rename `mnat`/`mnat_auth` into `mono_nat`.

See merge request iris/iris!572

CHANGELOG.md

@@ -41,21 +41,23 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   `auth_auth_valid*`, `auth_frag_valid*`, or `auth_both_valid*` instead.
 * Rename `auth_update_core_id` into `auth_update_frac_alloc`.
 * Add the camera of discardable fractions `dfrac`. This is a generalization of
-  the normal fractional camera. See `theories/algebra/dfrac.v` for further information.
+  the normal fractional camera.
+  See [algebra.dfrac](iris/algebra/dfrac.v) for further information.
 * Rename `cmra_monotone_valid` into `cmra_morphism_valid` (this rename was
   forgotten in !56).
 * Add `gmap_view`, a camera providing a "view of a `gmap`". The authoritative
   element is any `gmap`; the fragment provides fractional ownership of a single
   key, including support for persistent read-only ownership through `dfrac`.
-  See `theories/algebra/lib/gmap_view.v` for further information.
+  See [algebra.lib.gmap_view](iris/algebra/lib/gmap_view.v) for further information.
   NOTE: The API surface for `gmap_view` is experimental and subject to change.
 * Move the `*_validI` and `*_equivI` lemmas to a new module, `base_logic.algebra`.
   That module is exported by `base_logic.base_logic` so it should usually be
   available everywhere without further changes.
 * The authoritative fragment `✓ (◯ b : auth A)` is no longer definitionally
   equal to `✓ b`.
-* Add `mnat_auth`, a wrapper for `auth max_nat`. The result is an authoritative
+* Add `mono_nat`, a wrapper for `auth max_nat`. The result is an authoritative
   `nat` where a fragment is a lower bound whose ownership is persistent.
+  See [algebra.lib.mono_nat](iris/algebra/lib/mono_nat.v) for further information.
 * Change `*_valid` lemma statements involving fractions to use `Qp` addition and
   inequality instead of RA composition and validity (also in `base_logic` and
   the higher layers).
@@ -123,9 +125,9 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   `uPred.discrete_fun_validI` to the new `base_logic.algebra` module. That
   module is exported by `base_logic.base_logic` so these names are now usually
   available everywhere, and no longer inside the `uPred` module.
-* Add an `mnat` library on top of `mnat_auth` that supports ghost state which is
-  an authoritative, monotonically-increasing `nat` with a proposition giving a
-  persistent lower bound. See `base_logic.lib.mnat` for further details.
+* Define a ghost state library on top of the `mono_nat` resource algebra.
+  See [base_logic.lib.mono_nat](iris/base_logic/lib/mono_nat.v) for further
+  information.
 * Remove the `gen_heap` notations `l ↦ -` and `l ↦{q} -`. They were barely used
   and looked very confusing in context: `l ↦ - ∗ P` looks like a magic wand.
 * Change `gen_inv_heap` notation `l ↦□ I` to `l ↦_I □`, so that `↦□` can be used

_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

iris/algebra/lib/mnat_auth.v → iris/algebra/lib/mono_nat.v

@@ -2,88 +2,90 @@ 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
+(** Authoritative CMRA over [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.
+Definition mono_nat   := auth max_natUR.
+Definition mono_natR  := authR max_natUR.
+Definition mono_natUR := 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
+(** [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 mnat_auth_auth (q : Qp) (n : nat) : mnat_auth :=
+Definition mono_nat_auth (q : Qp) (n : nat) : mono_nat :=
   ●{q} MaxNat n ⋅ ◯ MaxNat n.
-Definition mnat_auth_frag (n : nat) : mnat_auth := ◯ MaxNat n.
+Definition mono_nat_lb (n : nat) : mono_nat := ◯ MaxNat n.
 
-Section mnat_auth.
+Section mono_nat.
   Implicit Types (n : nat).
 
-  Global Instance mnat_auth_frag_core_id n : CoreId (mnat_auth_frag n).
+  Global Instance mono_nat_lb_core_id n : CoreId (mono_nat_lb 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.
+  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 /mnat_auth_auth auth_auth_frac_op.
+    rewrite /mono_nat_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).
+  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 [mnat_auth_frag_op] useful for weakening a fragment to a
+  (** rephrasing of [mono_nat_lb_op] useful for weakening a fragment to a
   smaller lower-bound *)
-  Lemma mnat_auth_frag_op_le_l n n' :
+  Lemma mono_nat_lb_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.
+    mono_nat_lb n = mono_nat_lb n' ⋅ mono_nat_lb n.
+  Proof. intros. rewrite mono_nat_lb_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.
+  Lemma mono_nat_auth_frac_valid q n : ✓ mono_nat_auth q n ↔ (q ≤ 1)%Qp.
   Proof.
-    rewrite /mnat_auth_auth (comm _ (●{q2} _)) -!assoc (assoc _ (◯ _)).
+    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 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.
+  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 /mnat_auth_auth /mnat_auth_frag -assoc -auth_frag_op.
+    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 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.
+  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 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.
+  Lemma mono_nat_included q n : mono_nat_lb n ≼ mono_nat_auth q n.
   Proof. apply cmra_included_r. Qed.
 
-  Lemma mnat_auth_update n n' :
+  Lemma mono_nat_update n n' :
     n ≤ n' →
-    mnat_auth_auth 1 n ~~> mnat_auth_auth 1 n'.
+    mono_nat_auth 1 n ~~> mono_nat_auth 1 n'.
   Proof.
-    intros. rewrite /mnat_auth_auth /mnat_auth_frag.
+    intros. rewrite /mono_nat_auth /mono_nat_lb.
     by apply auth_update, max_nat_local_update.
   Qed.
-End mnat_auth.
+End mono_nat.
 
-Typeclasses Opaque mnat_auth_auth mnat_auth_frag.
+Typeclasses Opaque mono_nat_auth mono_nat_lb.

iris/base_logic/lib/mnat.v

-(** 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.

iris/base_logic/lib/mono_nat.v

+(** 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' ∗ mono_nat_lb_own γ n'.
+  Proof.
+    iIntros (?) "Hauth".
+    iAssert (mono_nat_auth_own γ 1 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.
+End mono_nat.