big_op.v 24.4 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
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
(* 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}.

  Instance uPred_valid : Valid (uPred M) := λ P,  n x, {n} x  P n x.
  Instance uPred_validN : ValidN (uPred M) := λ n P,
     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.

  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN n).
  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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
  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 :=
    CMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin.

  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 :=
    UCMRAT (uPred M) uPred_cofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.

  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)) 
255
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
256
257
258
259
260
261
262
263
264
265
266
267
  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.
    - by rewrite (forall_elim 0) (forall_elim x) pure_equiv // True_impl.
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Lemma big_sepL_impl Φ Ψ l :
268
269
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
     [ 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)) 
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
387
    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.
      by rewrite pure_equiv // True_impl.
388
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
389
390
391
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
      by rewrite pure_equiv // True_impl.
392
393
394
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
395
396
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
     [ 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

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

464
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
465
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. 
466

467
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
468
  Proof. apply: big_opS_singleton. Qed.
469

470
  Lemma big_sepS_sepS Φ Ψ X :
471
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
472
  Proof. apply: big_opS_opS. Qed.
473

474
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
475
  Proof. apply (big_opS_commute _). Qed.
476

477
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
478
  Proof. apply (big_opS_commute _). Qed.
479

480
  Lemma big_sepS_always_if q Φ X :
481
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
482
  Proof. apply (big_opS_commute _). Qed.
483
484

  Lemma big_sepS_forall Φ X :
485
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x,  (x  X)  Φ x).
486
487
488
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
489
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
490
491
492
493
494
495
    induction X as [|x m ? IH] using collection_ind_L.
    { rewrite big_sepS_empty; auto. }
    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
    - by rewrite (forall_elim x) pure_equiv ?True_impl; last set_solver.
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
      by rewrite pure_equiv ?True_impl; last set_solver.
496
497
498
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
499
     ( x,  (x  X)  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
500
501
  Proof.
    rewrite always_and_sep_l always_forall.
502
    setoid_rewrite always_impl; setoid_rewrite always_pure.
503
504
505
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
506

507
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
508
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
509
  Global Instance big_sepS_persistent Φ X :
510
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
511
  Proof. rewrite /big_opS. apply _. Qed.
512
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
513
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
514
  Global Instance big_sepS_timeless Φ X :
515
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
516
  Proof. rewrite /big_opS. apply _. Qed.
517
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
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


(** ** 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.
586
End big_op.