upred_big_op.v 26.1 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
(** 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.
9 10 11
- The operator [ [★ list] k ↦ x ∈ l, P ] asserts that [P] holds separately for
  each element [x] at position [x] in the list [l]. This operator is a
  quantifier, and thus has the same precedence as [∀] and [∃].
12 13 14 15 16 17 18
- 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 [∃]. *)

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

30
(** * Other big ops *)
31 32 33 34 35 36 37 38 39 40 41
Definition uPred_big_sepL {M A} (l : list A)
  (Φ : nat  A  uPred M) : uPred M := [] (imap Φ l).
Instance: Params (@uPred_big_sepL) 2.
Typeclasses Opaque uPred_big_sepL.
Notation "'[★' 'list' ] k ↦ x ∈ l , P" := (uPred_big_sepL l (λ k x, P))
  (at level 200, l at level 10, k, x at level 1, right associativity,
   format "[★  list ]  k ↦ x  ∈  l ,  P") : uPred_scope.
Notation "'[★' 'list' ] x ∈ l , P" := (uPred_big_sepL l (λ _ x, P))
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[★  list ]  x  ∈  l ,  P") : uPred_scope.

42
Definition uPred_big_sepM {M} `{Countable K} {A}
43
    (m : gmap K A) (Φ : K  A  uPred M) : uPred M :=
44
  [] (curry Φ <$> map_to_list m).
45
Instance: Params (@uPred_big_sepM) 6.
46
Typeclasses Opaque uPred_big_sepM.
47 48 49
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.
50

51
Definition uPred_big_sepS {M} `{Countable A}
52
  (X : gset A) (Φ : A  uPred M) : uPred M := [] (Φ <$> elements X).
53
Instance: Params (@uPred_big_sepS) 5.
54
Typeclasses Opaque uPred_big_sepS.
55 56 57
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.
58

59
(** * Persistence and timelessness of lists of uPreds *)
60
Class PersistentL {M} (Ps : list (uPred M)) :=
61
  persistentL : Forall PersistentP Ps.
62
Arguments persistentL {_} _ {_}.
63

64 65 66 67
Class TimelessL {M} (Ps : list (uPred M)) :=
  timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.

68
(** * Properties *)
69
Section big_op.
70
Context {M : ucmraT}.
71 72 73
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

74
(** ** Generic big ops over lists of upreds *)
75
Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M).
76
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
77
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
78
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
79

80
Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
81
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
82
Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
83 84
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

85
Global Instance big_and_mono' : Proper (Forall2 () ==> ()) (@uPred_big_and M).
86
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
87
Global Instance big_sep_mono' : Proper (Forall2 () ==> ()) (@uPred_big_sep M).
88 89
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

90
Global Instance big_and_perm : Proper (() ==> ()) (@uPred_big_and M).
91 92
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
93 94
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
95
  - etrans; eauto.
96
Qed.
97
Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M).
98 99
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
100 101
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
102
  - etrans; eauto.
103
Qed.
104

105
Lemma big_and_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
106
Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
107
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
108
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
109

110
Lemma big_and_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
111
Proof.
112
  intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
113
Qed.
114
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
115
Proof.
116
  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
117 118
Qed.

119
Lemma big_sep_and Ps : [] Ps  [] Ps.
120
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
121

122
Lemma big_and_elem_of Ps P : P  Ps  [] Ps  P.
123
Proof. induction 1; simpl; auto with I. Qed.
124
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
125 126
Proof. induction 1; simpl; auto with I. Qed.

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

(** ** 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).
173
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
174 175 176 177 178
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.
179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
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.

  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.
  Proof.
    intros HΦ. apply big_sep_mono'.
    revert Φ Ψ HΦ. induction l as [|x l IH]=> Φ Ψ HΦ; first constructor.
    rewrite !imap_cons; constructor; eauto.
  Qed.
  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).
  Proof.
    intros ?; apply (anti_symm ()); apply big_sepL_mono;
      eauto using equiv_entails, equiv_entails_sym, lookup_weaken.
  Qed.

  Global Instance big_sepL_ne l n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (uPred_big_sepL (M:=M) l).
  Proof.
    intros Φ Ψ HΦ. apply big_sep_ne.
    revert Φ Ψ HΦ. induction l as [|x l IH]=> Φ Ψ HΦ; first constructor.
    rewrite !imap_cons; constructor. by apply HΦ. apply IH=> n'; apply HΦ.
  Qed.
  Global Instance big_sepL_proper' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
           (uPred_big_sepL (M:=M) l).
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepL_proper; intros; last apply HΦ. Qed.
  Global Instance big_sepL_mono' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
           (uPred_big_sepL (M:=M) l).
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepL_mono; intros; last apply HΦ. Qed.

  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 /uPred_big_sepL imap_cons. Qed.

  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y)  Φ 0 x.
  Proof. by rewrite big_sepL_cons big_sepL_nil right_id. 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 /uPred_big_sepL imap_app big_sep_app. Qed.

  Lemma big_sepL_lookup Φ l i x :
    l !! i = Some x  ([ list] ky  l, Φ k y)  Φ i x.
  Proof.
    intros. rewrite -(take_drop_middle l i x) // big_sepL_app big_sepL_cons.
    rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
    by rewrite sep_elim_r sep_elim_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
247 248 249 250 251 252
  Lemma big_sepL_elem_of (Φ : A  uPred M) l x :
    x  l  ([ list] y  l, Φ y)  Φ x.
  Proof.
    intros [i ?]%elem_of_list_lookup; eauto using (big_sepL_lookup (λ _, Φ)).
  Qed.

253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310
  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)).
  Proof. by rewrite /uPred_big_sepL imap_fmap. Qed.

  Lemma big_sepL_sepL Φ Ψ l :
    ([ list] kx  l, Φ k x  Ψ k x)
     ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ k x).
  Proof.
    revert Φ Ψ; induction l as [|x l IH]=> Φ Ψ.
    { by rewrite !big_sepL_nil left_id. }
    rewrite !big_sepL_cons IH.
    by rewrite -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _  _)%I]comm -!assoc.
  Qed.

  Lemma big_sepL_later Φ l :
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
  Proof.
    revert Φ. induction l as [|x l IH]=> Φ.
    { by rewrite !big_sepL_nil later_True. }
    by rewrite !big_sepL_cons later_sep IH.
  Qed.

  Lemma big_sepL_always Φ l :
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
  Proof.
    revert Φ. induction l as [|x l IH]=> Φ.
    { by rewrite !big_sepL_nil always_pure. }
    by rewrite !big_sepL_cons always_sep IH.
  Qed.

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

  Lemma big_sepL_forall Φ l :
    ( k x, PersistentP (Φ k x)) 
    ([ list] kx  l, Φ k x)  ( k x, l !! k = Some x  Φ k x).
  Proof.
    intros HΦ. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepL_lookup. }
    revert Φ HΦ. induction l as [|x l IH]=> Φ HΦ.
    { rewrite big_sepL_nil; auto with I. }
    rewrite big_sepL_cons. rewrite -always_and_sep_l; apply and_intro.
    - by rewrite (forall_elim 0) (forall_elim x) pure_equiv // True_impl.
    - rewrite -IH. apply forall_intro=> k; by rewrite (forall_elim (S k)).
  Qed.

  Lemma big_sepL_impl Φ Ψ l :
     ( k x, l !! k = Some x  Φ k x  Ψ k x)  ([ list] kx  l, Φ k x)
     [ list] kx  l, Ψ k x.
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
    setoid_rewrite always_impl; setoid_rewrite always_pure.
    rewrite -big_sepL_forall -big_sepL_sepL. apply big_sepL_mono; auto=> k x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
311 312 313 314 315
  Global Instance big_sepL_nil_persistent Φ :
    PersistentP ([ list] kx  [], Φ k x).
  Proof. rewrite /uPred_big_sepL. apply _. Qed.
  Global Instance big_sepL_persistent Φ l :
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  l, Φ k x).
316 317
  Proof. rewrite /uPred_big_sepL. apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
318 319 320 321 322
  Global Instance big_sepL_nil_timeless Φ :
    TimelessP ([ list] kx  [], Φ k x).
  Proof. rewrite /uPred_big_sepL. apply _. Qed.
  Global Instance big_sepL_timeless Φ l :
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  l, Φ k x).
323 324 325
  Proof. rewrite /uPred_big_sepL. apply _. Qed.
End list.

326

327
(** ** Big ops over finite maps *)
328 329 330
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
331
  Implicit Types Φ Ψ : K  A  uPred M.
332

333
  Lemma big_sepM_mono Φ Ψ m1 m2 :
334
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
335
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
336
  Proof.
337
    intros HX HΦ. trans ([ map] kx  m2, Φ k x)%I.
338
    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
339
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
340
      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
341
  Qed.
342 343 344
  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).
345 346 347 348
  Proof.
    intros ?; apply (anti_symm ()); apply big_sepM_mono;
      eauto using equiv_entails, equiv_entails_sym, lookup_weaken.
  Qed.
349 350 351 352 353

  Global Instance big_sepM_ne m n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (uPred_big_sepM (M:=M) m).
  Proof.
354
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
355
    apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ.
356
  Qed.
357
  Global Instance big_sepM_proper' m :
358
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
359
           (uPred_big_sepM (M:=M) m).
360
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
361
  Global Instance big_sepM_mono' m :
362
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
363
           (uPred_big_sepM (M:=M) m).
364
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
365

366
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
367
  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
368

369
  Lemma big_sepM_insert Φ m i x :
370
    m !! i = None 
371
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
372
  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
373

374
  Lemma big_sepM_delete Φ m i x :
375
    m !! i = Some x 
376
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
377 378 379 380
  Proof.
    intros. rewrite -big_sepM_insert ?lookup_delete //.
    by rewrite insert_delete insert_id.
  Qed.
381

382 383 384 385
  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.

386
  Lemma big_sepM_singleton Φ i x : ([ map] ky  {[i:=x]}, Φ k y)  Φ i x.
387 388 389 390
  Proof.
    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
    by rewrite big_sepM_empty right_id.
  Qed.
391

392 393 394 395 396 397 398
  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.

399
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
400
    m !! i = Some x 
401
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
402 403 404 405 406
  Proof.
    intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
    by rewrite -big_sepM_delete.
  Qed.

407
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
408
    m !! i = None 
409 410
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
411 412
  Proof.
    intros. rewrite big_sepM_insert // fn_lookup_insert.
413
    apply sep_proper, big_sepM_proper; auto=> k y ?.
414 415 416 417 418 419 420
    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.

421
  Lemma big_sepM_sepM Φ Ψ m :
422
       ([ map] kx  m, Φ k x  Ψ k x)
423
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
424
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
425 426
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
427
    by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _  _)%I]comm -!assoc.
428
  Qed.
429

430
  Lemma big_sepM_later Φ m :
431
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
432
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
433 434 435
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
    by rewrite later_sep IH.
436
  Qed.
437 438 439 440 441

  Lemma big_sepM_always Φ m :
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
  Proof.
    rewrite /uPred_big_sepM.
442
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?always_pure //.
443 444 445 446
    by rewrite always_sep IH.
  Qed.

  Lemma big_sepM_always_if p Φ m :
447
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
448
  Proof. destruct p; simpl; auto using big_sepM_always. Qed.
449 450 451 452 453 454 455

  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.
456
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
457 458 459
    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.
460
    - rewrite (forall_elim i) (forall_elim x) pure_equiv; last by left.
461 462
      by rewrite True_impl.
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
463
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
464 465 466 467
      by rewrite True_impl.
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
468
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
469 470 471
     [ map] kx  m, Ψ k x.
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
472
    setoid_rewrite always_impl; setoid_rewrite always_pure.
473 474 475
    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.
476

Robbert Krebbers's avatar
Robbert Krebbers committed
477 478 479
  Global Instance big_sepM_empty_persistent Φ :
    PersistentP ([ map] kx  , Φ k x).
  Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
480 481 482 483
  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
484 485 486
  Global Instance big_sepM_nil_timeless Φ :
    TimelessP ([ map] kx  , Φ k x).
  Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
487 488 489
  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.
490 491
End gmap.

492

493
(** ** Big ops over finite sets *)
494 495 496
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
497
  Implicit Types Φ : A  uPred M.
498

499
  Lemma big_sepS_mono Φ Ψ X Y :
500
    Y  X  ( x, x  Y  Φ x  Ψ x) 
501
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
502
  Proof.
503
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
504
    - by apply big_sep_contains, fmap_contains, elements_contains.
505
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
506
      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
507
  Qed.
508
  Lemma big_sepS_proper Φ Ψ X Y :
509 510
    X  Y  ( x, x  X  x  Y  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  ([ set] x  Y, Ψ x).
511
  Proof.
512 513
    move=> /collection_equiv_spec [??] ?; apply (anti_symm ());
      apply big_sepS_mono; eauto using equiv_entails, equiv_entails_sym.
514
  Qed.
515 516 517 518

  Lemma big_sepS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
  Proof.
519
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
520
    apply Forall_Forall2, Forall_true=> x; apply HΦ.
521
  Qed.
522
  Lemma big_sepS_proper' X :
523
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
524
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
525
  Lemma big_sepS_mono' X :
526
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
527
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
528

529
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
530
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
531

532
  Lemma big_sepS_insert Φ X x :
533
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
534
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
535
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
536
    x  X 
537 538
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
539 540 541 542 543
  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.
544
  Lemma big_sepS_fn_insert' Φ X x P :
545
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
546
  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
547

548
  Lemma big_sepS_delete Φ X x :
549
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
550
  Proof.
551 552
    intros. rewrite -big_sepS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
553
  Qed.
554

555 556 557
  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.

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

561
  Lemma big_sepS_sepS Φ Ψ X :
562
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
563
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
564 565
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
566
    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _  _)%I]comm -!assoc.
567 568
  Qed.

569
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
570
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
571 572 573
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
    by rewrite later_sep IH.
574
  Qed.
575

576
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
577 578
  Proof.
    rewrite /uPred_big_sepS.
579
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_pure.
580 581 582 583
    by rewrite always_sep IH.
  Qed.

  Lemma big_sepS_always_if q Φ X :
584
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
585
  Proof. destruct q; simpl; auto using big_sepS_always. Qed.
586 587 588 589 590 591

  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.
592
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
593 594 595
    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.
596
    - rewrite (forall_elim x) pure_equiv; last by left. by rewrite True_impl.
597
    - rewrite -IH. apply forall_mono=> y.
598
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
599 600 601 602
      by rewrite True_impl.
  Qed.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
611 612
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
  Proof. rewrite /uPred_big_sepS elements_empty. apply _. Qed.
613 614 615
  Global Instance big_sepS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
  Proof. rewrite /uPred_big_sepS. apply _. Qed.
616

Robbert Krebbers's avatar
Robbert Krebbers committed
617 618
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
  Proof. rewrite /uPred_big_sepS elements_empty. apply _. Qed.
619 620 621 622
  Global Instance big_sepS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
  Proof. rewrite /uPred_big_sepS. apply _. Qed.
End gset.
623
End big_op.