Library iris.algebra.lib.mono_Z
Authoritative CMRA over max_Z. The authoritative element is a
monotonically increasing Z, while a fragment is a lower bound.
Definition mono_Z {SI: sidx} := auth (option max_ZR).
Definition mono_ZR {SI: sidx} := authR (optionUR max_ZR).
Definition mono_ZUR {SI: sidx} := authUR (optionUR max_ZR).
mono_Z_auth is the authoritative element. The definition includes the
fragment at the same value so that lemma mono_Z_included, which states that
mono_Z_lb n ≼ mono_Z_auth dq n, holds. Without this trick, a frame-preserving
update lemma would be required instead.
Definition mono_Z_auth {SI : sidx} (dq : dfrac) (n : Z) : mono_Z :=
●{dq} (Some (MaxZ n)) ⋅ ◯ (Some (MaxZ n)).
Definition mono_Z_lb {SI : sidx} (n : Z) : mono_Z := ◯ (Some (MaxZ n)).
Notation "●MZ dq a" := (mono_Z_auth dq a)
(at level 20, dq custom dfrac at level 1, format "●MZ dq a").
Notation "◯MZ a" := (mono_Z_lb a) (at level 20).
Section mono_Z.
Context {SI : sidx}.
Implicit Types (n : Z).
Local Open Scope Z_scope.
Global Instance mono_Z_lb_core_id n : CoreId (◯MZ n).
Proof. apply _. Qed.
Global Instance mono_Z_auth_core_id l : CoreId (●MZ□ l).
Proof. apply _. Qed.
Lemma mono_Z_auth_dfrac_op dq1 dq2 n :
●MZ{dq1 ⋅ dq2} n ≡ ●MZ{dq1} n ⋅ ●MZ{dq2} n.
Proof.
rewrite /mono_Z_auth auth_auth_dfrac_op.
rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
by rewrite -core_id_dup (comm _ (◯ _)).
Qed.
Lemma mono_Z_lb_op n1 n2 :
◯MZ (n1 `max` n2) = ◯MZ n1 ⋅ ◯MZ n2.
Proof. rewrite -auth_frag_op -Some_op max_Z_op //. Qed.
Lemma mono_Z_auth_lb_op dq n :
●MZ{dq} n ≡ ●MZ{dq} n ⋅ ◯MZ n.
Proof.
rewrite /mono_Z_auth /mono_Z_lb.
rewrite -!assoc -auth_frag_op -Some_op max_Z_op.
rewrite Z.max_id //.
Qed.
Global Instance mono_Z_auth_dfrac_is_op dq dq1 dq2 n :
IsOp dq dq1 dq2 → IsOp' (●MZ{dq} n) (●MZ{dq1} n) (●MZ{dq2} n).
Proof. rewrite /IsOp' /IsOp⇒ →. rewrite mono_Z_auth_dfrac_op //. Qed.
Global Instance mono_Z_lb_max_is_op n n1 n2 :
IsOp (MaxZ n) (MaxZ n1) (MaxZ n2) → IsOp' (◯MZ n) (◯MZ n1) (◯MZ n2).
Proof. rewrite /IsOp' /IsOp /mono_Z_lb⇒ →. done. Qed.
●{dq} (Some (MaxZ n)) ⋅ ◯ (Some (MaxZ n)).
Definition mono_Z_lb {SI : sidx} (n : Z) : mono_Z := ◯ (Some (MaxZ n)).
Notation "●MZ dq a" := (mono_Z_auth dq a)
(at level 20, dq custom dfrac at level 1, format "●MZ dq a").
Notation "◯MZ a" := (mono_Z_lb a) (at level 20).
Section mono_Z.
Context {SI : sidx}.
Implicit Types (n : Z).
Local Open Scope Z_scope.
Global Instance mono_Z_lb_core_id n : CoreId (◯MZ n).
Proof. apply _. Qed.
Global Instance mono_Z_auth_core_id l : CoreId (●MZ□ l).
Proof. apply _. Qed.
Lemma mono_Z_auth_dfrac_op dq1 dq2 n :
●MZ{dq1 ⋅ dq2} n ≡ ●MZ{dq1} n ⋅ ●MZ{dq2} n.
Proof.
rewrite /mono_Z_auth auth_auth_dfrac_op.
rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
by rewrite -core_id_dup (comm _ (◯ _)).
Qed.
Lemma mono_Z_lb_op n1 n2 :
◯MZ (n1 `max` n2) = ◯MZ n1 ⋅ ◯MZ n2.
Proof. rewrite -auth_frag_op -Some_op max_Z_op //. Qed.
Lemma mono_Z_auth_lb_op dq n :
●MZ{dq} n ≡ ●MZ{dq} n ⋅ ◯MZ n.
Proof.
rewrite /mono_Z_auth /mono_Z_lb.
rewrite -!assoc -auth_frag_op -Some_op max_Z_op.
rewrite Z.max_id //.
Qed.
Global Instance mono_Z_auth_dfrac_is_op dq dq1 dq2 n :
IsOp dq dq1 dq2 → IsOp' (●MZ{dq} n) (●MZ{dq1} n) (●MZ{dq2} n).
Proof. rewrite /IsOp' /IsOp⇒ →. rewrite mono_Z_auth_dfrac_op //. Qed.
Global Instance mono_Z_lb_max_is_op n n1 n2 :
IsOp (MaxZ n) (MaxZ n1) (MaxZ n2) → IsOp' (◯MZ n) (◯MZ n1) (◯MZ n2).
Proof. rewrite /IsOp' /IsOp /mono_Z_lb⇒ →. done. Qed.
rephrasing of mono_Z_lb_op useful for weakening a fragment to a
smaller lower-bound
Lemma mono_Z_lb_op_le_l n n' :
n' ≤ n →
◯MZ n = ◯MZ n' ⋅ ◯MZ n.
Proof. intros. rewrite -mono_Z_lb_op Z.max_r //. Qed.
Lemma mono_Z_auth_dfrac_valid dq n : (✓ ●MZ{dq} n) ↔ ✓ dq.
Proof.
rewrite /mono_Z_auth auth_both_dfrac_valid_discrete /=. naive_solver.
Qed.
Lemma mono_Z_auth_valid n : ✓ ●MZ n.
Proof. by apply auth_both_valid. Qed.
Lemma mono_Z_auth_dfrac_op_valid dq1 dq2 n1 n2 :
✓ (●MZ{dq1} n1 ⋅ ●MZ{dq2} n2) ↔ ✓ (dq1 ⋅ dq2) ∧ n1 = n2.
Proof.
rewrite /mono_Z_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_Z_auth_op_valid n1 n2 :
✓ (●MZ n1 ⋅ ●MZ n2) ↔ False.
Proof. rewrite mono_Z_auth_dfrac_op_valid. naive_solver. Qed.
Lemma mono_Z_both_dfrac_valid dq n m :
✓ (●MZ{dq} n ⋅ ◯MZ m) ↔ ✓ dq ∧ m ≤ n.
Proof.
rewrite /mono_Z_auth /mono_Z_lb -assoc -auth_frag_op.
rewrite auth_both_dfrac_valid_discrete Some_included_total max_Z_included /=.
naive_solver lia.
Qed.
Lemma mono_Z_both_valid n m :
✓ (●MZ n ⋅ ◯MZ m) ↔ m ≤ n.
Proof. rewrite mono_Z_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
Lemma mono_Z_lb_mono n1 n2 : n1 ≤ n2 → ◯MZ n1 ≼ ◯MZ n2.
Proof.
intros. by apply auth_frag_mono, Some_included_total, max_Z_included.
Qed.
Lemma mono_Z_included dq n : ◯MZ n ≼ ●MZ{dq} n.
Proof. apply: cmra_included_r. Qed.
Lemma mono_Z_update {n} n' :
n ≤ n' → ●MZ n ~~> ●MZ n'.
Proof.
intros. rewrite /mono_Z_auth /mono_Z_lb.
by apply auth_update, option_local_update, max_Z_local_update.
Qed.
Lemma mono_Z_auth_persist n dq :
●MZ{dq} n ~~> ●MZ□ n.
Proof.
intros. rewrite /mono_Z_auth /mono_Z_lb.
eapply cmra_update_op_proper; last done.
eapply auth_update_auth_persist.
Qed.
Lemma mono_Z_auth_unpersist n :
●MZ□ n ~~>: λ k, ∃ q, k = ●MZ{# q} n.
Proof. eapply auth_updateP_both_unpersist. Qed.
End mono_Z.
Global Typeclasses Opaque mono_Z_auth mono_Z_lb.
n' ≤ n →
◯MZ n = ◯MZ n' ⋅ ◯MZ n.
Proof. intros. rewrite -mono_Z_lb_op Z.max_r //. Qed.
Lemma mono_Z_auth_dfrac_valid dq n : (✓ ●MZ{dq} n) ↔ ✓ dq.
Proof.
rewrite /mono_Z_auth auth_both_dfrac_valid_discrete /=. naive_solver.
Qed.
Lemma mono_Z_auth_valid n : ✓ ●MZ n.
Proof. by apply auth_both_valid. Qed.
Lemma mono_Z_auth_dfrac_op_valid dq1 dq2 n1 n2 :
✓ (●MZ{dq1} n1 ⋅ ●MZ{dq2} n2) ↔ ✓ (dq1 ⋅ dq2) ∧ n1 = n2.
Proof.
rewrite /mono_Z_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_Z_auth_op_valid n1 n2 :
✓ (●MZ n1 ⋅ ●MZ n2) ↔ False.
Proof. rewrite mono_Z_auth_dfrac_op_valid. naive_solver. Qed.
Lemma mono_Z_both_dfrac_valid dq n m :
✓ (●MZ{dq} n ⋅ ◯MZ m) ↔ ✓ dq ∧ m ≤ n.
Proof.
rewrite /mono_Z_auth /mono_Z_lb -assoc -auth_frag_op.
rewrite auth_both_dfrac_valid_discrete Some_included_total max_Z_included /=.
naive_solver lia.
Qed.
Lemma mono_Z_both_valid n m :
✓ (●MZ n ⋅ ◯MZ m) ↔ m ≤ n.
Proof. rewrite mono_Z_both_dfrac_valid dfrac_valid_own. naive_solver. Qed.
Lemma mono_Z_lb_mono n1 n2 : n1 ≤ n2 → ◯MZ n1 ≼ ◯MZ n2.
Proof.
intros. by apply auth_frag_mono, Some_included_total, max_Z_included.
Qed.
Lemma mono_Z_included dq n : ◯MZ n ≼ ●MZ{dq} n.
Proof. apply: cmra_included_r. Qed.
Lemma mono_Z_update {n} n' :
n ≤ n' → ●MZ n ~~> ●MZ n'.
Proof.
intros. rewrite /mono_Z_auth /mono_Z_lb.
by apply auth_update, option_local_update, max_Z_local_update.
Qed.
Lemma mono_Z_auth_persist n dq :
●MZ{dq} n ~~> ●MZ□ n.
Proof.
intros. rewrite /mono_Z_auth /mono_Z_lb.
eapply cmra_update_op_proper; last done.
eapply auth_update_auth_persist.
Qed.
Lemma mono_Z_auth_unpersist n :
●MZ□ n ~~>: λ k, ∃ q, k = ●MZ{# q} n.
Proof. eapply auth_updateP_both_unpersist. Qed.
End mono_Z.
Global Typeclasses Opaque mono_Z_auth mono_Z_lb.