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.
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
  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.
40
    - intros n P Q ??. by ofe_subst.
41
42
43
44
45
46
47
48
49
50
51
52
53
54
    - 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.

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

  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.

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

  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
75
76
  Global Instance uPred_laterN_homomorphism n : UCMRAHomomorphism (uPred_laterN n).
  Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
77
78
79
80
81
82
83
84
85
86
87
  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 *)
88
Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) (λ k x, P) l)
89
  (at level 200, l at level 10, k, x at level 1, right associativity,
90
   format "[∗  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
91
Notation "'[∗' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) (λ _ x, P) l)
92
  (at level 200, l at level 10, x at level 1, right associativity,
93
   format "[∗  list ]  x  ∈  l ,  P") : uPred_scope.
94

95
96
97
98
Notation "'[∗]' Ps" :=
  (big_opL (M:=uPredUR _) (λ _ x, x) Ps) (at level 20) : uPred_scope.

Notation "'[∗' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) (λ k x, P) m)
99
  (at level 200, m at level 10, k, x at level 1, right associativity,
100
   format "[∗  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
101
Notation "'[∗' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) (λ _ x, P) m)
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, P) X)
106
  (at level 200, X at level 10, x at level 1, right associativity,
107
   format "[∗  set ]  x  ∈  X ,  P") : uPred_scope.
108

109
Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) (λ x, P) X)
Robbert Krebbers's avatar
Robbert Krebbers committed
110
111
112
  (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
Hint Mode PersistentL + ! : typeclass_instances.
118

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

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

130
131
132
133
134
135
136
137
138
139
140
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).
141
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
142
143
144
145
146
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.
147
148
Global Instance imap_persistent {A} (f : nat  A  uPred M) xs :
  ( i x, PersistentP (f i x))  PersistentL (imap f xs).
149
Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
150
151

(** ** Timelessness *)
152
Global Instance big_sep_timeless Ps : TimelessL Ps  TimelessP ([] Ps).
153
154
155
156
157
158
159
160
161
162
163
164
165
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).
166
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
167
168
169
170
171
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.
172
173
Global Instance imap_timeless {A} (f : nat  A  uPred M) xs :
  ( i x, TimelessP (f i x))  TimelessL (imap f xs).
174
Proof. revert f. induction xs; simpl; constructor; naive_solver. Qed.
175
176
177
178
179
180
181

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

182
  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y)  True.
183
  Proof. done. Qed.
184
185
  Lemma big_sepL_nil' P Φ : P  [ list] ky  nil, Φ k y.
  Proof. apply True_intro. Qed.
186
  Lemma big_sepL_cons Φ x l :
187
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
188
  Proof. by rewrite big_opL_cons. Qed.
189
  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
190
191
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
192
193
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
194
195
  Proof. by rewrite big_opL_app. Qed.

196
197
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
198
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
199
  Proof. apply big_opL_forall; apply _. Qed.
200
201
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
202
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
203
  Proof. apply big_opL_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
204
205
206
  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.
207

208
209
210
211
212
213
214
  Global Instance big_sepL_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
           (big_opL (M:=uPredUR M) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
  Global Instance big_sep_mono' :
    Proper (Forall2 () ==> ()) (big_opL (M:=uPredUR M) (λ _ P, P)).
  Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
215

216
217
218
219
  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.
220
221
222
    intros Hli. rewrite -(take_drop_middle l i x) // big_sepL_app /=.
    rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
    rewrite assoc -!(comm _ (Φ _ _)) -assoc. by apply sep_mono_r, wand_intro_l.
223
224
  Qed.

225
  Lemma big_sepL_lookup Φ l i x :
226
    l !! i = Some x  ([ list] ky  l, Φ k y)  Φ i x.
227
  Proof. intros. apply uPred_included. by apply: big_opL_lookup. Qed.
228

Robbert Krebbers's avatar
Robbert Krebbers committed
229
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
230
    x  l  ([ list] y  l, Φ y)  Φ x.
231
  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
232

233
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  uPred M) l :
234
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
235
  Proof. by rewrite big_opL_fmap. Qed.
236
237

  Lemma big_sepL_sepL Φ Ψ l :
238
239
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
240
  Proof. by rewrite big_opL_opL. Qed.
241

242
243
244
245
246
  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.

247
  Lemma big_sepL_later Φ l :
248
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
249
  Proof. apply (big_opL_commute _). Qed.
250

Robbert Krebbers's avatar
Robbert Krebbers committed
251
252
253
254
  Lemma big_sepL_laterN Φ n l :
    ^n ([ list] kx  l, Φ k x)  ([ list] kx  l, ^n Φ k x).
  Proof. apply (big_opL_commute _). Qed.

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

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

  Lemma big_sepL_forall Φ l :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
265
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
266
267
268
269
270
271
272
  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.
273
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
274
275
276
277
    - 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
278
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
279
     [ list] kx  l, Ψ k x.
280
281
282
283
284
285
286
  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
287
  Global Instance big_sepL_nil_persistent Φ :
288
    PersistentP ([ list] kx  [], Φ k x).
289
  Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
  Global Instance big_sepL_persistent Φ l :
291
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  l, Φ k x).
292
293
294
295
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
  Global Instance big_sepL_persistent_id Ps : PersistentL Ps  PersistentP ([] Ps).
  Proof. induction 1; apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
296
  Global Instance big_sepL_nil_timeless Φ :
297
    TimelessP ([ list] kx  [], Φ k x).
298
  Proof. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
  Global Instance big_sepL_timeless Φ l :
300
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  l, Φ k x).
301
302
303
  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
  Global Instance big_sepL_timeless_id Ps : TimelessL Ps  TimelessP ([] Ps).
  Proof. induction 1; apply _. Qed.
304
305
End list.

306
307
308
309
310
311
312
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) :
Robbert Krebbers's avatar
Robbert Krebbers committed
313
314
    ([ list] kx  zip_with f l1 l2, Φ k x)
     ([ list] kx  l1,  y, l2 !! k = Some y  Φ k (f x y)).
315
  Proof.
316
317
    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2]//.
    - apply (anti_symm _), True_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
318
319
320
321
      trans ([ list] __  x :: l1, True : uPred M)%I.
      + rewrite big_sepL_forall. auto using forall_intro, impl_intro_l, True_intro.
      + apply big_sepL_mono=> k y _. apply forall_intro=> z.
        by apply impl_intro_l, pure_elim_l.
322
    - rewrite /= IH. apply sep_proper=> //. apply (anti_symm _).
Robbert Krebbers's avatar
Robbert Krebbers committed
323
324
      + apply forall_intro=>z /=. by apply impl_intro_r, pure_elim_r=>-[->].
      + rewrite (forall_elim y) /=. by eapply impl_elim, pure_intro.
325
326
  Qed.
End list2.
327

328
(** ** Big ops over finite maps *)
329
330
331
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
332
  Implicit Types Φ Ψ : K  A  uPred M.
333

334
  Lemma big_sepM_mono Φ Ψ m1 m2 :
335
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
336
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
337
  Proof.
338
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
339
    - rewrite /big_opM. by apply big_sepL_submseteq, map_to_list_submseteq.
340
    - apply big_opM_forall; apply _ || auto.
341
  Qed.
342
343
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
344
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
345
  Proof. apply big_opM_proper. Qed.
346

347
348
349
350
  Global Instance big_sepM_mono' :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> (=) ==> ())
           (big_opM (M:=uPredUR M) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
351

352
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
353
  Proof. by rewrite big_opM_empty. Qed.
354
355
  Lemma big_sepM_empty' P Φ : P  [ map] kx  , Φ k x.
  Proof. rewrite big_sepM_empty. apply True_intro. Qed.
356

357
  Lemma big_sepM_insert Φ m i x :
358
    m !! i = None 
359
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
360
  Proof. apply: big_opM_insert. Qed.
361

362
  Lemma big_sepM_delete Φ m i x :
363
    m !! i = Some x 
364
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
365
  Proof. apply: big_opM_delete. Qed.
366

367
368
369
370
371
372
373
  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.

374
  Lemma big_sepM_lookup Φ m i x :
375
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
376
377
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
378
379
380
  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.
381

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

385
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
386
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
387
  Proof. by rewrite big_opM_fmap. Qed.
388

Robbert Krebbers's avatar
Robbert Krebbers committed
389
390
391
  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).
392
  Proof. apply: big_opM_insert_override. Qed.
393

Robbert Krebbers's avatar
Robbert Krebbers committed
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
  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.

414
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
415
    m !! i = None 
416
417
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
418
419
  Proof. apply: big_opM_fn_insert. Qed.

420
421
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
422
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
423
  Proof. apply: big_opM_fn_insert'. Qed.
424

425
  Lemma big_sepM_sepM Φ Ψ m :
426
    ([ map] kx  m, Φ k x  Ψ k x)
427
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
428
  Proof. apply: big_opM_opM. Qed.
429

430
431
432
433
434
  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.

435
  Lemma big_sepM_later Φ m :
436
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
437
  Proof. apply (big_opM_commute _). Qed.
438

Robbert Krebbers's avatar
Robbert Krebbers committed
439
440
441
442
  Lemma big_sepM_laterN Φ n m :
    ^n ([ map] kx  m, Φ k x)  ([ map] kx  m, ^n Φ k x).
  Proof. apply (big_opM_commute _). Qed.

443
  Lemma big_sepM_always Φ m :
444
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
445
  Proof. apply (big_opM_commute _). Qed.
446
447

  Lemma big_sepM_always_if p Φ m :
448
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
449
  Proof. apply (big_opM_commute _). Qed.
450
451
452

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
453
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
454
455
456
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
457
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
458
459
460
    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.
461
      by rewrite pure_True // True_impl.
462
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
463
464
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
465
      by rewrite pure_True // True_impl.
466
467
468
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
469
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
470
     [ map] kx  m, Ψ k x.
471
472
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
473
    setoid_rewrite always_impl; setoid_rewrite always_pure.
474
475
476
    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.
477

Robbert Krebbers's avatar
Robbert Krebbers committed
478
  Global Instance big_sepM_empty_persistent Φ :
479
    PersistentP ([ map] kx  , Φ k x).
480
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
481
  Global Instance big_sepM_persistent Φ m :
482
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
483
  Proof. intros. apply big_sepL_persistent=> _ [??]; apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
484
  Global Instance big_sepM_nil_timeless Φ :
485
    TimelessP ([ map] kx  , Φ k x).
486
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
487
  Global Instance big_sepM_timeless Φ m :
488
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
489
  Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
490
491
End gmap.

492

493
(** ** Big ops over finite sets *)
494
495
496
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
497
  Implicit Types Φ : A  uPred M.
498

499
  Lemma big_sepS_mono Φ Ψ X Y :
500
    Y  X  ( x, x  Y  Φ x  Ψ x) 
501
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
502
  Proof.
503
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
504
    - rewrite /big_opM. by apply big_sepL_submseteq, elements_submseteq.
505
    - apply big_opS_forall; apply _ || auto.
506
  Qed.
507
508
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
509
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
510
  Proof. apply: big_opS_proper. Qed.
511

512
513
514
  Global Instance big_sepS_mono' :
     Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opS (M:=uPredUR M) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_opS_forall; apply _ || intros; apply Hf. Qed.
515

516
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
517
  Proof. by rewrite big_opS_empty. Qed.
518
519
  Lemma big_sepS_empty' P Φ : P  [ set] x  , Φ x.
  Proof. rewrite big_sepS_empty. apply True_intro. Qed.
520

521
  Lemma big_sepS_insert Φ X x :
522
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
523
524
  Proof. apply: big_opS_insert. Qed.

525
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
526
    x  X 
527
528
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
529
530
  Proof. apply: big_opS_fn_insert. Qed.

531
  Lemma big_sepS_fn_insert' Φ X x P :
532
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
533
  Proof. apply: big_opS_fn_insert'. Qed.
534

Robbert Krebbers's avatar
Robbert Krebbers committed
535
536
537
538
539
  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.

540
  Lemma big_sepS_delete Φ X x :
541
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
542
  Proof. apply: big_opS_delete. Qed.
543

544
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
545
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
546

547
548
549
550
551
552
553
  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.

554
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
555
  Proof. apply: big_opS_singleton. Qed.
556

557
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
Ralf Jung's avatar
Ralf Jung committed
558
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
559
560
561
562
563
564
565
566
567
568
569
  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.

570
571
572
573
574
575
576
577
578
579
580
  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.

581
  Lemma big_sepS_sepS Φ Ψ X :
582
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
583
  Proof. apply: big_opS_opS. Qed.
584

585
586
587
588
  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.

589
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
590
  Proof. apply (big_opS_commute _). Qed.
591

Robbert Krebbers's avatar
Robbert Krebbers committed
592
593
594
595
  Lemma big_sepS_laterN Φ n X :
    ^n ([ set] y  X, Φ y)  ([ set] y  X, ^n Φ y).
  Proof. apply (big_opS_commute _). Qed.

596
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
597
  Proof. apply (big_opS_commute _). Qed.
598

599
  Lemma big_sepS_always_if q Φ X :
600
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
601
  Proof. apply (big_opS_commute _). Qed.
602
603

  Lemma big_sepS_forall Φ X :
Ralf Jung's avatar
Ralf Jung committed
604
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
605
606
607
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
608
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
609
    induction X as [|x X ? IH] using collection_ind_L.
610
611
    { rewrite big_sepS_empty; auto. }
    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
612
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
613
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
614
      by rewrite pure_True ?True_impl; last set_solver.
615
616
617
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
618
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
619
620
  Proof.
    rewrite always_and_sep_l always_forall.
621
    setoid_rewrite always_impl; setoid_rewrite always_pure.
622
623
624
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
625

626
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
627
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
628
  Global Instance big_sepS_persistent Φ X :
629
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
630
  Proof. rewrite /big_opS. apply _. Qed.
631
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
632
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
633
  Global Instance big_sepS_timeless Φ X :
634
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
635
  Proof. rewrite /big_opS. apply _. Qed.
636
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
637

Robbert Krebbers's avatar
Robbert Krebbers committed
638
639
640
641
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
642
643
644
645
646
647
648
649
650
651
652
653

(** ** 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.
654
    - rewrite /big_opM. by apply big_sepL_submseteq, gmultiset_elements_submseteq.
Robbert Krebbers's avatar
Robbert Krebbers committed
655
656
657
658
659
660
661
    - 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.

662
663
664
  Global Instance big_sepMS_mono' :
     Proper (pointwise_relation _ () ==> (=) ==> ()) (big_opMS (M:=uPredUR M) (A:=A)).
  Proof. intros f g Hf m ? <-. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
665
666
667

  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  True.
  Proof. by rewrite big_opMS_empty. Qed.
668
669
  Lemma big_sepMS_empty' P Φ : P  [ mset] x  , Φ x.
  Proof. rewrite big_sepMS_empty. apply True_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
670
671
672
673
674
675
676
677
678
679
680
681

  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. 

682
683
684
685
686
687
688
  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
689
690
691
692
693
694
695
  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.

696
697
698
699
  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