upred_big_op.v 18.1 KB
Newer Older
1
From iris.algebra Require Export upred list cmra_big_op.
2
From iris.prelude Require Import gmap fin_collections functions.
3
Import uPred.
4

5
6
7
Notation "'[★]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.

Notation "'[★' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P))
8
9
  (at level 200, l at level 10, k, x at level 1, right associativity,
   format "[★  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
10
Notation "'[★' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P))
11
12
13
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[★  list ]  x  ∈  l ,  P") : uPred_scope.

14
Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P))
15
16
  (at level 200, m at level 10, k, x at level 1, right associativity,
   format "[★  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
17
Notation "'[★' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ _ x, P))
18
19
  (at level 200, m at level 10, x at level 1, right associativity,
   format "[★  map ]  x  ∈  m ,  P") : uPred_scope.
20

21
Notation "'[★' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P))
22
23
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[★  set ]  x  ∈  X ,  P") : uPred_scope.
24

25
(** * Persistence and timelessness of lists of uPreds *)
26
Class PersistentL {M} (Ps : list (uPred M)) :=
27
  persistentL : Forall PersistentP Ps.
28
Arguments persistentL {_} _ {_}.
29

30
31
32
33
Class TimelessL {M} (Ps : list (uPred M)) :=
  timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.

34
(** * Properties *)
35
Section big_op.
36
Context {M : ucmraT}.
37
38
39
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

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

44
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
45
Proof. by rewrite big_op_app. Qed.
46

47
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
48
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
49
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
50
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
51

52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
(** ** Persistence *)
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
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).
67
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
68
69
70
71
72
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.
73
74
75
76
77
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.
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93

(** ** Timelessness *)
Global Instance big_sep_timeless Ps : TimelessL Ps  TimelessP ([] Ps).
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).
94
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
95
96
97
98
99
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.
100
101
102
103
104
105
106
107
108
109
110
111
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.

112
113
114
115
116
117
118
119
120
121
122
123
  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y)  True.
  Proof. done. Qed.
  Lemma big_sepL_cons Φ x l :
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
  Proof. by rewrite big_opL_cons. Qed.
  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
  Proof. by rewrite big_opL_app. Qed.

124
125
126
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
127
128
  Proof. apply big_opL_forall; apply _. Qed.

129
130
131
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
132
  Proof. apply big_opL_proper. Qed.
133
134
135

  Global Instance big_sepL_mono' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
136
137
           (big_opL (M:=uPredUR M) l).
  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
138
139
140

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

Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
    x  l  ([ list] y  l, Φ y)  Φ x.
145
  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
146

147
148
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  uPred M) l :
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
149
  Proof. by rewrite big_opL_fmap. Qed.
150
151
152
153

  Lemma big_sepL_sepL Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
154
  Proof. by rewrite big_opL_opL. Qed.
155
156
157

  Lemma big_sepL_later Φ l :
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
158
  Proof. apply (big_opL_commute _). Qed.
159
160
161

  Lemma big_sepL_always Φ l :
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
162
  Proof. apply (big_opL_commute _). Qed.
163
164
165

  Lemma big_sepL_always_if p Φ l :
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
166
  Proof. apply (big_opL_commute _). Qed.
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191

  Lemma big_sepL_forall Φ l :
    ( k x, PersistentP (Φ k x)) 
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
  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 :
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
     [ list] kx  l, Ψ k x.
  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
192
193
  Global Instance big_sepL_nil_persistent Φ :
    PersistentP ([ list] kx  [], Φ k x).
194
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
195
196
  Global Instance big_sepL_persistent Φ l :
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  l, Φ k x).
197
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
198
199
  Global Instance big_sepL_nil_timeless Φ :
    TimelessP ([ list] kx  [], Φ k x).
200
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
202
  Global Instance big_sepL_timeless Φ l :
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  l, Φ k x).
203
  Proof. rewrite /big_opL. apply _. Qed.
204
205
End list.

206

207
(** ** Big ops over finite maps *)
208
209
210
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
211
  Implicit Types Φ Ψ : K  A  uPred M.
212

213
  Lemma big_sepM_mono Φ Ψ m1 m2 :
214
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
215
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
216
  Proof.
217
218
219
220
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, map_to_list_contains.
    - apply big_opM_forall; apply _ || auto.
221
  Qed.
222

223
224
225
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
226
  Proof. apply big_opM_proper. Qed.
227
228

  Global Instance big_sepM_mono' m :
229
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
230
231
           (big_opM (M:=uPredUR M) m).
  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
232

233
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
234
  Proof. by rewrite big_opM_empty. Qed.
235

236
  Lemma big_sepM_insert Φ m i x :
237
    m !! i = None 
238
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
239
  Proof. apply: big_opM_insert. Qed.
240

241
  Lemma big_sepM_delete Φ m i x :
242
    m !! i = Some x 
243
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
244
  Proof. apply: big_opM_delete. Qed.
245

246
247
  Lemma big_sepM_lookup Φ m i x :
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
248
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. 
249

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

253
254
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
255
  Proof. by rewrite big_opM_fmap. Qed.
256

257
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
258
    m !! i = Some x 
259
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
260
  Proof. apply: big_opM_insert_override. Qed.
261

262
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
263
    m !! i = None 
264
265
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
266
267
  Proof. apply: big_opM_fn_insert. Qed.

268
269
270
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
271
  Proof. apply: big_opM_fn_insert'. Qed.
272

273
  Lemma big_sepM_sepM Φ Ψ m :
274
       ([ map] kx  m, Φ k x  Ψ k x)
275
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
276
  Proof. apply: big_opM_opM. Qed.
277

278
279
  Lemma big_sepM_later Φ m :
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
280
  Proof. apply (big_opM_commute _). Qed.
281

282
283
  Lemma big_sepM_always Φ m :
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
284
  Proof. apply (big_opM_commute _). Qed.
285
286

  Lemma big_sepM_always_if p Φ m :
287
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
288
  Proof. apply (big_opM_commute _). Qed.
289
290
291
292
293
294
295

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
296
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
297
298
299
300
    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.
301
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
302
303
304
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
      by rewrite pure_equiv // True_impl.
305
306
307
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
308
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
309
310
311
     [ map] kx  m, Ψ k x.
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
312
    setoid_rewrite always_impl; setoid_rewrite always_pure.
313
314
315
    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.
316

Robbert Krebbers's avatar
Robbert Krebbers committed
317
318
  Global Instance big_sepM_empty_persistent Φ :
    PersistentP ([ map] kx  , Φ k x).
319
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
320
321
322
  Global Instance big_sepM_persistent Φ m :
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
323
324
  Global Instance big_sepM_nil_timeless Φ :
    TimelessP ([ map] kx  , Φ k x).
325
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
326
327
328
  Global Instance big_sepM_timeless Φ m :
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
329
330
End gmap.

331

332
(** ** Big ops over finite sets *)
333
334
335
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
336
  Implicit Types Φ : A  uPred M.
337

338
  Lemma big_sepS_mono Φ Ψ X Y :
339
    Y  X  ( x, x  Y  Φ x  Ψ x) 
340
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
341
  Proof.
342
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
343
344
345
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, elements_contains.
    - apply big_opS_forall; apply _ || auto.
346
  Qed.
347
348
349
350
351

  Lemma big_sepS_mono' X :
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

352
  Lemma big_sepS_proper Φ Ψ X Y :
353
354
    X  Y  ( x, x  X  x  Y  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  ([ set] x  Y, Ψ x).
355
  Proof. apply: big_opS_proper. Qed.
356

357
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
358
  Proof. by rewrite big_opS_empty. Qed.
359

360
  Lemma big_sepS_insert Φ X x :
361
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
362
363
  Proof. apply: big_opS_insert. Qed.

364
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
365
    x  X 
366
367
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
368
369
  Proof. apply: big_opS_fn_insert. Qed.

370
  Lemma big_sepS_fn_insert' Φ X x P :
371
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
372
  Proof. apply: big_opS_fn_insert'. Qed.
373

374
  Lemma big_sepS_delete Φ X x :
375
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
376
  Proof. apply: big_opS_delete. Qed.
377

378
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
379
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. 
380

381
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
382
  Proof. apply: big_opS_singleton. Qed.
383

384
  Lemma big_sepS_sepS Φ Ψ X :
385
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
386
  Proof. apply: big_opS_opS. Qed.
387

388
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
389
  Proof. apply (big_opS_commute _). Qed.
390
391

  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
392
  Proof. apply (big_opS_commute _). Qed.
393

394
  Lemma big_sepS_always_if q Φ X :
395
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
396
  Proof. apply (big_opS_commute _). Qed.
397
398
399
400
401
402

  Lemma big_sepS_forall Φ X :
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x,  (x  X)  Φ x).
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
403
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
404
405
406
407
408
409
    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.
410
411
412
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
413
     ( x,  (x  X)  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
414
415
  Proof.
    rewrite always_and_sep_l always_forall.
416
    setoid_rewrite always_impl; setoid_rewrite always_pure.
417
418
419
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
420

Robbert Krebbers's avatar
Robbert Krebbers committed
421
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
422
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
423
424
  Global Instance big_sepS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
425
  Proof. rewrite /big_opS. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
426
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
427
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
428
429
  Global Instance big_sepS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
430
  Proof. rewrite /big_opS. apply _. Qed.
431
End gset.
432
End big_op.