big_op.v 25.3 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.

Robbert Krebbers's avatar
Robbert Krebbers committed
152
  Global Instance big_sepL_nil_persistent Φ :
153
    Persistent ([ list] kx  [], Φ k x).
154
  Proof. simpl; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
  Global Instance big_sepL_persistent Φ l :
156
    ( k x, Persistent (Φ k x))  Persistent ([ list] kx  l, Φ k x).
157
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
158
  Global Instance big_sepL_persistent_id Ps :
159
    TCForall Persistent Ps  Persistent ([] Ps).
160
  Proof. induction 1; simpl; apply _. Qed.
161

Robbert Krebbers's avatar
Robbert Krebbers committed
162
  Global Instance big_sepL_nil_timeless Φ :
163
    Timeless ([ list] kx  [], Φ k x).
164
  Proof. simpl; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  Global Instance big_sepL_timeless Φ l :
166
    ( k x, Timeless (Φ k x))  Timeless ([ list] kx  l, Φ k x).
167
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
168
  Global Instance big_sepL_timeless_id Ps :
169
    TCForall Timeless Ps  Timeless ([] Ps).
170
  Proof. induction 1; simpl; apply _. Qed.
171
172
End list.

173
174
175
176
177
178
179
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
180
181
    ([ list] kx  zip_with f l1 l2, Φ k x)
     ([ list] kx  l1,  y, l2 !! k = Some y  Φ k (f x y)).
182
  Proof.
183
    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //.
184
    - apply (anti_symm _), True_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
185
186
187
188
      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.
189
    - rewrite /= IH. apply sep_proper=> //. apply (anti_symm _).
Robbert Krebbers's avatar
Robbert Krebbers committed
190
191
      + apply forall_intro=>z /=. by apply impl_intro_r, pure_elim_r=>-[->].
      + rewrite (forall_elim y) /=. by eapply impl_elim, pure_intro.
192
193
  Qed.
End list2.
194

195
(** ** Big ops over finite maps *)
196
197
198
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
199
  Implicit Types Φ Ψ : K  A  uPred M.
200

201
  Lemma big_sepM_mono Φ Ψ m1 m2 :
202
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
203
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
204
  Proof.
205
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
206
    - rewrite /big_opM. by apply big_sepL_submseteq, map_to_list_submseteq.
207
    - apply big_opM_forall; apply _ || auto.
208
  Qed.
209
210
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
211
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
212
  Proof. apply big_opM_proper. Qed.
213

214
215
  Global Instance big_sepM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
216
           (big_opM (@uPred_sep M) (K:=K) (A:=A)).
217
  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
218

219
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
220
  Proof. by rewrite big_opM_empty. Qed.
221
222
  Lemma big_sepM_empty' P Φ : P  [ map] kx  , Φ k x.
  Proof. rewrite big_sepM_empty. apply True_intro. Qed.
223

224
  Lemma big_sepM_insert Φ m i x :
225
    m !! i = None 
226
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
227
  Proof. apply big_opM_insert. Qed.
228

229
  Lemma big_sepM_delete Φ m i x :
230
    m !! i = Some x 
231
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
232
  Proof. apply big_opM_delete. Qed.
233

234
235
236
237
238
239
240
  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.

241
  Lemma big_sepM_lookup Φ m i x :
242
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
243
  Proof. intros. by rewrite big_sepM_lookup_acc // sep_elim_l. Qed.
244

Robbert Krebbers's avatar
Robbert Krebbers committed
245
246
247
  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.
248

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

252
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
253
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
254
  Proof. by rewrite big_opM_fmap. Qed.
255

Robbert Krebbers's avatar
Robbert Krebbers committed
256
257
258
  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).
259
  Proof. apply big_opM_insert_override. Qed.
260

Robbert Krebbers's avatar
Robbert Krebbers committed
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
  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.

281
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
282
    m !! i = None 
283
284
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
285
  Proof. apply big_opM_fn_insert. Qed.
286

287
288
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
289
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
290
  Proof. apply big_opM_fn_insert'. Qed.
291

292
  Lemma big_sepM_sepM Φ Ψ m :
293
    ([ map] kx  m, Φ k x  Ψ k x)
294
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
295
  Proof. apply big_opM_opM. Qed.
296

297
298
299
300
301
  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.

302
  Lemma big_sepM_later Φ m :
303
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
304
  Proof. apply (big_opM_commute _). Qed.
305

Robbert Krebbers's avatar
Robbert Krebbers committed
306
307
308
309
  Lemma big_sepM_laterN Φ n m :
    ^n ([ map] kx  m, Φ k x)  ([ map] kx  m, ^n Φ k x).
  Proof. apply (big_opM_commute _). Qed.

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

314
  Lemma big_sepM_persistently_if p Φ m :
315
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
316
  Proof. apply (big_opM_commute _). Qed.
317
318

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

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
336
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
337
     [ map] kx  m, Ψ k x.
338
  Proof.
339
340
    rewrite persistently_and_sep_l. do 2 setoid_rewrite persistently_forall.
    setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
341
    rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
342
    by rewrite persistently_impl_wand persistently_elim wand_elim_l.
343
  Qed.
344

Robbert Krebbers's avatar
Robbert Krebbers committed
345
  Global Instance big_sepM_empty_persistent Φ :
346
    Persistent ([ map] kx  , Φ k x).
347
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
348
  Global Instance big_sepM_persistent Φ m :
349
    ( k x, Persistent (Φ k x))  Persistent ([ map] kx  m, Φ k x).
350
  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
351
  Global Instance big_sepM_nil_timeless Φ :
352
    Timeless ([ map] kx  , Φ k x).
353
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
354
  Global Instance big_sepM_timeless Φ m :
355
    ( k x, Timeless (Φ k x))  Timeless ([ map] kx  m, Φ k x).
356
  Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
357
358
End gmap.

359

360
(** ** Big ops over finite sets *)
361
362
363
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
364
  Implicit Types Φ : A  uPred M.
365

366
  Lemma big_sepS_mono Φ Ψ X Y :
367
    Y  X  ( x, x  Y  Φ x  Ψ x) 
368
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
369
  Proof.
370
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
371
    - rewrite /big_opM. by apply big_sepL_submseteq, elements_submseteq.
372
    - apply big_opS_forall; apply _ || auto.
373
  Qed.
374
375
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
376
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
377
  Proof. apply big_opS_proper. Qed.
378

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

383
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
384
  Proof. by rewrite big_opS_empty. Qed.
385
386
  Lemma big_sepS_empty' P Φ : P  [ set] x  , Φ x.
  Proof. rewrite big_sepS_empty. apply True_intro. Qed.
387

388
  Lemma big_sepS_insert Φ X x :
389
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
390
  Proof. apply big_opS_insert. Qed.
391

392
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
393
    x  X 
394
395
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
396
  Proof. apply big_opS_fn_insert. Qed.
397

398
  Lemma big_sepS_fn_insert' Φ X x P :
399
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
400
  Proof. apply big_opS_fn_insert'. Qed.
401

Robbert Krebbers's avatar
Robbert Krebbers committed
402
403
404
  Lemma big_sepS_union Φ X Y :
    X  Y 
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
405
  Proof. apply big_opS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
406

407
  Lemma big_sepS_delete Φ X x :
408
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
409
  Proof. apply big_opS_delete. Qed.
410

411
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
412
  Proof. intros. rewrite big_sepS_delete //. auto with I. Qed.
413

414
415
416
417
418
419
420
  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.

421
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
422
  Proof. apply big_opS_singleton. Qed.
423

424
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
Ralf Jung's avatar
Ralf Jung committed
425
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
426
427
428
429
430
431
432
433
434
435
436
  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.

437
438
439
440
441
442
443
444
445
446
447
  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.

448
  Lemma big_sepS_sepS Φ Ψ X :
449
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
450
  Proof. apply big_opS_opS. Qed.
451

452
453
454
455
  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.

456
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
457
  Proof. apply (big_opS_commute _). Qed.
458

Robbert Krebbers's avatar
Robbert Krebbers committed
459
460
461
462
  Lemma big_sepS_laterN Φ n X :
    ^n ([ set] y  X, Φ y)  ([ set] y  X, ^n Φ y).
  Proof. apply (big_opS_commute _). Qed.

463
  Lemma big_sepS_persistently Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
464
  Proof. apply (big_opS_commute _). Qed.
465

466
  Lemma big_sepS_persistently_if q Φ X :
467
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
468
  Proof. apply (big_opS_commute _). Qed.
469
470

  Lemma big_sepS_forall Φ X :
471
    ( x, Persistent (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
472
473
474
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
475
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
476
    induction X as [|x X ? IH] using collection_ind_L.
477
    { rewrite big_sepS_empty; auto. }
478
    rewrite big_sepS_insert // -and_sep_l. apply and_intro.
479
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
480
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
481
      by rewrite pure_True ?True_impl; last set_solver.
482
483
484
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
485
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
486
  Proof.
487
488
    rewrite persistently_and_sep_l persistently_forall.
    setoid_rewrite persistently_impl; setoid_rewrite persistently_pure.
489
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
490
    by rewrite persistently_impl_wand persistently_elim wand_elim_l.
491
  Qed.
492

493
  Global Instance big_sepS_empty_persistent Φ : Persistent ([ set] x  , Φ x).
494
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
495
  Global Instance big_sepS_persistent Φ X :
496
    ( x, Persistent (Φ x))  Persistent ([ set] x  X, Φ x).
497
  Proof. rewrite /big_opS. apply _. Qed.
498
  Global Instance big_sepS_nil_timeless Φ : Timeless ([ set] x  , Φ x).
499
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
500
  Global Instance big_sepS_timeless Φ X :
501
    ( x, Timeless (Φ x))  Timeless ([ set] x  X, Φ x).
502
  Proof. rewrite /big_opS. apply _. Qed.
503
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
504

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

Robbert Krebbers's avatar
Robbert Krebbers committed
509
510
511
512
513
514
515
516
517
518
519
520

(** ** 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.
521
    - rewrite /big_opM. by apply big_sepL_submseteq, gmultiset_elements_submseteq.
Robbert Krebbers's avatar
Robbert Krebbers committed
522
523
524
525
526
    - 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).
527
  Proof. apply big_opMS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
528

529
  Global Instance big_sepMS_mono' :
530
     Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opMS (@uPred_sep M) (A:=A)).
531
  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
532
533
534

  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  True.
  Proof. by rewrite big_opMS_empty. Qed.
535
536
  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
537
538
539

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
540
  Proof. apply big_opMS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
541
542
543

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

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

549
550
551
552
553
554
555
  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
556
  Lemma big_sepMS_singleton Φ x : ([ mset] y  {[ x ]}, Φ y)  Φ x.
557
  Proof. apply big_opMS_singleton. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
558
559
560

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

563
564
565
566
  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
567
568
569
  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
570
571
572
573
  Lemma big_sepMS_laterN Φ n X :
    ^n ([ mset] y  X, Φ y)  ([ mset] y  X, ^n Φ y).
  Proof. apply (big_opMS_commute _). Qed.

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

577
  Lemma big_sepMS_persistently_if q Φ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
578
579
580
    ?q ([ mset] y  X, Φ y)  ([ mset] y  X, ?q Φ y).
  Proof. apply (big_opMS_commute _). Qed.

581
  Global Instance big_sepMS_empty_persistent Φ : Persistent ([ mset] x  , Φ x).
Robbert Krebbers's avatar
Robbert Krebbers committed
582
583
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_persistent Φ X :
584
    ( x, Persistent (Φ x))  Persistent ([ mset] x  X, Φ x).
Robbert Krebbers's avatar
Robbert Krebbers committed
585
  Proof. rewrite /big_opMS. apply _. Qed.
586
  Global Instance big_sepMS_nil_timeless Φ : Timeless ([ mset] x  , Φ x).
Robbert Krebbers's avatar
Robbert Krebbers committed
587
588
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_timeless Φ X :
589
    ( x, Timeless (Φ x))  Timeless ([ mset] x  X, Φ x).
Robbert Krebbers's avatar
Robbert Krebbers committed
590
591
  Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
592
End big_op.
593

594
Hint Resolve big_sepL_nil' big_sepM_empty' big_sepS_empty' big_sepMS_empty' | 0.