big_op.v 29.4 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
(* 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}.

11 12
  Instance uPred_valid_inst : Valid (uPred M) := λ P,  n x, {n} x  P n x.
  Instance uPred_validN_inst : ValidN (uPred M) := λ n P,
13 14 15 16
     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.

17
  Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN_inst n).
18 19 20 21 22 23 24 25
  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
  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 :=
55
    CMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin.
56 57 58 59 60 61 62 63 64 65 66

  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 :=
67
    UCMRAT (uPred M) uPred_ofe_mixin uPred_cmra_mixin uPred_ucmra_mixin.
68 69 70 71 72 73 74 75

  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
76 77
  Global Instance uPred_laterN_homomorphism n : UCMRAHomomorphism (uPred_laterN n).
  Proof. split; [split|]. apply _. apply laterN_sep. apply laterN_True. Qed.
78 79 80 81 82 83 84 85 86 87 88
  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 *)
89
Notation "'[∗]' Ps" := (big_op (M:=uPredUR _) Ps) (at level 20) : uPred_scope.
90

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

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
109 110 111 112
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.

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

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

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

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

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

135
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
136
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
137
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
138
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
139
Lemma big_sep_elem_of_acc Ps P : P  Ps  [] Ps  P  (P - [] Ps).
140
Proof. intros [k ->]%elem_of_Permutation. by apply sep_mono_r, wand_intro_l. Qed.
141

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

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

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

214 215
  Lemma big_sepL_mono Φ Ψ 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_forall; apply _. Qed.
218 219
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
220
    ([ list] k  y  l, Φ k y)  ([ list] k  y  l, Ψ k y).
221
  Proof. apply big_opL_proper. Qed.
222 223 224
  Lemma big_sepL_contains (Φ : A  uPred M) l1 l2 :
    l1 `contains` l2  ([ list] y  l2, Φ y)  [ list] y  l1, Φ y.
  Proof. intros ?. apply uPred_included. by apply: big_opL_contains. Qed.
225 226 227

  Global Instance big_sepL_mono' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
228 229
           (big_opL (M:=uPredUR M) l).
  Proof. intros f g Hf. apply big_opL_forall; apply _ || intros; apply Hf. Qed.
230

231 232 233 234
  Lemma big_sepL_lookup_acc Φ l i x :
    l !! i = Some x 
    ([ list] ky  l, Φ k y)  Φ i x  (Φ i x - ([ list] ky  l, Φ k y)).
  Proof.
235 236
    intros Hli. apply big_sep_elem_of_acc, (elem_of_list_lookup_2 _ i).
    by rewrite list_lookup_imap Hli.
237 238
  Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
243
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
244
    x  l  ([ list] y  l, Φ y)  Φ x.
245
  Proof. intros. apply uPred_included. by apply: big_opL_elem_of. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
246

247
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  uPred M) l :
248
    ([ list] ky  f <$> l, Φ k y)  ([ list] ky  l, Φ k (f y)).
249
  Proof. by rewrite big_opL_fmap. Qed.
250 251

  Lemma big_sepL_sepL Φ Ψ l :
252 253
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
254
  Proof. by rewrite big_opL_opL. Qed.
255

256 257 258 259 260
  Lemma big_sepL_and Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
  Proof. auto using big_sepL_mono with I. Qed.

261
  Lemma big_sepL_later Φ l :
262
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
263
  Proof. apply (big_opL_commute _). Qed.
264

Robbert Krebbers's avatar
Robbert Krebbers committed
265 266 267 268
  Lemma big_sepL_laterN Φ n l :
    ^n ([ list] kx  l, Φ k x)  ([ list] kx  l, ^n Φ k x).
  Proof. apply (big_opL_commute _). Qed.

269
  Lemma big_sepL_always Φ l :
270
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
271
  Proof. apply (big_opL_commute _). Qed.
272 273

  Lemma big_sepL_always_if p Φ l :
274
    ?p ([ list] kx  l, Φ k x)  ([ list] kx  l, ?p Φ k x).
275
  Proof. apply (big_opL_commute _). Qed.
276 277 278

  Lemma big_sepL_forall Φ l :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
279
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
280 281 282 283 284 285 286
  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.
287
    - by rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
288 289 290 291
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Lemma big_sepL_impl Φ Ψ l :
Ralf Jung's avatar
Ralf Jung committed
292
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
293
     [ list] kx  l, Ψ k x.
294 295 296 297 298 299 300
  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
301
  Global Instance big_sepL_nil_persistent Φ :
302
    PersistentP ([ list] kx  [], Φ k x).
303
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
  Global Instance big_sepL_persistent Φ l :
305
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  l, Φ k x).
306
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
307
  Global Instance big_sepL_nil_timeless Φ :
308
    TimelessP ([ list] kx  [], Φ k x).
309
  Proof. rewrite /big_opL. apply _. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
310
  Global Instance big_sepL_timeless Φ l :
311
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  l, Φ k x).
312
  Proof. rewrite /big_opL. apply _. Qed.
313 314
End list.

315

316
(** ** Big ops over finite maps *)
317 318 319
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
320
  Implicit Types Φ Ψ : K  A  uPred M.
321

322
  Lemma big_sepM_mono Φ Ψ m1 m2 :
323
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
324
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
325
  Proof.
326
    intros Hm HΦ. trans ([ map] kx  m2, Φ k x)%I.
327 328 329
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, map_to_list_contains.
    - apply big_opM_forall; apply _ || auto.
330
  Qed.
331 332
  Lemma big_sepM_proper Φ Ψ m :
    ( k x, m !! k = Some x  Φ k x  Ψ k x) 
333
    ([ map] k  x  m, Φ k x)  ([ map] k  x  m, Ψ k x).
334
  Proof. apply big_opM_proper. Qed.
335 336

  Global Instance big_sepM_mono' m :
337
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
338 339
           (big_opM (M:=uPredUR M) m).
  Proof. intros f g Hf. apply big_opM_forall; apply _ || intros; apply Hf. Qed.
340

341
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
342
  Proof. by rewrite big_opM_empty. Qed.
343

344
  Lemma big_sepM_insert Φ m i x :
345
    m !! i = None 
346
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
347
  Proof. apply: big_opM_insert. Qed.
348

349
  Lemma big_sepM_delete Φ m i x :
350
    m !! i = Some x 
351
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
352
  Proof. apply: big_opM_delete. Qed.
353

354 355 356 357 358 359 360
  Lemma big_sepM_lookup_acc Φ m i x :
    m !! i = Some x 
    ([ map] ky  m, Φ k y)  Φ i x  (Φ i x - ([ map] ky  m, Φ k y)).
  Proof.
    intros. rewrite big_sepM_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

361
  Lemma big_sepM_lookup Φ m i x :
362
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
363 364
  Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
365 366 367
  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.
368

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

372
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
373
    ([ map] ky  f <$> m, Φ k y)  ([ map] ky  m, Φ k (f y)).
374
  Proof. by rewrite big_opM_fmap. Qed.
375

Robbert Krebbers's avatar
Robbert Krebbers committed
376 377 378
  Lemma big_sepM_insert_override Φ m i x x' :
    m !! i = Some x  (Φ i x  Φ i x') 
    ([ map] ky  <[i:=x']> m, Φ k y)  ([ map] ky  m, Φ k y).
379
  Proof. apply: big_opM_insert_override. Qed.
380

Robbert Krebbers's avatar
Robbert Krebbers committed
381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400
  Lemma big_sepM_insert_override_1 Φ m i x x' :
    m !! i = Some x 
    ([ map] ky  <[i:=x']> m, Φ k y) 
      (Φ i x' - Φ i x) - ([ map] ky  m, Φ k y).
  Proof.
    intros ?. apply wand_intro_l.
    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
    by rewrite assoc wand_elim_l -big_sepM_delete.
  Qed.

  Lemma big_sepM_insert_override_2 Φ m i x x' :
    m !! i = Some x 
    ([ map] ky  m, Φ k y) 
      (Φ i x - Φ i x') - ([ map] ky  <[i:=x']> m, Φ k y).
  Proof.
    intros ?. apply wand_intro_l.
    rewrite {1}big_sepM_delete //; rewrite assoc wand_elim_l.
    rewrite -insert_delete big_sepM_insert ?lookup_delete //.
  Qed.

401
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
402
    m !! i = None 
403 404
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
405 406
  Proof. apply: big_opM_fn_insert. Qed.

407 408
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
409
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k)  (P  [ map] ky  m, Φ k).
410
  Proof. apply: big_opM_fn_insert'. Qed.
411

412
  Lemma big_sepM_sepM Φ Ψ m :
413
    ([ map] kx  m, Φ k x  Ψ k x)
414
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
415
  Proof. apply: big_opM_opM. Qed.
416

417 418 419 420 421
  Lemma big_sepM_and Φ Ψ m :
    ([ map] kx  m, Φ k x  Ψ k x)
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
  Proof. auto using big_sepM_mono with I. Qed.

422
  Lemma big_sepM_later Φ m :
423
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
424
  Proof. apply (big_opM_commute _). Qed.
425

Robbert Krebbers's avatar
Robbert Krebbers committed
426 427 428 429
  Lemma big_sepM_laterN Φ n m :
    ^n ([ map] kx  m, Φ k x)  ([ map] kx  m, ^n Φ k x).
  Proof. apply (big_opM_commute _). Qed.

430
  Lemma big_sepM_always Φ m :
431
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
432
  Proof. apply (big_opM_commute _). Qed.
433 434

  Lemma big_sepM_always_if p Φ m :
435
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
436
  Proof. apply (big_opM_commute _). Qed.
437 438 439

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
Ralf Jung's avatar
Ralf Jung committed
440
    ([ map] kx  m, Φ k x)  ( k x, m !! k = Some x  Φ k x).
441 442 443
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
444
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
445 446 447
    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.
448
      by rewrite pure_True // True_impl.
449
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
450 451
      apply impl_intro_l, pure_elim_l=> ?.
      rewrite lookup_insert_ne; last by intros ?; simplify_map_eq.
452
      by rewrite pure_True // True_impl.
453 454 455
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
Ralf Jung's avatar
Ralf Jung committed
456
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
457
     [ map] kx  m, Ψ k x.
458 459
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
460
    setoid_rewrite always_impl; setoid_rewrite always_pure.
461 462 463
    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.
464

Robbert Krebbers's avatar
Robbert Krebbers committed
465
  Global Instance big_sepM_empty_persistent Φ :
466
    PersistentP ([ map] kx  , Φ k x).
467
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
468
  Global Instance big_sepM_persistent Φ m :
469
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
470
  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
471
  Global Instance big_sepM_nil_timeless Φ :
472
    TimelessP ([ map] kx  , Φ k x).
473
  Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
474
  Global Instance big_sepM_timeless Φ m :
475
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
476
  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
477 478
End gmap.

479

480
(** ** Big ops over finite sets *)
481 482 483
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
484
  Implicit Types Φ : A  uPred M.
485

486
  Lemma big_sepS_mono Φ Ψ X Y :
487
    Y  X  ( x, x  Y  Φ x  Ψ x) 
488
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
489
  Proof.
490
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
491 492 493
    - apply uPred_included. apply: big_op_contains.
      by apply fmap_contains, elements_contains.
    - apply big_opS_forall; apply _ || auto.
494
  Qed.
495 496
  Lemma big_sepS_proper Φ Ψ X :
    ( x, x  X  Φ x  Ψ x) 
497
    ([ set] x  X, Φ x)  ([ set] x  X, Ψ x).
498
  Proof. apply: big_opS_proper. Qed.
499

500
  Global Instance big_sepS_mono' X :
501 502 503
     Proper (pointwise_relation _ () ==> ()) (big_opS (M:=uPredUR M) X).
  Proof. intros f g Hf. apply big_opS_forall; apply _ || intros; apply Hf. Qed.

504
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
505
  Proof. by rewrite big_opS_empty. Qed.
506

507
  Lemma big_sepS_insert Φ X x :
508
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
509 510
  Proof. apply: big_opS_insert. Qed.

511
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
512
    x  X 
513 514
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
515 516
  Proof. apply: big_opS_fn_insert. Qed.

517
  Lemma big_sepS_fn_insert' Φ X x P :
518
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
519
  Proof. apply: big_opS_fn_insert'. Qed.
520

Robbert Krebbers's avatar
Robbert Krebbers committed
521 522 523 524 525
  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.

526
  Lemma big_sepS_delete Φ X x :
527
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
528
  Proof. apply: big_opS_delete. Qed.
529

530
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
531
  Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
532

533 534 535 536 537 538 539
  Lemma big_sepS_elem_of_acc Φ X x :
    x  X 
    ([ set] y  X, Φ y)  Φ x  (Φ x - ([ set] y  X, Φ y)).
  Proof.
    intros. rewrite big_sepS_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

540
  Lemma big_sepS_singleton Φ x : ([ set] y  {[ x ]}, Φ y)  Φ x.
541
  Proof. apply: big_opS_singleton. Qed.
542

543
  Lemma big_sepS_filter (P : A  Prop) `{ x, Decision (P x)} Φ X :
Ralf Jung's avatar
Ralf Jung committed
544
    ([ set] y  filter P X, Φ y)  ([ set] y  X, P y  Φ y).
545 546 547 548 549 550 551 552 553 554 555
  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.

556 557 558 559 560 561 562 563 564 565 566
  Lemma big_sepS_filter_acc (P : A  Prop) `{ y, Decision (P y)} Φ X Y :
    ( y, y  Y  P y  y  X) 
    ([ set] y  X, Φ y) -
      ([ set] y  Y, P y  Φ y) 
      (([ set] y  Y, P y  Φ y) - [ set] y  X, Φ y).
  Proof.
    intros ?. destruct (proj1 (subseteq_disjoint_union_L (filter P Y) X))
      as (Z&->&?); first set_solver.
    rewrite big_sepS_union // big_sepS_filter. by apply sep_mono_r, wand_intro_l.
  Qed.

567
  Lemma big_sepS_sepS Φ Ψ X :
568
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
569
  Proof. apply: big_opS_opS. Qed.
570

571 572 573 574
  Lemma big_sepS_and Φ Ψ X :
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
  Proof. auto using big_sepS_mono with I. Qed.

575
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
576
  Proof. apply (big_opS_commute _). Qed.
577

Robbert Krebbers's avatar
Robbert Krebbers committed
578 579 580 581
  Lemma big_sepS_laterN Φ n X :
    ^n ([ set] y  X, Φ y)  ([ set] y  X, ^n Φ y).
  Proof. apply (big_opS_commute _). Qed.

582
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
583
  Proof. apply (big_opS_commute _). Qed.
584

585
  Lemma big_sepS_always_if q Φ X :
586
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
587
  Proof. apply (big_opS_commute _). Qed.
588 589

  Lemma big_sepS_forall Φ X :
Ralf Jung's avatar
Ralf Jung committed
590
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x)  ( x, x  X  Φ x).
591 592 593
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
594
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
595
    induction X as [|x X ? IH] using collection_ind_L.
596 597
    { rewrite big_sepS_empty; auto. }
    rewrite big_sepS_insert // -always_and_sep_l. apply and_intro.
598
    - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
599
    - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
600
      by rewrite pure_True ?True_impl; last set_solver.
601 602 603
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
Ralf Jung's avatar
Ralf Jung committed
604
     ( x, x  X  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
605 606
  Proof.
    rewrite always_and_sep_l always_forall.
607
    setoid_rewrite always_impl; setoid_rewrite always_pure.
608 609 610
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
611

612
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
613
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
614
  Global Instance big_sepS_persistent Φ X :
615
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
616
  Proof. rewrite /big_opS. apply _. Qed.
617
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
618
  Proof. rewrite /big_opS elements_empty. apply _. Qed.
619
  Global Instance big_sepS_timeless Φ X :
620
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
621
  Proof. rewrite /big_opS. apply _. Qed.
622
End gset.
Robbert Krebbers's avatar
Robbert Krebbers committed
623

Robbert Krebbers's avatar
Robbert Krebbers committed
624 625 626 627
Lemma big_sepM_dom `{Countable K} {A} (Φ : K  uPred M) (m : gmap K A) :
  ([ map] k_  m, Φ k)  ([ set] k  dom _ m, Φ k).
Proof. apply: big_opM_dom. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666

(** ** 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. 

667 668 669 670 671 672 673
  Lemma big_sepMS_elem_of_acc Φ X x :
    x  X 
    ([ mset] y  X, Φ y)  Φ x  (Φ x - ([ mset] y  X, Φ y)).
  Proof.
    intros. rewrite big_sepMS_delete //. by apply sep_mono_r, wand_intro_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
674 675 676 677 678 679 680
  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.

681 682 683 684
  Lemma big_sepMS_and Φ Ψ X :
    ([ mset] y  X, Φ y  Ψ y)  ([ mset] y  X, Φ y)  ([ mset] y  X, Ψ y).
  Proof. auto using big_sepMS_mono with I. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
685 686 687
  Lemma big_sepMS_later Φ X :  ([ mset] y  X, Φ y)  ([ mset] y  X,  Φ y).
  Proof. apply (big_opMS_commute _). Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed