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
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
Lemma big_sep_elem_of_acc Ps P : P  Ps  [] Ps  P  (P - [] Ps).
140
Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed.
141

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

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

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

214
215
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
216
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
217
  Proof. apply big_opL_forall; apply _. Qed.
218
219
  Lemma big_sepL_proper Φ Ψ 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_proper. Qed.
222
223
224
  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.
225
226
227

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

231
232
233
234
  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.
235
236
    intros Hli. apply big_sep_elem_of_acc, (elem_of_list_lookup_2 _ i).
    by rewrite list_lookup_imap Hli.
237
238
  Qed.

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

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

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

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

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

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

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

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

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

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

315
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
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.
343

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

507

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
652
653
654
655
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
656
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

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

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

709
710
711
712
  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.

<