big_op.v 21.1 KB
Newer Older
1 2
From iris.algebra Require Export list cmra_big_op.
From iris.base_logic Require Export base_logic.
3
From iris.prelude Require Import gmap fin_collections 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 26 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
(* 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.

  Lemma uPred_cmra_validN_op_l n P Q : {n} (P  Q)%I  {n} P.
  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 88 89
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))
90 91
  (at level 200, l at level 10, k, x at level 1, right associativity,
   format "[★  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
92
Notation "'[★' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P))
93 94 95
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[★  list ]  x  ∈  l ,  P") : uPred_scope.

96
Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ k x, P))
97 98
  (at level 200, m at level 10, k, x at level 1, right associativity,
   format "[★  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
99
Notation "'[★' 'map' ] x ∈ m , P" := (big_opM (M:=uPredUR _) m (λ _ x, P))
100 101
  (at level 200, m at level 10, x at level 1, right associativity,
   format "[★  map ]  x  ∈  m ,  P") : uPred_scope.
102

103
Notation "'[★' 'set' ] x ∈ X , P" := (big_opS (M:=uPredUR _) X (λ x, P))
104 105
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[★  set ]  x  ∈  X ,  P") : uPred_scope.
106

107
(** * Persistence and timelessness of lists of uPreds *)
108
Class PersistentL {M} (Ps : list (uPred M)) :=
109
  persistentL : Forall PersistentP Ps.
110
Arguments persistentL {_} _ {_}.
111

112 113 114 115
Class TimelessL {M} (Ps : list (uPred M)) :=
  timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.

116
(** * Properties *)
117
Section big_op.
118
Context {M : ucmraT}.
119 120 121
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

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

126
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
127
Proof. by rewrite big_op_app. Qed.
128

129
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
130
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
131
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
132
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
133

134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
(** ** 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).
149
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
150 151 152 153 154
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.
155 156 157 158 159
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.
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175

(** ** 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).
176
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
177 178 179 180 181
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.
182 183 184 185 186 187 188 189 190 191 192 193
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.

194 195 196 197 198 199 200 201 202 203 204 205
  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.

206 207 208
  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.
209
  Proof. apply big_opL_forall; apply _. Qed.
210 211 212
  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).
213
  Proof. apply big_opL_proper. Qed.
214 215 216

  Global Instance big_sepL_mono' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
217 218
           (big_opL (M:=uPredUR M) l).
  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
219 220 221

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

Robbert Krebbers's avatar
Robbert Krebbers committed
224 225
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
    x  l  ([ list] y  l, Φ y)  Φ x.
226
  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
227

228 229
  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)).
230
  Proof. by rewrite big_opL_fmap. Qed.
231 232 233 234

  Lemma big_sepL_sepL Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
235
  Proof. by rewrite big_opL_opL. Qed.
236 237 238

  Lemma big_sepL_later Φ l :
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
239
  Proof. apply (big_opL_commute _). Qed.
240 241 242

  Lemma big_sepL_always Φ l :
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
243
  Proof. apply (big_opL_commute _). Qed.
244 245 246

  Lemma big_sepL_always_if p Φ l :
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
247
  Proof. apply (big_opL_commute _). Qed.
248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272

  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
273 274
  Global Instance big_sepL_nil_persistent Φ :
    PersistentP ([ list] kx  [], Φ k x).
275
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
276 277
  Global Instance big_sepL_persistent Φ l :
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  l, Φ k x).
278
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
279 280
  Global Instance big_sepL_nil_timeless Φ :
    TimelessP ([ list] kx  [], Φ k x).
281
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
282 283
  Global Instance big_sepL_timeless Φ l :
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  l, Φ k x).
284
  Proof. rewrite /big_opL. apply _. Qed.
285 286
End list.

287

288
(** ** Big ops over finite maps *)
289 290 291
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
292
  Implicit Types Φ Ψ : K  A  uPred M.
293

294
  Lemma big_sepM_mono Φ Ψ m1 m2 :
295
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
296
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
297
  Proof.
298 299 300 301
    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.
302
  Qed.
303 304 305
  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).
306
  Proof. apply big_opM_proper. Qed.
307 308

  Global Instance big_sepM_mono' m :
309
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
310 311
           (big_opM (M:=uPredUR M) m).
  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
312

313
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
314
  Proof. by rewrite big_opM_empty. Qed.
315

316
  Lemma big_sepM_insert Φ m i x :
317
    m !! i = None 
318
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
319
  Proof. apply: big_opM_insert. Qed.
320

321
  Lemma big_sepM_delete Φ m i x :
322
    m !! i = Some x 
323
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
324
  Proof. apply: big_opM_delete. Qed.
325

326 327
  Lemma big_sepM_lookup Φ m i x :
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
328
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. 
329

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

333 334
  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)).
335
  Proof. by rewrite big_opM_fmap. Qed.
336

337
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
338
    m !! i = Some x 
339
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
340
  Proof. apply: big_opM_insert_override. Qed.
341

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

348 349 350
  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).
351
  Proof. apply: big_opM_fn_insert'. Qed.
352

353
  Lemma big_sepM_sepM Φ Ψ m :
354
       ([ map] kx  m, Φ k x  Ψ k x)
355
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
356
  Proof. apply: big_opM_opM. Qed.
357

358 359
  Lemma big_sepM_later Φ m :
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
360
  Proof. apply (big_opM_commute _). Qed.
361

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

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

  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.
376
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
377 378 379 380
    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.
381
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
382 383 384
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
      by rewrite pure_equiv // True_impl.
385 386 387
  Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
397 398
  Global Instance big_sepM_empty_persistent Φ :
    PersistentP ([ map] kx  , Φ k x).
399
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
400 401 402
  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
403 404
  Global Instance big_sepM_nil_timeless Φ :
    TimelessP ([ map] kx  , Φ k x).
405
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
406 407 408
  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.
409 410
End gmap.

411

412
(** ** Big ops over finite sets *)
413 414 415
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
416
  Implicit Types Φ : A  uPred M.
417

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

432
  Global Instance big_sepS_mono' X :
433 434 435
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

436
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
437
  Proof. by rewrite big_opS_empty. Qed.
438

439
  Lemma big_sepS_insert Φ X x :
440
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
441 442
  Proof. apply: big_opS_insert. Qed.

443
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
444
    x  X 
445 446
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
447 448
  Proof. apply: big_opS_fn_insert. Qed.

449
  Lemma big_sepS_fn_insert' Φ X x P :
450
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
451
  Proof. apply: big_opS_fn_insert'. Qed.
452

453
  Lemma big_sepS_delete Φ X x :
454
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
455
  Proof. apply: big_opS_delete. Qed.
456

457
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
458
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. 
459

460
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
461
  Proof. apply: big_opS_singleton. Qed.
462

463
  Lemma big_sepS_sepS Φ Ψ X :
464
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
465
  Proof. apply: big_opS_opS. Qed.
466

467
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
468
  Proof. apply (big_opS_commute _). Qed.
469 470

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

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

  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.
482
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
483 484 485 486 487 488
    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.
489 490 491
  Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
500
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
501
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
502 503
  Global Instance big_sepS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
504
  Proof. rewrite /big_opS. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
505
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
506
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
507 508
  Global Instance big_sepS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
509
  Proof. rewrite /big_opS. apply _. Qed.
510
End gset.
511
End big_op.