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

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

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

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

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

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

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

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

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

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

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

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

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

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

95
96
97
98
  Lemma big_sepL_lookup_acc Φ l i x :
    l !! i = Some x 
    ([ list] ky  l, Φ k y)  Φ i x  (Φ i x - ([ list] ky  l, Φ k y)).
  Proof.
99
100
101
    intros Hli. rewrite -(take_drop_middle l i x) // big_sepL_app /=.
    rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
    rewrite assoc -!(comm _ (Φ _ _)) -assoc. by apply sep_mono_r, wand_intro_l.
102
103
  Qed.

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

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

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

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

123
124
125
  Lemma big_sepL_and Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
Robbert Krebbers's avatar
Robbert Krebbers committed
126
  Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
127

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

Robbert Krebbers's avatar
Robbert Krebbers committed
132
  Lemma big_sepL_forall `{AffineBI PROP} Φ l :
133
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
134
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
135
136
137
  Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
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'|].
    rewrite big_sepL_cons. rewrite -persistent_and_sep_l; 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.

Robbert Krebbers's avatar
Robbert Krebbers committed
161
  Global Instance big_sepL_nil_persistent `{AffineBI PROP} Φ :
162
    Persistent ([ list] kx  [], Φ k x).
163
  Proof. simpl; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
166
167
168
169
170
171
172
  Global Instance big_sepL_persistent1 Φ l :
    ( k x, Persistent (Φ k x)) 
    l  [] 
    Persistent ([ list] kx  l, Φ k x).
  Proof.
    intros. rewrite /Persistent (big_opL_commute1 bi_persistently (R:=())) //.
    apply big_opL_proper=> k y ?. by apply persistent_persistently.
  Qed.
  Global Instance big_sepL_persistent `{AffineBI PROP} Φ l :
173
    ( k x, Persistent (Φ k x))  Persistent ([ list] kx  l, Φ k x).
174
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
175
  Global Instance big_sepL_persistent_id `{AffineBI PROP} Ps :
176
    TCForall Persistent Ps  Persistent ([] Ps).
177
  Proof. induction 1; simpl; apply _. Qed.
178
End sep_list.
179

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  Lemma big_sepM_impl Φ Ψ m :
Robbert Krebbers's avatar
Robbert Krebbers committed
417
418
419
    ([ map] kx  m, Φ k x) -
     ( k x, m !! k = Some x  Φ k x - Ψ k x) -
    [ map] kx  m, Ψ k x.
420
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
422
423
424
425
426
427
428
429
430
431
    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.
432
  Qed.
433

Robbert Krebbers's avatar
Robbert Krebbers committed
434
  Global Instance big_sepM_empty_persistent `{AffineBI PROP} Φ :
435
    Persistent ([ map] kx  , Φ k x).
436
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
437
  Global Instance big_sepM_persistent `{AffineBI PROP} Φ m :
438
    ( k x, Persistent (Φ k x))  Persistent ([ map] kx  m, Φ k x).
439
  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
440
441
End gmap.

442

443
(** ** Big ops over finite sets *)
444
445
446
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
Robbert Krebbers's avatar
Robbert Krebbers committed
447
  Implicit Types Φ : A  PROP.
448

Robbert Krebbers's avatar
Robbert Krebbers committed
449
450
451
452
  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.
453
454
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
455
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
456
  Proof. apply big_opS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
457
458
459
  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.
460

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

Robbert Krebbers's avatar
Robbert Krebbers committed
465
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  emp.
466
  Proof. by rewrite big_opS_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
467
468
  Lemma big_sepS_empty' `{!AffineBI PROP} P Φ : P  [ set] x  , Φ x.
  Proof. rewrite big_sepS_empty. apply: affine. Qed.
469

470
  Lemma big_sepS_insert Φ X x :
471
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
472
  Proof. apply big_opS_insert. Qed.
473

Robbert Krebbers's avatar
Robbert Krebbers committed
474
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  PROP) f X x b :
475
    x  X 
476
477
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
478
  Proof. apply big_opS_fn_insert. Qed.
479

480
  Lemma big_sepS_fn_insert' Φ X x P :
481
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
482
  Proof. apply big_opS_fn_insert'. Qed.
483

Robbert Krebbers's avatar
Robbert Krebbers committed
484
485
486
  Lemma big_sepS_union Φ X Y :
    X  Y 
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
487
  Proof. apply big_opS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
488

489
  Lemma big_sepS_delete Φ X x :
490
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
491
  Proof. apply big_opS_delete. Qed.
492

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

497
498
499
500
501
502
503
  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.

504
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
505
  Proof. apply big_opS_singleton. Qed.
506

Robbert Krebbers's avatar
Robbert Krebbers committed
507
508
509
  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).
510
511
512
513
514
515
  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
516
      by rewrite decide_True // IH.
517
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
518
      by rewrite !big_sepS_insert // decide_False // IH left_id.
519
520
  Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
533
534
535
536
537
538
539
540
541
542
543
544
545
  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.

546
  Lemma big_sepS_sepS Φ Ψ X :
547
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
548
  Proof. apply big_opS_opS. Qed.
549

550
551
  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
552
  Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
553

Robbert Krebbers's avatar
Robbert Krebbers committed
554
555
  Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
     ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
556
557
  Proof. apply (big_opS_commute _). Qed.

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

  Lemma big_sepS_impl Φ Ψ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
572
573
574
    ([ set] x  X, Φ x) -
     ( x, x  X  Φ x - Ψ x) -
    [ set] x  X, Ψ x.
575
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
576
577
578
579
580
581
582
583
584
    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.
585
  Qed.
586

Robbert Krebbers's avatar
Robbert Krebbers committed
587
588
  Global Instance big_sepS_empty_persistent `{AffineBI PROP} Φ :
    Persistent ([ set] x  , Φ x).
589
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
590
  Global Instance big_sepS_persistent `{AffineBI PROP} Φ X :
591
    ( x, Persistent (Φ x))  Persistent ([ set] x  X, Φ x).
592
  Proof. rewrite /big_opS. apply _. Qed.
593
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
594

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

Robbert Krebbers's avatar
Robbert Krebbers committed
599
600
601
602
603

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

Robbert Krebbers's avatar
Robbert Krebbers committed
606
607
608
609
  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
610
611
612
  Lemma big_sepMS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  ([ mset] x  X, Ψ x).
613
  Proof. apply big_opMS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
614
615
616
  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
617

618
  Global Instance big_sepMS_mono' :
Robbert Krebbers's avatar
Robbert Krebbers committed
619
620
     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
621

Robbert Krebbers's avatar
Robbert Krebbers committed
622
  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
623
  Proof. by rewrite big_opMS_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
624
625
  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
626
627
628

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
629
  Proof. apply big_opMS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
630
631
632

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

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

639
640
641
642
643
644
645
  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
646
  Lemma big_sepMS_singleton Φ x : ([ mset] y  {[ x ]}, Φ y)  Φ x.
647
  Proof. apply big_opMS_singleton. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
648
649
650

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

653
654
  Lemma big_sepMS_and Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
655
  Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
656

Robbert Krebbers's avatar
Robbert Krebbers committed
657
658
  Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
     ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
659
660
  Proof. apply (big_opMS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
  Global Instance big_sepMS_empty_persistent `{AffineBI PROP} Φ :
    Persistent ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_persistent `{AffineBI PROP} Φ X :
    ( x, Persistent (Φ x))  Persistent ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
End bi_big_op.

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

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

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

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