big_op.v 36.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.algebra Require Export big_op.
2
From iris.bi Require Import derived_laws_sbi plainly.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From stdpp Require Import countable fin_collections functions.
4
Set Default Proof Using "Type".
5
Import interface.bi derived_laws_bi.bi.
6

7
(* Notations *)
Ralf Jung's avatar
Ralf Jung committed
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
  (big_opL bi_sep (λ k x, P) l) : bi_scope.
Notation "'[∗' 'list]' x ∈ l , P" :=
  (big_opL bi_sep (λ _ x, P) l) : bi_scope.

Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope.

Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
  (big_opL bi_and (λ k x, P) l) : bi_scope.
Notation "'[∧' 'list]' x ∈ l , P" :=
  (big_opL bi_and (λ _ x, P) l) : bi_scope.

Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps) : bi_scope.

Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m) : bi_scope.
Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m) : bi_scope.

Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X) : bi_scope.

Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scope.
28

29
(** * Properties *)
Robbert Krebbers's avatar
Robbert Krebbers committed
30
31
32
Section bi_big_op.
Context {PROP : bi}.
Implicit Types Ps Qs : list PROP.
33
34
Implicit Types A : Type.

35
(** ** Big ops over lists *)
36
Section sep_list.
37
38
  Context {A : Type}.
  Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
  Implicit Types Φ Ψ : nat  A  PROP.
40

Robbert Krebbers's avatar
Robbert Krebbers committed
41
  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y)  emp.
42
  Proof. done. Qed.
43
  Lemma big_sepL_nil' `{BiAffine PROP} P Φ : P  [ list] ky  nil, Φ k y.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  Proof. apply (affine _). Qed.
45
  Lemma big_sepL_cons Φ x l :
46
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
47
  Proof. by rewrite big_opL_cons. Qed.
48
  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
49
50
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
51
52
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
53
54
  Proof. by rewrite big_opL_app. Qed.

55
56
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
57
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
58
  Proof. apply big_opL_forall; apply _. Qed.
59
60
  Lemma big_sepL_proper Φ Ψ 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_proper. Qed.
63
  Lemma big_sepL_submseteq `{BiAffine PROP} (Φ : A  PROP) l1 l2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
64
    l1 + l2  ([ list] y  l2, Φ y)  [ list] y  l1, Φ y.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
66
67
  Proof.
    intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l.
  Qed.
68

69
70
  Global Instance big_sepL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
71
           (big_opL (@bi_sep PROP) (A:=A)).
72
  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
73
  Global Instance big_sepL_id_mono' :
Robbert Krebbers's avatar
Robbert Krebbers committed
74
    Proper (Forall2 () ==> ()) (big_opL (@bi_sep M) (λ _ P, P)).
75
  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
76

77
  Lemma big_sepL_emp l : ([ list] ky  l, emp) @{PROP} emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
79
  Proof. by rewrite big_opL_unit. Qed.

80
81
82
83
  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.
84
85
86
    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.
87
88
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
89
  Lemma big_sepL_lookup Φ l i x `{!Absorbing (Φ i x)} :
90
    l !! i = Some x  ([ list] ky  l, Φ k y)  Φ i x.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
  Proof. intros. rewrite big_sepL_lookup_acc //. by rewrite sep_elim_l. Qed.
92

Robbert Krebbers's avatar
Robbert Krebbers committed
93
  Lemma big_sepL_elem_of (Φ : A  PROP) l x `{!Absorbing (Φ x)} :
94
    x  l  ([ list] y  l, Φ y)  Φ x.
95
96
97
  Proof.
    intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)).
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
98

Robbert Krebbers's avatar
Robbert Krebbers committed
99
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  PROP) l :
100
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
101
  Proof. by rewrite big_opL_fmap. Qed.
102
103

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

108
109
110
  Lemma big_sepL_and Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
112

113
  Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
114
    <pers> ([ list] kx  l, Φ k x)  [ list] kx  l, <pers> (Φ k x).
115
  Proof. apply (big_opL_commute _). Qed.
116

117
  Lemma big_sepL_forall `{BiAffine PROP} Φ l :
118
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
119
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
120
121
122
  Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepL_lookup. }
    revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ; [by auto using big_sepL_nil'|].
125
    rewrite big_sepL_cons. rewrite -persistent_and_sep; apply and_intro.
126
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
127
128
129
130
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Lemma big_sepL_impl Φ Ψ l :
Robbert Krebbers's avatar
Robbert Krebbers committed
131
    ([ list] kx  l, Φ k x) -
132
     ( k x, l !! k = Some x  Φ k x - Ψ k x) -
Robbert Krebbers's avatar
Robbert Krebbers committed
133
    [ list] kx  l, Ψ k x.
134
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
    apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=.
    { by rewrite sep_elim_r. }
137
    rewrite intuitionistically_sep_dup -assoc [( _  _)%I]comm -!assoc assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
    apply sep_mono.
    - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
140
      by rewrite intuitionistically_elim wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
141
    - rewrite comm -(IH (Φ  S) (Ψ  S)) /=.
142
      apply sep_mono_l, affinely_mono, persistently_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
      apply forall_intro=> k. by rewrite (forall_elim (S k)).
144
145
  Qed.

146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
  Lemma big_sepL_delete Φ l i x :
    l !! i = Some x 
    ([ list] ky  l, Φ k y)
     Φ i x  [ list] ky  l, if decide (k = i) then emp else Φ k y.
  Proof.
    intros. rewrite -(take_drop_middle l i x) // !big_sepL_app /= Nat.add_0_r.
    rewrite take_length_le; last eauto using lookup_lt_Some, Nat.lt_le_incl.
    rewrite decide_True // left_id.
    rewrite assoc -!(comm _ (Φ _ _)) -assoc. do 2 f_equiv.
    - apply big_sepL_proper=> k y Hk. apply lookup_lt_Some in Hk.
      rewrite take_length in Hk. by rewrite decide_False; last lia.
    - apply big_sepL_proper=> k y _. by rewrite decide_False; last lia.
  Qed.

  Lemma big_sepL_delete' `{!BiAffine PROP} Φ l i x :
    l !! i = Some x 
    ([ list] ky  l, Φ k y)  Φ i x  [ list] ky  l,  k  i   Φ k y.
  Proof.
    intros. rewrite big_sepL_delete //. (do 2 f_equiv)=> k y.
    rewrite -decide_emp. by repeat case_decide.
  Qed.

168
  Global Instance big_sepL_nil_persistent Φ :
169
    Persistent ([ list] kx  [], Φ k x).
170
  Proof. simpl; apply _. Qed.
171
  Global Instance big_sepL_persistent Φ l :
172
    ( k x, Persistent (Φ k x))  Persistent ([ list] kx  l, Φ k x).
173
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
174
  Global Instance big_sepL_persistent_id Ps :
175
    TCForall Persistent Ps  Persistent ([] Ps).
176
  Proof. induction 1; simpl; apply _. Qed.
177

178
179
180
  Global Instance big_sepL_nil_affine Φ :
    Affine ([ list] kx  [], Φ k x).
  Proof. simpl; apply _. Qed.
181
182
183
  Global Instance big_sepL_affine Φ l :
    ( k x, Affine (Φ k x))  Affine ([ list] kx  l, Φ k x).
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
184
185
  Global Instance big_sepL_affine_id Ps : TCForall Affine Ps  Affine ([] Ps).
  Proof. induction 1; simpl; apply _. Qed.
186
End sep_list.
187

188
Section sep_list2.
189
190
  Context {A : Type}.
  Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
  Implicit Types Φ Ψ : nat  A  PROP.
192
193
194
  (* 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
195
    ([ list] kx  zip_with f l1 l2, Φ k x)
Robbert Krebbers's avatar
Robbert Krebbers committed
196
     ([ list] kx  l1, if l2 !! k is Some y then Φ k (f x y) else emp).
197
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
200
    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=.
    - by rewrite big_sepL_emp left_id.
    - by rewrite IH.
201
  Qed.
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
End sep_list2.

Section and_list.
  Context {A : Type}.
  Implicit Types l : list A.
  Implicit Types Φ Ψ : nat  A  PROP.

  Lemma big_andL_nil Φ : ([ list] ky  nil, Φ k y)  True.
  Proof. done. Qed.
  Lemma big_andL_nil' P Φ : P  [ list] ky  nil, Φ k y.
  Proof. by apply pure_intro. Qed.
  Lemma big_andL_cons Φ x l :
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
  Proof. by rewrite big_opL_cons. Qed.
  Lemma big_andL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_andL_app Φ l1 l2 :
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
  Proof. by rewrite big_opL_app. Qed.

  Lemma big_andL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
  Proof. apply big_opL_forall; apply _. Qed.
  Lemma big_andL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
  Proof. apply big_opL_proper. Qed.
  Lemma big_andL_submseteq (Φ : A  PROP) l1 l2 :
    l1 + l2  ([ list] y  l2, Φ y)  [ list] y  l1, Φ y.
  Proof.
    intros [l ->]%submseteq_Permutation. by rewrite big_andL_app and_elim_l.
  Qed.

  Global Instance big_andL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
           (big_opL (@bi_and PROP) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
241
  Global Instance big_andL_id_mono' :
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
    Proper (Forall2 () ==> ()) (big_opL (@bi_and M) (λ _ P, P)).
  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

  Lemma big_andL_lookup Φ l i x `{!Absorbing (Φ i x)} :
    l !! i = Some x  ([ list] ky  l, Φ k y)  Φ i x.
  Proof.
    intros. rewrite -(take_drop_middle l i x) // big_andL_app /=.
    rewrite Nat.add_0_r take_length_le;
      eauto using lookup_lt_Some, Nat.lt_le_incl, and_elim_l', and_elim_r'.
  Qed.

  Lemma big_andL_elem_of (Φ : A  PROP) l x `{!Absorbing (Φ x)} :
    x  l  ([ list] y  l, Φ y)  Φ x.
  Proof.
    intros [i ?]%elem_of_list_lookup; eauto using (big_andL_lookup (λ _, Φ)).
  Qed.

  Lemma big_andL_fmap {B} (f : A  B) (Φ : nat  B  PROP) l :
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
  Proof. by rewrite big_opL_fmap. Qed.

  Lemma big_andL_andL Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
  Proof. by rewrite big_opL_opL. Qed.

  Lemma big_andL_and Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
  Proof. auto using and_intro, big_andL_mono, and_elim_l, and_elim_r. Qed.

  Lemma big_andL_persistently Φ l :
274
    <pers> ([ list] kx  l, Φ k x)  [ list] kx  l, <pers> (Φ k x).
275
276
  Proof. apply (big_opL_commute _). Qed.

277
  Lemma big_andL_forall `{BiAffine PROP} Φ l :
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
  Proof.
    apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_andL_lookup. }
    revert Φ. induction l as [|x l IH]=> Φ; [by auto using big_andL_nil'|].
    rewrite big_andL_cons. apply and_intro.
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Global Instance big_andL_nil_persistent Φ :
    Persistent ([ list] kx  [], Φ k x).
  Proof. simpl; apply _. Qed.
  Global Instance big_andL_persistent Φ l :
    ( k x, Persistent (Φ k x))  Persistent ([ list] kx  l, Φ k x).
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
295

296
End and_list.
297

298
(** ** Big ops over finite maps *)
299
300
301
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
  Implicit Types Φ Ψ : K  A  PROP.
303

Robbert Krebbers's avatar
Robbert Krebbers committed
304
305
306
307
  Lemma big_sepM_mono Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
    ([ map] k  x  m, Φ k x)  [ map] k  x  m, Ψ k x.
  Proof. apply big_opM_forall; apply _ || auto. Qed.
308
309
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
310
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
311
  Proof. apply big_opM_proper. Qed.
312
  Lemma big_sepM_subseteq `{BiAffine PROP} Φ m1 m2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
313
314
    m2  m1  ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Φ k x.
  Proof. intros. by apply big_sepL_submseteq, map_to_list_submseteq. Qed.
315

316
317
  Global Instance big_sepM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
318
319
           (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_sepM_mono=> ???; apply Hf. Qed.
320

Robbert Krebbers's avatar
Robbert Krebbers committed
321
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  emp.
322
  Proof. by rewrite big_opM_empty. Qed.
323
  Lemma big_sepM_empty' `{BiAffine PROP} P Φ : P  [ map] kx  , Φ k x.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
  Proof. rewrite big_sepM_empty. apply: affine. Qed.
325

326
  Lemma big_sepM_insert Φ m i x :
327
    m !! i = None 
328
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
329
  Proof. apply big_opM_insert. Qed.
330

331
  Lemma big_sepM_delete Φ m i x :
332
    m !! i = Some x 
333
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
334
  Proof. apply big_opM_delete. Qed.
335

336
337
338
339
340
341
342
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
343
  Lemma big_sepM_lookup Φ m i x `{!Absorbing (Φ i x)} :
344
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
  Proof. intros. rewrite big_sepM_lookup_acc //. by rewrite sep_elim_l. Qed.
346

Robbert Krebbers's avatar
Robbert Krebbers committed
347
  Lemma big_sepM_lookup_dom (Φ : K  PROP) m i `{!Absorbing (Φ i)} :
Robbert Krebbers's avatar
Robbert Krebbers committed
348
349
    is_Some (m !! i)  ([ map] k_  m, Φ k)  Φ i.
  Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
350

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

Robbert Krebbers's avatar
Robbert Krebbers committed
354
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  PROP) m :
355
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
356
  Proof. by rewrite big_opM_fmap. Qed.
357

Robbert Krebbers's avatar
Robbert Krebbers committed
358
359
360
  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).
361
  Proof. apply big_opM_insert_override. Qed.
362

Robbert Krebbers's avatar
Robbert Krebbers committed
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
  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.

Robbert Krebbers's avatar
Robbert Krebbers committed
383
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  PROP) (f : K  B) m i x b :
384
    m !! i = None 
385
386
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
387
  Proof. apply big_opM_fn_insert. Qed.
388

Robbert Krebbers's avatar
Robbert Krebbers committed
389
  Lemma big_sepM_fn_insert' (Φ : K  PROP) m i x P :
390
    m !! i = None 
391
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
392
  Proof. apply big_opM_fn_insert'. Qed.
393

394
  Lemma big_sepM_sepM Φ Ψ m :
395
    ([ map] kx  m, Φ k x  Ψ k x)
396
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
397
  Proof. apply big_opM_opM. Qed.
398

399
400
401
  Lemma big_sepM_and Φ Ψ m :
    ([ map] kx  m, Φ k x  Ψ k x)
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
Robbert Krebbers's avatar
Robbert Krebbers committed
402
  Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
403

404
  Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
405
    (<pers> ([ map] kx  m, Φ k x))  ([ map] kx  m, <pers> (Φ k x)).
406
  Proof. apply (big_opM_commute _). Qed.
407

408
  Lemma big_sepM_forall `{BiAffine PROP} Φ m :
409
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
410
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
411
412
413
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
414
415
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepM_lookup. }
    induction m as [|i x m ? IH] using map_ind; auto using big_sepM_empty'.
416
    rewrite big_sepM_insert // -persistent_and_sep. apply and_intro.
417
    - rewrite (forall_elim i) (forall_elim x) lookup_insert.
418
      by rewrite pure_True // True_impl.
419
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
420
421
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
422
      by rewrite pure_True // True_impl.
423
424
425
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Robbert Krebbers's avatar
Robbert Krebbers committed
426
    ([ map] kx  m, Φ k x) -
427
     ( k x, m !! k = Some x  Φ k x - Ψ k x) -
Robbert Krebbers's avatar
Robbert Krebbers committed
428
    [ map] kx  m, Ψ k x.
429
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
430
431
    apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
    { by rewrite sep_elim_r. }
432
    rewrite !big_sepM_insert // intuitionistically_sep_dup.
433
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
434
    - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
435
      by rewrite True_impl intuitionistically_elim wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
436
    - rewrite comm -IH /=.
437
      apply sep_mono_l, affinely_mono, persistently_mono, forall_mono=> k.
Robbert Krebbers's avatar
Robbert Krebbers committed
438
439
440
      apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
      by rewrite pure_True // True_impl.
441
  Qed.
442

443
  Global Instance big_sepM_empty_persistent Φ :
444
    Persistent ([ map] kx  , Φ k x).
445
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
446
  Global Instance big_sepM_persistent Φ m :
447
    ( k x, Persistent (Φ k x))  Persistent ([ map] kx  m, Φ k x).
448
  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
449

450
451
452
  Global Instance big_sepM_empty_affine Φ :
    Affine ([ map] kx  , Φ k x).
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
453
454
  Global Instance big_sepM_affine Φ m :
    ( k x, Affine (Φ k x))  Affine ([ map] kx  m, Φ k x).
455
  Proof. intros. apply big_sepL_affine=> _ [??]; apply _. Qed.
456
457
End gmap.

458
(** ** Big ops over finite sets *)
459
460
461
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
  Implicit Types Φ : A  PROP.
463

Robbert Krebbers's avatar
Robbert Krebbers committed
464
465
466
467
  Lemma big_sepS_mono Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
  Proof. intros. apply big_opS_forall; apply _ || auto. Qed.
468
469
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
470
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
471
  Proof. apply big_opS_proper. Qed.
472
  Lemma big_sepS_subseteq `{BiAffine PROP} Φ X Y :
Robbert Krebbers's avatar
Robbert Krebbers committed
473
474
    Y  X  ([ set] x  X, Φ x)  [ set] x  Y, Φ x.
  Proof. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
475

476
  Global Instance big_sepS_mono' :
Robbert Krebbers's avatar
Robbert Krebbers committed
477
478
     Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opS (@bi_sep PROP) (A:=A)).
  Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
479

Robbert Krebbers's avatar
Robbert Krebbers committed
480
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  emp.
481
  Proof. by rewrite big_opS_empty. Qed.
482
  Lemma big_sepS_empty' `{!BiAffine PROP} P Φ : P  [ set] x  , Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
483
  Proof. rewrite big_sepS_empty. apply: affine. Qed.
484

485
  Lemma big_sepS_insert Φ X x :
486
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
487
  Proof. apply big_opS_insert. Qed.
488

Robbert Krebbers's avatar
Robbert Krebbers committed
489
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  PROP) f X x b :
490
    x  X 
491
492
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
493
  Proof. apply big_opS_fn_insert. Qed.
494

495
  Lemma big_sepS_fn_insert' Φ X x P :
496
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
497
  Proof. apply big_opS_fn_insert'. Qed.
498

Robbert Krebbers's avatar
Robbert Krebbers committed
499
  Lemma big_sepS_union Φ X Y :
500
    X ## Y 
Robbert Krebbers's avatar
Robbert Krebbers committed
501
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
502
  Proof. apply big_opS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
503

504
  Lemma big_sepS_delete Φ X x :
505
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
506
  Proof. apply big_opS_delete. Qed.
507

Robbert Krebbers's avatar
Robbert Krebbers committed
508
509
  Lemma big_sepS_elem_of Φ X x `{!Absorbing (Φ x)} :
    x  X  ([ set] y  X, Φ y)  Φ x.
Robbert Krebbers's avatar
Robbert Krebbers committed
510
  Proof. intros. rewrite big_sepS_delete //. by rewrite sep_elim_l. Qed.
511

512
513
514
515
516
517
518
  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.

519
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
520
  Proof. apply big_opS_singleton. Qed.
521

Robbert Krebbers's avatar
Robbert Krebbers committed
522
523
524
  Lemma big_sepS_filter' (P : A  Prop) `{ x, Decision (P x)} Φ X :
    ([ set] y  filter P X, Φ y)
     ([ set] y  X, if decide (P y) then Φ y else emp).
525
526
527
528
529
530
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
531
      by rewrite decide_True // IH.
532
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
533
      by rewrite !big_sepS_insert // decide_False // IH left_id.
534
535
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
536
  Lemma big_sepS_filter_acc' (P : A  Prop) `{ y, Decision (P y)} Φ X Y :
537
538
    ( y, y  Y  P y  y  X) 
    ([ set] y  X, Φ y) -
Robbert Krebbers's avatar
Robbert Krebbers committed
539
540
      ([ set] y  Y, if decide (P y) then Φ y else emp) 
      (([ set] y  Y, if decide (P y) then Φ y else emp) - [ set] y  X, Φ y).
541
542
543
  Proof.
    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
      as (Z&->&?); first set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
544
545
    rewrite big_sepS_union // big_sepS_filter'.
    by apply sep_mono_r, wand_intro_l.
546
547
  Qed.

548
  Lemma big_sepS_filter `{BiAffine PROP}
Robbert Krebbers's avatar
Robbert Krebbers committed
549
550
551
552
      (P : A  Prop) `{ x, Decision (P x)} Φ X :
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
  Proof. setoid_rewrite <-decide_emp. apply big_sepS_filter'. Qed.

553
  Lemma big_sepS_filter_acc `{BiAffine PROP}
Robbert Krebbers's avatar
Robbert Krebbers committed
554
555
556
557
558
559
560
      (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. setoid_rewrite <-decide_emp. by apply big_sepS_filter_acc'. Qed.

561
  Lemma big_sepS_sepS Φ Ψ X :
562
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
563
  Proof. apply big_opS_opS. Qed.
564

565
566
  Lemma big_sepS_and Φ Ψ X :
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
567
  Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
568

569
  Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
570
    <pers> ([ set] y  X, Φ y)  [ set] y  X, <pers> (Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
571
572
  Proof. apply (big_opS_commute _). Qed.

573
  Lemma big_sepS_forall `{BiAffine PROP} Φ X :
574
    ( x, Persistent (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
575
576
577
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
578
579
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepS_elem_of. }
    induction X as [|x X ? IH] using collection_ind_L; auto using big_sepS_empty'.
580
    rewrite big_sepS_insert // -persistent_and_sep. apply and_intro.
581
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
582
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
583
      by rewrite pure_True ?True_impl; last set_solver.
584
585
586
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
587
    ([ set] x  X, Φ x) -
588
     ( x, x  X  Φ x - Ψ x) -
Robbert Krebbers's avatar
Robbert Krebbers committed
589
    [ set] x  X, Ψ x.
590
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
591
592
    apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
    { by rewrite sep_elim_r. }
593
    rewrite !big_sepS_insert // intuitionistically_sep_dup.
594
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
595
    - rewrite (forall_elim x) pure_True; last set_solver.
596
      by rewrite True_impl intuitionistically_elim wand_elim_l.
597
    - rewrite comm -IH /=. apply sep_mono_l, affinely_mono, persistently_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
598
599
      apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_True ?True_impl; last set_solver.
600
  Qed.
601

602
  Global Instance big_sepS_empty_persistent Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
603
    Persistent ([ set] x  , Φ x).
604
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
605
  Global Instance big_sepS_persistent Φ X :
606
    ( x, Persistent (Φ x))  Persistent ([ set] x  X, Φ x).
607
  Proof. rewrite /big_opS. apply _. Qed.
608

609
610
  Global Instance big_sepS_empty_affine Φ : Affine ([ set] x  , Φ x).
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
611
612
613
  Global Instance big_sepS_affine Φ X :
    ( x, Affine (Φ x))  Affine ([ set] x  X, Φ x).
  Proof. rewrite /big_opS. apply _. Qed.
614
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
615

Robbert Krebbers's avatar
Robbert Krebbers committed
616
Lemma big_sepM_dom `{Countable K} {A} (Φ : K  PROP) (m : gmap K A) :
Robbert Krebbers's avatar
Robbert Krebbers committed
617
  ([ map] k_  m, Φ k)  ([ set] k  dom _ m, Φ k).
618
Proof. apply big_opM_dom. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
619

Robbert Krebbers's avatar
Robbert Krebbers committed
620
621
622
623
(** ** Big ops over finite multisets *)
Section gmultiset.
  Context `{Countable A}.
  Implicit Types X : gmultiset A.
Robbert Krebbers's avatar
Robbert Krebbers committed
624
  Implicit Types Φ : A  PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
625

Robbert Krebbers's avatar
Robbert Krebbers committed
626
627
628
629
  Lemma big_sepMS_mono Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  [ mset] x  X, Ψ x.
  Proof. intros. apply big_opMS_forall; apply _ || auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
630
631
632
  Lemma big_sepMS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  ([ mset] x  X, Ψ x).
633
  Proof. apply big_opMS_proper. Qed.
634
  Lemma big_sepMS_subseteq `{BiAffine PROP} Φ X Y :
Robbert Krebbers's avatar
Robbert Krebbers committed
635
636
    Y  X  ([ mset] x  X, Φ x)  [ mset] x  Y, Φ x.
  Proof. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
637

638
  Global Instance big_sepMS_mono' :