big_op.v 26.1 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
76
77
78
79
80
81
82
83
84
85
86

  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.
  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 *)
87
Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
88

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
107
108
109
110
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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  Lemma big_sepL_sepL Φ Ψ l :
243
244
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
245
  Proof. by rewrite big_opL_opL. Qed.
246
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
251

  Lemma big_sepL_always Φ l :
252
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
253
  Proof. apply (big_opL_commute _). Qed.
254
255

  Lemma big_sepL_always_if p Φ l :
256
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
257
  Proof. apply (big_opL_commute _). Qed.
258
259
260

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

297

298
(** ** Big ops over finite maps *)
299
300
301
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
302
  Implicit Types Φ Ψ : K  A  uPred M.
303

304
  Lemma big_sepM_mono Φ Ψ m1 m2 :
305
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
306
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
307
  Proof.
308
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
309
310
311
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, map_to_list_contains.
    - apply big_opM_forall; apply _ || auto.
312
  Qed.
313
314
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
315
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
316
  Proof. apply big_opM_proper. Qed.
317
318

  Global Instance big_sepM_mono' m :
319
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
320
321
           (big_opM (M:=uPredUR M) m).
  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
322

323
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
324
  Proof. by rewrite big_opM_empty. Qed.
325

326
  Lemma big_sepM_insert Φ m i x :
327
    m !! i = None 
328
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
329
  Proof. apply: big_opM_insert. Qed.
330

331
  Lemma big_sepM_delete Φ m i x :
332
    m !! i = Some x 
333
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
334
  Proof. apply: big_opM_delete. Qed.
335

336
337
338
339
340
341
342
  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.

343
  Lemma big_sepM_lookup Φ m i x :
344
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
345
346
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
347
348
349
  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.
350

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

354
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
355
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
356
  Proof. by rewrite big_opM_fmap. Qed.
357

358
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
359
    m !! i = Some x 
360
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
361
  Proof. apply: big_opM_insert_override. Qed.
362

363
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
364
    m !! i = None 
365
366
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
367
368
  Proof. apply: big_opM_fn_insert. Qed.

369
370
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
371
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
372
  Proof. apply: big_opM_fn_insert'. Qed.
373

374
  Lemma big_sepM_sepM Φ Ψ m :
375
376
       ([ map] kx  m, Φ k x  Ψ k x)
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
377
  Proof. apply: big_opM_opM. Qed.
378

379
  Lemma big_sepM_later Φ m :
380
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
381
  Proof. apply (big_opM_commute _). Qed.
382

383
  Lemma big_sepM_always Φ m :
384
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
385
  Proof. apply (big_opM_commute _). Qed.
386
387

  Lemma big_sepM_always_if p Φ m :
388
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
389
  Proof. apply (big_opM_commute _). Qed.
390
391
392

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
393
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
394
395
396
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
397
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
398
399
400
    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.
401
      by rewrite pure_True // True_impl.
402
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
403
404
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
405
      by rewrite pure_True // True_impl.
406
407
408
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
409
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
410
     [ map] kx  m, Ψ k x.
411
412
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
413
    setoid_rewrite always_impl; setoid_rewrite always_pure.
414
415
416
    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.
417

Robbert Krebbers's avatar
Robbert Krebbers committed
418
  Global Instance big_sepM_empty_persistent Φ :
419
    PersistentP ([ map] kx  , Φ k x).
420
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
421
  Global Instance big_sepM_persistent Φ m :
422
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
423
  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
424
  Global Instance big_sepM_nil_timeless Φ :
425
    TimelessP ([ map] kx  , Φ k x).
426
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
427
  Global Instance big_sepM_timeless Φ m :
428
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
429
  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
430
431
End gmap.

432

433
(** ** Big ops over finite sets *)
434
435
436
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
437
  Implicit Types Φ : A  uPred M.
438

439
  Lemma big_sepS_mono Φ Ψ X Y :
440
    Y  X  ( x, x  Y  Φ x  Ψ x) 
441
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
442
  Proof.
443
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
444
445
446
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, elements_contains.
    - apply big_opS_forall; apply _ || auto.
447
  Qed.
448
449
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
450
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
451
  Proof. apply: big_opS_proper. Qed.
452

453
  Global Instance big_sepS_mono' X :
454
455
456
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

457
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
458
  Proof. by rewrite big_opS_empty. Qed.
459

460
  Lemma big_sepS_insert Φ X x :
461
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
462
463
  Proof. apply: big_opS_insert. Qed.

464
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
465
    x  X 
466
467
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
468
469
  Proof. apply: big_opS_fn_insert. Qed.

470
  Lemma big_sepS_fn_insert' Φ X x P :
471
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
472
  Proof. apply: big_opS_fn_insert'. Qed.
473

Robbert Krebbers's avatar
Robbert Krebbers committed
474
475
476
477
478
  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.

479
  Lemma big_sepS_delete Φ X x :
480
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
481
  Proof. apply: big_opS_delete. Qed.
482

483
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
484
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
485

486
487
488
489
490
491
492
  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.

493
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
494
  Proof. apply: big_opS_singleton. Qed.
495

496
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
Ralf Jung's avatar
Ralf Jung committed
497
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
498
499
500
501
502
503
504
505
506
507
508
  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.

509
  Lemma big_sepS_sepS Φ Ψ X :
510
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
511
  Proof. apply: big_opS_opS. Qed.
512

513
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
514
  Proof. apply (big_opS_commute _). Qed.
515

516
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
517
  Proof. apply (big_opS_commute _). Qed.
518

519
  Lemma big_sepS_always_if q Φ X :
520
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
521
  Proof. apply (big_opS_commute _). Qed.
522
523

  Lemma big_sepS_forall Φ X :
Ralf Jung's avatar
Ralf Jung committed
524
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
525
526
527
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
528
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
529
    induction X as [|x X ? IH] using collection_ind_L.
530
531
    { rewrite big_sepS_empty; auto. }
    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
532
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
533
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
534
      by rewrite pure_True ?True_impl; last set_solver.
535
536
537
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
538
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
539
540
  Proof.
    rewrite always_and_sep_l always_forall.
541
    setoid_rewrite always_impl; setoid_rewrite always_pure.
542
543
544
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
545

546
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
547
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
548
  Global Instance big_sepS_persistent Φ X :
549
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
550
  Proof. rewrite /big_opS. apply _. Qed.
551
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
552
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
553
  Global Instance big_sepS_timeless Φ X :
554
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
555
  Proof. rewrite /big_opS. apply _. Qed.
556
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596


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

597
598
599
600
601
602
603
  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
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
  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.

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

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

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

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