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

6
(* Notations *)
Robbert Krebbers's avatar
Robbert Krebbers committed
7
Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l)
8
  (at level 200, l at level 10, k, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10
   format "[∗  list]  k ↦ x  ∈  l ,  P") : bi_scope.
Notation "'[∗' 'list]' x ∈ l , P" := (big_opL bi_sep (λ _ x, P) l)
11
  (at level 200, l at level 10, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
12
   format "[∗  list]  x  ∈  l ,  P") : bi_scope.
13

14
Notation "'[∗]' Ps" :=
Robbert Krebbers's avatar
Robbert Krebbers committed
15
  (big_opL bi_sep (λ _ x, x) Ps) (at level 20) : bi_scope.
16

17
18
19
20
21
22
23
24
25
26
Notation "'[∧' 'list]' k ↦ x ∈ l , P" := (big_opL bi_and (λ k x, P) l)
  (at level 200, l at level 10, k, x at level 1, right associativity,
   format "[∧  list]  k ↦ x  ∈  l ,  P") : bi_scope.
Notation "'[∧' 'list]' x ∈ l , P" := (big_opL bi_and (λ _ x, P) l)
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[∧  list]  x  ∈  l ,  P") : bi_scope.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
27
Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m)
28
  (at level 200, m at level 10, k, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
29
30
   format "[∗  map]  k ↦ x  ∈  m ,  P") : bi_scope.
Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m)
31
  (at level 200, m at level 10, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
32
   format "[∗  map]  x  ∈  m ,  P") : bi_scope.
33

Robbert Krebbers's avatar
Robbert Krebbers committed
34
Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X)
35
  (at level 200, X at level 10, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
36
   format "[∗  set]  x  ∈  X ,  P") : bi_scope.
37

Robbert Krebbers's avatar
Robbert Krebbers committed
38
Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
Robbert Krebbers's avatar
Robbert Krebbers committed
39
  (at level 200, X at level 10, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
40
   format "[∗  mset]  x  ∈  X ,  P") : bi_scope.
41

42
(** * Properties *)
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
46
47
Module bi.
Import interface.bi derived.bi.
Section bi_big_op.
Context {PROP : bi}.
Implicit Types Ps Qs : list PROP.
48
49
Implicit Types A : Type.

50
(** ** Big ops over lists *)
51
Section sep_list.
52
53
  Context {A : Type}.
  Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  Implicit Types Φ Ψ : nat  A  PROP.
55

Robbert Krebbers's avatar
Robbert Krebbers committed
56
  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y)  emp.
57
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
  Lemma big_sepL_nil' `{AffineBI PROP} P Φ : P  [ list] ky  nil, Φ k y.
  Proof. apply (affine _). Qed.
60
  Lemma big_sepL_cons Φ x l :
61
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
62
  Proof. by rewrite big_opL_cons. Qed.
63
  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
64
65
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
66
67
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
68
69
  Proof. by rewrite big_opL_app. Qed.

70
71
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
72
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
73
  Proof. apply big_opL_forall; apply _. Qed.
74
75
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
76
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
77
  Proof. apply big_opL_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  Lemma big_sepL_submseteq `{AffineBI PROP} (Φ : A  PROP) l1 l2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
79
    l1 + l2  ([ list] y  l2, Φ y)  [ list] y  l1, Φ y.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
  Proof.
    intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l.
  Qed.
83

84
85
  Global Instance big_sepL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
86
           (big_opL (@bi_sep PROP) (A:=A)).
87
88
  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
  Global Instance big_sep_mono' :
Robbert Krebbers's avatar
Robbert Krebbers committed
89
    Proper (Forall2 () ==> ()) (big_opL (@bi_sep M) (λ _ P, P)).
90
  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
91

Robbert Krebbers's avatar
Robbert Krebbers committed
92
93
94
  Lemma big_sepL_emp l : ([ list] ky  l, emp)  (emp : PROP).
  Proof. by rewrite big_opL_unit. Qed.

95
96
97
98
  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.
99
100
101
    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.
102
103
  Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
108
  Lemma big_sepL_elem_of (Φ : A  PROP) l x `{!Absorbing (Φ x)} :
109
    x  l  ([ list] y  l, Φ y)  Φ x.
110
111
112
  Proof.
    intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)).
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
113

Robbert Krebbers's avatar
Robbert Krebbers committed
114
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  PROP) l :
115
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
116
  Proof. by rewrite big_opL_fmap. Qed.
117
118

  Lemma big_sepL_sepL Φ Ψ l :
119
120
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
121
  Proof. by rewrite big_opL_opL. Qed.
122

123
124
125
  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
126
  Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
127

Robbert Krebbers's avatar
Robbert Krebbers committed
128
  Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
129
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
130
  Proof. apply (big_opL_commute _). Qed.
131

Robbert Krebbers's avatar
Robbert Krebbers committed
132
  Lemma big_sepL_forall `{AffineBI PROP} Φ l :
133
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
134
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
135
136
137
  Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
      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'|].
140
    rewrite big_sepL_cons. rewrite -persistent_and_sep; apply and_intro.
141
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
142
143
144
145
    - 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
146
147
148
    ([ list] kx  l, Φ k x) -
     ( k x, l !! k = Some x  Φ k x - Ψ k x) -
    [ list] kx  l, Ψ k x.
149
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
154
155
156
157
158
    apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=.
    { by rewrite sep_elim_r. }
    rewrite bare_persistently_sep_dup -assoc [( _  _)%I]comm -!assoc assoc.
    apply sep_mono.
    - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
      by rewrite bare_persistently_elim wand_elim_l.
    - rewrite comm -(IH (Φ  S) (Ψ  S)) /=.
      apply sep_mono_l, bare_mono, persistently_mono.
      apply forall_intro=> k. by rewrite (forall_elim (S k)).
159
160
  Qed.

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

172
Section sep_list2.
173
174
  Context {A : Type}.
  Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  Implicit Types Φ Ψ : nat  A  PROP.
176
177
178
  (* 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
179
    ([ list] kx  zip_with f l1 l2, Φ k x)
Robbert Krebbers's avatar
Robbert Krebbers committed
180
     ([ list] kx  l1, if l2 !! k is Some y then Φ k (f x y) else emp).
181
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
182
183
184
    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=.
    - by rewrite big_sepL_emp left_id.
    - by rewrite IH.
185
  Qed.
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
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
241
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
274
275
276
277
278
279
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.
  Global Instance big_and_mono' :
    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 :
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
  Proof. apply (big_opL_commute _). Qed.

  Lemma big_andL_forall `{AffineBI PROP} Φ l :
    ([ 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.
End and_list.
280

281
(** ** Big ops over finite maps *)
282
283
284
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
Robbert Krebbers's avatar
Robbert Krebbers committed
285
  Implicit Types Φ Ψ : K  A  PROP.
286

Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
289
290
  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.
291
292
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
293
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
294
  Proof. apply big_opM_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
295
296
297
  Lemma big_sepM_subseteq `{AffineBI PROP} Φ m1 m2 :
    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.
298

299
300
  Global Instance big_sepM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
           (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_sepM_mono=> ???; apply Hf. Qed.
303

Robbert Krebbers's avatar
Robbert Krebbers committed
304
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  emp.
305
  Proof. by rewrite big_opM_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
307
  Lemma big_sepM_empty' `{AffineBI PROP} P Φ : P  [ map] kx  , Φ k x.
  Proof. rewrite big_sepM_empty. apply: affine. Qed.
308

309
  Lemma big_sepM_insert Φ m i x :
310
    m !! i = None 
311
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
312
  Proof. apply big_opM_insert. Qed.
313

314
  Lemma big_sepM_delete Φ m i x :
315
    m !! i = Some x 
316
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
317
  Proof. apply big_opM_delete. Qed.
318

319
320
321
322
323
324
325
  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
326
  Lemma big_sepM_lookup Φ m i x `{!Absorbing (Φ i x)} :
327
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
328
  Proof. intros. by rewrite big_sepM_lookup_acc // sep_elim_l. Qed.
329

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
341
342
343
  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).
344
  Proof. apply big_opM_insert_override. Qed.
345

Robbert Krebbers's avatar
Robbert Krebbers committed
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
  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
366
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  PROP) (f : K  B) m i x b :
367
    m !! i = None 
368
369
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
370
  Proof. apply big_opM_fn_insert. Qed.
371

Robbert Krebbers's avatar
Robbert Krebbers committed
372
  Lemma big_sepM_fn_insert' (Φ : K  PROP) m i x P :
373
    m !! i = None 
374
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
375
  Proof. apply big_opM_fn_insert'. Qed.
376

377
  Lemma big_sepM_sepM Φ Ψ m :
378
    ([ map] kx  m, Φ k x  Ψ k x)
379
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
380
  Proof. apply big_opM_opM. Qed.
381

382
383
384
  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
385
  Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
386

Robbert Krebbers's avatar
Robbert Krebbers committed
387
  Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
388
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
389
  Proof. apply (big_opM_commute _). Qed.
390

Robbert Krebbers's avatar
Robbert Krebbers committed
391
  Lemma big_sepM_forall `{AffineBI PROP} Φ m :
392
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
393
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
394
395
396
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
397
398
      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'.
399
    rewrite big_sepM_insert // -persistent_and_sep. apply and_intro.
400
    - rewrite (forall_elim i) (forall_elim x) lookup_insert.
401
      by rewrite pure_True // True_impl.
402
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
403
404
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
405
      by rewrite pure_True // True_impl.
406
407
408
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Robbert Krebbers's avatar
Robbert Krebbers committed
409
410
411
    ([ map] kx  m, Φ k x) -
     ( k x, m !! k = Some x  Φ k x - Ψ k x) -
    [ map] kx  m, Ψ k x.
412
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
414
415
416
417
418
419
420
421
422
423
    apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
    { by rewrite sep_elim_r. }
    rewrite !big_sepM_insert // bare_persistently_sep_dup.
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
    - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
      by rewrite True_impl bare_persistently_elim wand_elim_l.
    - rewrite comm -IH /=.
      apply sep_mono_l, bare_mono, persistently_mono, forall_mono=> k.
      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.
424
  Qed.
425

426
  Global Instance big_sepM_empty_persistent Φ :
427
    Persistent ([ map] kx  , Φ k x).
428
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
429
  Global Instance big_sepM_persistent Φ m :
430
    ( k x, Persistent (Φ k x))  Persistent ([ map] kx  m, Φ k x).
431
  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
432
433
End gmap.

434
(** ** Big ops over finite sets *)
435
436
437
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
Robbert Krebbers's avatar
Robbert Krebbers committed
438
  Implicit Types Φ : A  PROP.
439

Robbert Krebbers's avatar
Robbert Krebbers committed
440
441
442
443
  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.
444
445
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
446
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
447
  Proof. apply big_opS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
448
449
450
  Lemma big_sepS_subseteq `{AffineBI PROP} Φ X Y :
    Y  X  ([ set] x  X, Φ x)  [ set] x  Y, Φ x.
  Proof. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
451

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

Robbert Krebbers's avatar
Robbert Krebbers committed
456
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  emp.
457
  Proof. by rewrite big_opS_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
458
459
  Lemma big_sepS_empty' `{!AffineBI PROP} P Φ : P  [ set] x  , Φ x.
  Proof. rewrite big_sepS_empty. apply: affine. Qed.
460

461
  Lemma big_sepS_insert Φ X x :
462
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
463
  Proof. apply big_opS_insert. Qed.
464

Robbert Krebbers's avatar
Robbert Krebbers committed
465
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  PROP) f X x b :
466
    x  X 
467
468
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
469
  Proof. apply big_opS_fn_insert. Qed.
470

471
  Lemma big_sepS_fn_insert' Φ X x P :
472
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
473
  Proof. apply big_opS_fn_insert'. Qed.
474

Robbert Krebbers's avatar
Robbert Krebbers committed
475
476
477
  Lemma big_sepS_union Φ X Y :
    X  Y 
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
478
  Proof. apply big_opS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
479

480
  Lemma big_sepS_delete Φ X x :
481
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
482
  Proof. apply big_opS_delete. Qed.
483

Robbert Krebbers's avatar
Robbert Krebbers committed
484
485
486
  Lemma big_sepS_elem_of Φ X x `{!Absorbing (Φ x)} :
    x  X  ([ set] y  X, Φ y)  Φ x.
  Proof. intros. rewrite big_sepS_delete; auto. Qed.
487

488
489
490
491
492
493
494
  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.

495
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
496
  Proof. apply big_opS_singleton. Qed.
497

Robbert Krebbers's avatar
Robbert Krebbers committed
498
499
500
  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).
501
502
503
504
505
506
  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
507
      by rewrite decide_True // IH.
508
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
509
      by rewrite !big_sepS_insert // decide_False // IH left_id.
510
511
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
512
  Lemma big_sepS_filter_acc' (P : A  Prop) `{ y, Decision (P y)} Φ X Y :
513
514
    ( y, y  Y  P y  y  X) 
    ([ set] y  X, Φ y) -
Robbert Krebbers's avatar
Robbert Krebbers committed
515
516
      ([ 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).
517
518
519
  Proof.
    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
      as (Z&->&?); first set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
520
521
    rewrite big_sepS_union // big_sepS_filter'.
    by apply sep_mono_r, wand_intro_l.
522
523
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
524
525
526
527
528
529
530
531
532
533
534
535
536
  Lemma big_sepS_filter `{AffineBI PROP}
      (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.

  Lemma big_sepS_filter_acc `{AffineBI PROP}
      (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.

537
  Lemma big_sepS_sepS Φ Ψ X :
538
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
539
  Proof. apply big_opS_opS. Qed.
540

541
542
  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
543
  Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
544

Robbert Krebbers's avatar
Robbert Krebbers committed
545
546
  Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
     ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
547
548
  Proof. apply (big_opS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
549
  Lemma big_sepS_forall `{AffineBI PROP} Φ X :
550
    ( x, Persistent (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
551
552
553
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
554
555
      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'.
556
    rewrite big_sepS_insert // -persistent_and_sep. apply and_intro.
557
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
558
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
559
      by rewrite pure_True ?True_impl; last set_solver.
560
561
562
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
563
564
565
    ([ set] x  X, Φ x) -
     ( x, x  X  Φ x - Ψ x) -
    [ set] x  X, Ψ x.
566
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
567
568
569
570
571
572
573
574
575
    apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
    { by rewrite sep_elim_r. }
    rewrite !big_sepS_insert // bare_persistently_sep_dup.
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
    - rewrite (forall_elim x) pure_True; last set_solver.
      by rewrite True_impl bare_persistently_elim wand_elim_l.
    - rewrite comm -IH /=. apply sep_mono_l, bare_mono, persistently_mono.
      apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_True ?True_impl; last set_solver.
576
  Qed.
577
  Global Instance big_sepS_empty_persistent Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
578
    Persistent ([ set] x  , Φ x).
579
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
580
  Global Instance big_sepS_persistent Φ X :
581
    ( x, Persistent (Φ x))  Persistent ([ set] x  X, Φ x).
582
  Proof. rewrite /big_opS. apply _. Qed.
583
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
584

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

Robbert Krebbers's avatar
Robbert Krebbers committed
589
590
591
592
593

(** ** Big ops over finite multisets *)
Section gmultiset.
  Context `{Countable A}.
  Implicit Types X : gmultiset A.
Robbert Krebbers's avatar
Robbert Krebbers committed
594
  Implicit Types Φ : A  PROP.
Robbert Krebbers's avatar
Robbert Krebbers committed
595

Robbert Krebbers's avatar
Robbert Krebbers committed
596
597
598
599
  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
600
601
602
  Lemma big_sepMS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  ([ mset] x  X, Ψ x).
603
  Proof. apply big_opMS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
604
605
606
  Lemma big_sepMS_subseteq `{AffineBI PROP} Φ X Y :
    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
607

608
  Global Instance big_sepMS_mono' :
Robbert Krebbers's avatar
Robbert Krebbers committed
609
610
     Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opMS (@bi_sep PROP) (A:=A)).
  Proof. intros f g Hf m ? <-. by apply big_sepMS_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
611

Robbert Krebbers's avatar
Robbert Krebbers committed
612
  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
613
  Proof. by rewrite big_opMS_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
615
  Lemma big_sepMS_empty' `{!AffineBI PROP} P Φ : P  [ mset] x  , Φ x.
  Proof. rewrite big_sepMS_empty. apply: affine. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
616
617
618

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
619
  Proof. apply big_opMS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
620
621
622

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

Robbert Krebbers's avatar
Robbert Krebbers committed
625
626
  Lemma big_sepMS_elem_of Φ X x `{!Absorbing (Φ x)} :
    x  X  ([ mset] y  X, Φ y)  Φ x.
627
  Proof. intros. by rewrite big_sepMS_delete // sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
628

629
630
631
632
633
634
635
  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
636
  Lemma big_sepMS_singleton Φ x : ([ mset] y  {[ x ]}, Φ y)  Φ x.
637
  Proof. apply big_opMS_singleton. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
638
639
640

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

643
644
  Lemma big_sepMS_and Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
645
  Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
646

Robbert Krebbers's avatar
Robbert Krebbers committed
647
648
  Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
     ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
649
650
  Proof. apply (big_opMS_commute _). Qed.

651
  Global Instance big_sepMS_empty_persistent Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
652
653
    Persistent ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
654
  Global Instance big_sepMS_persistent Φ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
    ( x, Persistent (Φ x))  Persistent ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
End bi_big_op.

(** * Properties for step-indexed BIs*)
Section sbi_big_op.
Context {PROP : sbi}.
Implicit Types Ps Qs : list PROP.
Implicit Types A : Type.

(** ** Big ops over lists *)
Section list.
  Context {A : Type}.
  Implicit Types l : list A.
  Implicit Types Φ Ψ : nat  A  PROP.

  Lemma big_sepL_later `{AffineBI PROP} Φ l :
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
  Proof. apply (big_opL_commute _). Qed.

  Lemma big_sepL_laterN `{AffineBI PROP} Φ n l :
    ^n ([ list] k