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

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
      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_affine Φ l :
    ( k x, Affine (Φ k x))  Affine ([ list] kx  l, Φ k x).
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
174
End sep_list.
175

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

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

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

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

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

313
  Lemma big_sepM_insert Φ m i x :
314
    m !! i = None 
315
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
316
  Proof. apply big_opM_insert. Qed.
317

318
  Lemma big_sepM_delete Φ m i x :
319
    m !! i = Some x 
320
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
321
  Proof. apply big_opM_delete. Qed.
322

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
345
346
347
  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).
348
  Proof. apply big_opM_insert_override. Qed.
349

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

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

381
  Lemma big_sepM_sepM Φ Ψ m :
382
    ([ map] kx  m, Φ k x  Ψ k x)
383
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
384
  Proof. apply big_opM_opM. Qed.
385

386
387
388
  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
389
  Proof. auto using and_intro, big_sepM_mono, and_elim_l, and_elim_r. Qed.
390

Robbert Krebbers's avatar
Robbert Krebbers committed
391
  Lemma big_sepM_persistently `{AffineBI PROP} Φ m :
392
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
393
  Proof. apply (big_opM_commute _). Qed.
394

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

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

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

  Global Instance big_sepM_affine Φ m :
    ( k x, Affine (Φ k x))  Affine ([ map] kx  m, Φ k x).
  Proof.
     intros. apply big_sepL_affine=> _ [??]; apply _.
  Qed.
442
443
End gmap.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  Lemma big_sepS_impl Φ Ψ X :
Robbert Krebbers's avatar
Robbert Krebbers committed
573
574
575
    ([ set] x  X, Φ x) -
     ( x, x  X  Φ x - Ψ x) -
    [ set] x  X, Ψ x.
576
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
577
578
579
580
581
582
583
584
585
    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.
586
  Qed.
587
  Global Instance big_sepS_empty_persistent Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
588
    Persistent ([ set] x  , Φ x).
589
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
590
  Global Instance big_sepS_persistent Φ X :
591
    ( x, Persistent (Φ x))  Persistent ([ set] x  X, Φ x).
592
  Proof. rewrite /big_opS. apply _. Qed.
593
594
595
596

  Global Instance big_sepS_affine Φ X :
    ( x, Affine (Φ x))  Affine ([ set] x  X, Φ x).
  Proof. rewrite /big_opS. apply _. Qed.
597
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
598

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

Robbert Krebbers's avatar
Robbert Krebbers committed
603
604
605
606
607

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

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

622
  Global Instance big_sepMS_mono' :
Robbert Krebbers's avatar
Robbert Krebbers committed
623
624
     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
625

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

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
633
  Proof. apply big_opMS_union. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
634
635
636

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

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

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

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

657
658
  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
659
  Proof. auto using and_intro, big_sepMS_mono, and_elim_l, and_elim_r. Qed.
660

Robbert Krebbers's avatar
Robbert Krebbers committed
661
662
  Lemma big_sepMS_persistently `{AffineBI PROP} Φ X :
     ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
Robbert Krebbers's avatar
Robbert Krebbers committed
663
664
  Proof. apply (big_opMS_commute _). Qed.

665
  Global Instance big_sepMS_empty_persistent Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
666
667
    Persistent ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
668
  Global Instance big_sepMS_persistent Φ X :<