Library iris.algebra.lib.mono_nat

From iris.algebra Require Export auth.
From iris.algebra Require Import numbers updates.

Authoritative CMRA over max_nat. The authoritative element is a monotonically increasing nat, while a fragment is a lower bound.

Definition mono_nat {SI : sidx} := auth max_natUR.
Definition mono_natR {SI : sidx} := authR max_natUR.
Definition mono_natUR {SI : sidx} := 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 {SI : sidx} (dq : dfrac) (n : nat) : mono_nat :=
  ●{dq } MaxNat n ⋅ ◯ MaxNat n.
Definition mono_nat_lb {SI : sidx} (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.
  Context {SI : sidx}.
  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.