upred_big_op.v 18.4 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 _). apply later_True. apply later_sep. 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 _). apply always_pure. apply always_sep. Qed.
163
164
165
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
191

  Lemma big_sepL_always_if p Φ l :
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
  Proof. destruct p; simpl; auto using big_sepL_always. Qed.

  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 _). apply later_True. apply later_sep. 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 _). apply always_pure. apply always_sep. 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. destruct p; simpl; auto using big_sepM_always. 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 _). apply later_True. apply later_sep. Qed.
390
391

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

394
  Lemma big_sepS_always_if q Φ X :
395
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
396
  Proof. destruct q; simpl; auto using big_sepS_always. 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.