big_op.v 24.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
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. 
333

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

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

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

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

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

357
  Lemma big_sepM_sepM Φ Ψ m :
358
359
       ([ map] kx  m, Φ k x  Ψ k x)
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
360
  Proof. apply: big_opM_opM. Qed.
361

362
  Lemma big_sepM_later Φ m :
363
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
364
  Proof. apply (big_opM_commute _). Qed.
365

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

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

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

  Lemma big_sepM_impl Φ Ψ m :
392
393
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
     [ map] kx  m, Ψ k x.
394
395
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
396
    setoid_rewrite always_impl; setoid_rewrite always_pure.
397
398
399
    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.
400

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

415

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

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

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

440
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
441
  Proof. by rewrite big_opS_empty. Qed.
442

443
  Lemma big_sepS_insert Φ X x :
444
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
445
446
  Proof. apply: big_opS_insert. Qed.

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

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

457
  Lemma big_sepS_delete Φ X x :
458
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
459
  Proof. apply: big_opS_delete. Qed.
460

461
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
462
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. 
463

464
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
465
  Proof. apply: big_opS_singleton. Qed.
466

467
  Lemma big_sepS_sepS Φ Ψ X :
468
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
469
  Proof. apply: big_opS_opS. Qed.
470

471
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
472
  Proof. apply (big_opS_commute _). Qed.
473

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

477
  Lemma big_sepS_always_if q Φ X :
478
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
479
  Proof. apply (big_opS_commute _). Qed.
480
481

  Lemma big_sepS_forall Φ X :
482
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x,  (x  X)  Φ x).
483
484
485
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
486
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
487
488
489
490
491
492
    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.
493
494
495
  Qed.

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

504
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
505
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
506
  Global Instance big_sepS_persistent Φ X :
507
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
508
  Proof. rewrite /big_opS. apply _. Qed.
509
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
510
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
511
  Global Instance big_sepS_timeless Φ X :
512
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
513
  Proof. rewrite /big_opS. apply _. Qed.
514
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
515
516
517
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


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