big_op.v 36 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 //. by rewrite 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

128
129
130
131
  Lemma big_sepL_plainly `{AffineBI PROP} Φ l :
    bi_plainly ([ list] kx  l, Φ k x)  [ list] kx  l, bi_plainly (Φ k x).
  Proof. apply (big_opL_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
132
  Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
133
134
    bi_persistently ([ list] kx  l, Φ k x) 
    [ list] kx  l, bi_persistently (Φ k x).
135
  Proof. apply (big_opL_commute _). Qed.
136

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

166
167
168
169
170
171
172
173
174
175
  Global Instance big_sepL_nil_plain Φ :
    Plain ([ list] kx  [], Φ k x).
  Proof. simpl; apply _. Qed.
  Global Instance big_sepL_plain Φ l :
    ( k x, Plain (Φ k x))  Plain ([ list] kx  l, Φ k x).
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
  Global Instance big_sepL_plain_id Ps :
    TCForall Plain Ps  Plain ([] Ps).
  Proof. induction 1; simpl; apply _. Qed.

176
  Global Instance big_sepL_nil_persistent Φ :
177
    Persistent ([ list] kx  [], Φ k x).
178
  Proof. simpl; apply _. Qed.
179
  Global Instance big_sepL_persistent Φ l :
180
    ( k x, Persistent (Φ k x))  Persistent ([ list] kx  l, Φ k x).
181
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
182
  Global Instance big_sepL_persistent_id Ps :
183
    TCForall Persistent Ps  Persistent ([] Ps).
184
  Proof. induction 1; simpl; apply _. Qed.
185

186
187
188
  Global Instance big_sepL_nil_affine Φ :
    Affine ([ list] kx  [], Φ k x).
  Proof. simpl; apply _. Qed.
189
190
191
  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.
192
193
  Global Instance big_sepL_affine_id Ps : TCForall Affine Ps  Affine ([] Ps).
  Proof. induction 1; simpl; apply _. Qed.
194
End sep_list.
195

196
Section sep_list2.
197
198
  Context {A : Type}.
  Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
199
  Implicit Types Φ Ψ : nat  A  PROP.
200
201
202
  (* 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
203
    ([ list] kx  zip_with f l1 l2, Φ k x)
Robbert Krebbers's avatar
Robbert Krebbers committed
204
     ([ list] kx  l1, if l2 !! k is Some y then Φ k (f x y) else emp).
205
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
208
    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=.
    - by rewrite big_sepL_emp left_id.
    - by rewrite IH.
209
  Qed.
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
280
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.

281
282
283
284
  Lemma big_andL_plainly Φ l :
    bi_plainly ([ list] kx  l, Φ k x)  [ list] kx  l, bi_plainly (Φ k x).
  Proof. apply (big_opL_commute _). Qed.

285
  Lemma big_andL_persistently Φ l :
286
287
    bi_persistently ([ list] kx  l, Φ k x) 
    [ list] kx  l, bi_persistently (Φ k x).
288
289
290
291
292
293
294
295
296
297
298
299
300
301
  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.

302
303
304
305
306
307
308
  Global Instance big_andL_nil_plain Φ :
    Plain ([ list] kx  [], Φ k x).
  Proof. simpl; apply _. Qed.
  Global Instance big_andL_plain Φ l :
    ( k x, Plain (Φ k x))  Plain ([ list] kx  l, Φ k x).
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.

309
310
311
312
313
314
315
  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.
316

317
(** ** Big ops over finite maps *)
318
319
320
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
Robbert Krebbers's avatar
Robbert Krebbers committed
321
  Implicit Types Φ Ψ : K  A  PROP.
322

Robbert Krebbers's avatar
Robbert Krebbers committed
323
324
325
326
  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.
327
328
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
329
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
330
  Proof. apply big_opM_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
331
332
333
  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.
334

335
336
  Global Instance big_sepM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
337
338
           (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_sepM_mono=> ???; apply Hf. Qed.
339

Robbert Krebbers's avatar
Robbert Krebbers committed
340
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  emp.
341
  Proof. by rewrite big_opM_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
342
343
  Lemma big_sepM_empty' `{AffineBI PROP} P Φ : P  [ map] kx  , Φ k x.
  Proof. rewrite big_sepM_empty. apply: affine. Qed.
344

345
  Lemma big_sepM_insert Φ m i x :
346
    m !! i = None 
347
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
348
  Proof. apply big_opM_insert. Qed.
349

350
  Lemma big_sepM_delete Φ m i x :
351
    m !! i = Some x 
352
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
353
  Proof. apply big_opM_delete. Qed.
354

355
356
357
358
359
360
361
  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
362
  Lemma big_sepM_lookup Φ m i x `{!Absorbing (Φ i x)} :
363
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
  Proof. intros. rewrite big_sepM_lookup_acc //. by rewrite sep_elim_l. Qed.
365

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
377
378
379
  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).
380
  Proof. apply big_opM_insert_override. Qed.
381

Robbert Krebbers's avatar
Robbert Krebbers committed
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
  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
402
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  PROP) (f : K  B) m i x b :
403
    m !! i = None 
404
405
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
406
  Proof. apply big_opM_fn_insert. Qed.
407

Robbert Krebbers's avatar
Robbert Krebbers committed
408
  Lemma big_sepM_fn_insert' (Φ : K  PROP) m i x P :
409
    m !! i = None 
410
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
411
  Proof. apply big_opM_fn_insert'. Qed.
412

413
  Lemma big_sepM_sepM Φ Ψ m :
414
    ([ map] kx  m, Φ k x  Ψ k x)
415
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
416
  Proof. apply big_opM_opM. Qed.
417

418
419
420
  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
421
  Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
422

423
424
425
426
  Lemma big_sepM_plainly `{AffineBI PROP} Φ m :
    bi_plainly ([ map] kx  m, Φ k x)  [ map] kx  m, bi_plainly (Φ k x).
  Proof. apply (big_opM_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
427
  Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
428
429
    (bi_persistently ([ map] kx  m, Φ k x)) 
      ([ map] kx  m, bi_persistently (Φ k x)).
430
  Proof. apply (big_opM_commute _). Qed.
431

Robbert Krebbers's avatar
Robbert Krebbers committed
432
  Lemma big_sepM_forall `{AffineBI PROP} Φ m :
433
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
434
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
435
436
437
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
438
439
      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'.
440
    rewrite big_sepM_insert // -persistent_and_sep. apply and_intro.
441
    - rewrite (forall_elim i) (forall_elim x) lookup_insert.
442
      by rewrite pure_True // True_impl.
443
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
444
445
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
446
      by rewrite pure_True // True_impl.
447
448
449
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Robbert Krebbers's avatar
Robbert Krebbers committed
450
    ([ map] kx  m, Φ k x) -
451
     ( k x, m !! k = Some x  Φ k x - Ψ k x) -
Robbert Krebbers's avatar
Robbert Krebbers committed
452
    [ map] kx  m, Ψ k x.
453
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
454
455
    apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
    { by rewrite sep_elim_r. }
456
    rewrite !big_sepM_insert // affinely_persistently_sep_dup.
457
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
458
    - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
459
      by rewrite True_impl affinely_persistently_elim wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
460
    - rewrite comm -IH /=.
461
      apply sep_mono_l, affinely_mono, persistently_mono, forall_mono=> k.
Robbert Krebbers's avatar
Robbert Krebbers committed
462
463
464
      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.
465
  Qed.
466

467
468
469
470
471
472
  Global Instance big_sepM_empty_plain Φ : Plain ([ map] kx  , Φ k x).
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
  Global Instance big_sepM_plain Φ m :
    ( k x, Plain (Φ k x))  Plain ([ map] kx   m, Φ k x).
  Proof. intros. apply (big_sepL_plain _ _)=> _ [??]; apply _. Qed.

473
  Global Instance big_sepM_empty_persistent Φ :
474
    Persistent ([ map] kx  , Φ k x).
475
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
476
  Global Instance big_sepM_persistent Φ m :
477
    ( k x, Persistent (Φ k x))  Persistent ([ map] kx  m, Φ k x).
478
  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
479

480
481
482
  Global Instance big_sepM_empty_affine Φ :
    Affine ([ map] kx  , Φ k x).
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
483
484
  Global Instance big_sepM_affine Φ m :
    ( k x, Affine (Φ k x))  Affine ([ map] kx  m, Φ k x).
485
  Proof. intros. apply big_sepL_affine=> _ [??]; apply _. Qed.
486
487
End gmap.

488
(** ** Big ops over finite sets *)
489
490
491
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
Robbert Krebbers's avatar
Robbert Krebbers committed
492
  Implicit Types Φ : A  PROP.
493

Robbert Krebbers's avatar
Robbert Krebbers committed
494
495
496
497
  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.
498
499
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
500
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
501
  Proof. apply big_opS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
502
503
504
  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.
505

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

Robbert Krebbers's avatar
Robbert Krebbers committed
510
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  emp.
511
  Proof. by rewrite big_opS_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
512
513
  Lemma big_sepS_empty' `{!AffineBI PROP} P Φ : P  [ set] x  , Φ x.
  Proof. rewrite big_sepS_empty. apply: affine. Qed.
514

515
  Lemma big_sepS_insert Φ X x :
516
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
517
  Proof. apply big_opS_insert. Qed.
518

Robbert Krebbers's avatar
Robbert Krebbers committed
519
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  PROP) f X x b :
520
    x  X 
521
522
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
523
  Proof. apply big_opS_fn_insert. Qed.
524

525
  Lemma big_sepS_fn_insert' Φ X x P :
526
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
527
  Proof. apply big_opS_fn_insert'. Qed.
528

Robbert Krebbers's avatar
Robbert Krebbers committed
529
530
531
  Lemma big_sepS_union Φ X Y :
    X  Y 
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
532
  Proof. apply big_opS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
533

534
  Lemma big_sepS_delete Φ X x :
535
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
536
  Proof. apply big_opS_delete. Qed.
537

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

542
543
544
545
546
547
548
  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.

549
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
550
  Proof. apply big_opS_singleton. Qed.
551

Robbert Krebbers's avatar
Robbert Krebbers committed
552
553
554
  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).
555
556
557
558
559
560
  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
561
      by rewrite decide_True // IH.
562
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
563
      by rewrite !big_sepS_insert // decide_False // IH left_id.
564
565
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
566
  Lemma big_sepS_filter_acc' (P : A  Prop) `{ y, Decision (P y)} Φ X Y :
567
568
    ( y, y  Y  P y  y  X) 
    ([ set] y  X, Φ y) -
Robbert Krebbers's avatar
Robbert Krebbers committed
569
570
      ([ 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).
571
572
573
  Proof.
    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
      as (Z&->&?); first set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
574
575
    rewrite big_sepS_union // big_sepS_filter'.
    by apply sep_mono_r, wand_intro_l.
576
577
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
578
579
580
581
582
583
584
585
586
587
588
589
590
  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.

591
  Lemma big_sepS_sepS Φ Ψ X :
592
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
593
  Proof. apply big_opS_opS. Qed.
594

595
596
  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
597
  Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
598

599
600
601
602
  Lemma big_sepS_plainly `{AffineBI PROP} Φ X :
    bi_plainly ([ set] y  X, Φ y)  [ set] y  X, bi_plainly (Φ y).
  Proof. apply (big_opS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
603
  Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
604
    bi_persistently ([ set] y  X, Φ y)  [ set] y  X, bi_persistently (Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
605
606
  Proof. apply (big_opS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
607
  Lemma big_sepS_forall `{AffineBI PROP} Φ X :
608
    ( x, Persistent (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
609
610
611
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
612
613
      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'.
614
    rewrite big_sepS_insert // -persistent_and_sep. apply and_intro.
615
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
616
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
617
      by rewrite pure_True ?True_impl; last set_solver.
618
619
620
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
621
    ([ set] x  X, Φ x) -
622
     ( x, x  X  Φ x - Ψ x) -
Robbert Krebbers's avatar
Robbert Krebbers committed
623
    [ set] x  X, Ψ x.
624
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
625
626
    apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
    { by rewrite sep_elim_r. }
627
    rewrite !big_sepS_insert // affinely_persistently_sep_dup.
628
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
629
    - rewrite (forall_elim x) pure_True; last set_solver.
630
631
      by rewrite True_impl affinely_persistently_elim wand_elim_l.
    - rewrite comm -IH /=. apply sep_mono_l, affinely_mono, persistently_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
632
633
      apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_True ?True_impl; last set_solver.
634
  Qed.
635
636
637
638
639
640
641

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

642
  Global Instance big_sepS_empty_persistent Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
643
    Persistent ([ set] x  , Φ x).
644
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
645
  Global Instance big_sepS_persistent Φ X :
646
    ( x, Persistent (Φ x))  Persistent ([ set] x  X, Φ x).
647
  Proof. rewrite /big_opS. apply _. Qed.
648

649
650
  Global Instance big_sepS_empty_affine Φ : Affine ([ set] x  , Φ x).
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
651
652
653
  Global Instance big_sepS_affine Φ X :
    ( x, Affine (Φ x))  Affine ([ set] x  X, Φ x).
  Proof. rewrite /big_opS. apply _. Qed.
Robbert Krebbers's avatar