big_op.v 29 KB
Newer Older
1
2
From iris.algebra Require Export list cmra_big_op.
From iris.base_logic Require Export base_logic.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.prelude Require Import gmap fin_collections gmultiset functions.
4
Import uPred.
5

6
7
8
9
10
(* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
CMRA structure on uPred. *)
Section cmra.
  Context {M : ucmraT}.

11
12
  Instance uPred_valid_inst : Valid (uPred M) := λ P,  n x, {n} x  P n x.
  Instance uPred_validN_inst : ValidN (uPred M) := λ n P,
13
14
15
16
     n' x, n'  n  {n'} x  P n' x.
  Instance uPred_op : Op (uPred M) := uPred_sep.
  Instance uPred_pcore : PCore (uPred M) := λ _, Some True%I.

17
  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN_inst n).
18
19
20
21
22
23
24
25
  Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed.

  Lemma uPred_validN_alt n (P : uPred M) : {n} P  P {n} True%I.
  Proof.
    unseal=> HP; split=> n' x ??; split; [done|].
    intros _. by apply HP.
  Qed.

26
  Lemma uPred_cmra_validN_op_l n P Q : {n} (P  Q)%I  {n} P.
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
  Proof.
    unseal. intros HPQ n' x ??.
    destruct (HPQ n' x) as (x1&x2&->&?&?); auto.
    eapply uPred_mono with x1; eauto using cmra_includedN_l.
  Qed.

  Lemma uPred_included P Q : P  Q  Q  P.
  Proof. intros [P' ->]. apply sep_elim_l. Qed.

  Definition uPred_cmra_mixin : CMRAMixin (uPred M).
  Proof.
    apply cmra_total_mixin; try apply _ || by eauto.
    - intros n P Q ??. by cofe_subst.
    - intros P; split.
      + intros HP n n' x ?. apply HP.
      + intros HP n x. by apply (HP n).
    - intros n P HP n' x ?. apply HP; auto.
    - intros P. by rewrite left_id.
    - intros P Q _. exists True%I. by rewrite left_id.
    - intros n P Q. apply uPred_cmra_validN_op_l.
    - intros n P Q1 Q2 HP HPQ. exists True%I, P; split_and!.
      + by rewrite left_id.
      + move: HP; by rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt.
      + move: HP; rewrite HPQ=> /uPred_cmra_validN_op_l /uPred_validN_alt=> ->.
        by rewrite left_id.
  Qed.

  Canonical Structure uPredR :=
55
    CMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin.
56
57
58
59
60
61
62
63
64
65
66

  Instance uPred_empty : Empty (uPred M) := True%I.

  Definition uPred_ucmra_mixin : UCMRAMixin (uPred M).
  Proof.
    split; last done.
    - by rewrite /empty /uPred_empty uPred_pure_eq.
    - intros P. by rewrite left_id.
  Qed.

  Canonical Structure uPredUR :=
67
    UCMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
68
69
70
71
72
73
74
75

  Global Instance uPred_always_homomorphism : UCMRAHomomorphism uPred_always.
  Proof. split; [split|]. apply _. apply always_sep. apply always_pure. Qed.
  Global Instance uPred_always_if_homomorphism b :
    UCMRAHomomorphism (uPred_always_if b).
  Proof. split; [split|]. apply _. apply always_if_sep. apply always_if_pure. Qed.
  Global Instance uPred_later_homomorphism : UCMRAHomomorphism uPred_later.
  Proof. split; [split|]. apply _. apply later_sep. apply later_True. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
77
  Global Instance uPred_laterN_homomorphism n : UCMRAHomomorphism (uPred_laterN n).
  Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
78
79
80
81
82
83
84
85
86
87
88
  Global Instance uPred_except_0_homomorphism :
    CMRAHomomorphism uPred_except_0.
  Proof. split. apply _. apply except_0_sep. Qed.
  Global Instance uPred_ownM_homomorphism : UCMRAHomomorphism uPred_ownM.
  Proof. split; [split|]. apply _. apply ownM_op. apply ownM_empty'. Qed.
End cmra.

Arguments uPredR : clear implicits.
Arguments uPredUR : clear implicits.

(* Notations *)
89
Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
90

91
Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P))
92
  (at level 200, l at level 10, k, x at level 1, right associativity,
93
94
   format "[∗  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
Notation "'[∗' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P))
95
  (at level 200, l at level 10, x at level 1, right associativity,
96
   format "[∗  list ]  x  ∈  l ,  P") : uPred_scope.
97

98
Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P))
99
  (at level 200, m at level 10, k, x at level 1, right associativity,
100
101
   format "[∗  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
Notation "'[∗' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ _ x, P))
102
  (at level 200, m at level 10, x at level 1, right associativity,
103
   format "[∗  map ]  x  ∈  m ,  P") : uPred_scope.
104

105
Notation "'[∗' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P))
106
  (at level 200, X at level 10, x at level 1, right associativity,
107
   format "[∗  set ]  x  ∈  X ,  P") : uPred_scope.
108

Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
112
Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) X (λ x, P))
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[∗  mset ]  x  ∈  X ,  P") : uPred_scope.

113
(** * Persistence and timelessness of lists of uPreds *)
114
Class PersistentL {M} (Ps : list (uPred M)) :=
115
  persistentL : Forall PersistentP Ps.
116
Arguments persistentL {_} _ {_}.
117

118
119
120
121
Class TimelessL {M} (Ps : list (uPred M)) :=
  timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.

122
(** * Properties *)
123
Section big_op.
124
Context {M : ucmraT}.
125
126
127
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

128
129
Global Instance big_sep_mono' :
  Proper (Forall2 () ==> ()) (big_op (M:=uPredUR M)).
130
131
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

132
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
133
Proof. by rewrite big_op_app. Qed.
134

135
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
136
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
137
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
138
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
139
140
141
142
143
144
Lemma big_sep_elem_of_acc Ps P : P  Ps  [] Ps  P  (P - [] Ps).
Proof.
  intros (Ps1&Ps2&->)%elem_of_list_split.
  rewrite !big_sep_app /=. rewrite assoc (comm _ _ P) -assoc.
  by apply sep_mono_r, wand_intro_l.
Qed.
145

146
(** ** Persistence *)
147
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
148
149
150
151
152
153
154
155
156
157
158
159
160
Proof. induction 1; apply _. Qed.

Global Instance nil_persistent : PersistentL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_persistent P Ps :
  PersistentP P  PersistentL Ps  PersistentL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_persistent Ps Ps' :
  PersistentL Ps  PersistentL Ps'  PersistentL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.

Global Instance fmap_persistent {A} (f : A  uPred M) xs :
  ( x, PersistentP (f x))  PersistentL (f <$> xs).
161
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
162
163
164
165
166
Global Instance zip_with_persistent {A B} (f : A  B  uPred M) xs ys :
  ( x y, PersistentP (f x y))  PersistentL (zip_with f xs ys).
Proof.
  unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
167
168
169
170
171
Global Instance imap_persistent {A} (f : nat  A  uPred M) xs :
  ( i x, PersistentP (f i x))  PersistentL (imap f xs).
Proof.
  rewrite /PersistentL /imap=> ?. generalize 0. induction xs; constructor; auto.
Qed.
172
173

(** ** Timelessness *)
174
Global Instance big_sep_timeless Ps : TimelessL Ps  TimelessP ([] Ps).
175
176
177
178
179
180
181
182
183
184
185
186
187
Proof. induction 1; apply _. Qed.

Global Instance nil_timeless : TimelessL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_timeless P Ps :
  TimelessP P  TimelessL Ps  TimelessL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_timeless Ps Ps' :
  TimelessL Ps  TimelessL Ps'  TimelessL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.

Global Instance fmap_timeless {A} (f : A  uPred M) xs :
  ( x, TimelessP (f x))  TimelessL (f <$> xs).
188
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
189
190
191
192
193
Global Instance zip_with_timeless {A B} (f : A  B  uPred M) xs ys :
  ( x y, TimelessP (f x y))  TimelessL (zip_with f xs ys).
Proof.
  unfold TimelessL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
194
195
196
197
198
199
200
201
202
203
204
205
Global Instance imap_timeless {A} (f : nat  A  uPred M) xs :
  ( i x, TimelessP (f i x))  TimelessL (imap f xs).
Proof.
  rewrite /TimelessL /imap=> ?. generalize 0. induction xs; constructor; auto.
Qed.

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

206
  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y)  True.
207
208
  Proof. done. Qed.
  Lemma big_sepL_cons Φ x l :
209
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
210
  Proof. by rewrite big_opL_cons. Qed.
211
  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
212
213
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
214
215
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
216
217
  Proof. by rewrite big_opL_app. Qed.

218
219
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
220
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
221
  Proof. apply big_opL_forall; apply _. Qed.
222
223
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
224
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
225
  Proof. apply big_opL_proper. Qed.
226
227
228

  Global Instance big_sepL_mono' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
229
230
           (big_opL (M:=uPredUR M) l).
  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
231
232

  Lemma big_sepL_lookup Φ l i x :
233
    l !! i = Some x  ([ list] ky  l, Φ k y)  Φ i x.
234
  Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed.
235

Robbert Krebbers's avatar
Robbert Krebbers committed
236
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
237
    x  l  ([ list] y  l, Φ y)  Φ x.
238
  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
239

240
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  uPred M) l :
241
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
242
  Proof. by rewrite big_opL_fmap. Qed.
243
244

  Lemma big_sepL_sepL Φ Ψ l :
245
246
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
247
  Proof. by rewrite big_opL_opL. Qed.
248

249
250
251
252
253
  Lemma big_sepL_and Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
  Proof. auto using big_sepL_mono with I. Qed.

254
  Lemma big_sepL_later Φ l :
255
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
256
  Proof. apply (big_opL_commute _). Qed.
257

Robbert Krebbers's avatar
Robbert Krebbers committed
258
259
260
261
  Lemma big_sepL_laterN Φ n l :
    ^n ([ list] kx  l, Φ k x)  ([ list] kx  l, ^n Φ k x).
  Proof. apply (big_opL_commute _). Qed.

262
  Lemma big_sepL_always Φ l :
263
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
264
  Proof. apply (big_opL_commute _). Qed.
265
266

  Lemma big_sepL_always_if p Φ l :
267
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
268
  Proof. apply (big_opL_commute _). Qed.
269
270
271

  Lemma big_sepL_forall Φ l :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
272
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
273
274
275
276
277
278
279
  Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. }
    revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
    { rewrite big_sepL_nil; auto with I. }
    rewrite big_sepL_cons. rewrite -always_and_sep_l; apply and_intro.
280
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
281
282
283
284
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Lemma big_sepL_impl Φ Ψ l :
Ralf Jung's avatar
Ralf Jung committed
285
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
286
     [ list] kx  l, Ψ k x.
287
288
289
290
291
292
293
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
    setoid_rewrite always_impl; setoid_rewrite always_pure.
    rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
294
  Global Instance big_sepL_nil_persistent Φ :
295
    PersistentP ([ list] kx  [], Φ k x).
296
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
297
  Global Instance big_sepL_persistent Φ l :
298
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  l, Φ k x).
299
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
300
  Global Instance big_sepL_nil_timeless Φ :
301
    TimelessP ([ list] kx  [], Φ k x).
302
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
  Global Instance big_sepL_timeless Φ l :
304
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  l, Φ k x).
305
  Proof. rewrite /big_opL. apply _. Qed.
306
307
End list.

308

309
(** ** Big ops over finite maps *)
310
311
312
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
313
  Implicit Types Φ Ψ : K  A  uPred M.
314

315
  Lemma big_sepM_mono Φ Ψ m1 m2 :
316
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
317
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
318
  Proof.
319
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
320
321
322
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, map_to_list_contains.
    - apply big_opM_forall; apply _ || auto.
323
  Qed.
324
325
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
326
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
327
  Proof. apply big_opM_proper. Qed.
328
329

  Global Instance big_sepM_mono' m :
330
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
331
332
           (big_opM (M:=uPredUR M) m).
  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
333

334
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
335
  Proof. by rewrite big_opM_empty. Qed.
336

337
  Lemma big_sepM_insert Φ m i x :
338
    m !! i = None 
339
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
340
  Proof. apply: big_opM_insert. Qed.
341

342
  Lemma big_sepM_delete Φ m i x :
343
    m !! i = Some x 
344
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
345
  Proof. apply: big_opM_delete. Qed.
346

347
348
349
350
351
352
353
  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.

354
  Lemma big_sepM_lookup Φ m i x :
355
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
356
357
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
358
359
360
  Lemma big_sepM_lookup_dom (Φ : K  uPred M) m i :
    is_Some (m !! i)  ([ map] k_  m, Φ k)  Φ i.
  Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
361

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

365
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
366
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
367
  Proof. by rewrite big_opM_fmap. Qed.
368

Robbert Krebbers's avatar
Robbert Krebbers committed
369
370
371
  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).
372
  Proof. apply: big_opM_insert_override. Qed.
373

Robbert Krebbers's avatar
Robbert Krebbers committed
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
  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.

394
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
395
    m !! i = None 
396
397
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
398
399
  Proof. apply: big_opM_fn_insert. Qed.

400
401
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
402
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
403
  Proof. apply: big_opM_fn_insert'. Qed.
404

405
  Lemma big_sepM_sepM Φ Ψ m :
406
    ([ map] kx  m, Φ k x  Ψ k x)
407
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
408
  Proof. apply: big_opM_opM. Qed.
409

410
411
412
413
414
  Lemma big_sepM_and Φ Ψ m :
    ([ map] kx  m, Φ k x  Ψ k x)
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
  Proof. auto using big_sepM_mono with I. Qed.

415
  Lemma big_sepM_later Φ m :
416
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
417
  Proof. apply (big_opM_commute _). Qed.
418

Robbert Krebbers's avatar
Robbert Krebbers committed
419
420
421
422
  Lemma big_sepM_laterN Φ n m :
    ^n ([ map] kx  m, Φ k x)  ([ map] kx  m, ^n Φ k x).
  Proof. apply (big_opM_commute _). Qed.

423
  Lemma big_sepM_always Φ m :
424
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
425
  Proof. apply (big_opM_commute _). Qed.
426
427

  Lemma big_sepM_always_if p Φ m :
428
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
429
  Proof. apply (big_opM_commute _). Qed.
430
431
432

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
433
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
434
435
436
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
437
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
438
439
440
    induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
    rewrite big_sepM_insert // -always_and_sep_l. apply and_intro.
    - rewrite (forall_elim i) (forall_elim x) lookup_insert.
441
      by rewrite pure_True // True_impl.
442
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
443
444
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
445
      by rewrite pure_True // True_impl.
446
447
448
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
449
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
450
     [ map] kx  m, Ψ k x.
451
452
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
453
    setoid_rewrite always_impl; setoid_rewrite always_pure.
454
455
456
    rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
457

Robbert Krebbers's avatar
Robbert Krebbers committed
458
  Global Instance big_sepM_empty_persistent Φ :
459
    PersistentP ([ map] kx  , Φ k x).
460
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
461
  Global Instance big_sepM_persistent Φ m :
462
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
463
  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
464
  Global Instance big_sepM_nil_timeless Φ :
465
    TimelessP ([ map] kx  , Φ k x).
466
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
467
  Global Instance big_sepM_timeless Φ m :
468
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
469
  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
470
471
End gmap.

472

473
(** ** Big ops over finite sets *)
474
475
476
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
477
  Implicit Types Φ : A  uPred M.
478

479
  Lemma big_sepS_mono Φ Ψ X Y :
480
    Y  X  ( x, x  Y  Φ x  Ψ x) 
481
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
482
  Proof.
483
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
484
485
486
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, elements_contains.
    - apply big_opS_forall; apply _ || auto.
487
  Qed.
488
489
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
490
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
491
  Proof. apply: big_opS_proper. Qed.
492

493
  Global Instance big_sepS_mono' X :
494
495
496
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

497
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
498
  Proof. by rewrite big_opS_empty. Qed.
499

500
  Lemma big_sepS_insert Φ X x :
501
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
502
503
  Proof. apply: big_opS_insert. Qed.

504
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
505
    x  X 
506
507
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
508
509
  Proof. apply: big_opS_fn_insert. Qed.

510
  Lemma big_sepS_fn_insert' Φ X x P :
511
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
512
  Proof. apply: big_opS_fn_insert'. Qed.
513

Robbert Krebbers's avatar
Robbert Krebbers committed
514
515
516
517
518
  Lemma big_sepS_union Φ X Y :
    X  Y 
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
  Proof. apply: big_opS_union. Qed.

519
  Lemma big_sepS_delete Φ X x :
520
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
521
  Proof. apply: big_opS_delete. Qed.
522

523
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
524
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
525

526
527
528
529
530
531
532
  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.

533
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
534
  Proof. apply: big_opS_singleton. Qed.
535

536
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
Ralf Jung's avatar
Ralf Jung committed
537
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
538
539
540
541
542
543
544
545
546
547
548
  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.
      by rewrite IH pure_True // left_id.
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
      by rewrite !big_sepS_insert // IH pure_False // False_impl left_id.
  Qed.

549
550
551
552
553
554
555
556
557
558
559
  Lemma big_sepS_filter_acc (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 ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
      as (Z&->&?); first set_solver.
    rewrite big_sepS_union // big_sepS_filter. by apply sep_mono_r, wand_intro_l.
  Qed.

560
  Lemma big_sepS_sepS Φ Ψ X :
561
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
562
  Proof. apply: big_opS_opS. Qed.
563

564
565
566
567
  Lemma big_sepS_and Φ Ψ X :
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
  Proof. auto using big_sepS_mono with I. Qed.

568
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
569
  Proof. apply (big_opS_commute _). Qed.
570

Robbert Krebbers's avatar
Robbert Krebbers committed
571
572
573
574
  Lemma big_sepS_laterN Φ n X :
    ^n ([ set] y  X, Φ y)  ([ set] y  X, ^n Φ y).
  Proof. apply (big_opS_commute _). Qed.

575
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
576
  Proof. apply (big_opS_commute _). Qed.
577

578
  Lemma big_sepS_always_if q Φ X :
579
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
580
  Proof. apply (big_opS_commute _). Qed.
581
582

  Lemma big_sepS_forall Φ X :
Ralf Jung's avatar
Ralf Jung committed
583
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
584
585
586
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
587
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
588
    induction X as [|x X ? IH] using collection_ind_L.
589
590
    { rewrite big_sepS_empty; auto. }
    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
591
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
592
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
593
      by rewrite pure_True ?True_impl; last set_solver.
594
595
596
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
597
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
598
599
  Proof.
    rewrite always_and_sep_l always_forall.
600
    setoid_rewrite always_impl; setoid_rewrite always_pure.
601
602
603
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
604

605
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
606
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
607
  Global Instance big_sepS_persistent Φ X :
608
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
609
  Proof. rewrite /big_opS. apply _. Qed.
610
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
611
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
612
  Global Instance big_sepS_timeless Φ X :
613
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
614
  Proof. rewrite /big_opS. apply _. Qed.
615
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
616

Robbert Krebbers's avatar
Robbert Krebbers committed
617
618
619
620
Lemma big_sepM_dom `{Countable K} {A} (Φ : K  uPred M) (m : gmap K A) :
  ([ map] k_  m, Φ k)  ([ set] k  dom _ m, Φ k).
Proof. apply: big_opM_dom. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
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
649
650
651
652
653
654
655
656
657
658
659

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

  Lemma big_sepMS_mono Φ Ψ X Y :
    Y  X  ( x, x  Y  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  [ mset] x  Y, Ψ x.
  Proof.
    intros HX HΦ. trans ([ mset] x  Y, Φ x)%I.
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, gmultiset_elements_contains.
    - apply big_opMS_forall; apply _ || auto.
  Qed.
  Lemma big_sepMS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  ([ mset] x  X, Ψ x).
  Proof. apply: big_opMS_proper. Qed.

  Global Instance big_sepMS_mono' X :
     Proper (pointwise_relation _ () ==> ()) (big_opMS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.

  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  True.
  Proof. by rewrite big_opMS_empty. Qed.

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
  Proof. apply: big_opMS_union. Qed.

  Lemma big_sepMS_delete Φ X x :
    x  X  ([ mset] y  X, Φ y)  Φ x  [ mset] y  X  {[ x ]}, Φ y.
  Proof. apply: big_opMS_delete. Qed.

  Lemma big_sepMS_elem_of Φ X x : x  X  ([ mset] y  X, Φ y)  Φ x.
  Proof. intros. apply uPred_included. by apply: big_opMS_elem_of. Qed. 

660
661
662
663
664
665
666
  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
667
668
669
670
671
672
673
  Lemma big_sepMS_singleton Φ x : ([ mset] y  {[ x ]}, Φ y)  Φ x.
  Proof. apply: big_opMS_singleton. Qed.

  Lemma big_sepMS_sepMS Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
  Proof. apply: big_opMS_opMS. Qed.

674
675
676
677
  Lemma big_sepMS_and Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
  Proof. auto using big_sepMS_mono with I. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
678
679
680
  Lemma big_sepMS_later Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
  Proof. apply (big_opMS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
681
682
683
684
  Lemma big_sepMS_laterN Φ n X :
    ^n ([ mset] y  X, Φ y)  ([ mset] y  X, ^n Φ y).
  Proof. apply (big_opMS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
  Lemma big_sepMS_always Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
  Proof. apply (big_opMS_commute _). Qed.

  Lemma big_sepMS_always_if q Φ X :
    ?q ([ mset] y  X, Φ y)  ([ mset] y  X, ?q Φ y).
  Proof. apply (big_opMS_commute _). Qed.

  Global Instance big_sepMS_empty_persistent Φ : PersistentP ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
  Global Instance big_sepMS_nil_timeless Φ : TimelessP ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
703
End big_op.