-
Notifications
You must be signed in to change notification settings - Fork 0
/
mono_nat.v
161 lines (139 loc) · 6.54 KB
/
mono_nat.v
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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
(* Edit of the Iris mono_nat to support persistent ownership. *)
(** Ghost state for a monotonically increasing nat, wrapping the [mono_natR]
RA. Provides an authoritative proposition [mono_nat_auth_own γ q n] for the
underlying number [n] and a persistent proposition [mono_nat_lb_own γ m]
witnessing that the authoritative nat is at least m.
The key rules are [mono_nat_lb_own_valid], which asserts that an auth at [n] and
a lower-bound at [m] imply that [m ≤ n], and [mono_nat_update], which allows to
increase the auth element. At any time the auth nat can be "snapshotted" with
[mono_nat_get_lb] to produce a persistent lower-bound proposition. *)
From iris.proofmode Require Import proofmode.
From iris.algebra.lib Require Import mono_nat.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export own.
From iris.prelude Require Import options.
Class mono_natG Σ :=
MonoNatG { mono_natG_inG : inG Σ mono_natR; }.
Local Existing Instance mono_natG_inG.
Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
Proof. solve_inG. Qed.
Local Definition mono_nat_auth_own_def `{!mono_natG Σ}
(γ : gname) (q : Qp) (n : nat) : iProp Σ :=
own γ (●MN{#q} n).
Local 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).
Local Definition mono_nat_auth_own_unseal :
@mono_nat_auth_own = @mono_nat_auth_own_def := mono_nat_auth_own_aux.(seal_eq).
Global Arguments mono_nat_auth_own {Σ _} γ q n.
Local Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
own γ (◯MN n).
Local 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).
Local Definition mono_nat_lb_own_unseal :
@mono_nat_lb_own = @mono_nat_lb_own_def := mono_nat_lb_own_aux.(seal_eq).
Global Arguments mono_nat_lb_own {Σ _} γ n.
Local Definition mono_nat_persistent_def `{!mono_natG Σ}
(γ : gname) (n : nat) : iProp Σ :=
own γ (●MN□ n).
Local Definition mono_nat_persistent_aux : seal (@mono_nat_persistent_def).
Proof. by eexists. Qed.
Definition mono_nat_persistent := mono_nat_persistent_aux.(unseal).
Local Definition mono_nat_persistent_unseal :
@mono_nat_persistent = @mono_nat_persistent_def := mono_nat_persistent_aux.(seal_eq).
Global Arguments mono_nat_persistent {Σ _} γ n.
Local Ltac unseal := rewrite
?mono_nat_auth_own_unseal /mono_nat_auth_own_def
?mono_nat_lb_own_unseal /mono_nat_lb_own_def
?mono_nat_persistent_unseal /mono_nat_persistent_def.
Section mono_nat.
Context `{!mono_natG Σ}.
Implicit Types (n m : nat).
Global Instance mono_nat_auth_own_timeless γ q n : Timeless (mono_nat_auth_own γ q n).
Proof. unseal. apply _. Qed.
Global Instance mono_nat_lb_own_timeless γ n : Timeless (mono_nat_lb_own γ n).
Proof. unseal. apply _. Qed.
Global Instance mono_nat_lb_own_persistent γ n : Persistent (mono_nat_lb_own γ n).
Proof. unseal. apply _. Qed.
Global Instance mono_nat_persistent_timeless γ n : Timeless (mono_nat_persistent γ n).
Proof. unseal. apply _. Qed.
Global Instance mono_nat_persistent_persistent γ n : Persistent (mono_nat_persistent γ n).
Proof. unseal. apply _. Qed.
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_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.
Lemma mono_nat_auth_own_agree γ q1 q2 n1 n2 :
mono_nat_auth_own γ q1 n1 -∗
mono_nat_auth_own γ q2 n2 -∗
⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
Proof.
unseal. iIntros "H1 H2".
by iCombine "H1 H2" gives %?%mono_nat_auth_dfrac_op_valid.
Qed.
Lemma mono_nat_auth_own_exclusive γ n1 n2 :
mono_nat_auth_own γ 1 n1 -∗ mono_nat_auth_own γ 1 n2 -∗ False.
Proof.
iIntros "H1 H2".
by iDestruct (mono_nat_auth_own_agree with "H1 H2") as %[[] _].
Qed.
Lemma mono_nat_lb_own_valid γ q n m :
mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
Proof.
unseal. iIntros "Hauth Hlb".
by iCombine "Hauth Hlb" gives %?%mono_nat_both_dfrac_valid.
Qed.
Lemma mono_nat_persistent_lb_own_valid γ n m :
mono_nat_persistent γ n -∗ mono_nat_lb_own γ m -∗ ⌜m ≤ n⌝.
Proof.
unseal. iIntros "Hpers Hlb".
by iCombine "Hpers Hlb" gives %[_ ?]%mono_nat_both_dfrac_valid.
Qed.
Lemma mono_nat_persistent_agree γ n1 n2 :
mono_nat_persistent γ n1 -∗
mono_nat_persistent γ n2 -∗
⌜n1 = n2⌝.
Proof.
unseal. iIntros "H1 H2".
by iCombine "H1 H2" gives %[_ ?]%mono_nat_auth_dfrac_op_valid.
Qed.
(** The conclusion of this lemma is persistent; the proofmode will preserve
the [mono_nat_auth_own] in the premise as long as the conclusion is introduced
to the persistent context, for example with [iDestruct (mono_nat_lb_own_get
with "Hauth") as "#Hfrag"]. *)
Lemma mono_nat_lb_own_get γ q n :
mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ n.
Proof. unseal. iApply own_mono; apply mono_nat_included. Qed.
Lemma mono_nat_persistent_lb_own_get γ n :
mono_nat_persistent γ n -∗ mono_nat_lb_own γ n.
Proof. unseal. iApply own_mono; apply mono_nat_included. Qed.
Lemma mono_nat_own_persist γ q n :
mono_nat_auth_own γ q n ==∗ mono_nat_persistent γ n.
Proof. unseal. iApply own_update; apply mono_nat_auth_persist. Qed.
Lemma mono_nat_lb_own_le {γ n} n' :
n' ≤ n →
mono_nat_lb_own γ n -∗ mono_nat_lb_own γ n'.
Proof. unseal. intros. by iApply own_mono; apply mono_nat_lb_mono. Qed.
Lemma mono_nat_lb_own_0 γ :
⊢ |==> mono_nat_lb_own γ 0.
Proof. unseal. iApply own_unit. Qed.
Lemma mono_nat_own_alloc n :
⊢ |==> ∃ γ, mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
Proof.
unseal. iMod (own_alloc (●MN n ⋅ ◯MN n)) as (γ) "[??]".
{ apply mono_nat_both_valid; auto. }
auto with iFrame.
Qed.
Lemma mono_nat_own_update {γ n} n' :
n ≤ n' →
mono_nat_auth_own γ 1 n ==∗ mono_nat_auth_own γ 1 n' ∗ mono_nat_lb_own γ n'.
Proof.
iIntros (?) "Hauth".
iAssert (mono_nat_auth_own γ 1 n') with "[> Hauth]" as "Hauth".
{ unseal. iApply (own_update with "Hauth"). by apply mono_nat_update. }
iModIntro. iSplit; [done|]. by iApply mono_nat_lb_own_get.
Qed.
End mono_nat.