iris-coq/iris/algebra/lib/mono_nat.v at master · JasonGross/iris-coq · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
From iris.algebra Require Export auth.
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 {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.