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

5
6
(** We define the following big operators:

7
- The operator [ [★] Ps ] folds [★] over the list [Ps].
8
  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
22
23
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.
24
Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
25

26
(** * Other big ops *)
27
28
29
30
31
32
33
34
35
36
37
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.

38
Definition uPred_big_sepM {M} `{Countable K} {A}
39
    (m : gmap K A) (Φ : K  A  uPred M) : uPred M :=
40
  [] (curry Φ <$> map_to_list m).
41
Instance: Params (@uPred_big_sepM) 6.
42
Typeclasses Opaque uPred_big_sepM.
43
44
45
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.
46
47
48
Notation "'[★' 'map' ] x ∈ m , P" := (uPred_big_sepM m (λ _ x, P))
  (at level 200, m at level 10, x at level 1, right associativity,
   format "[★  map ]  x  ∈  m ,  P") : uPred_scope.
49

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

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

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

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

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

81
Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M).
82
83
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
84
85
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
86
  - etrans; eauto.
87
Qed.
88

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

92
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
93
Proof.
94
  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
95
Qed.
96
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
97
98
Proof. induction 1; simpl; auto with I. Qed.

99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
(** ** Persistence *)
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
Proof. induction 1; apply _. Qed.

Global Instance nil_persistent : PersistentL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_persistent P Ps :
  PersistentP P  PersistentL Ps  PersistentL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_persistent Ps Ps' :
  PersistentL Ps  PersistentL Ps'  PersistentL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.

Global Instance fmap_persistent {A} (f : A  uPred M) xs :
  ( x, PersistentP (f x))  PersistentL (f <$> xs).
114
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
115
116
117
118
119
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.
120
121
122
123
124
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.
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140

(** ** Timelessness *)
Global Instance big_sep_timeless Ps : TimelessL Ps  TimelessP ([] Ps).
Proof. induction 1; apply _. Qed.

Global Instance nil_timeless : TimelessL (@nil (uPred M)).
Proof. constructor. Qed.
Global Instance cons_timeless P Ps :
  TimelessP P  TimelessL Ps  TimelessL (P :: Ps).
Proof. by constructor. Qed.
Global Instance app_timeless Ps Ps' :
  TimelessL Ps  TimelessL Ps'  TimelessL (Ps ++ Ps').
Proof. apply Forall_app_2. Qed.

Global Instance fmap_timeless {A} (f : A  uPred M) xs :
  ( x, TimelessP (f x))  TimelessL (f <$> xs).
141
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
142
143
144
145
146
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.
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
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
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
215
216
217
218
219
220
  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.

221
222
223
224
225
226
227
228
229
230
231
232
233
234
  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.

235
236
237
238
  Lemma big_sepL_commute (Ψ: uPred M  uPred M) `{!Proper (() ==> ()) Ψ} Φ l :
    Ψ True  True 
    ( P Q, Ψ (P  Q)  Ψ P  Ψ Q) 
    Ψ ([ list] kx  l, Φ k x)  ([ list] kx  l, Ψ (Φ k x)).
239
  Proof.
240
241
    intros ??. revert Φ. induction l as [|x l IH]=> Φ //.
    by rewrite !big_sepL_cons -IH.
242
  Qed.
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
  Lemma big_sepL_op_commute {B : ucmraT}
      (Ψ: B  uPred M) `{!Proper (() ==> ()) Ψ} (f : nat  A  B) l :
    Ψ   True 
    ( x y, Ψ (x  y)  Ψ x  Ψ y) 
    Ψ ([ list] kx  l, f k x)  ([ list] kx  l, Ψ (f k x)).
  Proof.
    intros ??. revert f. induction l as [|x l IH]=> f //.
    by rewrite big_sepL_cons big_opL_cons -IH.
  Qed.
  Lemma big_sepL_op_commute1 {B : ucmraT}
      (Ψ: B  uPred M) `{!Proper (() ==> ()) Ψ} (f : nat  A  B) l :
    ( x y, Ψ (x  y)  Ψ x  Ψ y) 
    l  [] 
    Ψ ([ list] kx  l, f k x)  ([ list] kx  l, Ψ (f k x)).
  Proof.
    intros ??. revert f. induction l as [|x [|x' l'] IH]=> f //.
    { by rewrite big_sepL_singleton big_opL_singleton. }
    by rewrite big_sepL_cons big_opL_cons -IH.
  Qed.

  Lemma big_sepL_later Φ l :
     ([ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
  Proof. apply (big_sepL_commute _); auto using later_True, later_sep. Qed.
266
267
268

  Lemma big_sepL_always Φ l :
    ( [ list] kx  l, Φ k x)  ([ list] kx  l,  Φ k x).
269
  Proof. apply (big_sepL_commute _); auto using always_pure, always_sep. Qed.
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

  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
299
300
301
302
303
  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).
304
305
  Proof. rewrite /uPred_big_sepL. apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
306
307
308
309
310
  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).
311
312
313
  Proof. rewrite /uPred_big_sepL. apply _. Qed.
End list.

314

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

321
  Lemma big_sepM_mono Φ Ψ m1 m2 :
322
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
323
    ([ map] k  x  m1, Φ k x)  [ map] k  x  m2, Ψ k x.
324
  Proof.
325
    intros HX HΦ. trans ([ map] kx  m2, Φ k x)%I.
326
    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
327
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
328
      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
329
  Qed.
330
331
332
  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).
333
334
335
336
  Proof.
    intros ?; apply (anti_symm ()); apply big_sepM_mono;
      eauto using equiv_entails, equiv_entails_sym, lookup_weaken.
  Qed.
337
338
339
340
341

  Global Instance big_sepM_ne m n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (uPred_big_sepM (M:=M) m).
  Proof.
342
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
343
    apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ.
344
  Qed.
345
  Global Instance big_sepM_proper' m :
346
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
347
           (uPred_big_sepM (M:=M) m).
348
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
349
  Global Instance big_sepM_mono' m :
350
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
351
           (uPred_big_sepM (M:=M) m).
352
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
353

354
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
355
  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
356

357
  Lemma big_sepM_insert Φ m i x :
358
    m !! i = None 
359
    ([ map] ky  <[i:=x]> m, Φ k y)  Φ i x  [ map] ky  m, Φ k y.
360
  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
361

362
  Lemma big_sepM_delete Φ m i x :
363
    m !! i = Some x 
364
    ([ map] ky  m, Φ k y)  Φ i x  [ map] ky  delete i m, Φ k y.
365
366
367
368
  Proof.
    intros. rewrite -big_sepM_insert ?lookup_delete //.
    by rewrite insert_delete insert_id.
  Qed.
369

370
371
372
373
  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.

374
  Lemma big_sepM_singleton Φ i x : ([ map] ky  {[i:=x]}, Φ k y)  Φ i x.
375
376
377
378
  Proof.
    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
    by rewrite big_sepM_empty right_id.
  Qed.
379

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

387
  Lemma big_sepM_insert_override (Φ : K  uPred M) m i x y :
388
    m !! i = Some x 
389
    ([ map] k_  <[i:=y]> m, Φ k)  ([ map] k_  m, Φ k).
390
391
392
393
394
  Proof.
    intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
    by rewrite -big_sepM_delete.
  Qed.

395
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
396
    m !! i = None 
397
398
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
     (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
399
400
  Proof.
    intros. rewrite big_sepM_insert // fn_lookup_insert.
401
    apply sep_proper, big_sepM_proper; auto=> k y ?.
402
403
404
405
406
407
408
    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.

409
  Lemma big_sepM_sepM Φ Ψ m :
410
       ([ map] kx  m, Φ k x  Ψ k x)
411
     ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x).
412
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
413
414
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
415
    by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _  _)%I]comm -!assoc.
416
  Qed.
417

418
419
420
421
  Lemma big_sepM_commute (Ψ: uPred M  uPred M) `{!Proper (() ==> ()) Ψ} Φ m :
    Ψ True  True 
    ( P Q, Ψ (P  Q)  Ψ P  Ψ Q) 
    Ψ ([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ (Φ k x)).
422
  Proof.
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
    intros ??. rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; rewrite //= -?IH; auto.
  Qed.
  Lemma big_sepM_op_commute {B : ucmraT}
      (Ψ: B  uPred M) `{!Proper (() ==> ()) Ψ} (f : K  A  B) m :
    Ψ   True 
    ( x y, Ψ (x  y)  Ψ x  Ψ y) 
    Ψ ([ map] kx  m, f k x)  ([ map] kx  m, Ψ (f k x)).
  Proof.
    intros ??. rewrite /big_opM /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; rewrite //= -?IH; auto.
  Qed.
  Lemma big_sepM_op_commute1 {B : ucmraT}
      (Ψ: B  uPred M) `{!Proper (() ==> ()) Ψ} (f : K  A  B) m :
    ( x y, Ψ (x  y)  Ψ x  Ψ y) 
    m   
    Ψ ([ map] kx  m, f k x)  ([ map] kx  m, Ψ (f k x)).
  Proof.
    rewrite -map_to_list_empty'. intros ??. rewrite /big_opM /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] [|i' x'] IH];
      csimpl in *; rewrite ?right_id -?IH //.
444
  Qed.
445

446
447
448
449
  Lemma big_sepM_later Φ m :
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
  Proof. apply (big_sepM_commute _); auto using later_True, later_sep. Qed.

450
451
  Lemma big_sepM_always Φ m :
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
452
  Proof. apply (big_sepM_commute _); auto using always_pure, always_sep. Qed.
453
454

  Lemma big_sepM_always_if p Φ m :
455
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
456
  Proof. destruct p; simpl; auto using big_sepM_always. Qed.
457
458
459
460
461
462
463

  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.
464
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
465
466
467
    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.
468
    - rewrite (forall_elim i) (forall_elim x) pure_equiv; last by left.
469
470
      by rewrite True_impl.
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
471
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
472
473
474
475
      by rewrite True_impl.
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
476
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
477
478
479
     [ map] kx  m, Ψ k x.
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
480
    setoid_rewrite always_impl; setoid_rewrite always_pure.
481
482
483
    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.
484

Robbert Krebbers's avatar
Robbert Krebbers committed
485
486
487
  Global Instance big_sepM_empty_persistent Φ :
    PersistentP ([ map] kx  , Φ k x).
  Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
488
489
490
491
  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
492
493
494
  Global Instance big_sepM_nil_timeless Φ :
    TimelessP ([ map] kx  , Φ k x).
  Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
495
496
497
  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.
498
499
End gmap.

500

501
(** ** Big ops over finite sets *)
502
503
504
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
505
  Implicit Types Φ : A  uPred M.
506

507
  Lemma big_sepS_mono Φ Ψ X Y :
508
    Y  X  ( x, x  Y  Φ x  Ψ x) 
509
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
510
  Proof.
511
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
512
    - by apply big_sep_contains, fmap_contains, elements_contains.
513
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
514
      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
515
  Qed.
516
  Lemma big_sepS_proper Φ Ψ X Y :
517
518
    X  Y  ( x, x  X  x  Y  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  ([ set] x  Y, Ψ x).
519
  Proof.
520
521
    move=> /collection_equiv_spec [??] ?; apply (anti_symm ());
      apply big_sepS_mono; eauto using equiv_entails, equiv_entails_sym.
522
  Qed.
523
524
525
526

  Lemma big_sepS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
  Proof.
527
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
528
    apply Forall_Forall2, Forall_true=> x; apply HΦ.
529
  Qed.
530
  Lemma big_sepS_proper' X :
531
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
532
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
533
  Lemma big_sepS_mono' X :
534
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
535
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
536

537
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
538
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
539

540
  Lemma big_sepS_insert Φ X x :
541
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
542
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
543
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
544
    x  X 
545
546
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
547
548
549
550
551
  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.
552
  Lemma big_sepS_fn_insert' Φ X x P :
553
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
554
  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
555

556
  Lemma big_sepS_delete Φ X x :
557
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
558
  Proof.
559
560
    intros. rewrite -big_sepS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
561
  Qed.
562

563
564
565
  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.

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

569
  Lemma big_sepS_sepS Φ Ψ X :
570
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
571
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
572
573
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
574
    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _  _)%I]comm -!assoc.
575
576
  Qed.

577
578
579
580
  Lemma big_sepS_commute (Ψ: uPred M  uPred M) `{!Proper (() ==> ()) Ψ} Φ X :
    Ψ True  True 
    ( P Q, Ψ (P  Q)  Ψ P  Ψ Q) 
    Ψ ([ set] x  X, Φ x)  ([ set] x  X, Ψ (Φ x)).
581
  Proof.
582
583
    intros ??. rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; rewrite //= -?IH; auto.
584
  Qed.
585
586
587
588
589
  Lemma big_sepS_op_commute {B : ucmraT}
      (Ψ: B  uPred M) `{!Proper (() ==> ()) Ψ} (f : A  B) X :
    Ψ   True 
    ( x y, Ψ (x  y)  Ψ x  Ψ y) 
    Ψ ([ set] x  X, f x)  ([ set] x  X, Ψ (f x)).
590
  Proof.
591
592
593
594
595
596
597
598
599
600
601
602
    intros ??. rewrite /big_opS /uPred_big_sepS.
    induction (elements X) as [|x l IH]; rewrite //= -?IH; auto.
  Qed.
  Lemma big_sepS_op_commute1 {B : ucmraT}
      (Ψ: B  uPred M) `{!Proper (() ==> ()) Ψ} (f : A  B) X :
    ( x y, Ψ (x  y)  Ψ x  Ψ y) 
    X   
    Ψ ([ set] x  X, f x)  ([ set] x  X, Ψ (f x)).
  Proof.
    rewrite -elements_empty'. intros ??. rewrite /big_opS /uPred_big_sepS.
    induction (elements X) as [|x [|x' l] IH];
      csimpl in *; rewrite ?right_id -?IH //.
603
604
  Qed.

605
606
607
608
609
610
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
  Proof. apply (big_sepS_commute _); auto using later_True, later_sep. Qed.

  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
  Proof. apply (big_sepS_commute _); auto using always_pure, always_sep. Qed.

611
  Lemma big_sepS_always_if q Φ X :
612
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
613
  Proof. destruct q; simpl; auto using big_sepS_always. Qed.
614
615
616
617
618
619

  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.
620
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
621
622
623
    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.
624
    - rewrite (forall_elim x) pure_equiv; last by left. by rewrite True_impl.
625
    - rewrite -IH. apply forall_mono=> y.
626
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
627
628
629
630
      by rewrite True_impl.
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
631
       ( x,  (x  X)  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
632
633
  Proof.
    rewrite always_and_sep_l always_forall.
634
    setoid_rewrite always_impl; setoid_rewrite always_pure.
635
636
637
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
638

Robbert Krebbers's avatar
Robbert Krebbers committed
639
640
  Global Instance big_sepS_empty_persistent Φ : PersistentP ([ set] x  , Φ x).
  Proof. rewrite /uPred_big_sepS elements_empty. apply _. Qed.
641
642
643
  Global Instance big_sepS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
  Proof. rewrite /uPred_big_sepS. apply _. Qed.
644

Robbert Krebbers's avatar
Robbert Krebbers committed
645
646
  Global Instance big_sepS_nil_timeless Φ : TimelessP ([ set] x  , Φ x).
  Proof. rewrite /uPred_big_sepS elements_empty. apply _. Qed.
647
648
649
650
  Global Instance big_sepS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
  Proof. rewrite /uPred_big_sepS. apply _. Qed.
End gset.
651
End big_op.