gset.v 6.85 KB
Newer Older
1
From iris.algebra Require Export cmra.
2
From iris.algebra Require Import updates local_updates.
3
From iris.prelude Require Export collections gmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
(* The union CMRA *)
Section gset.
  Context `{Countable K}.
  Implicit Types X Y : gset K.

  Canonical Structure gsetC := leibnizC (gset K).

  Instance gset_valid : Valid (gset K) := λ _, True.
  Instance gset_op : Op (gset K) := union.
  Instance gset_pcore : PCore (gset K) := λ _, Some .

  Lemma gset_op_union X Y : X  Y = X  Y.
  Proof. done. Qed.
  Lemma gset_core_empty X : core X = .
  Proof. done. Qed.
  Lemma gset_included X Y : X  Y  X  Y.
  Proof.
    split.
    - intros [Z ->]. rewrite gset_op_union. set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L. by exists Z.
  Qed.

  Lemma gset_ra_mixin : RAMixin (gset K).
  Proof.
    apply ra_total_mixin; eauto.
    - solve_proper.
    - solve_proper.
    - solve_proper.
    - intros X1 X2 X3. by rewrite !gset_op_union assoc_L.
    - intros X1 X2. by rewrite !gset_op_union comm_L.
    - intros X. by rewrite gset_op_union gset_core_empty left_id_L.
    - intros X1 X2 _. by rewrite gset_included !gset_core_empty.
  Qed.
  Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.

  Lemma gset_ucmra_mixin : UCMRAMixin (gset K).
  Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed.
  Canonical Structure gsetUR :=
    discreteUR (gset K) gset_ra_mixin gset_ucmra_mixin.

  Lemma gset_opM X mY : X ? mY = X  from_option id  mY.
  Proof. destruct mY; by rewrite /= ?right_id_L. Qed.

  Lemma gset_update X Y : X ~~> Y.
  Proof. done. Qed.

  Lemma gset_local_update X Y mXf : X  Y  X ~l~> Y @ mXf.
  Proof.
    intros (Z&->&?)%subseteq_disjoint_union_L.
    intros; apply local_update_total; split; [done|]; simpl.
    intros mZ _. rewrite !gset_opM=> HX. by rewrite (comm_L _ X) -!assoc_L HX.
  Qed.
End gset.

(* The disjoint union CMRA *)
60
61
62
63
64
Inductive gset_disj K `{Countable K} :=
  | GSet : gset K  gset_disj K
  | GSetBot : gset_disj K.
Arguments GSet {_ _ _} _.
Arguments GSetBot {_ _ _}.
Robbert Krebbers's avatar
Robbert Krebbers committed
65

66
Section gset_disj.
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
  Context `{Countable K}.
  Arguments op _ _ !_ !_ /.

  Canonical Structure gset_disjC := leibnizC (gset_disj K).

  Instance gset_disj_valid : Valid (gset_disj K) := λ X,
    match X with GSet _ => True | GSetBot => False end.
  Instance gset_disj_empty : Empty (gset_disj K) := GSet .
  Instance gset_disj_op : Op (gset_disj K) := λ X Y,
    match X, Y with
    | GSet X, GSet Y => if decide (X  Y) then GSet (X  Y) else GSetBot
    | _, _ => GSetBot
    end.
  Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some .

  Ltac gset_disj_solve :=
    repeat (simpl || case_decide);
    first [apply (f_equal GSet)|done|exfalso]; set_solver by eauto.

86
  Lemma gset_disj_included X Y : GSet X  GSet Y  X  Y.
87
88
89
90
91
92
  Proof.
    split.
    - move=> [[Z|]]; simpl; try case_decide; set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L.
      exists (GSet Z). gset_disj_solve.
  Qed.
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
  Lemma gset_disj_valid_inv_l X Y :  (GSet X  Y)   Y', Y = GSet Y'  X  Y'.
  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
  Lemma gset_disj_union X Y : X  Y  GSet X  GSet Y = GSet (X  Y).
  Proof. intros. by rewrite /= decide_True. Qed.
  Lemma gset_disj_valid_op X Y :  (GSet X  GSet Y)  X  Y.
  Proof. simpl. case_decide; by split. Qed.

  Lemma gset_disj_ra_mixin : RAMixin (gset_disj K).
  Proof.
    apply ra_total_mixin; eauto.
    - intros [?|]; destruct 1; gset_disj_solve.
    - by constructor.
    - by destruct 1.
    - intros [X1|] [X2|] [X3|]; gset_disj_solve.
    - intros [X1|] [X2|]; gset_disj_solve.
    - intros [X|]; gset_disj_solve.
    - exists (GSet ); gset_disj_solve.
    - intros [X1|] [X2|]; gset_disj_solve.
  Qed.
  Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.

  Lemma gset_disj_ucmra_mixin : UCMRAMixin (gset_disj K).
  Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
  Canonical Structure gset_disjUR :=
    discreteUR (gset_disj K) gset_disj_ra_mixin gset_disj_ucmra_mixin.

  Arguments op _ _ _ _ : simpl never.

121
  Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K  Prop) X :
122
123
    ( Y, X  Y   j, j  Y  P j) 
    ( i, i  X  P i  Q (GSet ({[i]}  X)))  GSet X ~~>: Q.
124
  Proof.
125
126
127
    intros Hfresh HQ.
    apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
    destruct (Hfresh (X  Y)) as (i&?&?); first set_solver.
128
129
130
131
    exists (GSet ({[ i ]}  X)); split.
    - apply HQ; set_solver by eauto.
    - apply gset_disj_valid_op. set_solver by eauto.
  Qed.
132
  Lemma gset_disj_alloc_updateP_strong' P X :
133
134
    ( Y, X  Y   j, j  Y  P j) 
    GSet X ~~>: λ Y,  i, Y = GSet ({[ i ]}  X)  i  X  P i.
135
  Proof. eauto using gset_disj_alloc_updateP_strong. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
136

137
  Lemma gset_disj_alloc_empty_updateP_strong P (Q : gset_disj K  Prop) :
138
139
    ( Y : gset K,  j, j  Y  P j) 
    ( i, P i  Q (GSet {[i]}))  GSet  ~~>: Q.
140
  Proof.
141
    intros. apply (gset_disj_alloc_updateP_strong P); eauto.
142
    intros i; rewrite right_id_L; auto.
143
  Qed.
144
  Lemma gset_disj_alloc_empty_updateP_strong' P :
145
146
    ( Y : gset K,  j, j  Y  P j) 
    GSet  ~~>: λ Y,  i, Y = GSet {[ i ]}  P i.
147
  Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.
148

149
150
151
  Section fresh_updates.
    Context `{Fresh K (gset K), !FreshSpec K (gset K)}.

152
    Lemma gset_disj_alloc_updateP (Q : gset_disj K  Prop) X :
153
154
      ( i, i  X  Q (GSet ({[i]}  X)))  GSet X ~~>: Q.
    Proof.
155
      intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto.
156
157
      intros Y ?; exists (fresh Y); eauto using is_fresh.
    Qed.
158
159
160
    Lemma gset_disj_alloc_updateP' X :
      GSet X ~~>: λ Y,  i, Y = GSet ({[ i ]}  X)  i  X.
    Proof. eauto using gset_disj_alloc_updateP. Qed.
161

162
    Lemma gset_disj_alloc_empty_updateP (Q : gset_disj K  Prop) :
163
      ( i, Q (GSet {[i]}))  GSet  ~~>: Q.
164
165
166
167
168
    Proof.
      intro. apply gset_disj_alloc_updateP. intros i; rewrite right_id_L; auto.
    Qed.
    Lemma gset_disj_alloc_empty_updateP' : GSet  ~~>: λ Y,  i, Y = GSet {[ i ]}.
    Proof. eauto using gset_disj_alloc_empty_updateP. Qed.
169
  End fresh_updates.
Zhen Zhang's avatar
Zhen Zhang committed
170

171
  Lemma gset_disj_alloc_local_update X i Xf :
Robbert Krebbers's avatar
Robbert Krebbers committed
172
173
174
175
176
177
178
    i  X  i  Xf  GSet X ~l~> GSet ({[i]}  X) @ Some (GSet Xf).
  Proof.
    intros ??; apply local_update_total; split; simpl.
    - rewrite !gset_disj_valid_op; set_solver.
    - intros mZ ?%gset_disj_valid_op HXf.
      rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
  Qed.
179
  Lemma gset_disj_alloc_empty_local_update i Xf :
180
181
182
    i  Xf  GSet  ~l~> GSet {[i]} @ Some (GSet Xf).
  Proof.
    intros. rewrite -(right_id_L _ _ {[i]}).
183
    apply gset_disj_alloc_local_update; set_solver.
184
  Qed.
185
End gset_disj.
186
187
188

Arguments gset_disjR _ {_ _}.
Arguments gset_disjUR _ {_ _}.