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

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

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

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

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

37
Definition uPred_big_sepS {M} `{Countable A}
38
  (X : gset A) (Φ : A  uPred M) : uPred M := [] (Φ <$> elements X).
39
Instance: Params (@uPred_big_sepS) 5.
40 41 42
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.
43

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

49
(** * Properties *)
50
Section big_op.
51
Context {M : ucmraT}.
52 53 54
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

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

61
Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
62
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
63
Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
64 65
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

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

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

86
Lemma big_and_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
87
Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
88
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs)  [] Ps  [] Qs.
89
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
90

91
Lemma big_and_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
92
Proof.
93
  intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
94
Qed.
95
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
96
Proof.
97
  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
98 99
Qed.

100
Lemma big_sep_and Ps : [] Ps  [] Ps.
101
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
102

103
Lemma big_and_elem_of Ps P : P  Ps  [] Ps  P.
104
Proof. induction 1; simpl; auto with I. Qed.
105
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
106 107
Proof. induction 1; simpl; auto with I. Qed.

108
(** ** Big ops over finite maps *)
109 110 111
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
112
  Implicit Types Φ Ψ : K  A  uPred M.
113

114
  Lemma big_sepM_mono Φ Ψ m1 m2 :
115
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
116
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
117
  Proof.
118
    intros HX HΦ. trans ([ map] kx  m2, Φ k x)%I.
119
    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
120
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
121
      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
122
  Qed.
123
  Lemma big_sepM_proper Φ Ψ m1 m2 :
124
    m1  m2  ( k x, m1 !! k = Some x  m2 !! k = Some x  Φ k x  Ψ k x) 
125
    ([ map] k  x  m1, Φ k x)  ([ map] k  x  m2, Ψ k x).
126
  Proof.
127 128 129
    (* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives
    File "./algebra/upred_big_op.v", line 114, characters 4-131:
    Anomaly: Uncaught exception Univ.AlreadyDeclared. Please report. *)
130
    intros [??] ?; apply (anti_symm ()); apply big_sepM_mono;
131
      eauto using equiv_entails, equiv_entails_sym, @lookup_weaken.
132
  Qed.
133 134 135 136 137

  Global Instance big_sepM_ne m n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (uPred_big_sepM (M:=M) m).
  Proof.
138
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
139
    apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ.
140
  Qed.
141
  Global Instance big_sepM_proper' m :
142
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
143
           (uPred_big_sepM (M:=M) m).
144
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
145
  Global Instance big_sepM_mono' m :
146
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
147
           (uPred_big_sepM (M:=M) m).
148
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
149

150
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
151
  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
152

153
  Lemma big_sepM_insert Φ m i x :
154
    m !! i = None 
155
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
156
  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
157

158
  Lemma big_sepM_delete Φ m i x :
159
    m !! i = Some x 
160
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
161 162 163 164
  Proof.
    intros. rewrite -big_sepM_insert ?lookup_delete //.
    by rewrite insert_delete insert_id.
  Qed.
165

166 167 168 169
  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.

170
  Lemma big_sepM_singleton Φ i x : ([ map] ky  {[i:=x]}, Φ k y)  Φ i x.
171 172 173 174
  Proof.
    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
    by rewrite big_sepM_empty right_id.
  Qed.
175

176 177 178 179 180 181 182
  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.

183
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
184
    m !! i = Some x 
185
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
186 187 188 189 190
  Proof.
    intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
    by rewrite -big_sepM_delete.
  Qed.

191
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
192
    m !! i = None 
193 194
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
195 196 197 198 199 200 201 202 203 204
  Proof.
    intros. rewrite big_sepM_insert // fn_lookup_insert.
    apply sep_proper, big_sepM_proper; auto=> k y ??.
    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.

205
  Lemma big_sepM_sepM Φ Ψ m :
206
       ([ map] kx  m, Φ k x  Ψ k x)
207
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
208
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
209 210
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
211
    by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _  _)%I]comm -!assoc.
212
  Qed.
213

214
  Lemma big_sepM_later Φ m :
215
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
216
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
217 218 219
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
    by rewrite later_sep IH.
220
  Qed.
221 222 223 224 225

  Lemma big_sepM_always Φ m :
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
  Proof.
    rewrite /uPred_big_sepM.
226
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?always_pure //.
227 228 229 230
    by rewrite always_sep IH.
  Qed.

  Lemma big_sepM_always_if p Φ m :
231
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
232
  Proof. destruct p; simpl; auto using big_sepM_always. Qed.
233 234 235 236 237 238 239

  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.
240
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
241 242 243
    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.
244
    - rewrite (forall_elim i) (forall_elim x) pure_equiv; last by left.
245 246
      by rewrite True_impl.
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
247
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
248 249 250 251
      by rewrite True_impl.
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
252
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
253 254 255
     [ map] kx  m, Ψ k x.
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
256
    setoid_rewrite always_impl; setoid_rewrite always_pure.
257 258 259
    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.
260 261
End gmap.

262
(** ** Big ops over finite sets *)
263 264 265
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
266
  Implicit Types Φ : A  uPred M.
267

268
  Lemma big_sepS_mono Φ Ψ X Y :
269
    Y  X  ( x, x  Y  Φ x  Ψ x) 
270
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
271
  Proof.
272
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
273
    - by apply big_sep_contains, fmap_contains, elements_contains.
274
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
275
      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
276
  Qed.
277
  Lemma big_sepS_proper Φ Ψ X Y :
278 279
    X  Y  ( x, x  X  x  Y  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  ([ set] x  Y, Ψ x).
280 281 282 283
  Proof.
    intros [??] ?; apply (anti_symm ()); apply big_sepS_mono;
      eauto using equiv_entails, equiv_entails_sym.
  Qed.
284 285 286 287

  Lemma big_sepS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
  Proof.
288
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
289
    apply Forall_Forall2, Forall_true=> x; apply HΦ.
290
  Qed.
291
  Lemma big_sepS_proper' X :
292
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
293
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
294
  Lemma big_sepS_mono' X :
295
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
296
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
297

298
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
299
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
300

301
  Lemma big_sepS_insert Φ X x :
302
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
303
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
304
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
305
    x  X 
306 307
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
308 309 310 311 312
  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.
313
  Lemma big_sepS_fn_insert' Φ X x P :
314
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
315
  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
316

317
  Lemma big_sepS_delete Φ X x :
318
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
319
  Proof.
320 321
    intros. rewrite -big_sepS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
322
  Qed.
323

324 325 326
  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.

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

330
  Lemma big_sepS_sepS Φ Ψ X :
331
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
332
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
333 334
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
335
    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _  _)%I]comm -!assoc.
336 337
  Qed.

338
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
339
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
340 341 342
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
    by rewrite later_sep IH.
343
  Qed.
344

345
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
346 347
  Proof.
    rewrite /uPred_big_sepS.
348
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_pure.
349 350 351 352
    by rewrite always_sep IH.
  Qed.

  Lemma big_sepS_always_if q Φ X :
353
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
354
  Proof. destruct q; simpl; auto using big_sepS_always. Qed.
355 356 357 358 359 360

  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.
361
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
362 363 364
    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.
365
    - rewrite (forall_elim x) pure_equiv; last by left. by rewrite True_impl.
366
    - rewrite -IH. apply forall_mono=> y.
367
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
368 369 370 371
      by rewrite True_impl.
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
372
       ( x,  (x  X)  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
373 374
  Proof.
    rewrite always_and_sep_l always_forall.
375
    setoid_rewrite always_impl; setoid_rewrite always_pure.
376 377 378
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
379
End gset.
380

381
(** ** Persistence *)
382
Global Instance big_and_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
383
Proof. induction 1; apply _. Qed.
384
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
385 386
Proof. induction 1; apply _. Qed.

387
Global Instance nil_persistent : PersistentL (@nil (uPred M)).
388
Proof. constructor. Qed.
389
Global Instance cons_persistent P Ps :
390
  PersistentP P  PersistentL Ps  PersistentL (P :: Ps).
391
Proof. by constructor. Qed.
392 393
Global Instance app_persistent Ps Ps' :
  PersistentL Ps  PersistentL Ps'  PersistentL (Ps ++ Ps').
394
Proof. apply Forall_app_2. Qed.
395
Global Instance zip_with_persistent {A B} (f : A  B  uPred M) xs ys :
396
  ( x y, PersistentP (f x y))  PersistentL (zip_with f xs ys).
397 398 399
Proof.
  unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
400
End big_op.