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

Robbert Krebbers's avatar
Robbert Krebbers committed
17
Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m)
18
  (at level 200, m at level 10, k, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
   format "[∗  map]  k ↦ x  ∈  m ,  P") : bi_scope.
Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m)
21
  (at level 200, m at level 10, x at level 1, right associativity,
Robbert Krebbers's avatar
Robbert Krebbers committed
22
   format "[∗  map]  x  ∈  m ,  P") : bi_scope.
23

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

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

32
(** * Properties *)
Robbert Krebbers's avatar
Robbert Krebbers committed
33
34
35
36
37
Module bi.
Import interface.bi derived.bi.
Section bi_big_op.
Context {PROP : bi}.
Implicit Types Ps Qs : list PROP.
38
39
Implicit Types A : Type.

40
41
42
43
(** ** Big ops over lists *)
Section list.
  Context {A : Type}.
  Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  Implicit Types Φ Ψ : nat  A  PROP.
45

Robbert Krebbers's avatar
Robbert Krebbers committed
46
  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y)  emp.
47
  Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
49
  Lemma big_sepL_nil' `{AffineBI PROP} P Φ : P  [ list] ky  nil, Φ k y.
  Proof. apply (affine _). Qed.
50
  Lemma big_sepL_cons Φ x l :
51
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
52
  Proof. by rewrite big_opL_cons. Qed.
53
  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
54
55
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
56
57
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
58
59
  Proof. by rewrite big_opL_app. Qed.

60
61
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
62
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
63
  Proof. apply big_opL_forall; apply _. Qed.
64
65
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
66
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
67
  Proof. apply big_opL_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
  Lemma big_sepL_submseteq `{AffineBI PROP} (Φ : A  PROP) l1 l2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
69
    l1 + l2  ([ list] y  l2, Φ y)  [ list] y  l1, Φ y.
Robbert Krebbers's avatar
Robbert Krebbers committed
70
71
72
  Proof.
    intros [l ->]%submseteq_Permutation. by rewrite big_sepL_app sep_elim_l.
  Qed.
73

74
75
  Global Instance big_sepL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
76
           (big_opL (@bi_sep PROP) (A:=A)).
77
78
  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
79
    Proper (Forall2 () ==> ()) (big_opL (@bi_sep M) (λ _ P, P)).
80
  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
81

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

85
86
87
88
  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.
89
90
91
    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.
92
93
  Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
98
  Lemma big_sepL_elem_of (Φ : A  PROP) l x `{!Absorbing (Φ x)} :
99
    x  l  ([ list] y  l, Φ y)  Φ x.
100
101
102
  Proof.
    intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)).
  Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
103

Robbert Krebbers's avatar
Robbert Krebbers committed
104
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  PROP) l :
105
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
106
  Proof. by rewrite big_opL_fmap. Qed.
107
108

  Lemma big_sepL_sepL Φ Ψ l :
109
110
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
111
  Proof. by rewrite big_opL_opL. Qed.
112

113
114
115
  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
116
  Proof. auto using and_intro, big_sepL_mono, and_elim_l, and_elim_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
117

Robbert Krebbers's avatar
Robbert Krebbers committed
118
  Lemma big_sepL_persistently `{AffineBI PROP} Φ l :
119
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
120
  Proof. apply (big_opL_commute _). Qed.
121

Robbert Krebbers's avatar
Robbert Krebbers committed
122
  Lemma big_sepL_forall `{AffineBI PROP} Φ l :
123
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
124
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
125
126
127
  Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
130
      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.
131
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
132
133
134
135
    - 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
136
137
138
    ([ list] kx  l, Φ k x) -
     ( k x, l !! k = Some x  Φ k x - Ψ k x) -
    [ list] kx  l, Ψ k x.
139
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
140
141
142
143
144
145
146
147
148
    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)).
149
150
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
151
  Global Instance big_sepL_nil_persistent `{AffineBI PROP} Φ :
152
    Persistent ([ list] kx  [], Φ k x).
153
  Proof. simpl; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
156
157
158
159
160
161
162
  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 :
163
    ( k x, Persistent (Φ k x))  Persistent ([ list] kx  l, Φ k x).
164
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  Global Instance big_sepL_persistent_id `{AffineBI PROP} Ps :
166
    TCForall Persistent Ps  Persistent ([] Ps).
167
  Proof. induction 1; simpl; apply _. Qed.
168
169
End list.

170
171
172
Section list2.
  Context {A : Type}.
  Implicit Types l : list A.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  Implicit Types Φ Ψ : nat  A  PROP.
174
175
176
  (* 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
177
    ([ list] kx  zip_with f l1 l2, Φ k x)
Robbert Krebbers's avatar
Robbert Krebbers committed
178
     ([ list] kx  l1, if l2 !! k is Some y then Φ k (f x y) else emp).
179
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
180
181
182
    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=.
    - by rewrite big_sepL_emp left_id.
    - by rewrite IH.
183
184
  Qed.
End list2.
185

186
(** ** Big ops over finite maps *)
187
188
189
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
Robbert Krebbers's avatar
Robbert Krebbers committed
190
  Implicit Types Φ Ψ : K  A  PROP.
191

Robbert Krebbers's avatar
Robbert Krebbers committed
192
193
194
195
  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.
196
197
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
198
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
199
  Proof. apply big_opM_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
201
202
  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.
203

204
205
  Global Instance big_sepM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
Robbert Krebbers's avatar
Robbert Krebbers committed
206
207
           (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_sepM_mono=> ???; apply Hf. Qed.
208

Robbert Krebbers's avatar
Robbert Krebbers committed
209
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  emp.
210
  Proof. by rewrite big_opM_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
212
  Lemma big_sepM_empty' `{AffineBI PROP} P Φ : P  [ map] kx  , Φ k x.
  Proof. rewrite big_sepM_empty. apply: affine. Qed.
213

214
  Lemma big_sepM_insert Φ m i x :
215
    m !! i = None 
216
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
217
  Proof. apply big_opM_insert. Qed.
218

219
  Lemma big_sepM_delete Φ m i x :
220
    m !! i = Some x 
221
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
222
  Proof. apply big_opM_delete. Qed.
223

224
225
226
227
228
229
230
  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
231
  Lemma big_sepM_lookup Φ m i x `{!Absorbing (Φ i x)} :
232
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
233
  Proof. intros. by rewrite big_sepM_lookup_acc // sep_elim_l. Qed.
234

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
246
247
248
  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).
249
  Proof. apply big_opM_insert_override. Qed.
250

Robbert Krebbers's avatar
Robbert Krebbers committed
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
  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
271
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  PROP) (f : K  B) m i x b :
272
    m !! i = None 
273
274
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
275
  Proof. apply big_opM_fn_insert. Qed.
276

Robbert Krebbers's avatar
Robbert Krebbers committed
277
  Lemma big_sepM_fn_insert' (Φ : K  PROP) m i x P :
278
    m !! i = None 
279
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
280
  Proof. apply big_opM_fn_insert'. Qed.
281

282
  Lemma big_sepM_sepM Φ Ψ m :
283
    ([ map] kx  m, Φ k x  Ψ k x)
284
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
285
  Proof. apply big_opM_opM. Qed.
286

287
288
289
  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
290
  Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
291

Robbert Krebbers's avatar
Robbert Krebbers committed
292
  Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
293
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
294
  Proof. apply (big_opM_commute _). Qed.
295

Robbert Krebbers's avatar
Robbert Krebbers committed
296
  Lemma big_sepM_forall `{AffineBI PROP} Φ m :
297
    ( k x, Persistent (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
298
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
299
300
301
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
302
303
304
      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.
305
    - rewrite (forall_elim i) (forall_elim x) lookup_insert.
306
      by rewrite pure_True // True_impl.
307
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
308
309
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
310
      by rewrite pure_True // True_impl.
311
312
313
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Robbert Krebbers's avatar
Robbert Krebbers committed
314
315
316
    ([ map] kx  m, Φ k x) -
     ( k x, m !! k = Some x  Φ k x - Ψ k x) -
    [ map] kx  m, Ψ k x.
317
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
318
319
320
321
322
323
324
325
326
327
328
    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.
329
  Qed.
330

Robbert Krebbers's avatar
Robbert Krebbers committed
331
  Global Instance big_sepM_empty_persistent `{AffineBI PROP} Φ :
332
    Persistent ([ map] kx  , Φ k x).
333
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
334
  Global Instance big_sepM_persistent `{AffineBI PROP} Φ m :
335
    ( k x, Persistent (Φ k x))  Persistent ([ map] kx  m, Φ k x).
336
  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
337
338
End gmap.

339

340
(** ** Big ops over finite sets *)
341
342
343
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
Robbert Krebbers's avatar
Robbert Krebbers committed
344
  Implicit Types Φ : A  PROP.
345

Robbert Krebbers's avatar
Robbert Krebbers committed
346
347
348
349
  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.
350
351
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
352
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
353
  Proof. apply big_opS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
354
355
356
  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.
357

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

Robbert Krebbers's avatar
Robbert Krebbers committed
362
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  emp.
363
  Proof. by rewrite big_opS_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
364
365
  Lemma big_sepS_empty' `{!AffineBI PROP} P Φ : P  [ set] x  , Φ x.
  Proof. rewrite big_sepS_empty. apply: affine. Qed.
366

367
  Lemma big_sepS_insert Φ X x :
368
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
369
  Proof. apply big_opS_insert. Qed.
370

Robbert Krebbers's avatar
Robbert Krebbers committed
371
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  PROP) f X x b :
372
    x  X 
373
374
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
375
  Proof. apply big_opS_fn_insert. Qed.
376

377
  Lemma big_sepS_fn_insert' Φ X x P :
378
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
379
  Proof. apply big_opS_fn_insert'. Qed.
380

Robbert Krebbers's avatar
Robbert Krebbers committed
381
382
383
  Lemma big_sepS_union Φ X Y :
    X  Y 
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
384
  Proof. apply big_opS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
385

386
  Lemma big_sepS_delete Φ X x :
387
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
388
  Proof. apply big_opS_delete. Qed.
389

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

394
395
396
397
398
399
400
  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.

401
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
402
  Proof. apply big_opS_singleton. Qed.
403

Robbert Krebbers's avatar
Robbert Krebbers committed
404
405
406
  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).
407
408
409
410
411
412
  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
413
      by rewrite decide_True // IH.
414
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
      by rewrite !big_sepS_insert // decide_False // IH left_id.
416
417
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
418
  Lemma big_sepS_filter_acc' (P : A  Prop) `{ y, Decision (P y)} Φ X Y :
419
420
    ( y, y  Y  P y  y  X) 
    ([ set] y  X, Φ y) -
Robbert Krebbers's avatar
Robbert Krebbers committed
421
422
      ([ 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).
423
424
425
  Proof.
    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
      as (Z&->&?); first set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
427
    rewrite big_sepS_union // big_sepS_filter'.
    by apply sep_mono_r, wand_intro_l.
428
429
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
430
431
432
433
434
435
436
437
438
439
440
441
442
  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.

443
  Lemma big_sepS_sepS Φ Ψ X :
444
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
445
  Proof. apply big_opS_opS. Qed.
446

447
448
  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
449
  Proof. auto using and_intro, big_sepS_mono, and_elim_l, and_elim_r. Qed.
450

Robbert Krebbers's avatar
Robbert Krebbers committed
451
452
  Lemma big_sepS_persistently `{AffineBI PROP} Φ X :
     ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
453
454
  Proof. apply (big_opS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
455
  Lemma big_sepS_forall `{AffineBI PROP} Φ X :
456
    ( x, Persistent (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
457
458
459
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
Robbert Krebbers's avatar
Robbert Krebbers committed
460
461
462
      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.
463
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
464
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
465
      by rewrite pure_True ?True_impl; last set_solver.
466
467
468
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
469
470
471
    ([ set] x  X, Φ x) -
     ( x, x  X  Φ x - Ψ x) -
    [ set] x  X, Ψ x.
472
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
473
474
475
476
477
478
479
480
481
    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.
482
  Qed.
483

Robbert Krebbers's avatar
Robbert Krebbers committed
484
485
  Global Instance big_sepS_empty_persistent `{AffineBI PROP} Φ :
    Persistent ([ set] x  , Φ x).
486
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
487
  Global Instance big_sepS_persistent `{AffineBI PROP} Φ X :
488
    ( x, Persistent (Φ x))  Persistent ([ set] x  X, Φ x).
489
  Proof. rewrite /big_opS. apply _. Qed.
490
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
491

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

Robbert Krebbers's avatar
Robbert Krebbers committed
496
497
498
499
500

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

Robbert Krebbers's avatar
Robbert Krebbers committed
503
504
505
506
  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
507
508
509
  Lemma big_sepMS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  ([ mset] x  X, Ψ x).
510
  Proof. apply big_opMS_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
511
512
513
  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
514

515
  Global Instance big_sepMS_mono' :
Robbert Krebbers's avatar
Robbert Krebbers committed
516
517
     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
518

Robbert Krebbers's avatar
Robbert Krebbers committed
519
  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  emp.
Robbert Krebbers's avatar
Robbert Krebbers committed
520
  Proof. by rewrite big_opMS_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
521
522
  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
523
524
525

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
526
  Proof. apply big_opMS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
527
528
529

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

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

536
537
538
539
540
541
542
  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
543
  Lemma big_sepMS_singleton Φ x : ([ mset] y  {[ x ]}, Φ y)  Φ x.
544
  Proof. apply big_opMS_singleton. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
545
546
547

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
  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.

  Global Instance big_sepL_nil_timeless Φ :
    Timeless ([ list] kx  [], Φ k x).
  Proof. simpl; apply _. Qed.
  Global Instance big_sepL_timeless Φ l :
    ( k x, Timeless (Φ k x))  Timeless ([ list] kx  l, Φ k x).
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
  Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
    TCForall Timeless Ps  Timeless ([] Ps).
  Proof. induction 1; simpl; apply _. Qed.
End list.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
  Lemma big_sepM_later `{AffineBI PROP} Φ m :
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
  Proof. apply (big_opM_commute _). Qed.

  Lemma big_sepM_laterN `{AffineBI PROP} Φ n m :
    ^n ([ map] kx  m, Φ k x)  ([ map] kx  m, ^n Φ k x).
  Proof. apply (big_opM_commute _). Qed.

  Global Instance big_sepM_nil_timeless Φ :
    Timeless ([ map] kx  , Φ k x).
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
  Global Instance big_sepM_timeless Φ m :
    ( k x, Timeless (Φ k x))  Timeless ([ map] kx  m, Φ k x).
  Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
End gmap.

(** ** Big ops over finite sets *)
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
  Implicit Types Φ : A  PROP.

  Lemma big_sepS_later `{AffineBI PROP} Φ X :
     ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
  Proof. apply (big_opS_commute _). Qed.

  Lemma big_sepS_laterN `{AffineBI PROP} Φ n X :
    ^n ([ set] y  X, Φ y)  ([ set] y  X, ^n Φ y).
  Proof. apply (big_opS_commute _). Qed.

  Global Instance big_sepS_nil_timeless Φ : Timeless ([ set] x  , Φ x).
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
  Global Instance big_sepS_timeless Φ X :
    ( x, Timeless (Φ x))  Timeless ([ set] x  X, Φ x).
  Proof. rewrite /big_opS. apply _. Qed.
End gset.

(** ** Big ops over finite multisets *)
Section gmultiset.
  Context `{Countable A}.
  Implicit Types X : gmultiset A.
  Implicit Types Φ : A  PROP.

  Lemma big_sepMS_later `{AffineBI PROP} Φ X :
     ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
649
650
  Proof. apply (big_opMS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
651
652
  Lemma big_sepMS_laterN `{AffineBI PROP} Φ n X :
    ^n ([ mset] y  X, Φ y)  ([ mset] y  X, ^n Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
653
654
  Proof. apply (big_opMS_commute _). Qed.

655
  Global Instance big_sepMS_nil_timeless Φ : Timeless ([ mset] x  , Φ x).
Robbert Krebbers's avatar
Robbert Krebbers committed
656
657
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_timeless Φ X :
658
    ( x, Timeless (Φ x))  Timeless ([ mset] x  X, Φ x).
Robbert Krebbers's avatar
Robbert Krebbers committed
659
660
  Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
Robbert Krebbers's avatar
Robbert Krebbers committed
661
662
End sbi_big_op.
End bi.
663

Robbert Krebbers's avatar
Robbert Krebbers committed
664
665
Hint Resolve bi.big_sepL_nil' bi.big_sepM_empty'
  bi.big_sepS_empty' bi.big_sepMS_empty' | 0.