big_op.v 33.4 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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
132
  Lemma big_sepL_forall `{AffineBI PROP} Φ l :
133
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
134
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
135
136
137
  Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_sepL_lookup. }
    revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ; [by auto using big_sepL_nil'|].
140
    rewrite big_sepL_cons. rewrite -persistent_and_sep; apply and_intro.
141
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
142
143
144
145
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Lemma big_sepL_impl Φ Ψ l :
Robbert Krebbers's avatar
Robbert Krebbers committed
146
147
148
    ([ list] kx  l, Φ k x) -
     ( k x, l !! k = Some x  Φ k x - Ψ k x) -
    [ list] kx  l, Ψ k x.
149
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
152
153
154
155
156
157
158
    apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=.
    { by rewrite sep_elim_r. }
    rewrite bare_persistently_sep_dup -assoc [( _  _)%I]comm -!assoc assoc.
    apply sep_mono.
    - rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
      by rewrite bare_persistently_elim wand_elim_l.
    - rewrite comm -(IH (Φ  S) (Ψ  S)) /=.
      apply sep_mono_l, bare_mono, persistently_mono.
      apply forall_intro=> k. by rewrite (forall_elim (S k)).
159
160
  Qed.

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

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

181
Section sep_list2.
182
183
  Context {A : Type}.
  Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
184
  Implicit Types Φ Ψ : nat  A  PROP.
185
186
187
  (* 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
188
    ([ list] kx  zip_with f l1 l2, Φ k x)
Robbert Krebbers's avatar
Robbert Krebbers committed
189
     ([ list] kx  l1, if l2 !! k is Some y then Φ k (f x y) else emp).
190
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
192
193
    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=.
    - by rewrite big_sepL_emp left_id.
    - by rewrite IH.
194
  Qed.
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
End sep_list2.

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

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

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

  Global Instance big_andL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
           (big_opL (@bi_and PROP) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
  Global Instance big_and_mono' :
    Proper (Forall2 () ==> ()) (big_opL (@bi_and M) (λ _ P, P)).
  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

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

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

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

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

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

  Lemma big_andL_persistently Φ l :
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
  Proof. apply (big_opL_commute _). Qed.

  Lemma big_andL_forall `{AffineBI PROP} Φ l :
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
  Proof.
    apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply: big_andL_lookup. }
    revert Φ. induction l as [|x l IH]=> Φ; [by auto using big_andL_nil'|].
    rewrite big_andL_cons. apply and_intro.
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Global Instance big_andL_nil_persistent Φ :
    Persistent ([ list] kx  [], Φ k x).
  Proof. simpl; apply _. Qed.
  Global Instance big_andL_persistent Φ l :
    ( k x, Persistent (Φ k x))  Persistent ([ list] kx  l, Φ k x).
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
End and_list.
289

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

Robbert Krebbers's avatar
Robbert Krebbers committed
296
297
298
299
  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.
300
301
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
302
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
303
  Proof. apply big_opM_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
305
306
  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.
307

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

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

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

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

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

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

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
396
  Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
397
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
398
  Proof. apply (big_opM_commute _). Qed.
399

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

  Lemma big_sepM_impl Φ Ψ m :
Robbert Krebbers's avatar
Robbert Krebbers committed
418
419
420
    ([ map] kx  m, Φ k x) -
     ( k x, m !! k = Some x  Φ k x - Ψ k x) -
    [ map] kx  m, Ψ k x.
421
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
422
423
424
425
426
427
428
429
430
431
432
    apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
    { by rewrite sep_elim_r. }
    rewrite !big_sepM_insert // bare_persistently_sep_dup.
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
    - rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
      by rewrite True_impl bare_persistently_elim wand_elim_l.
    - rewrite comm -IH /=.
      apply sep_mono_l, bare_mono, persistently_mono, forall_mono=> k.
      apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
      by rewrite pure_True // True_impl.
433
  Qed.
434

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
456
457
458
459
  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.
460
461
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
462
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
463
  Proof. apply big_opS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
464
465
466
  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.
467

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

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

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

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

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

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

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

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

504
505
506
507
508
509
510
  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.

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
540
541
542
543
544
545
546
547
548
549
550
551
552
  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.

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
561
562
  Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
     ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
563
564
  Proof. apply (big_opS_commute _). Qed.

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

  Lemma big_sepS_impl Φ Ψ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
579
580
581
    ([ set] x  X, Φ x) -
     ( x, x  X  Φ x - Ψ x) -
    [ set] x  X, Ψ x.
582
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
583
584
585
586
587
588
589
590
591
    apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
    { by rewrite sep_elim_r. }
    rewrite !big_sepS_insert // bare_persistently_sep_dup.
    rewrite -assoc [( _  _)%I]comm -!assoc assoc. apply sep_mono.
    - rewrite (forall_elim x) pure_True; last set_solver.
      by rewrite True_impl bare_persistently_elim wand_elim_l.
    - rewrite comm -IH /=. apply sep_mono_l, bare_mono, persistently_mono.
      apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_True ?True_impl; last set_solver.
592
  Qed.
593
  Global Instance big_sepS_empty_persistent Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
594
    Persistent ([ set] x  , Φ x).
595
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
596
  Global Instance big_sepS_persistent Φ X :
597
    ( x, Persistent (Φ x))  Persistent ([ set] x  X, Φ x).
598
  Proof. rewrite /big_opS. apply _. Qed.
599

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
611
612
613
614
615

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

Robbert Krebbers's avatar
Robbert Krebbers committed
618
619
620
621
  Lemma big_sepMS_mono Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  [ mset] x  X, Ψ x.
  Proof. intros. apply big_opMS_forall; apply _ || auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
622
623
624
  Lemma big_sepMS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  ([ mset] x  X, Ψ x).
625
  Proof. apply big_opMS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
626
627
628
  Lemma big_sepMS_subseteq `{AffineBI PROP} Φ X Y :
    Y  X  ([ mset] x  X, Φ x)  [ mset] x  Y, Φ x.
  Proof. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
629

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

Robbert Krebbers's avatar
Robbert Krebbers committed
634
  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
635
  Proof. by rewrite big_opMS_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
636
637
  Lemma big_sepMS_empty' `{!AffineBI PROP} P Φ : P  [ mset] x  , Φ x.
  Proof. rewrite big_sepMS_empty. apply: affine. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
638
639
640

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
641
  Proof. apply big_opMS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
642
643
644

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

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

651
652
653
654
655
656
657
  Lemma big_sepMS_elem_of_acc Φ X x :
    x  X 
    ([ mset] y  X, Φ y)  Φ x  (Φ x - ([ mset] y  X, Φ y)).
  Proof.
    intros. rewrite big_sepMS_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
658
  Lemma big_sepMS_singleton Φ x : ([ mset] y  {[ x ]}, Φ y)  Φ x.
659
  Proof. apply big_opMS_singleton. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
660
661
662

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

665
666
  Lemma big_sepMS_and Φ Ψ X :
    ([ mset] y  X, Φ</