big_op.v 36.2 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.algebra Require Export big_op.
2
From iris.bi Require 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
    <pers> ([ list] kx  l, Φ k x)  [ list] kx  l, <pers> (Φ k x).
131
  Proof. apply (big_opL_commute _). Qed.
132

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

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

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

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

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

290
End and_list.
291

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

398
  Lemma big_sepM_persistently `{BiAffine PROP} Φ m :
399
    (<pers> ([ map] kx  m, Φ k x))  ([ map] kx  m, <pers> (Φ k x)).
400
  Proof. apply (big_opM_commute _). Qed.
401

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

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

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

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

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

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

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

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

479
  Lemma big_sepS_insert Φ X x :
480
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
481
  Proof. apply big_opS_insert. Qed.
482

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

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

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

498
  Lemma big_sepS_delete Φ X x :
499
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
500
  Proof. apply big_opS_delete. Qed.
501

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

506
507
508
509
510
511
512
  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.

513
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
514
  Proof. apply big_opS_singleton. Qed.
515

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

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

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

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

555
  Lemma big_sepS_sepS Φ Ψ X :
556
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
557
  Proof. apply big_opS_opS. Qed.
558

559
560
  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
561
  Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
562

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

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

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

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

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

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

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