Library iris.algebra.lib.mono_nat
From iris.algebra Require Export auth.
From iris.algebra Require Import numbers updates.
From iris.prelude Require Import options.
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 dq n, holds. Without this trick, a
frame-preserving update lemma would be required instead.
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.
Notation "●MN dq a" := (mono_nat_auth dq a)
(at level 20, dq custom dfrac at level 1, format "●MN dq a").
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 (◯MN n).
Proof. apply _. Qed.
Global Instance mono_nat_auth_core_id l : CoreId (●MN□ l).
Proof. apply _. Qed.
Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
●MN{dq1 ⋅ dq2} n ≡ ●MN{dq1} n ⋅ ●MN{dq2} n.
Proof.
rewrite /mono_nat_auth auth_auth_dfrac_op.
rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
by rewrite -core_id_dup (comm _ (◯ _)).
Qed.
Lemma mono_nat_lb_op n1 n2 :
◯MN (n1 `max` n2) = ◯MN n1 ⋅ ◯MN n2.
Proof. rewrite -auth_frag_op max_nat_op //. Qed.
Lemma mono_nat_auth_lb_op dq n :
●MN{dq} n ≡ ●MN{dq} n ⋅ ◯MN n.
Proof.
rewrite /mono_nat_auth /mono_nat_lb.
rewrite -!assoc -auth_frag_op max_nat_op.
rewrite Nat.max_id //.
Qed.
Global Instance mono_nat_auth_dfrac_is_op dq dq1 dq2 n :
IsOp dq dq1 dq2 → IsOp' (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n).
Proof. rewrite /IsOp' /IsOp⇒ →. rewrite mono_nat_auth_dfrac_op //. Qed.
Global Instance mono_nat_lb_max_is_op n n1 n2 :
IsOp (MaxNat n) (MaxNat n1) (MaxNat n2) → IsOp' (◯MN n) (◯MN n1) (◯MN n2).
Proof. rewrite /IsOp' /IsOp /mono_nat_lb⇒ →. done. Qed.
●{dq} MaxNat n ⋅ ◯ MaxNat n.
Definition mono_nat_lb (n : nat) : mono_nat := ◯ MaxNat n.
Notation "●MN dq a" := (mono_nat_auth dq a)
(at level 20, dq custom dfrac at level 1, format "●MN dq a").
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 (◯MN n).
Proof. apply _. Qed.
Global Instance mono_nat_auth_core_id l : CoreId (●MN□ l).
Proof. apply _. Qed.
Lemma mono_nat_auth_dfrac_op dq1 dq2 n :
●MN{dq1 ⋅ dq2} n ≡ ●MN{dq1} n ⋅ ●MN{dq2} n.
Proof.
rewrite /mono_nat_auth auth_auth_dfrac_op.
rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
by rewrite -core_id_dup (comm _ (◯ _)).
Qed.
Lemma mono_nat_lb_op n1 n2 :
◯MN (n1 `max` n2) = ◯MN n1 ⋅ ◯MN n2.
Proof. rewrite -auth_frag_op max_nat_op //. Qed.
Lemma mono_nat_auth_lb_op dq n :
●MN{dq} n ≡ ●MN{dq} n ⋅ ◯MN n.
Proof.
rewrite /mono_nat_auth /mono_nat_lb.
rewrite -!assoc -auth_frag_op max_nat_op.
rewrite Nat.max_id //.
Qed.
Global Instance mono_nat_auth_dfrac_is_op dq dq1 dq2 n :
IsOp dq dq1 dq2 → IsOp' (●MN{dq} n) (●MN{dq1} n) (●MN{dq2} n).
Proof. rewrite /IsOp' /IsOp⇒ →. rewrite mono_nat_auth_dfrac_op //. Qed.
Global Instance mono_nat_lb_max_is_op n n1 n2 :
IsOp (MaxNat n) (MaxNat n1) (MaxNat n2) → IsOp' (◯MN n) (◯MN n1) (◯MN n2).
Proof. rewrite /IsOp' /IsOp /mono_nat_lb⇒ →. done. 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 →
◯MN n = ◯MN n' ⋅ ◯MN n.
Proof. intros. rewrite -mono_nat_lb_op Nat.max_r //. Qed.
Lemma mono_nat_auth_dfrac_valid dq n : (✓ ●MN{dq} n) ↔ ✓ dq.
Proof.
rewrite /mono_nat_auth auth_both_dfrac_valid_discrete /=. naive_solver.
Qed.
Lemma mono_nat_auth_valid n : ✓ ●MN n.
Proof. by apply auth_both_valid. Qed.
Lemma mono_nat_auth_dfrac_op_valid dq1 dq2 n1 n2 :
✓ (●MN{dq1} n1 ⋅ ●MN{dq2} n2) ↔ ✓ (dq1 ⋅ dq2) ∧ n1 = n2.
Proof.
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.
Qed.
Lemma mono_nat_auth_op_valid n1 n2 :
✓ (●MN n1 ⋅ ●MN n2) ↔ False.
Proof. rewrite mono_nat_auth_dfrac_op_valid. naive_solver. Qed.
Lemma mono_nat_both_dfrac_valid dq n m :
✓ (●MN{dq} n ⋅ ◯MN m) ↔ ✓ dq ∧ m ≤ n.
Proof.
rewrite /mono_nat_auth /mono_nat_lb -assoc -auth_frag_op.
rewrite auth_both_dfrac_valid_discrete max_nat_included /=.
naive_solver lia.
Qed.
Lemma mono_nat_both_valid n m :
✓ (●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 → ◯MN n1 ≼ ◯MN n2.
Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
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' → ●MN n ~~> ●MN n'.
Proof.
intros. rewrite /mono_nat_auth /mono_nat_lb.
by apply auth_update, max_nat_local_update.
Qed.
Lemma mono_nat_auth_persist n dq :
●MN{dq} n ~~> ●MN□ n.
Proof.
intros. rewrite /mono_nat_auth /mono_nat_lb.
eapply cmra_update_op_proper; last done.
eapply auth_update_auth_persist.
Qed.
Lemma mono_nat_auth_unpersist n :
●MN□ n ~~>: λ k, ∃ q, k = ●MN{# q} n.
Proof. eapply auth_updateP_both_unpersist. Qed.
End mono_nat.
Global Typeclasses Opaque mono_nat_auth mono_nat_lb.
n' ≤ n →
◯MN n = ◯MN n' ⋅ ◯MN n.
Proof. intros. rewrite -mono_nat_lb_op Nat.max_r //. Qed.
Lemma mono_nat_auth_dfrac_valid dq n : (✓ ●MN{dq} n) ↔ ✓ dq.
Proof.
rewrite /mono_nat_auth auth_both_dfrac_valid_discrete /=. naive_solver.
Qed.
Lemma mono_nat_auth_valid n : ✓ ●MN n.
Proof. by apply auth_both_valid. Qed.
Lemma mono_nat_auth_dfrac_op_valid dq1 dq2 n1 n2 :
✓ (●MN{dq1} n1 ⋅ ●MN{dq2} n2) ↔ ✓ (dq1 ⋅ dq2) ∧ n1 = n2.
Proof.
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.
Qed.
Lemma mono_nat_auth_op_valid n1 n2 :
✓ (●MN n1 ⋅ ●MN n2) ↔ False.
Proof. rewrite mono_nat_auth_dfrac_op_valid. naive_solver. Qed.
Lemma mono_nat_both_dfrac_valid dq n m :
✓ (●MN{dq} n ⋅ ◯MN m) ↔ ✓ dq ∧ m ≤ n.
Proof.
rewrite /mono_nat_auth /mono_nat_lb -assoc -auth_frag_op.
rewrite auth_both_dfrac_valid_discrete max_nat_included /=.
naive_solver lia.
Qed.
Lemma mono_nat_both_valid n m :
✓ (●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 → ◯MN n1 ≼ ◯MN n2.
Proof. intros. by apply auth_frag_mono, max_nat_included. Qed.
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' → ●MN n ~~> ●MN n'.
Proof.
intros. rewrite /mono_nat_auth /mono_nat_lb.
by apply auth_update, max_nat_local_update.
Qed.
Lemma mono_nat_auth_persist n dq :
●MN{dq} n ~~> ●MN□ n.
Proof.
intros. rewrite /mono_nat_auth /mono_nat_lb.
eapply cmra_update_op_proper; last done.
eapply auth_update_auth_persist.
Qed.
Lemma mono_nat_auth_unpersist n :
●MN□ n ~~>: λ k, ∃ q, k = ●MN{# q} n.
Proof. eapply auth_updateP_both_unpersist. Qed.
End mono_nat.
Global Typeclasses Opaque mono_nat_auth mono_nat_lb.