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

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

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

210
211
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
212
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
213
  Proof. apply big_opL_forall; apply _. Qed.
214
215
  Lemma big_sepL_proper Φ Ψ 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_proper. Qed.
218
219
220

  Global Instance big_sepL_mono' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
221
222
           (big_opL (M:=uPredUR M) l).
  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
223
224

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

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

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

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

  Lemma big_sepL_later Φ l :
242
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
243
  Proof. apply (big_opL_commute _). Qed.
244
245

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

  Lemma big_sepL_always_if p Φ l :
250
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
251
  Proof. apply (big_opL_commute _). Qed.
252
253
254

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

291

292
(** ** Big ops over finite maps *)
293
294
295
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
296
  Implicit Types Φ Ψ : K  A  uPred M.
297

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

  Global Instance big_sepM_mono' m :
313
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
314
315
           (big_opM (M:=uPredUR M) m).
  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
316

317
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
318
  Proof. by rewrite big_opM_empty. Qed.
319

320
  Lemma big_sepM_insert Φ m i x :
321
    m !! i = None 
322
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
323
  Proof. apply: big_opM_insert. Qed.
324

325
  Lemma big_sepM_delete Φ m i x :
326
    m !! i = Some x 
327
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
328
  Proof. apply: big_opM_delete. Qed.
329

330
  Lemma big_sepM_lookup Φ m i x :
331
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
332
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
333
334
335
  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.
336

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

340
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
341
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
342
  Proof. by rewrite big_opM_fmap. Qed.
343

344
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
345
    m !! i = Some x 
346
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
347
  Proof. apply: big_opM_insert_override. Qed.
348

349
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
350
    m !! i = None 
351
352
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
353
354
  Proof. apply: big_opM_fn_insert. Qed.

355
356
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
357
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
358
  Proof. apply: big_opM_fn_insert'. Qed.
359

360
  Lemma big_sepM_sepM Φ Ψ m :
361
362
       ([ map] kx  m, Φ k x  Ψ k x)
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
363
  Proof. apply: big_opM_opM. Qed.
364

365
  Lemma big_sepM_later Φ m :
366
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
367
  Proof. apply (big_opM_commute _). Qed.
368

369
  Lemma big_sepM_always Φ m :
370
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
371
  Proof. apply (big_opM_commute _). Qed.
372
373

  Lemma big_sepM_always_if p Φ m :
374
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
375
  Proof. apply (big_opM_commute _). Qed.
376
377
378

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
379
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
380
381
382
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
383
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
384
385
386
    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.
387
      by rewrite pure_True // True_impl.
388
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
389
390
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
391
      by rewrite pure_True // True_impl.
392
393
394
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
395
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
396
     [ map] kx  m, Ψ k x.
397
398
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
399
    setoid_rewrite always_impl; setoid_rewrite always_pure.
400
401
402
    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.
403

Robbert Krebbers's avatar
Robbert Krebbers committed
404
  Global Instance big_sepM_empty_persistent Φ :
405
    PersistentP ([ map] kx  , Φ k x).
406
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
407
  Global Instance big_sepM_persistent Φ m :
408
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
409
  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
  Global Instance big_sepM_nil_timeless Φ :
411
    TimelessP ([ map] kx  , Φ k x).
412
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
413
  Global Instance big_sepM_timeless Φ m :
414
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
415
  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
416
417
End gmap.

418

419
(** ** Big ops over finite sets *)
420
421
422
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
423
  Implicit Types Φ : A  uPred M.
424

425
  Lemma big_sepS_mono Φ Ψ X Y :
426
    Y  X  ( x, x  Y  Φ x  Ψ x) 
427
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
428
  Proof.
429
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
430
431
432
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, elements_contains.
    - apply big_opS_forall; apply _ || auto.
433
  Qed.
434
435
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
436
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
437
  Proof. apply: big_opS_proper. Qed.
438

439
  Global Instance big_sepS_mono' X :
440
441
442
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

443
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
444
  Proof. by rewrite big_opS_empty. Qed.
445

446
  Lemma big_sepS_insert Φ X x :
447
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
448
449
  Proof. apply: big_opS_insert. Qed.

450
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
451
    x  X 
452
453
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
454
455
  Proof. apply: big_opS_fn_insert. Qed.

456
  Lemma big_sepS_fn_insert' Φ X x P :
457
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
458
  Proof. apply: big_opS_fn_insert'. Qed.
459

Robbert Krebbers's avatar
Robbert Krebbers committed
460
461
462
463
464
  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.

465
  Lemma big_sepS_delete Φ X x :
466
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
467
  Proof. apply: big_opS_delete. Qed.
468

469
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
470
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
471

472
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
473
  Proof. apply: big_opS_singleton. Qed.
474

475
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
Ralf Jung's avatar
Ralf Jung committed
476
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
477
478
479
480
481
482
483
484
485
486
487
  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.

488
  Lemma big_sepS_sepS Φ Ψ X :
489
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
490
  Proof. apply: big_opS_opS. Qed.
491

492
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
493
  Proof. apply (big_opS_commute _). Qed.
494

495
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
496
  Proof. apply (big_opS_commute _). Qed.
497

498
  Lemma big_sepS_always_if q Φ X :
499
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
500
  Proof. apply (big_opS_commute _). Qed.
501
502

  Lemma big_sepS_forall Φ X :
Ralf Jung's avatar
Ralf Jung committed
503
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
504
505
506
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
507
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
508
    induction X as [|x X ? IH] using collection_ind_L.
509
510
    { rewrite big_sepS_empty; auto. }
    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
511
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
512
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
513
      by rewrite pure_True ?True_impl; last set_solver.
514
515
516
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
517
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
518
519
  Proof.
    rewrite always_and_sep_l always_forall.
520
    setoid_rewrite always_impl; setoid_rewrite always_pure.
521
522
523
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
524

525
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
526
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
527
  Global Instance big_sepS_persistent Φ X :
528
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
529
  Proof. rewrite /big_opS. apply _. Qed.
530
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
531
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
532
  Global Instance big_sepS_timeless Φ X :
533
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
534
  Proof. rewrite /big_opS. apply _. Qed.
535
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
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
597
598
599
600
601
602
603


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

  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.
604
End big_op.