Commit 6b448546 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

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.
parent 0385975a
......@@ -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
......
......@@ -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.
(** 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.
(** 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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment