Commit ec624937 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/mono_nat' into 'master'

mono_nat algebra: add dfrac support and notation

See merge request iris/iris!759
parents 901016fc 230ff113
......@@ -23,6 +23,14 @@ lemma.
* Remove `view_auth_frac_op`, `auth_auth_frac_op`, `gmap_view_auth_frac_op`; the
corresponding `dfrac` lemmas can be used instead (together with `dfrac_op_own`
if needed).
* Equip `mono_nat` algebra with support for `dfrac`, make API more consistent,
and add notation for algebra elements. See `iris/algebra/lib/mono_nat.v` for
details. This affects some existing terms and lemmas:
- `mono_nat_auth` now takes a `dfrac`, but the recommendation is to port to the notation.
- `mono_nat_lb_op`: direction of equality is swapped.
- `mono_nat_auth_frac_op`, `mono_nat_auth_frac_op_valid`,
`mono_nat_auth_frac_valid`, `mono_nat_both_frac_valid`: use `dfrac` variant
**Changes in `bi`:**
......@@ -11,32 +11,42 @@ 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
[mono_nat_lb n ≼ mono_nat_auth dq 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_auth (dq : dfrac) (n : nat) : mono_nat :=
{dq} MaxNat n MaxNat n.
Definition mono_nat_lb (n : nat) : mono_nat := MaxNat n.
(** FIXME: Refactor these notations using custom entries once Coq bug #13654
has been fixed. *)
Notation "●MN{ dq } a" :=
(mono_nat_auth dq a) (at level 20, format "●MN{ dq } a").
Notation "●MN{# q } a" :=
(mono_nat_auth (DfracOwn q) a) (at level 20, format "●MN{# q } a").
Notation "●MN□ a" := (mono_nat_auth DfracDiscarded a) (at level 20, format "●MN□ a").
Notation "●MN a" := (mono_nat_auth (DfracOwn 1) a) (at level 20).
Notation "◯MN a" := (mono_nat_lb a) (at level 20).
Section mono_nat.
Implicit Types (n : nat).
Global Instance mono_nat_lb_core_id n : CoreId (mono_nat_lb n).
Global Instance mono_nat_lb_core_id n : CoreId (MN 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.
Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
MN{dq1 dq2} n MN{dq1} n MN{dq2} n.
rewrite /mono_nat_auth -dfrac_op_own auth_auth_dfrac_op.
rewrite (comm _ ({#q2} _)) -!assoc (assoc _ ( _)).
rewrite /mono_nat_auth auth_auth_dfrac_op.
rewrite (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
by rewrite -core_id_dup (comm _ ( _)).
Lemma mono_nat_lb_op n1 n2 :
mono_nat_lb n1 mono_nat_lb n2 = mono_nat_lb (n1 `max` n2).
MN (n1 `max` n2) = MN n1 MN n2.
Proof. rewrite -auth_frag_op max_nat_op //. Qed.
Lemma mono_nat_auth_lb_op q n :
mono_nat_auth q n mono_nat_auth q n mono_nat_lb n.
Lemma mono_nat_auth_lb_op dq n :
MN{dq} n MN{dq} n MN n.
rewrite /mono_nat_auth /mono_nat_lb.
rewrite -!assoc -auth_frag_op max_nat_op.
......@@ -47,53 +57,60 @@ Section mono_nat.
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.
MN n = MN n' MN 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.
Lemma mono_nat_auth_dfrac_valid dq n : ( MN{dq} n) dq.
rewrite /mono_nat_auth auth_both_dfrac_valid_discrete /=. naive_solver.
Lemma mono_nat_auth_valid n : mono_nat_auth 1 n.
Lemma mono_nat_auth_valid n : MN 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.
Lemma mono_nat_auth_dfrac_op_valid dq1 dq2 n1 n2 :
(MN{dq1} n1 MN{dq2} n2) (dq1 dq2) n1 = n2.
rewrite /mono_nat_auth (comm _ ({#q2} _)) -!assoc (assoc _ ( _)).
rewrite /mono_nat_auth (comm _ ({dq2} _)) -!assoc (assoc _ ( _)).
rewrite -auth_frag_op (comm _ ( _)) assoc. split.
- move=> /cmra_valid_op_l /auth_auth_dfrac_op_valid. naive_solver.
- intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op.
by apply auth_both_dfrac_valid_discrete.
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.
(MN n1 MN n2) False.
Proof. rewrite mono_nat_auth_dfrac_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.
Lemma mono_nat_both_dfrac_valid dq n m :
(MN{dq} n MN m) dq m n.
rewrite /mono_nat_auth /mono_nat_lb -assoc -auth_frag_op.
rewrite auth_both_dfrac_valid_discrete max_nat_included /=.
naive_solver lia.
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.
(MN n MN m) m n.
Proof. rewrite mono_nat_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
Lemma mono_nat_lb_mono n1 n2 : n1 n2 mono_nat_lb n1 mono_nat_lb n2.
Lemma mono_nat_lb_mono n1 n2 : n1 n2 MN n1 MN 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.
Lemma mono_nat_included dq n : MN n MN{dq} 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'.
n n' MN n ~~> MN n'.
intros. rewrite /mono_nat_auth /mono_nat_lb.
by apply auth_update, max_nat_local_update.
Lemma mono_nat_auth_persist n dq :
MN{dq} n ~~> MN n.
intros. rewrite /mono_nat_auth /mono_nat_lb.
eapply cmra_update_op_proper; last done.
eapply auth_update_auth_persist.
End mono_nat.
Typeclasses Opaque mono_nat_auth mono_nat_lb.
......@@ -21,7 +21,7 @@ Proof. solve_inG. Qed.
Definition mono_nat_auth_own_def `{!mono_natG Σ}
(γ : gname) (q : Qp) (n : nat) : iProp Σ :=
own γ (mono_nat_auth q n).
own γ (MN{#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 :
......@@ -29,7 +29,7 @@ Definition mono_nat_auth_own_eq :
Global Arguments mono_nat_auth_own {Σ _} γ q n.
Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
own γ (mono_nat_lb n).
own γ (MN 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 :
......@@ -53,7 +53,7 @@ Section mono_nat.
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.
Proof. unseal. intros p q. rewrite -own_op -mono_nat_auth_dfrac_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.
......@@ -64,7 +64,7 @@ Section mono_nat.
(q1 + q2 1)%Qp n1 = n2.
unseal. iIntros "H1 H2".
iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_frac_op_valid; done.
iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_dfrac_op_valid; done.
Lemma mono_nat_auth_own_exclusive γ n1 n2 :
mono_nat_auth_own γ 1 n1 - mono_nat_auth_own γ 1 n2 - False.
......@@ -77,7 +77,7 @@ Section mono_nat.
mono_nat_auth_own γ q n - mono_nat_lb_own γ m - (q 1)%Qp m n.
unseal. iIntros "Hauth Hlb".
iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mono_nat_both_frac_valid.
iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mono_nat_both_dfrac_valid.
......@@ -97,7 +97,7 @@ Section mono_nat.
Lemma mono_nat_own_alloc n :
|==> γ, mono_nat_auth_own γ 1 n mono_nat_lb_own γ n.
unseal. iMod (own_alloc (mono_nat_auth 1 n mono_nat_lb n)) as (γ) "[??]".
unseal. iMod (own_alloc (MN n MN n)) as (γ) "[??]".
{ apply mono_nat_both_valid; auto. }
auto with iFrame.
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