mono_nat.v 4.78 KB
Newer Older
1
2
3
4
5
6
7
8
9
(** 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. *)
Ralf Jung's avatar
Ralf Jung committed
10
From iris.proofmode Require Import proofmode.
11
12
13
14
15
16
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 Σ :=
17
18
  MonoNatG { mono_natG_inG : inG Σ mono_natR; }.
Local Existing Instance mono_natG_inG.
19
Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
20
Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ  mono_natG Σ.
21
22
23
24
Proof. solve_inG. Qed.

Definition mono_nat_auth_own_def `{!mono_natG Σ}
    (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
25
  own γ (MN{#q} n).
26
27
28
29
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).
Definition mono_nat_auth_own_eq :
  @mono_nat_auth_own = @mono_nat_auth_own_def := mono_nat_auth_own_aux.(seal_eq).
Ralf Jung's avatar
Ralf Jung committed
30
Global Arguments mono_nat_auth_own {Σ _} γ q n.
31
32

Definition mono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
33
  own γ (MN n).
34
35
36
37
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).
Definition mono_nat_lb_own_eq :
  @mono_nat_lb_own = @mono_nat_lb_own_def := mono_nat_lb_own_aux.(seal_eq).
Ralf Jung's avatar
Ralf Jung committed
38
Global Arguments mono_nat_lb_own {Σ _} γ n.
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56

Local Ltac unseal := rewrite
  ?mono_nat_auth_own_eq /mono_nat_auth_own_def
  ?mono_nat_lb_own_eq /mono_nat_lb_own_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_auth_own_fractional γ n :
    Fractional (λ q, mono_nat_auth_own γ q n).
57
  Proof. unseal. intros p q. rewrite -own_op -mono_nat_auth_dfrac_op //. Qed.
58
59
60
61
62
63
64
65
66
67
  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".
68
    iDestruct (own_valid_2 with "H1 H2") as %?%mono_nat_auth_dfrac_op_valid; done.
69
70
71
72
73
74
75
76
77
78
79
80
  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".
81
    iDestruct (own_valid_2 with "Hauth Hlb") as %Hvalid%mono_nat_both_dfrac_valid.
82
83
84
85
86
87
88
89
90
91
92
    auto.
  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. apply own_mono, mono_nat_included. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
93
  Lemma mono_nat_lb_own_le {γ n} n' :
94
95
96
97
98
99
100
    n'  n 
    mono_nat_lb_own γ n - mono_nat_lb_own γ n'.
  Proof. unseal. intros. by apply own_mono, mono_nat_lb_mono. Qed.

  Lemma mono_nat_own_alloc n :
     |==>  γ, mono_nat_auth_own γ 1 n  mono_nat_lb_own γ n.
  Proof.
101
    unseal. iMod (own_alloc (MN n  MN n)) as (γ) "[??]".
102
103
104
105
    { apply mono_nat_both_valid; auto. }
    auto with iFrame.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
106
  Lemma mono_nat_own_update {γ n} n' :
107
108
109
    n  n' 
    mono_nat_auth_own γ 1 n == mono_nat_auth_own γ 1 n'  mono_nat_lb_own γ n'.
  Proof.
110
111
112
113
    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.
114
115
  Qed.
End mono_nat.