big_op.v 30.8 KB
Newer Older
1
2
From iris.algebra Require Export list cmra_big_op.
From iris.base_logic Require Export base_logic.
Ralf Jung's avatar
Ralf Jung committed
3
From stdpp 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
Hint Mode PersistentL + ! : typeclass_instances.
119

120
121
122
Class TimelessL {M} (Ps : list (uPred M)) :=
  timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.
123
Hint Mode TimelessP + ! : typeclass_instances.
124

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
Lemma big_sep_submseteq Ps Qs : Qs + Ps  [] Ps  [] Qs.
Proof. intros. apply uPred_included. by apply: big_op_submseteq. Qed.
140
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
141
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
142
Lemma big_sep_elem_of_acc Ps P : P  Ps  [] Ps  P  (P - [] Ps).
143
Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed.
144

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

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

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

217
218
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
219
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
220
  Proof. apply big_opL_forall; apply _. Qed.
221
222
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
223
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
224
  Proof. apply big_opL_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
226
227
  Lemma big_sepL_submseteq (Φ : A  uPred M) l1 l2 :
    l1 + l2  ([ list] y  l2, Φ y)  [ list] y  l1, Φ y.
  Proof. intros ?. apply uPred_included. by apply: big_opL_submseteq. Qed.
228
229
230

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

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

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

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

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

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

259
260
261
262
263
  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.

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

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

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

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

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

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
344
345
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.
346

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

353
  Lemma big_sepM_mono Φ Ψ m1 m2 :
354
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
355
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
356
  Proof.
357
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
358
359
    - apply uPred_included. apply: big_op_submseteq.
      by apply fmap_submseteq, map_to_list_submseteq.
360
    - apply big_opM_forall; apply _ || auto.
361
  Qed.
362
363
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
364
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
365
  Proof. apply big_opM_proper. Qed.
366
367

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

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

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

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

385
386
387
388
389
390
391
  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.

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

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

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

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

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

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

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

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

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

448
449
450
451
452
  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.

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

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

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

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

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

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

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

510

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

517
  Lemma big_sepS_mono Φ Ψ X Y :
518
    Y  X  ( x, x  Y  Φ x  Ψ x) 
519
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
520
  Proof.
521
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
522
523
    - apply uPred_included. apply: big_op_submseteq.
      by apply fmap_submseteq, elements_submseteq.
524
    - apply big_opS_forall; apply _ || auto.
525
  Qed.
526
527
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
528
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
529
  Proof. apply: big_opS_proper. Qed.
530

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

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

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

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

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

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

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

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

564
565
566
567
568
569
570
  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.

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

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

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

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

602
603
604
605
  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.

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

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

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

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

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
655
656
657
658
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
659
660
661
662
663
664
665
666
667
668
669
670

(** ** 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
671
672
    - apply uPred_included. apply: big_op_submseteq.
      by apply fmap_submseteq, gmultiset_elements_submseteq.
Robbert Krebbers's avatar
Robbert Krebbers committed
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
    - 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. 

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

712
713
714
715
  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
716
717
718
  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
719
720
721
722
  Lemma big_sepMS_laterN Φ n X :
    ^n ([ mset] y  X,