big_op.v 26.6 KB
Newer Older
1
From iris.algebra Require Export list big_op.
2
From iris.base_logic Require Export base_logic.
Ralf Jung's avatar
Ralf Jung committed
3
From stdpp Require Import gmap fin_collections gmultiset functions.
4
Set Default Proof Using "Type".
5
Import uPred.
6

7
(* Notations *)
8
Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL uPred_sep (λ k x, P) l)
9
  (at level 200, l at level 10, k, x at level 1, right associativity,
10
11
   format "[∗  list]  k ↦ x  ∈  l ,  P") : uPred_scope.
Notation "'[∗' 'list]' x ∈ l , P" := (big_opL uPred_sep (λ _ x, P) l)
12
  (at level 200, l at level 10, x at level 1, right associativity,
13
   format "[∗  list]  x  ∈  l ,  P") : uPred_scope.
14

15
Notation "'[∗]' Ps" :=
16
  (big_opL uPred_sep (λ _ x, x) Ps) (at level 20) : uPred_scope.
17

18
Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM uPred_sep (λ k x, P) m)
19
  (at level 200, m at level 10, k, x at level 1, right associativity,
20
21
   format "[∗  map]  k ↦ x  ∈  m ,  P") : uPred_scope.
Notation "'[∗' 'map]' x ∈ m , P" := (big_opM uPred_sep (λ _ x, P) m)
22
  (at level 200, m at level 10, x at level 1, right associativity,
23
   format "[∗  map]  x  ∈  m ,  P") : uPred_scope.
24

25
Notation "'[∗' 'set]' x ∈ X , P" := (big_opS uPred_sep (λ x, P) X)
26
  (at level 200, X at level 10, x at level 1, right associativity,
27
   format "[∗  set]  x  ∈  X ,  P") : uPred_scope.
28

29
Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS uPred_sep (λ x, P) X)
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  (at level 200, X at level 10, x at level 1, right associativity,
31
   format "[∗  mset]  x  ∈  X ,  P") : uPred_scope.
32

33
(** * Properties *)
34
Section big_op.
35
Context {M : ucmraT}.
36
37
38
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

39
40
41
42
43
44
(** ** Big ops over lists *)
Section list.
  Context {A : Type}.
  Implicit Types l : list A.
  Implicit Types Φ Ψ : nat  A  uPred M.

45
  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y)  True.
46
  Proof. done. Qed.
47
48
  Lemma big_sepL_nil' P Φ : P  [ list] ky  nil, Φ k y.
  Proof. apply True_intro. Qed.
49
  Lemma big_sepL_cons Φ x l :
50
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
51
  Proof. by rewrite big_opL_cons. Qed.
52
  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
53
54
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
55
56
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
57
58
  Proof. by rewrite big_opL_app. Qed.

59
60
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
61
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
62
  Proof. apply big_opL_forall; apply _. Qed.
63
64
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
65
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
66
  Proof. apply big_opL_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
  Lemma big_sepL_submseteq (Φ : A  uPred M) l1 l2 :
    l1 + l2  ([ list] y  l2, Φ y)  [ list] y  l1, Φ y.
69
  Proof. intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l. Qed.
70

71
72
  Global Instance big_sepL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
73
           (big_opL (@uPred_sep M) (A:=A)).
74
75
  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
  Global Instance big_sep_mono' :
76
    Proper (Forall2 () ==> ()) (big_opL (@uPred_sep M) (λ _ P, P)).
77
  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
78

79
80
81
82
  Lemma big_sepL_lookup_acc Φ l i x :
    l !! i = Some x 
    ([ list] ky  l, Φ k y)  Φ i x  (Φ i x - ([ list] ky  l, Φ k y)).
  Proof.
83
84
85
    intros Hli. rewrite -(take_drop_middle l i x) // big_sepL_app /=.
    rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
    rewrite assoc -!(comm _ (Φ _ _)) -assoc. by apply sep_mono_r, wand_intro_l.
86
87
  Qed.

88
  Lemma big_sepL_lookup Φ l i x :
89
    l !! i = Some x  ([ list] ky  l, Φ k y)  Φ i x.
90
  Proof. intros. by rewrite big_sepL_lookup_acc // sep_elim_l. Qed.
91

Robbert Krebbers's avatar
Robbert Krebbers committed
92
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
93
    x  l  ([ list] y  l, Φ y)  Φ x.
94
95
96
  Proof.
    intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)).
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
97

98
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  uPred M) l :
99
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
100
  Proof. by rewrite big_opL_fmap. Qed.
101
102

  Lemma big_sepL_sepL Φ Ψ l :
103
104
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
105
  Proof. by rewrite big_opL_opL. Qed.
106

107
108
109
110
111
  Lemma big_sepL_and Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
  Proof. auto using big_sepL_mono with I. Qed.

112
  Lemma big_sepL_later Φ l :
113
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
114
  Proof. apply (big_opL_commute _). Qed.
115

Robbert Krebbers's avatar
Robbert Krebbers committed
116
117
118
119
  Lemma big_sepL_laterN Φ n l :
    ^n ([ list] kx  l, Φ k x)  ([ list] kx  l, ^n Φ k x).
  Proof. apply (big_opL_commute _). Qed.

120
  Lemma big_sepL_persistently Φ l :
121
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
122
  Proof. apply (big_opL_commute _). Qed.
123

124
  Lemma big_sepL_persistently_if p Φ l :
125
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
126
  Proof. apply (big_opL_commute _). Qed.
127
128

  Lemma big_sepL_forall Φ l :
129
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
130
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
131
132
133
134
135
136
  Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. }
    revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
    { rewrite big_sepL_nil; auto with I. }
137
    rewrite big_sepL_cons. rewrite -and_sep_l; apply and_intro.
138
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
139
140
141
142
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Lemma big_sepL_impl Φ Ψ l :
Ralf Jung's avatar
Ralf Jung committed
143
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
144
     [ list] kx  l, Ψ k x.
145
  Proof.
146
147
    rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
    setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
148
    rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
149
    by rewrite persistently_impl_wand persistently_elim wand_elim_l.
150
151
  Qed.

152
153
154
155
156
157
158
159
  Global Instance big_sepL_nil_plain Φ : Plain ([ list] kx  [], Φ k x).
  Proof. simpl; apply _. Qed.
  Global Instance big_sepL_plain Φ l :
    ( k x, Plain (Φ k x))  Plain ([ list] kx  l, Φ k x).
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
  Global Instance big_sepL_plain_id Ps : TCForall Plain Ps  Plain ([] Ps).
  Proof. induction 1; simpl; apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
160
  Global Instance big_sepL_nil_persistent Φ :
161
    Persistent ([ list] kx  [], Φ k x).
162
  Proof. simpl; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  Global Instance big_sepL_persistent Φ l :
164
    ( k x, Persistent (Φ k x))  Persistent ([ list] kx  l, Φ k x).
165
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
166
  Global Instance big_sepL_persistent_id Ps :
167
    TCForall Persistent Ps  Persistent ([] Ps).
168
  Proof. induction 1; simpl; apply _. Qed.
169

Robbert Krebbers's avatar
Robbert Krebbers committed
170
  Global Instance big_sepL_nil_timeless Φ :
171
    Timeless ([ list] kx  [], Φ k x).
172
  Proof. simpl; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  Global Instance big_sepL_timeless Φ l :
174
    ( k x, Timeless (Φ k x))  Timeless ([ list] kx  l, Φ k x).
175
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
176
  Global Instance big_sepL_timeless_id Ps :
177
    TCForall Timeless Ps  Timeless ([] Ps).
178
  Proof. induction 1; simpl; apply _. Qed.
179
180
End list.

181
182
183
184
185
186
187
Section list2.
  Context {A : Type}.
  Implicit Types l : list A.
  Implicit Types Φ Ψ : nat  A  uPred M.
  (* Some lemmas depend on the generalized versions of the above ones. *)

  Lemma big_sepL_zip_with {B C} Φ f (l1 : list B) (l2 : list C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
188
189
    ([ list] kx  zip_with f l1 l2, Φ k x)
     ([ list] kx  l1,  y, l2 !! k = Some y  Φ k (f x y)).
190
  Proof.
191
    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //.
192
    - apply (anti_symm _), True_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
195
196
      trans ([ list] __  x :: l1, True : uPred M)%I.
      + rewrite big_sepL_forall. auto using forall_intro, impl_intro_l, True_intro.
      + apply big_sepL_mono=> k y _. apply forall_intro=> z.
        by apply impl_intro_l, pure_elim_l.
197
    - rewrite /= IH. apply sep_proper=> //. apply (anti_symm _).
Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
      + apply forall_intro=>z /=. by apply impl_intro_r, pure_elim_r=>-[->].
      + rewrite (forall_elim y) /=. by eapply impl_elim, pure_intro.
200
201
  Qed.
End list2.
202

203
(** ** Big ops over finite maps *)
204
205
206
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
207
  Implicit Types Φ Ψ : K  A  uPred M.
208

209
  Lemma big_sepM_mono Φ Ψ m1 m2 :
210
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
211
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
212
  Proof.
213
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
214
    - rewrite /big_opM. by apply big_sepL_submseteq, map_to_list_submseteq.
215
    - apply big_opM_forall; apply _ || auto.
216
  Qed.
217
218
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
219
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
220
  Proof. apply big_opM_proper. Qed.
221

222
223
  Global Instance big_sepM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
224
           (big_opM (@uPred_sep M) (K:=K) (A:=A)).
225
  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
226

227
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
228
  Proof. by rewrite big_opM_empty. Qed.
229
230
  Lemma big_sepM_empty' P Φ : P  [ map] kx  , Φ k x.
  Proof. rewrite big_sepM_empty. apply True_intro. Qed.
231

232
  Lemma big_sepM_insert Φ m i x :
233
    m !! i = None 
234
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
235
  Proof. apply big_opM_insert. Qed.
236

237
  Lemma big_sepM_delete Φ m i x :
238
    m !! i = Some x 
239
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
240
  Proof. apply big_opM_delete. Qed.
241

242
243
244
245
246
247
248
  Lemma big_sepM_lookup_acc Φ m i x :
    m !! i = Some x 
    ([ map] ky  m, Φ k y)  Φ i x  (Φ i x - ([ map] ky  m, Φ k y)).
  Proof.
    intros. rewrite big_sepM_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

249
  Lemma big_sepM_lookup Φ m i x :
250
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
251
  Proof. intros. by rewrite big_sepM_lookup_acc // sep_elim_l. Qed.
252

Robbert Krebbers's avatar
Robbert Krebbers committed
253
254
255
  Lemma big_sepM_lookup_dom (Φ : K  uPred M) m i :
    is_Some (m !! i)  ([ map] k_  m, Φ k)  Φ i.
  Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
256

257
  Lemma big_sepM_singleton Φ i x : ([ map] ky  {[i:=x]}, Φ k y)  Φ i x.
258
  Proof. by rewrite big_opM_singleton. Qed.
259

260
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
261
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
262
  Proof. by rewrite big_opM_fmap. Qed.
263

Robbert Krebbers's avatar
Robbert Krebbers committed
264
265
266
  Lemma big_sepM_insert_override Φ m i x x' :
    m !! i = Some x  (Φ i x  Φ i x') 
    ([ map] ky  <[i:=x']> m, Φ k y)  ([ map] ky  m, Φ k y).
267
  Proof. apply big_opM_insert_override. Qed.
268

Robbert Krebbers's avatar
Robbert Krebbers committed
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
  Lemma big_sepM_insert_override_1 Φ m i x x' :
    m !! i = Some x 
    ([ map] ky  <[i:=x']> m, Φ k y) 
      (Φ i x' - Φ i x) - ([ map] ky  m, Φ k y).
  Proof.
    intros ?. apply wand_intro_l.
    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
    by rewrite assoc wand_elim_l -big_sepM_delete.
  Qed.

  Lemma big_sepM_insert_override_2 Φ m i x x' :
    m !! i = Some x 
    ([ map] ky  m, Φ k y) 
      (Φ i x - Φ i x') - ([ map] ky  <[i:=x']> m, Φ k y).
  Proof.
    intros ?. apply wand_intro_l.
    rewrite {1}big_sepM_delete //; rewrite assoc wand_elim_l.
    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
  Qed.

289
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
290
    m !! i = None 
291
292
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
293
  Proof. apply big_opM_fn_insert. Qed.
294

295
296
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
297
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
298
  Proof. apply big_opM_fn_insert'. Qed.
299

300
  Lemma big_sepM_sepM Φ Ψ m :
301
    ([ map] kx  m, Φ k x  Ψ k x)
302
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
303
  Proof. apply big_opM_opM. Qed.
304

305
306
307
308
309
  Lemma big_sepM_and Φ Ψ m :
    ([ map] kx  m, Φ k x  Ψ k x)
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
  Proof. auto using big_sepM_mono with I. Qed.

310
  Lemma big_sepM_later Φ m :
311
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
312
  Proof. apply (big_opM_commute _). Qed.
313

Robbert Krebbers's avatar
Robbert Krebbers committed
314
315
316
317
  Lemma big_sepM_laterN Φ n m :
    ^n ([ map] kx  m, Φ k x)  ([ map] kx  m, ^n Φ k x).
  Proof. apply (big_opM_commute _). Qed.

318
  Lemma big_sepM_persistently Φ m :
319
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
320
  Proof. apply (big_opM_commute _). Qed.
321

322
  Lemma big_sepM_persistently_if p Φ m :
323
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
324
  Proof. apply (big_opM_commute _). Qed.
325
326

  Lemma big_sepM_forall Φ m :
327
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
328
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
329
330
331
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
332
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
333
    induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
334
    rewrite big_sepM_insert // -and_sep_l. apply and_intro.
335
    - rewrite (forall_elim i) (forall_elim x) lookup_insert.
336
      by rewrite pure_True // True_impl.
337
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
338
339
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
340
      by rewrite pure_True // True_impl.
341
342
343
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
344
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
345
     [ map] kx  m, Ψ k x.
346
  Proof.
347
348
    rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
    setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
349
    rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
350
    by rewrite persistently_impl_wand persistently_elim wand_elim_l.
351
  Qed.
352

353
354
355
356
357
358
  Global Instance big_sepM_empty_plain Φ : Plain ([ map] kx  , Φ k x).
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
  Global Instance big_sepM_plain Φ m :
    ( k x, Plain (Φ k x))  Plain ([ map] kx  m, Φ k x).
  Proof. intros. apply big_sepL_plain=> _ [??]; apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
359
  Global Instance big_sepM_empty_persistent Φ :
360
    Persistent ([ map] kx  , Φ k x).
361
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
362
  Global Instance big_sepM_persistent Φ m :
363
    ( k x, Persistent (Φ k x))  Persistent ([ map] kx  m, Φ k x).
364
  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
365

Robbert Krebbers's avatar
Robbert Krebbers committed
366
  Global Instance big_sepM_nil_timeless Φ :
367
    Timeless ([ map] kx  , Φ k x).
368
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
369
  Global Instance big_sepM_timeless Φ m :
370
    ( k x, Timeless (Φ k x))  Timeless ([ map] kx  m, Φ k x).
371
  Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
372
373
End gmap.

374

375
(** ** Big ops over finite sets *)
376
377
378
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
379
  Implicit Types Φ : A  uPred M.
380

381
  Lemma big_sepS_mono Φ Ψ X Y :
382
    Y  X  ( x, x  Y  Φ x  Ψ x) 
383
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
384
  Proof.
385
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
386
    - rewrite /big_opM. by apply big_sepL_submseteq, elements_submseteq.
387
    - apply big_opS_forall; apply _ || auto.
388
  Qed.
389
390
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
391
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
392
  Proof. apply big_opS_proper. Qed.
393

394
  Global Instance big_sepS_mono' :
395
     Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opS (@uPred_sep M) (A:=A)).
396
  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
397

398
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
399
  Proof. by rewrite big_opS_empty. Qed.
400
401
  Lemma big_sepS_empty' P Φ : P  [ set] x  , Φ x.
  Proof. rewrite big_sepS_empty. apply True_intro. Qed.
402

403
  Lemma big_sepS_insert Φ X x :
404
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
405
  Proof. apply big_opS_insert. Qed.
406

407
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
408
    x  X 
409
410
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
411
  Proof. apply big_opS_fn_insert. Qed.
412

413
  Lemma big_sepS_fn_insert' Φ X x P :
414
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
415
  Proof. apply big_opS_fn_insert'. Qed.
416

Robbert Krebbers's avatar
Robbert Krebbers committed
417
418
419
  Lemma big_sepS_union Φ X Y :
    X  Y 
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
420
  Proof. apply big_opS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
421

422
  Lemma big_sepS_delete Φ X x :
423
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
424
  Proof. apply big_opS_delete. Qed.
425

426
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
427
  Proof. intros. rewrite big_sepS_delete //. auto with I. Qed.
428

429
430
431
432
433
434
435
  Lemma big_sepS_elem_of_acc Φ X x :
    x  X 
    ([ set] y  X, Φ y)  Φ x  (Φ x - ([ set] y  X, Φ y)).
  Proof.
    intros. rewrite big_sepS_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

436
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
437
  Proof. apply big_opS_singleton. Qed.
438

439
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
Ralf Jung's avatar
Ralf Jung committed
440
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
441
442
443
444
445
446
447
448
449
450
451
  Proof.
    induction X as [|x X ? IH] using collection_ind_L.
    { by rewrite filter_empty_L !big_sepS_empty. }
    destruct (decide (P x)).
    - rewrite filter_union_L filter_singleton_L //.
      rewrite !big_sepS_insert //; last set_solver.
      by rewrite IH pure_True // left_id.
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
      by rewrite !big_sepS_insert // IH pure_False // False_impl left_id.
  Qed.

452
453
454
455
456
457
458
459
460
461
462
  Lemma big_sepS_filter_acc (P : A  Prop) `{ y, Decision (P y)} Φ X Y :
    ( y, y  Y  P y  y  X) 
    ([ set] y  X, Φ y) -
      ([ set] y  Y, P y  Φ y) 
      (([ set] y  Y, P y  Φ y) - [ set] y  X, Φ y).
  Proof.
    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
      as (Z&->&?); first set_solver.
    rewrite big_sepS_union // big_sepS_filter. by apply sep_mono_r, wand_intro_l.
  Qed.

463
  Lemma big_sepS_sepS Φ Ψ X :
464
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
465
  Proof. apply big_opS_opS. Qed.
466

467
468
469
470
  Lemma big_sepS_and Φ Ψ X :
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
  Proof. auto using big_sepS_mono with I. Qed.

471
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
472
  Proof. apply (big_opS_commute _). Qed.
473

Robbert Krebbers's avatar
Robbert Krebbers committed
474
475
476
477
  Lemma big_sepS_laterN Φ n X :
    ^n ([ set] y  X, Φ y)  ([ set] y  X, ^n Φ y).
  Proof. apply (big_opS_commute _). Qed.

478
  Lemma big_sepS_persistently Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
479
  Proof. apply (big_opS_commute _). Qed.
480

481
  Lemma big_sepS_persistently_if q Φ X :
482
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
483
  Proof. apply (big_opS_commute _). Qed.
484
485

  Lemma big_sepS_forall Φ X :
486
    ( x, Persistent (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
487
488
489
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
490
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
491
    induction X as [|x X ? IH] using collection_ind_L.
492
    { rewrite big_sepS_empty; auto. }
493
    rewrite big_sepS_insert // -and_sep_l. apply and_intro.
494
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
495
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
496
      by rewrite pure_True ?True_impl; last set_solver.
497
498
499
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
500
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
501
  Proof.
502
503
    rewrite persistently_and_sep_l persistently_forall.
    setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
504
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
505
    by rewrite persistently_impl_wand persistently_elim wand_elim_l.
506
  Qed.
507

508
509
510
511
512
513
  Global Instance big_sepS_empty_plain Φ : Plain ([ set] x  , Φ x).
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
  Global Instance big_sepS_plain Φ X :
    ( x, Plain (Φ x))  Plain ([ set] x  X, Φ x).
  Proof. rewrite /big_opS. apply _. Qed.

514
  Global Instance big_sepS_empty_persistent Φ : Persistent ([ set] x  , Φ x).
515
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
516
  Global Instance big_sepS_persistent Φ X :
517
    ( x, Persistent (Φ x))  Persistent ([ set] x  X, Φ x).
518
  Proof. rewrite /big_opS. apply _. Qed.
519

520
  Global Instance big_sepS_nil_timeless Φ : Timeless ([ set] x  , Φ x).
521
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
522
  Global Instance big_sepS_timeless Φ X :
523
    ( x, Timeless (Φ x))  Timeless ([ set] x  X, Φ x).
524
  Proof. rewrite /big_opS. apply _. Qed.
525
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
526

Robbert Krebbers's avatar
Robbert Krebbers committed
527
528
Lemma big_sepM_dom `{Countable K} {A} (Φ : K  uPred M) (m : gmap K A) :
  ([ map] k_  m, Φ k)  ([ set] k  dom _ m, Φ k).
529
Proof. apply big_opM_dom. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
530

Robbert Krebbers's avatar
Robbert Krebbers committed
531
532
533
534
535
536
537
538
539
540
541
542

(** ** Big ops over finite multisets *)
Section gmultiset.
  Context `{Countable A}.
  Implicit Types X : gmultiset A.
  Implicit Types Φ : A  uPred M.

  Lemma big_sepMS_mono Φ Ψ X Y :
    Y  X  ( x, x  Y  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  [ mset] x  Y, Ψ x.
  Proof.
    intros HX HΦ. trans ([ mset] x  Y, Φ x)%I.
543
    - rewrite /big_opM. by apply big_sepL_submseteq, gmultiset_elements_submseteq.
Robbert Krebbers's avatar
Robbert Krebbers committed
544
545
546
547
548
    - apply big_opMS_forall; apply _ || auto.
  Qed.
  Lemma big_sepMS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  ([ mset] x  X, Ψ x).
549
  Proof. apply big_opMS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
550

551
  Global Instance big_sepMS_mono' :
552
     Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opMS (@uPred_sep M) (A:=A)).
553
  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
555
556

  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  True.
  Proof. by rewrite big_opMS_empty. Qed.
557
558
  Lemma big_sepMS_empty' P Φ : P  [ mset] x  , Φ x.
  Proof. rewrite big_sepMS_empty. apply True_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
559
560
561

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
562
  Proof. apply big_opMS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
564
565

  Lemma big_sepMS_delete Φ X x :
    x  X  ([ mset] y  X, Φ y)  Φ x  [ mset] y  X  {[ x ]}, Φ y.
566
  Proof. apply big_opMS_delete. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
567
568

  Lemma big_sepMS_elem_of Φ X x : x  X  ([ mset] y  X, Φ y)  Φ x.
569
  Proof. intros. by rewrite big_sepMS_delete // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
570

571
572
573
574
575
576
577
  Lemma big_sepMS_elem_of_acc Φ X x :
    x  X 
    ([ mset] y  X, Φ y)  Φ x  (Φ x - ([ mset] y  X, Φ y)).
  Proof.
    intros. rewrite big_sepMS_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
578
  Lemma big_sepMS_singleton Φ x : ([ mset] y  {[ x ]}, Φ y)  Φ x.
579
  Proof. apply big_opMS_singleton. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
580
581
582

  Lemma big_sepMS_sepMS Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
583
  Proof. apply big_opMS_opMS. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
584

585
586
587
588
  Lemma big_sepMS_and Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
  Proof. auto using big_sepMS_mono with I. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
589
590
591
  Lemma big_sepMS_later Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
  Proof. apply (big_opMS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
592
593
594
595
  Lemma big_sepMS_laterN Φ n X :
    ^n ([ mset] y  X, Φ y)  ([ mset] y  X, ^n Φ y).
  Proof. apply (big_opMS_commute _). Qed.

596
  Lemma big_sepMS_persistently Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
597
598
  Proof. apply (big_opMS_commute _). Qed.

599
  Lemma big_sepMS_persistently_if q Φ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
600
601
602
    ?q ([ mset] y  X, Φ y)  ([ mset] y  X, ?q Φ y).
  Proof. apply (big_opMS_commute _). Qed.

603
604
605
606
607
608
  Global Instance big_sepMS_empty_plain Φ : Plain ([ mset] x  , Φ x).