big_op.v 25.1 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_always Φ l :
121
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
122
  Proof. apply (big_opL_commute _). Qed.
123
124

  Lemma big_sepL_always_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
129

  Lemma big_sepL_forall Φ l :
    ( k x, PersistentP (Φ 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
137
  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. }
    rewrite big_sepL_cons. rewrite -always_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
146
147
148
149
150
151
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
    setoid_rewrite always_impl; setoid_rewrite always_pure.
    rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.

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

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

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

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

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

212
213
  Global Instance big_sepM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
214
           (big_opM (@uPred_sep M) (A:=A)).
215
  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
216

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

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

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

232
233
234
235
236
237
238
  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.

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

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

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

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

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

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

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

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

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

295
296
297
298
299
  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.

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

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

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

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

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

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
334
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
335
     [ map] kx  m, Ψ k x.
336
337
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
338
    setoid_rewrite always_impl; setoid_rewrite always_pure.
339
340
341
    rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
342

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

357

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

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

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

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

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

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

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

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

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

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

412
413
414
415
416
417
418
  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.

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

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

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

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

450
451
452
453
  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.

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

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

461
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
462
  Proof. apply (big_opS_commute _). Qed.
463

464
  Lemma big_sepS_always_if q Φ X :
465
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
466
  Proof. apply (big_opS_commute _). Qed.
467
468

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

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
483
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
484
485
  Proof.
    rewrite always_and_sep_l always_forall.
486
    setoid_rewrite always_impl; setoid_rewrite always_pure.
487
488
489
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
490

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

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

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

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

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

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
  Lemma big_sepMS_always Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
  Proof. apply (big_opMS_commute _). Qed.

  Lemma big_sepMS_always_if q Φ X :
    ?q ([ mset] y  X, Φ y)  ([ mset] y  X, ?q Φ y).
  Proof. apply (big_opMS_commute _). Qed.

  Global Instance big_sepMS_empty_persistent Φ : PersistentP ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
  Global Instance big_sepMS_nil_timeless Φ : TimelessP ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
590
End big_op.
591

592
Hint Resolve big_sepM_empty' big_sepS_empty' big_sepMS_empty' | 0.