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

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

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

18
19
20
21
22
23
24
25
26
27
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
28
Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m)
29
  (at level 200, m at level 10, k, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
30
31
   format "[∗  map]  k ↦ x  ∈  m ,  P") : bi_scope.
Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m)
32
  (at level 200, m at level 10, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
33
   format "[∗  map]  x  ∈  m ,  P") : bi_scope.
34

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

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

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

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

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

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

85
86
  Global Instance big_sepL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
87
           (big_opL (@bi_sep PROP) (A:=A)).
88
89
  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
90
    Proper (Forall2 () ==> ()) (big_opL (@bi_sep M) (λ _ P, P)).
91
  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
92

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

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

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

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

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

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

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

129
  Lemma big_sepL_persistently `{BiAffine PROP} Φ l :
130
131
    bi_persistently ([ list] kx  l, Φ k x) 
    [ list] kx  l, bi_persistently (Φ k x).
132
  Proof. apply (big_opL_commute _). Qed.
133

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

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

173
174
175
  Global Instance big_sepL_nil_affine Φ :
    Affine ([ list] kx  [], Φ k x).
  Proof. simpl; apply _. Qed.
176
177
178
  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.
179
180
  Global Instance big_sepL_affine_id Ps : TCForall Affine Ps  Affine ([] Ps).
  Proof. induction 1; simpl; apply _. Qed.
181
End sep_list.
182

183
Section sep_list2.
184
185
  Context {A : Type}.
  Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
  Implicit Types Φ Ψ : nat  A  PROP.
187
188
189
  (* 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
190
    ([ list] kx  zip_with f l1 l2, Φ k x)
Robbert Krebbers's avatar
Robbert Krebbers committed
191
     ([ list] kx  l1, if l2 !! k is Some y then Φ k (f x y) else emp).
192
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
193
194
195
    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=.
    - by rewrite big_sepL_emp left_id.
    - by rewrite IH.
196
  Qed.
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
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 :
269
270
    bi_persistently ([ list] kx  l, Φ k x) 
    [ list] kx  l, bi_persistently (Φ k x).
271
272
  Proof. apply (big_opL_commute _). Qed.

273
  Lemma big_andL_forall `{BiAffine PROP} Φ l :
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
    ([ 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
291

292
End and_list.
293

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

Robbert Krebbers's avatar
Robbert Krebbers committed
300
301
302
303
  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.
304
305
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
306
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
307
  Proof. apply big_opM_proper. Qed.
308
  Lemma big_sepM_subseteq `{BiAffine PROP} Φ m1 m2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
309
310
    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.
311

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

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

322
  Lemma big_sepM_insert Φ m i x :
323
    m !! i = None 
324
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
325
  Proof. apply big_opM_insert. Qed.
326

327
  Lemma big_sepM_delete Φ m i x :
328
    m !! i = Some x 
329
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
330
  Proof. apply big_opM_delete. Qed.
331

332
333
334
335
336
337
338
  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
339
  Lemma big_sepM_lookup Φ m i x `{!Absorbing (Φ i x)} :
340
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
Robbert Krebbers's avatar
Robbert Krebbers committed
341
  Proof. intros. rewrite big_sepM_lookup_acc //. by rewrite sep_elim_l. Qed.
342

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
354
355
356
  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).
357
  Proof. apply big_opM_insert_override. Qed.
358

Robbert Krebbers's avatar
Robbert Krebbers committed
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
  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
379
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  PROP) (f : K  B) m i x b :
380
    m !! i = None 
381
382
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
383
  Proof. apply big_opM_fn_insert. Qed.
384

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

390
  Lemma big_sepM_sepM Φ Ψ m :
391
    ([ map] kx  m, Φ k x  Ψ k x)
392
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
393
  Proof. apply big_opM_opM. Qed.
394

395
396
397
  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
398
  Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
399

400
  Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
401
402
    (bi_persistently ([ map] kx  m, Φ k x)) 
      ([ map] kx  m, bi_persistently (Φ k x)).
403
  Proof. apply (big_opM_commute _). Qed.
404

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

  Lemma big_sepM_impl Φ Ψ m :
Robbert Krebbers's avatar
Robbert Krebbers committed
423
    ([ map] kx  m, Φ k x) -
424
     ( k x, m !! k = Some x  Φ k x - Ψ k x) -
Robbert Krebbers's avatar
Robbert Krebbers committed
425
    [ map] kx  m, Ψ k x.
426
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
428
    apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
    { by rewrite sep_elim_r. }
429
    rewrite !big_sepM_insert // affinely_persistently_sep_dup.
430
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
431
    - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
432
      by rewrite True_impl affinely_persistently_elim wand_elim_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
433
    - rewrite comm -IH /=.
434
      apply sep_mono_l, affinely_mono, persistently_mono, forall_mono=> k.
Robbert Krebbers's avatar
Robbert Krebbers committed
435
436
437
      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.
438
  Qed.
439

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
461
462
463
464
  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.
465
466
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
467
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
468
  Proof. apply big_opS_proper. Qed.
469
  Lemma big_sepS_subseteq `{BiAffine PROP} Φ X Y :
Robbert Krebbers's avatar
Robbert Krebbers committed
470
471
    Y  X  ([ set] x  X, Φ x)  [ set] x  Y, Φ x.
  Proof. intros. by apply big_sepL_submseteq, elements_submseteq. Qed.
472

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

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

482
  Lemma big_sepS_insert Φ X x :
483
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
484
  Proof. apply big_opS_insert. Qed.
485

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

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

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

501
  Lemma big_sepS_delete Φ X x :
502
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
503
  Proof. apply big_opS_delete. Qed.
504

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

509
510
511
512
513
514
515
  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.

516
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
517
  Proof. apply big_opS_singleton. Qed.
518

Robbert Krebbers's avatar
Robbert Krebbers committed
519
520
521
  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).
522
523
524
525
526
527
  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
528
      by rewrite decide_True // IH.
529
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
530
      by rewrite !big_sepS_insert // decide_False // IH left_id.
531
532
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
533
  Lemma big_sepS_filter_acc' (P : A  Prop) `{ y, Decision (P y)} Φ X Y :
534
535
    ( y, y  Y  P y  y  X) 
    ([ set] y  X, Φ y) -
Robbert Krebbers's avatar
Robbert Krebbers committed
536
537
      ([ 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).
538
539
540
  Proof.
    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
      as (Z&->&?); first set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
541
542
    rewrite big_sepS_union // big_sepS_filter'.
    by apply sep_mono_r, wand_intro_l.
543
544
  Qed.

545
  Lemma big_sepS_filter `{BiAffine PROP}
Robbert Krebbers's avatar
Robbert Krebbers committed
546
547
548
549
      (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.

550
  Lemma big_sepS_filter_acc `{BiAffine PROP}
Robbert Krebbers's avatar
Robbert Krebbers committed
551
552
553
554
555
556
557
      (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.

558
  Lemma big_sepS_sepS Φ Ψ X :
559
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
560
  Proof. apply big_opS_opS. Qed.
561

562
563
  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
564
  Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
565

566
  Lemma big_sepS_persistently `{BiAffine PROP} Φ X :
567
    bi_persistently ([ set] y  X, Φ y)  [ set] y  X, bi_persistently (Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
568
569
  Proof. apply (big_opS_commute _). Qed.

570
  Lemma big_sepS_forall `{BiAffine PROP} Φ X :
571
    ( x, Persistent (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
572
573
574
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
575
576
      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'.
577
    rewrite big_sepS_insert // -persistent_and_sep. apply and_intro.
578
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
579
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
580
      by rewrite pure_True ?True_impl; last set_solver.
581
582
583
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
584
    ([ set] x  X, Φ x) -
585
     ( x, x  X  Φ x - Ψ x) -
Robbert Krebbers's avatar
Robbert Krebbers committed
586
    [ set] x  X, Ψ x.
587
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
588
589
    apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
    { by rewrite sep_elim_r. }
590
    rewrite !big_sepS_insert // affinely_persistently_sep_dup.
591
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
592
    - rewrite (forall_elim x) pure_True; last set_solver.
593
594
      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
595
596
      apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_True ?True_impl; last set_solver.
597
  Qed.
598

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
617
618
619
620
(** ** Big ops over finite multisets *)
Section gmultiset.
  Context `{Countable A}.
  Implicit Types X : gmultiset A.