gset.v 8.42 KB
Newer Older
1
From stdpp Require Export sets gmap mapset.
2
From iris.algebra Require Export cmra.
3
From iris.algebra Require Import updates local_updates.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5

6 7 8 9 10
(* The union CMRA *)
Section gset.
  Context `{Countable K}.
  Implicit Types X Y : gset K.

11
  Canonical Structure gsetO := discreteO (gset K).
12 13

  Instance gset_valid : Valid (gset K) := λ _, True.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
  Instance gset_unit : Unit (gset K) := ( : gset K).
15
  Instance gset_op : Op (gset K) := union.
Amin Timany's avatar
Amin Timany committed
16
  Instance gset_pcore : PCore (gset K) := λ X, Some X.
17 18 19

  Lemma gset_op_union X Y : X  Y = X  Y.
  Proof. done. Qed.
Amin Timany's avatar
Amin Timany committed
20
  Lemma gset_core_self X : core X = X.
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
  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.
37
    - intros X. by rewrite gset_core_self idemp_L.
38 39 40
  Qed.
  Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.

41
  Global Instance gset_cmra_discrete : CmraDiscrete gsetR.
42 43
  Proof. apply discrete_cmra_discrete. Qed.

44
  Lemma gset_ucmra_mixin : UcmraMixin (gset K).
45
  Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed.
46
  Canonical Structure gsetUR := UcmraT (gset K) gset_ucmra_mixin.
47

48
  Lemma gset_opM X mY : X ? mY = X  default  mY.
49 50 51 52 53
  Proof. destruct mY; by rewrite /= ?right_id_L. Qed.

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

54
  Lemma gset_local_update X Y X' : X  X'  (X,Y) ~l~> (X',X').
55 56
  Proof.
    intros (Z&->&?)%subseteq_disjoint_union_L.
57 58
    rewrite local_update_unital_discrete=> Z' _ /leibniz_equiv_iff->.
    split. done. rewrite gset_op_union. set_solver.
59
  Qed.
Amin Timany's avatar
Amin Timany committed
60

61 62
  Global Instance gset_core_id X : CoreId X.
  Proof. by apply core_id_total; rewrite gset_core_self. Qed.
63 64
End gset.

65
Arguments gsetO _ {_ _}.
Amin Timany's avatar
Amin Timany committed
66 67 68
Arguments gsetR _ {_ _}.
Arguments gsetUR _ {_ _}.

69
(* The disjoint union CMRA *)
70 71 72 73 74
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
75

76
Section gset_disj.
77 78
  Context `{Countable K}.
  Arguments op _ _ !_ !_ /.
79 80
  Arguments cmra_op _ !_ !_ /.
  Arguments ucmra_op _ !_ !_ /.
81

82
  Canonical Structure gset_disjO := leibnizO (gset_disj K).
83 84 85

  Instance gset_disj_valid : Valid (gset_disj K) := λ X,
    match X with GSet _ => True | GSetBot => False end.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
  Instance gset_disj_unit : Unit (gset_disj K) := GSet .
87 88
  Instance gset_disj_op : Op (gset_disj K) := λ X Y,
    match X, Y with
89
    | GSet X, GSet Y => if decide (X ## Y) then GSet (X  Y) else GSetBot
90 91
    | _, _ => GSetBot
    end.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  Instance gset_disj_pcore : PCore (gset_disj K) := λ _, Some ε.
93 94 95 96 97

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

98
  Lemma gset_disj_included X Y : GSet X  GSet Y  X  Y.
99 100 101 102 103 104
  Proof.
    split.
    - move=> [[Z|]]; simpl; try case_decide; set_solver.
    - intros (Z&->&?)%subseteq_disjoint_union_L.
      exists (GSet Z). gset_disj_solve.
  Qed.
105
  Lemma gset_disj_valid_inv_l X Y :  (GSet X  Y)   Y', Y = GSet Y'  X ## Y'.
106
  Proof. destruct Y; repeat (simpl || case_decide); by eauto. Qed.
107
  Lemma gset_disj_union X Y : X ## Y  GSet X  GSet Y = GSet (X  Y).
108
  Proof. intros. by rewrite /= decide_True. Qed.
109
  Lemma gset_disj_valid_op X Y :  (GSet X  GSet Y)  X ## Y.
110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
  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.

126
  Global Instance gset_disj_cmra_discrete : CmraDiscrete gset_disjR.
127 128
  Proof. apply discrete_cmra_discrete. Qed.

129
  Lemma gset_disj_ucmra_mixin : UcmraMixin (gset_disj K).
130
  Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
131
  Canonical Structure gset_disjUR := UcmraT (gset_disj K) gset_disj_ucmra_mixin.
132 133 134

  Arguments op _ _ _ _ : simpl never.

135
  Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K  Prop) X :
136
    ( Y, X  Y   j, j  Y  P j) 
Ralf Jung's avatar
Ralf Jung committed
137 138
    ( i, i  X  P i  Q (GSet ({[i]}  X))) 
    GSet X ~~>: Q.
139
  Proof.
140 141 142
    intros Hfresh HQ.
    apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
    destruct (Hfresh (X  Y)) as (i&?&?); first set_solver.
143 144 145 146
    exists (GSet ({[ i ]}  X)); split.
    - apply HQ; set_solver by eauto.
    - apply gset_disj_valid_op. set_solver by eauto.
  Qed.
147
  Lemma gset_disj_alloc_updateP_strong' P X :
148 149
    ( Y, X  Y   j, j  Y  P j) 
    GSet X ~~>: λ Y,  i, Y = GSet ({[ i ]}  X)  i  X  P i.
150
  Proof. eauto using gset_disj_alloc_updateP_strong. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
151

152
  Lemma gset_disj_alloc_empty_updateP_strong P (Q : gset_disj K  Prop) :
153 154
    ( Y : gset K,  j, j  Y  P j) 
    ( i, P i  Q (GSet {[i]}))  GSet  ~~>: Q.
155
  Proof.
156
    intros. apply (gset_disj_alloc_updateP_strong P); eauto.
157
    intros i; rewrite right_id_L; auto.
158
  Qed.
159
  Lemma gset_disj_alloc_empty_updateP_strong' P :
160 161
    ( Y : gset K,  j, j  Y  P j) 
    GSet  ~~>: λ Y,  i, Y = GSet {[ i ]}  P i.
162
  Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.
163

164
  Section fresh_updates.
165
    Local Set Default Proof Using "Type*".
166
    Context `{!Infinite K}.
167

168
    Lemma gset_disj_alloc_updateP (Q : gset_disj K  Prop) X :
169 170
      ( i, i  X  Q (GSet ({[i]}  X)))  GSet X ~~>: Q.
    Proof.
171
      intro; eapply gset_disj_alloc_updateP_strong with (λ _, True); eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
172
      intros Y ?; exists (fresh Y). split. apply is_fresh. done.
173
    Qed.
174 175 176
    Lemma gset_disj_alloc_updateP' X :
      GSet X ~~>: λ Y,  i, Y = GSet ({[ i ]}  X)  i  X.
    Proof. eauto using gset_disj_alloc_updateP. Qed.
177

178
    Lemma gset_disj_alloc_empty_updateP (Q : gset_disj K  Prop) :
179
      ( i, Q (GSet {[i]}))  GSet  ~~>: Q.
180 181 182 183 184
    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.
185
  End fresh_updates.
Zhen Zhang's avatar
Zhen Zhang committed
186

187
  Lemma gset_disj_dealloc_local_update X Y :
Robbert Krebbers's avatar
Robbert Krebbers committed
188
    (GSet X, GSet Y) ~l~> (GSet (X  Y), GSet ).
189 190 191 192 193 194 195 196
  Proof.
    apply local_update_total_valid=> _ _ /gset_disj_included HYX.
    rewrite local_update_unital_discrete=> -[Xf|] _ /leibniz_equiv_iff //=.
    rewrite {1}/op /=. destruct (decide _) as [HXf|]; [intros[= ->]|done].
    by rewrite difference_union_distr_l_L
      difference_diag_L !left_id_L difference_disjoint_L.
  Qed.
  Lemma gset_disj_dealloc_empty_local_update X Z :
Robbert Krebbers's avatar
Robbert Krebbers committed
197
    (GSet Z  GSet X, GSet Z) ~l~> (GSet X, GSet ).
198
  Proof.
199 200 201
    apply local_update_total_valid=> /gset_disj_valid_op HZX _ _.
    assert (X = (Z  X)  Z) as HX by set_solver.
    rewrite gset_disj_union // {2}HX. apply gset_disj_dealloc_local_update.
202
  Qed.
203 204
  Lemma gset_disj_dealloc_op_local_update X Y Z :
    (GSet Z  GSet X, GSet Z  GSet Y) ~l~> (GSet X,GSet Y).
205
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
    rewrite -{2}(left_id ε _ (GSet Y)).
207
    apply op_local_update_frame, gset_disj_dealloc_empty_local_update.
208 209
  Qed.

210
  Lemma gset_disj_alloc_op_local_update X Y Z :
211
    Z ## X  (GSet X,GSet Y) ~l~> (GSet Z  GSet X, GSet Z  GSet Y).
212 213 214 215
  Proof.
    intros. apply op_local_update_discrete. by rewrite gset_disj_valid_op.
  Qed.
  Lemma gset_disj_alloc_local_update X Y Z :
216
    Z ## X  (GSet X,GSet Y) ~l~> (GSet (Z  X), GSet (Z  Y)).
Robbert Krebbers's avatar
Robbert Krebbers committed
217
  Proof.
218 219 220
    intros. apply local_update_total_valid=> _ _ /gset_disj_included ?.
    rewrite -!gset_disj_union //; last set_solver.
    auto using gset_disj_alloc_op_local_update.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
  Qed.
222
  Lemma gset_disj_alloc_empty_local_update X Z :
223
    Z ## X  (GSet X, GSet ) ~l~> (GSet (Z  X), GSet Z).
224
  Proof.
225
    intros. rewrite -{2}(right_id_L _ union Z).
226
    apply gset_disj_alloc_local_update; set_solver.
227
  Qed.
228
End gset_disj.
229

230
Arguments gset_disjO _ {_ _}.
231 232
Arguments gset_disjR _ {_ _}.
Arguments gset_disjUR _ {_ _}.