big_op.v 30.7 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
Set Default Proof Using "Type".
5
Import uPred.
6

7
8
9
10
11
(* 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}.

12
13
  Instance uPred_valid_inst : Valid (uPred M) := λ P,  n x, {n} x  P n x.
  Instance uPred_validN_inst : ValidN (uPred M) := λ n P,
14
15
16
17
     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.

18
  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN_inst n).
19
20
21
22
23
24
25
26
  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.

27
  Lemma uPred_cmra_validN_op_l n P Q : {n} (P  Q)%I  {n} P.
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
55
  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 :=
56
    CMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin.
57
58
59
60
61
62
63
64
65
66
67

  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 :=
68
    UCMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
69
70
71
72
73
74
75
76

  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
77
78
  Global Instance uPred_laterN_homomorphism n : UCMRAHomomorphism (uPred_laterN n).
  Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
79
80
81
82
83
84
85
86
87
88
89
  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 *)
90
Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
91

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
113
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.

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

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

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

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

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

136
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
137
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
138
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
139
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
140
Lemma big_sep_elem_of_acc Ps P : P  Ps  [] Ps  P  (P - [] Ps).
141
Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed.
142

143
(** ** Persistence *)
144
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
145
146
147
148
149
150
151
152
153
154
155
156
157
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).
158
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
159
160
161
162
163
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.
164
165
166
167
168
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.
169
170

(** ** Timelessness *)
171
Global Instance big_sep_timeless Ps : TimelessL Ps  TimelessP ([] Ps).
172
173
174
175
176
177
178
179
180
181
182
183
184
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).
185
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
186
187
188
189
190
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.
191
192
193
194
195
196
197
198
199
200
201
202
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.

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

215
216
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
217
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
218
  Proof. apply big_opL_forall; apply _. Qed.
219
220
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
221
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
222
  Proof. apply big_opL_proper. Qed.
223
224
225
  Lemma big_sepL_contains (Φ : A  uPred M) l1 l2 :
    l1 `contains` l2  ([ list] y  l2, Φ y)  [ list] y  l1, Φ y.
  Proof. intros ?. apply uPred_included. by apply: big_opL_contains. 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
233
234
235
  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.
236
237
    intros Hli. apply big_sep_elem_of_acc, (elem_of_list_lookup_2 _ i).
    by rewrite list_lookup_imap Hli.
238
239
  Qed.

240
  Lemma big_sepL_lookup Φ l i x :
241
    l !! i = Some x  ([ list] ky  l, Φ k y)  Φ i x.
242
  Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed.
243

Robbert Krebbers's avatar
Robbert Krebbers committed
244
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
245
    x  l  ([ list] y  l, Φ y)  Φ x.
246
  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
247

248
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  uPred M) l :
249
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
250
  Proof. by rewrite big_opL_fmap. Qed.
251
252

  Lemma big_sepL_sepL Φ Ψ l :
253
254
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
255
  Proof. by rewrite big_opL_opL. Qed.
256

257
258
259
260
261
  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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
266
267
268
269
  Lemma big_sepL_laterN Φ n l :
    ^n ([ list] kx  l, Φ k x)  ([ list] kx  l, ^n Φ k x).
  Proof. apply (big_opL_commute _). Qed.

270
  Lemma big_sepL_always Φ l :
271
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
272
  Proof. apply (big_opL_commute _). Qed.
273
274

  Lemma big_sepL_always_if p Φ l :
275
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
276
  Proof. apply (big_opL_commute _). Qed.
277
278
279

  Lemma big_sepL_forall Φ l :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
280
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
281
282
283
284
285
286
287
  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.
288
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
289
290
291
292
    - 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
293
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
294
     [ list] kx  l, Ψ k x.
295
296
297
298
299
300
301
  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
302
  Global Instance big_sepL_nil_persistent Φ :
303
    PersistentP ([ list] kx  [], Φ k x).
304
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
305
  Global Instance big_sepL_persistent Φ l :
306
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  l, Φ k x).
307
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
308
  Global Instance big_sepL_nil_timeless Φ :
309
    TimelessP ([ list] kx  [], Φ k x).
310
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
311
  Global Instance big_sepL_timeless Φ l :
312
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  l, Φ k x).
313
  Proof. rewrite /big_opL. apply _. Qed.
314
315
End list.

316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
Section list2.
  Context {A : Type}.
  Implicit Types l : list A.
  Implicit Types Φ Ψ : nat  A  uPred M.
  (* 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) :
    ([ list] kx  zip_with f l1 l2, Φ k x)  ([ list] kx  l1,  y, l2 !! k = Some y  Φ k (f x y)).
  Proof.
    revert Φ l2; induction l1; intros Φ l2; first by rewrite /= big_sepL_nil.
    destruct l2; simpl.
    { rewrite big_sepL_nil. apply (anti_symm _); last exact: True_intro.
      (* TODO: Can this be done simpler? *)
      rewrite -(big_sepL_mono (λ _ _, True%I)).
      - rewrite big_sepL_forall. apply forall_intro=>k. apply forall_intro=>b.
        apply impl_intro_r. apply True_intro.
      - intros k b _. apply forall_intro=>c. apply impl_intro_l. rewrite right_id.
        apply pure_elim'. done.
    }
    rewrite !big_sepL_cons. apply sep_proper; last exact: IHl1.
    apply (anti_symm _).
    - apply forall_intro=>c'. simpl. apply impl_intro_r.
      eapply pure_elim; first exact: and_elim_r. intros [=->].
      apply and_elim_l.
    - rewrite (forall_elim c). simpl. eapply impl_elim; first done.
      apply pure_intro. done.
  Qed.
End list2.
344

345
(** ** Big ops over finite maps *)
346
347
348
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
349
  Implicit Types Φ Ψ : K  A  uPred M.
350

351
  Lemma big_sepM_mono Φ Ψ m1 m2 :
352
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
353
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
354
  Proof.
355
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
356
357
358
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, map_to_list_contains.
    - apply big_opM_forall; apply _ || auto.
359
  Qed.
360
361
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
362
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
363
  Proof. apply big_opM_proper. Qed.
364
365

  Global Instance big_sepM_mono' m :
366
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
367
368
           (big_opM (M:=uPredUR M) m).
  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
369

370
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
371
  Proof. by rewrite big_opM_empty. Qed.
372

373
  Lemma big_sepM_insert Φ m i x :
374
    m !! i = None 
375
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
376
  Proof. apply: big_opM_insert. Qed.
377

378
  Lemma big_sepM_delete Φ m i x :
379
    m !! i = Some x 
380
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
381
  Proof. apply: big_opM_delete. Qed.
382

383
384
385
386
387
388
389
  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.

390
  Lemma big_sepM_lookup Φ m i x :
391
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
392
393
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
394
395
396
  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.
397

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

401
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
402
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
403
  Proof. by rewrite big_opM_fmap. Qed.
404

Robbert Krebbers's avatar
Robbert Krebbers committed
405
406
407
  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).
408
  Proof. apply: big_opM_insert_override. Qed.
409

Robbert Krebbers's avatar
Robbert Krebbers committed
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
  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.

430
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
431
    m !! i = None 
432
433
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
434
435
  Proof. apply: big_opM_fn_insert. Qed.

436
437
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
438
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
439
  Proof. apply: big_opM_fn_insert'. Qed.
440

441
  Lemma big_sepM_sepM Φ Ψ m :
442
    ([ map] kx  m, Φ k x  Ψ k x)
443
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
444
  Proof. apply: big_opM_opM. Qed.
445

446
447
448
449
450
  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.

451
  Lemma big_sepM_later Φ m :
452
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
453
  Proof. apply (big_opM_commute _). Qed.
454

Robbert Krebbers's avatar
Robbert Krebbers committed
455
456
457
458
  Lemma big_sepM_laterN Φ n m :
    ^n ([ map] kx  m, Φ k x)  ([ map] kx  m, ^n Φ k x).
  Proof. apply (big_opM_commute _). Qed.

459
  Lemma big_sepM_always Φ m :
460
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
461
  Proof. apply (big_opM_commute _). Qed.
462
463

  Lemma big_sepM_always_if p Φ m :
464
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
465
  Proof. apply (big_opM_commute _). Qed.
466
467
468

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
469
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
470
471
472
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
473
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
474
475
476
    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.
477
      by rewrite pure_True // True_impl.
478
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
479
480
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
481
      by rewrite pure_True // True_impl.
482
483
484
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
485
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
486
     [ map] kx  m, Ψ k x.
487
488
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
489
    setoid_rewrite always_impl; setoid_rewrite always_pure.
490
491
492
    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.
493

Robbert Krebbers's avatar
Robbert Krebbers committed
494
  Global Instance big_sepM_empty_persistent Φ :
495
    PersistentP ([ map] kx  , Φ k x).
496
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
497
  Global Instance big_sepM_persistent Φ m :
498
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
499
  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
500
  Global Instance big_sepM_nil_timeless Φ :
501
    TimelessP ([ map] kx  , Φ k x).
502
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
503
  Global Instance big_sepM_timeless Φ m :
504
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
505
  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
506
507
End gmap.

508

509
(** ** Big ops over finite sets *)
510
511
512
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
513
  Implicit Types Φ : A  uPred M.
514

515
  Lemma big_sepS_mono Φ Ψ X Y :
516
    Y  X  ( x, x  Y  Φ x  Ψ x) 
517
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
518
  Proof.
519
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
520
521
522
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, elements_contains.
    - apply big_opS_forall; apply _ || auto.
523
  Qed.
524
525
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
526
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
527
  Proof. apply: big_opS_proper. Qed.
528

529
  Global Instance big_sepS_mono' X :
530
531
532
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

533
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
534
  Proof. by rewrite big_opS_empty. Qed.
535

536
  Lemma big_sepS_insert Φ X x :
537
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
538
539
  Proof. apply: big_opS_insert. Qed.

540
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
541
    x  X 
542
543
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
544
545
  Proof. apply: big_opS_fn_insert. Qed.

546
  Lemma big_sepS_fn_insert' Φ X x P :
547
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
548
  Proof. apply: big_opS_fn_insert'. Qed.
549

Robbert Krebbers's avatar
Robbert Krebbers committed
550
551
552
553
554
  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.

555
  Lemma big_sepS_delete Φ X x :
556
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
557
  Proof. apply: big_opS_delete. Qed.
558

559
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
560
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
561

562
563
564
565
566
567
568
  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.

569
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
570
  Proof. apply: big_opS_singleton. Qed.
571

572
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
Ralf Jung's avatar
Ralf Jung committed
573
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
574
575
576
577
578
579
580
581
582
583
584
  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.

585
586
587
588
589
590
591
592
593
594
595
  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.

596
  Lemma big_sepS_sepS Φ Ψ X :
597
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
598
  Proof. apply: big_opS_opS. Qed.
599

600
601
602
603
  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.

604
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
605
  Proof. apply (big_opS_commute _). Qed.
606

Robbert Krebbers's avatar
Robbert Krebbers committed
607
608
609
610
  Lemma big_sepS_laterN Φ n X :
    ^n ([ set] y  X, Φ y)  ([ set] y  X, ^n Φ y).
  Proof. apply (big_opS_commute _). Qed.

611
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
612
  Proof. apply (big_opS_commute _). Qed.
613

614
  Lemma big_sepS_always_if q Φ X :
615
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
616
  Proof. apply (big_opS_commute _). Qed.
617
618

  Lemma big_sepS_forall Φ X :
Ralf Jung's avatar
Ralf Jung committed
619
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
620
621
622
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
623
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
624
    induction X as [|x X ? IH] using collection_ind_L.
625
626
    { rewrite big_sepS_empty; auto. }
    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
627
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
628
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
629
      by rewrite pure_True ?True_impl; last set_solver.
630
631
632
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
633
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
634
635
  Proof.
    rewrite always_and_sep_l always_forall.
636
    setoid_rewrite always_impl; setoid_rewrite always_pure.
637
638
639
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
640

641
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
642
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
643
  Global Instance big_sepS_persistent Φ X :
644
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
645
  Proof. rewrite /big_opS. apply _. Qed.
646
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
647
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
648
  Global Instance big_sepS_timeless Φ X :
649
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
650
  Proof. rewrite /big_opS. apply _. Qed.
651
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
652

Robbert Krebbers's avatar
Robbert Krebbers committed
653
654
655
656
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
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695

(** ** 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. 

696
697
698
699
700
701
702
  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
703
704
705
706
707
708
709
  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.

710
711