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

5
6
7
8
9
10
11
12
13
14
15
(** We define the following big operators:

- The operators [ [★] Ps ] and [ [∧] Ps ] fold [★] and [∧] over the list [Ps].
  This operator is not a quantifier, so it binds strongly.
- The operator [ [★ map] k ↦ x ∈ m, P ] asserts that [P] holds separately for
  each [k ↦ x] in the map [m]. This operator is a quantifier, and thus has the
  same precedence as [∀] and [∃].
- The operator [ [★ set] x ∈ X, P ] asserts that [P] holds separately for each
  [x] in the set [X]. This operator is a quantifier, and thus has the same
  precedence as [∀] and [∃]. *)

16
17
(** * Big ops over lists *)
(* These are the basic building blocks for other big ops *)
18
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M :=
19
20
  match Ps with [] => True | P :: Ps => P  uPred_big_and Ps end%I.
Instance: Params (@uPred_big_and) 1.
21
Notation "'[∧]' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
22
23
24
Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M :=
  match Ps with [] => True | P :: Ps => P  uPred_big_sep Ps end%I.
Instance: Params (@uPred_big_sep) 1.
25
Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
26

27
(** * Other big ops *)
28
Definition uPred_big_sepM {M} `{Countable K} {A}
29
    (m : gmap K A) (Φ : K  A  uPred M) : uPred M :=
30
  [] (curry Φ <$> map_to_list m).
31
Instance: Params (@uPred_big_sepM) 6.
32
Typeclasses Opaque uPred_big_sepM.
33
34
35
Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P))
  (at level 200, m at level 10, k, x at level 1, right associativity,
   format "[★  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
36

37
Definition uPred_big_sepS {M} `{Countable A}
38
  (X : gset A) (Φ : A  uPred M) : uPred M := [] (Φ <$> elements X).
39
Instance: Params (@uPred_big_sepS) 5.
40
Typeclasses Opaque uPred_big_sepS.
41
42
43
Notation "'[★' 'set' ] x ∈ X , P" := (uPred_big_sepS X (λ x, P))
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[★  set ]  x  ∈  X ,  P") : uPred_scope.
44

45
(** * Persistence and timelessness of lists of uPreds *)
46
Class PersistentL {M} (Ps : list (uPred M)) :=
47
  persistentL : Forall PersistentP Ps.
48
Arguments persistentL {_} _ {_}.
49

50
51
52
53
Class TimelessL {M} (Ps : list (uPred M)) :=
  timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.

54
(** * Properties *)
55
Section big_op.
56
Context {M : ucmraT}.
57
58
59
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

60
(** ** Big ops over lists *)
61
Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M).
62
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
63
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
64
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
65

66
Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
67
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
68
Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
69
70
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

71
Global Instance big_and_mono' : Proper (Forall2 () ==> ()) (@uPred_big_and M).
72
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
73
Global Instance big_sep_mono' : Proper (Forall2 () ==> ()) (@uPred_big_sep M).
74
75
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

76
Global Instance big_and_perm : Proper (() ==> ()) (@uPred_big_and M).
77
78
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
79
80
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
81
  - etrans; eauto.
82
Qed.
83
Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M).
84
85
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
86
87
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
88
  - etrans; eauto.
89
Qed.
90

91
Lemma big_and_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
92
Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
93
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
94
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
95

96
Lemma big_and_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
97
Proof.
98
  intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
99
Qed.
100
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
101
Proof.
102
  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
103
104
Qed.

105
Lemma big_sep_and Ps : [] Ps  [] Ps.
106
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
107

108
Lemma big_and_elem_of Ps P : P  Ps  [] Ps  P.
109
Proof. induction 1; simpl; auto with I. Qed.
110
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
111
112
Proof. induction 1; simpl; auto with I. Qed.

113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
(** ** Persistence *)
Global Instance big_and_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
Proof. induction 1; apply _. Qed.
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).
Proof. unfold PersistentL=> ?; induction xs; constructor; auto. Qed.
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.

(** ** Timelessness *)
Global Instance big_and_timeless Ps : TimelessL Ps  TimelessP ([] Ps).
Proof. induction 1; apply _. Qed.
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).
Proof. unfold TimelessL=> ?; induction xs; constructor; auto. Qed.
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.

161
(** ** Big ops over finite maps *)
162
163
164
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
165
  Implicit Types Φ Ψ : K  A  uPred M.
166

167
  Lemma big_sepM_mono Φ Ψ m1 m2 :
168
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
169
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
170
  Proof.
171
    intros HX HΦ. trans ([ map] kx  m2, Φ k x)%I.
172
    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
173
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
174
      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
175
  Qed.
176
177
178
  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).
179
180
181
182
  Proof.
    intros ?; apply (anti_symm ()); apply big_sepM_mono;
      eauto using equiv_entails, equiv_entails_sym, lookup_weaken.
  Qed.
183
184
185
186
187

  Global Instance big_sepM_ne m n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (uPred_big_sepM (M:=M) m).
  Proof.
188
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
189
    apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ.
190
  Qed.
191
  Global Instance big_sepM_proper' m :
192
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
193
           (uPred_big_sepM (M:=M) m).
194
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
195
  Global Instance big_sepM_mono' m :
196
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
197
           (uPred_big_sepM (M:=M) m).
198
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
199

200
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
201
  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
202

203
  Lemma big_sepM_insert Φ m i x :
204
    m !! i = None 
205
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
206
  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
207

208
  Lemma big_sepM_delete Φ m i x :
209
    m !! i = Some x 
210
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
211
212
213
214
  Proof.
    intros. rewrite -big_sepM_insert ?lookup_delete //.
    by rewrite insert_delete insert_id.
  Qed.
215

216
217
218
219
  Lemma big_sepM_lookup Φ m i x :
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
  Proof. intros. by rewrite big_sepM_delete // sep_elim_l. Qed.

220
  Lemma big_sepM_singleton Φ i x : ([ map] ky  {[i:=x]}, Φ k y)  Φ i x.
221
222
223
224
  Proof.
    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
    by rewrite big_sepM_empty right_id.
  Qed.
225

226
227
228
229
230
231
232
  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)).
  Proof.
    rewrite /uPred_big_sepM map_to_list_fmap -list_fmap_compose.
    f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
  Qed.

233
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
234
    m !! i = Some x 
235
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
236
237
238
239
240
  Proof.
    intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
    by rewrite -big_sepM_delete.
  Qed.

241
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
242
    m !! i = None 
243
244
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
245
246
  Proof.
    intros. rewrite big_sepM_insert // fn_lookup_insert.
247
    apply sep_proper, big_sepM_proper; auto=> k y ?.
248
249
250
251
252
253
254
    by rewrite fn_lookup_insert_ne; last set_solver.
  Qed.
  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).
  Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.

255
  Lemma big_sepM_sepM Φ Ψ m :
256
       ([ map] kx  m, Φ k x  Ψ k x)
257
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
258
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
259
260
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
261
    by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _  _)%I]comm -!assoc.
262
  Qed.
263

264
  Lemma big_sepM_later Φ m :
265
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
266
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
267
268
269
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
    by rewrite later_sep IH.
270
  Qed.
271
272
273
274
275

  Lemma big_sepM_always Φ m :
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
  Proof.
    rewrite /uPred_big_sepM.
276
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?always_pure //.
277
278
279
280
    by rewrite always_sep IH.
  Qed.

  Lemma big_sepM_always_if p Φ m :
281
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
282
  Proof. destruct p; simpl; auto using big_sepM_always. Qed.
283
284
285
286
287
288
289

  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.
290
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
291
292
293
    rewrite /uPred_big_sepM. setoid_rewrite <-elem_of_map_to_list.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; auto.
    rewrite -always_and_sep_l; apply and_intro.
294
    - rewrite (forall_elim i) (forall_elim x) pure_equiv; last by left.
295
296
      by rewrite True_impl.
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
297
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
298
299
300
301
      by rewrite True_impl.
  Qed.

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

  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.

  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.
318
319
End gmap.

320
(** ** Big ops over finite sets *)
321
322
323
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
324
  Implicit Types Φ : A  uPred M.
325

326
  Lemma big_sepS_mono Φ Ψ X Y :
327
    Y  X  ( x, x  Y  Φ x  Ψ x) 
328
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
329
  Proof.
330
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
331
    - by apply big_sep_contains, fmap_contains, elements_contains.
332
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
333
      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
334
  Qed.
335
  Lemma big_sepS_proper Φ Ψ X Y :
336
337
    X  Y  ( x, x  X  x  Y  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  ([ set] x  Y, Ψ x).
338
  Proof.
339
340
    move=> /collection_equiv_spec [??] ?; apply (anti_symm ());
      apply big_sepS_mono; eauto using equiv_entails, equiv_entails_sym.
341
  Qed.
342
343
344
345

  Lemma big_sepS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
  Proof.
346
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
347
    apply Forall_Forall2, Forall_true=> x; apply HΦ.
348
  Qed.
349
  Lemma big_sepS_proper' X :
350
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
351
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
352
  Lemma big_sepS_mono' X :
353
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
354
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
355

356
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
357
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
358

359
  Lemma big_sepS_insert Φ X x :
360
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
361
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
362
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
363
    x  X 
364
365
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
366
367
368
369
370
  Proof.
    intros. rewrite big_sepS_insert // fn_lookup_insert.
    apply sep_proper, big_sepS_proper; auto=> y ??.
    by rewrite fn_lookup_insert_ne; last set_solver.
  Qed.
371
  Lemma big_sepS_fn_insert' Φ X x P :
372
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
373
  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
374

375
  Lemma big_sepS_delete Φ X x :
376
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
377
  Proof.
378
379
    intros. rewrite -big_sepS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
380
  Qed.
381

382
383
384
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
  Proof. intros. by rewrite big_sepS_delete // sep_elim_l. Qed.

385
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
386
  Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
387

388
  Lemma big_sepS_sepS Φ Ψ X :
389
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
390
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
391
392
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
393
    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _  _)%I]comm -!assoc.
394
395
  Qed.

396
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
397
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
398
399
400
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
    by rewrite later_sep IH.
401
  Qed.
402

403
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
404
405
  Proof.
    rewrite /uPred_big_sepS.
406
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_pure.
407
408
409
410
    by rewrite always_sep IH.
  Qed.

  Lemma big_sepS_always_if q Φ X :
411
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
412
  Proof. destruct q; simpl; auto using big_sepS_always. Qed.
413
414
415
416
417
418

  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.
419
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
420
421
422
    rewrite /uPred_big_sepS. setoid_rewrite <-elem_of_elements.
    induction (elements X) as [|x l IH]; csimpl; auto.
    rewrite -always_and_sep_l; apply and_intro.
423
    - rewrite (forall_elim x) pure_equiv; last by left. by rewrite True_impl.
424
    - rewrite -IH. apply forall_mono=> y.
425
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
426
427
428
429
      by rewrite True_impl.
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
430
       ( x,  (x  X)  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
431
432
  Proof.
    rewrite always_and_sep_l always_forall.
433
    setoid_rewrite always_impl; setoid_rewrite always_pure.
434
435
436
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
437

438
439
440
  Global Instance big_sepS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
  Proof. rewrite /uPred_big_sepS. apply _. Qed.
441

442
443
444
445
  Global Instance big_sepS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
  Proof. rewrite /uPred_big_sepS. apply _. Qed.
End gset.
446
End big_op.