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
  Proof. apply big_opL_forall; apply _. Qed.
128
129
130
  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).
131
  Proof. apply big_opL_proper. Qed.
132
133
134

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

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

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

146
147
  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)).
148
  Proof. by rewrite big_opL_fmap. Qed.
149
150
151
152

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

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

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

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

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

205

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

212
  Lemma big_sepM_mono Φ Ψ m1 m2 :
213
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
214
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
215
  Proof.
216
217
218
219
    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.
220
  Qed.
221
222
223
  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).
224
  Proof. apply big_opM_proper. Qed.
225
226

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

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

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

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

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

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

251
252
  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)).
253
  Proof. by rewrite big_opM_fmap. Qed.
254

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

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

266
267
268
  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).
269
  Proof. apply: big_opM_fn_insert'. Qed.
270

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

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

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

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

  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.
294
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
295
296
297
298
    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.
299
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
300
301
302
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
      by rewrite pure_equiv // True_impl.
303
304
305
  Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
315
316
  Global Instance big_sepM_empty_persistent Φ :
    PersistentP ([ map] kx  , Φ k x).
317
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
318
319
320
  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
321
322
  Global Instance big_sepM_nil_timeless Φ :
    TimelessP ([ map] kx  , Φ k x).
323
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
324
325
326
  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.
327
328
End gmap.

329

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

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

350
  Global Instance big_sepS_mono' X :
351
352
353
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

354
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
355
  Proof. by rewrite big_opS_empty. Qed.
356

357
  Lemma big_sepS_insert Φ X x :
358
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
359
360
  Proof. apply: big_opS_insert. Qed.

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

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

371
  Lemma big_sepS_delete Φ X x :
372
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
373
  Proof. apply: big_opS_delete. Qed.
374

375
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
376
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. 
377

378
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
379
  Proof. apply: big_opS_singleton. Qed.
380

381
  Lemma big_sepS_sepS Φ Ψ X :
382
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
383
  Proof. apply: big_opS_opS. Qed.
384

385
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
386
  Proof. apply (big_opS_commute _). Qed.
387
388

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

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

  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.
400
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
401
402
403
404
405
406
    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.
407
408
409
  Qed.

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

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