big_op.v 25.2 KB
Newer Older
1 2
From iris.algebra Require Export list cmra_big_op.
From iris.base_logic Require Export base_logic.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.prelude Require Import gmap fin_collections gmultiset 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
(* 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.

26
  Lemma uPred_cmra_validN_op_l n P Q : {n} (P  Q)%I  {n} P.
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
  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
Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
88

89
Notation "'[∗' 'list' ] k ↦ x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ k x, P))
90
  (at level 200, l at level 10, k, x at level 1, right associativity,
91 92
   format "[∗  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
Notation "'[∗' 'list' ] x ∈ l , P" := (big_opL (M:=uPredUR _) l (λ _ x, P))
93
  (at level 200, l at level 10, x at level 1, right associativity,
94
   format "[∗  list ]  x  ∈  l ,  P") : uPred_scope.
95

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
107 108 109 110
Notation "'[∗' 'mset' ] x ∈ X , P" := (big_opMS (M:=uPredUR _) X (λ x, P))
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[∗  mset ]  x  ∈  X ,  P") : uPred_scope.

111
(** * Persistence and timelessness of lists of uPreds *)
112
Class PersistentL {M} (Ps : list (uPred M)) :=
113
  persistentL : Forall PersistentP Ps.
114
Arguments persistentL {_} _ {_}.
115

116 117 118 119
Class TimelessL {M} (Ps : list (uPred M)) :=
  timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.

120
(** * Properties *)
121
Section big_op.
122
Context {M : ucmraT}.
123 124 125
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

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

130
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
131
Proof. by rewrite big_op_app. Qed.
132

133
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
134
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
135
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
136
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
137

138
(** ** Persistence *)
139
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
140 141 142 143 144 145 146 147 148 149 150 151 152
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).
153
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
154 155 156 157 158
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.
159 160 161 162 163
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.
164 165

(** ** Timelessness *)
166
Global Instance big_sep_timeless Ps : TimelessL Ps  TimelessP ([] Ps).
167 168 169 170 171 172 173 174 175 176 177 178 179
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).
180
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
181 182 183 184 185
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.
186 187 188 189 190 191 192 193 194 195 196 197
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.

198
  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y)  True.
199 200
  Proof. done. Qed.
  Lemma big_sepL_cons Φ x l :
201
    ([ list] ky  x :: l, Φ k y)  Φ 0 x  [ list] ky  l, Φ (S k) y.
202
  Proof. by rewrite big_opL_cons. Qed.
203
  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
204 205
  Proof. by rewrite big_opL_singleton. Qed.
  Lemma big_sepL_app Φ l1 l2 :
206 207
    ([ list] ky  l1 ++ l2, Φ k y)
     ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
208 209
  Proof. by rewrite big_opL_app. Qed.

210 211
  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
212
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
213
  Proof. apply big_opL_forall; apply _. Qed.
214 215
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
216
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
217
  Proof. apply big_opL_proper. Qed.
218 219 220

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
228
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
229
    x  l  ([ list] y  l, Φ y)  Φ x.
230
  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
231

232
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  uPred M) l :
233
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
234
  Proof. by rewrite big_opL_fmap. Qed.
235 236

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

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

  Lemma big_sepL_always Φ l :
246
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
247
  Proof. apply (big_opL_commute _). Qed.
248 249

  Lemma big_sepL_always_if p Φ l :
250
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
251
  Proof. apply (big_opL_commute _). Qed.
252 253 254

  Lemma big_sepL_forall Φ l :
    ( k x, PersistentP (Φ k x)) 
255
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
256 257 258 259 260 261 262
  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.
263
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
264 265 266 267
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Lemma big_sepL_impl Φ Ψ l :
268 269
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
     [ list] kx  l, Ψ k x.
270 271 272 273 274 275 276
  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
277
  Global Instance big_sepL_nil_persistent Φ :
278
    PersistentP ([ list] kx  [], Φ k x).
279
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
280
  Global Instance big_sepL_persistent Φ l :
281
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  l, Φ k x).
282
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
283
  Global Instance big_sepL_nil_timeless Φ :
284
    TimelessP ([ list] kx  [], Φ k x).
285
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
286
  Global Instance big_sepL_timeless Φ l :
287
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  l, Φ k x).
288
  Proof. rewrite /big_opL. apply _. Qed.
289 290
End list.

291

292
(** ** Big ops over finite maps *)
293 294 295
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
296
  Implicit Types Φ Ψ : K  A  uPred M.
297

298
  Lemma big_sepM_mono Φ Ψ m1 m2 :
299
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
300
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
301
  Proof.
302
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
303 304 305
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, map_to_list_contains.
    - apply big_opM_forall; apply _ || auto.
306
  Qed.
307 308
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
309
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
310
  Proof. apply big_opM_proper. Qed.
311 312

  Global Instance big_sepM_mono' m :
313
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
314 315
           (big_opM (M:=uPredUR M) m).
  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
316

317
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
318
  Proof. by rewrite big_opM_empty. Qed.
319

320
  Lemma big_sepM_insert Φ m i x :
321
    m !! i = None 
322
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
323
  Proof. apply: big_opM_insert. Qed.
324

325
  Lemma big_sepM_delete Φ m i x :
326
    m !! i = Some x 
327
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
328
  Proof. apply: big_opM_delete. Qed.
329

330
  Lemma big_sepM_lookup Φ m i x :
331
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
332
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. 
Robbert Krebbers's avatar
Robbert Krebbers committed
333 334 335
  Lemma big_sepM_lookup_dom (Φ : K  uPred M) m i :
    is_Some (m !! i)  ([ map] k_  m, Φ k)  Φ i.
  Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
336

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

340
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
341
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
342
  Proof. by rewrite big_opM_fmap. Qed.
343

344
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
345
    m !! i = Some x 
346
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
347
  Proof. apply: big_opM_insert_override. Qed.
348

349
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
350
    m !! i = None 
351 352
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
353 354
  Proof. apply: big_opM_fn_insert. Qed.

355 356
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
357
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
358
  Proof. apply: big_opM_fn_insert'. Qed.
359

360
  Lemma big_sepM_sepM Φ Ψ m :
361 362
       ([ map] kx  m, Φ k x  Ψ k x)
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
363
  Proof. apply: big_opM_opM. Qed.
364

365
  Lemma big_sepM_later Φ m :
366
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
367
  Proof. apply (big_opM_commute _). Qed.
368

369
  Lemma big_sepM_always Φ m :
370
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
371
  Proof. apply (big_opM_commute _). Qed.
372 373

  Lemma big_sepM_always_if p Φ m :
374
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
375
  Proof. apply (big_opM_commute _). Qed.
376 377 378

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
379
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
380 381 382
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
383
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
384 385 386
    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.
387
      by rewrite pure_True // True_impl.
388
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
389 390
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
391
      by rewrite pure_True // True_impl.
392 393 394
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
395 396
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
     [ map] kx  m, Ψ k x.
397 398
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
399
    setoid_rewrite always_impl; setoid_rewrite always_pure.
400 401 402
    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.
403

Robbert Krebbers's avatar
Robbert Krebbers committed
404
  Global Instance big_sepM_empty_persistent Φ :
405
    PersistentP ([ map] kx  , Φ k x).
406
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
407
  Global Instance big_sepM_persistent Φ m :
408
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
409
  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
410
  Global Instance big_sepM_nil_timeless Φ :
411
    TimelessP ([ map] kx  , Φ k x).
412
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
413
  Global Instance big_sepM_timeless Φ m :
414
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
415
  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
416 417
End gmap.

418

419
(** ** Big ops over finite sets *)
420 421 422
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
423
  Implicit Types Φ : A  uPred M.
424

425
  Lemma big_sepS_mono Φ Ψ X Y :
426
    Y  X  ( x, x  Y  Φ x  Ψ x) 
427
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
428
  Proof.
429
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
430 431 432
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, elements_contains.
    - apply big_opS_forall; apply _ || auto.
433
  Qed.
434 435
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
436
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
437
  Proof. apply: big_opS_proper. Qed.
438

439
  Global Instance big_sepS_mono' X :
440 441 442
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

443
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
444
  Proof. by rewrite big_opS_empty. Qed.
445

446
  Lemma big_sepS_insert Φ X x :
447
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
448 449
  Proof. apply: big_opS_insert. Qed.

450
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
451
    x  X 
452 453
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
454 455
  Proof. apply: big_opS_fn_insert. Qed.

456
  Lemma big_sepS_fn_insert' Φ X x P :
457
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
458
  Proof. apply: big_opS_fn_insert'. Qed.
459

Robbert Krebbers's avatar
Robbert Krebbers committed
460 461 462 463 464
  Lemma big_sepS_union Φ X Y :
    X  Y 
    ([ set] y  X  Y, Φ y)  ([ set] y  X, Φ y)  ([ set] y  Y, Φ y).
  Proof. apply: big_opS_union. Qed.

465
  Lemma big_sepS_delete Φ X x :
466
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
467
  Proof. apply: big_opS_delete. Qed.
468

469
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
470
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed. 
471

472
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
473
  Proof. apply: big_opS_singleton. Qed.
474

475 476 477 478 479 480 481 482 483 484 485 486 487
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
    ([ set] y  filter P X, Φ y)  ([ set] y  X,  P y  Φ y).
  Proof.
    induction X as [|x X ? IH] using collection_ind_L.
    { by rewrite filter_empty_L !big_sepS_empty. }
    destruct (decide (P x)).
    - rewrite filter_union_L filter_singleton_L //.
      rewrite !big_sepS_insert //; last set_solver.
      by rewrite IH pure_True // left_id.
    - rewrite filter_union_L filter_singleton_not_L // left_id_L.
      by rewrite !big_sepS_insert // IH pure_False // False_impl left_id.
  Qed.

488
  Lemma big_sepS_sepS Φ Ψ X :
489
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
490
  Proof. apply: big_opS_opS. Qed.
491

492
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
493
  Proof. apply (big_opS_commute _). Qed.
494

495
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
496
  Proof. apply (big_opS_commute _). Qed.
497

498
  Lemma big_sepS_always_if q Φ X :
499
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
500
  Proof. apply (big_opS_commute _). Qed.
501 502

  Lemma big_sepS_forall Φ X :
503
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x,  (x  X)  Φ x).
504 505 506
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
507
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
508
    induction X as [|x X ? IH] using collection_ind_L.
509 510
    { rewrite big_sepS_empty; auto. }
    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
511
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
512
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
513
      by rewrite pure_True ?True_impl; last set_solver.
514 515 516
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
517
     ( x,  (x  X)  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
518 519
  Proof.
    rewrite always_and_sep_l always_forall.
520
    setoid_rewrite always_impl; setoid_rewrite always_pure.
521 522 523
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
524

525
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
526
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
527
  Global Instance big_sepS_persistent Φ X :
528
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
529
  Proof. rewrite /big_opS. apply _. Qed.
530
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
531
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
532
  Global Instance big_sepS_timeless Φ X :
533
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
534
  Proof. rewrite /big_opS. apply _. Qed.
535
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603


(** ** Big ops over finite multisets *)
Section gmultiset.
  Context `{Countable A}.
  Implicit Types X : gmultiset A.
  Implicit Types Φ : A  uPred M.

  Lemma big_sepMS_mono Φ Ψ X Y :
    Y  X  ( x, x  Y  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  [ mset] x  Y, Ψ x.
  Proof.
    intros HX HΦ. trans ([ mset] x  Y, Φ x)%I.
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, gmultiset_elements_contains.
    - apply big_opMS_forall; apply _ || auto.
  Qed.
  Lemma big_sepMS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
    ([ mset] x  X, Φ x)  ([ mset] x  X, Ψ x).
  Proof. apply: big_opMS_proper. Qed.

  Global Instance big_sepMS_mono' X :
     Proper (pointwise_relation _ () ==> ()) (big_opMS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opMS_forall; apply _ || intros; apply Hf. Qed.

  Lemma big_sepMS_empty Φ : ([ mset] x  , Φ x)  True.
  Proof. by rewrite big_opMS_empty. Qed.

  Lemma big_sepMS_union Φ X Y :
    ([ mset] y  X  Y, Φ y)  ([ mset] y  X, Φ y)  [ mset] y  Y, Φ y.
  Proof. apply: big_opMS_union. Qed.

  Lemma big_sepMS_delete Φ X x :
    x  X  ([ mset] y  X, Φ y)  Φ x  [ mset] y  X  {[ x ]}, Φ y.
  Proof. apply: big_opMS_delete. Qed.

  Lemma big_sepMS_elem_of Φ X x : x  X  ([ mset] y  X, Φ y)  Φ x.
  Proof. intros. apply uPred_included. by apply: big_opMS_elem_of. Qed. 

  Lemma big_sepMS_singleton Φ x : ([ mset] y  {[ x ]}, Φ y)  Φ x.
  Proof. apply: big_opMS_singleton. Qed.

  Lemma big_sepMS_sepMS Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
  Proof. apply: big_opMS_opMS. Qed.

  Lemma big_sepMS_later Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
  Proof. apply (big_opMS_commute _). Qed.

  Lemma big_sepMS_always Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
  Proof. apply (big_opMS_commute _). Qed.

  Lemma big_sepMS_always_if q Φ X :
    ?q ([ mset] y  X, Φ y)  ([ mset] y  X, ?q Φ y).
  Proof. apply (big_opMS_commute _). Qed.

  Global Instance big_sepMS_empty_persistent Φ : PersistentP ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
  Global Instance big_sepMS_nil_timeless Φ : TimelessP ([ mset] x  , Φ x).
  Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
  Global Instance big_sepMS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ mset] x  X, Φ x).
  Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
604
End big_op.