upred_big_op.v 25 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
247
248
249
250
251
252
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
311
312
313
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.

  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.

  Global Instance big_sepL_persistent Φ m :
    ( k x, PersistentP (Φ k x))  PersistentP ([ list] kx  m, Φ k x).
  Proof. rewrite /uPred_big_sepL. apply _. Qed.

  Global Instance big_sepL_timeless Φ m :
    ( k x, TimelessP (Φ k x))  TimelessP ([ list] kx  m, Φ k x).
  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
  Lemma big_sepM_later Φ m :
419
     ([ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
420
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
421
422
423
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
    by rewrite later_sep IH.
424
  Qed.
425
426
427
428
429

  Lemma big_sepM_always Φ m :
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
  Proof.
    rewrite /uPred_big_sepM.
430
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?always_pure //.
431
432
433
434
    by rewrite always_sep IH.
  Qed.

  Lemma big_sepM_always_if p Φ m :
435
    ?p ([ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
436
  Proof. destruct p; simpl; auto using big_sepM_always. Qed.
437
438
439
440
441
442
443

  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.
444
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
445
446
447
    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.
448
    - rewrite (forall_elim i) (forall_elim x) pure_equiv; last by left.
449
450
      by rewrite True_impl.
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
451
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
452
453
454
455
      by rewrite True_impl.
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
456
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
457
458
459
     [ map] kx  m, Ψ k x.
  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
465
466
467
468
469
470
471

  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.

  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.
472
473
End gmap.

474

475
(** ** Big ops over finite sets *)
476
477
478
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
479
  Implicit Types Φ : A  uPred M.
480

481
  Lemma big_sepS_mono Φ Ψ X Y :
482
    Y  X  ( x, x  Y  Φ x  Ψ x) 
483
    ([ set] x  X, Φ x)  [ set] x  Y, Ψ x.
484
  Proof.
485
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
486
    - by apply big_sep_contains, fmap_contains, elements_contains.
487
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
488
      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
489
  Qed.
490
  Lemma big_sepS_proper Φ Ψ X Y :
491
492
    X  Y  ( x, x  X  x  Y  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  ([ set] x  Y, Ψ x).
493
  Proof.
494
495
    move=> /collection_equiv_spec [??] ?; apply (anti_symm ());
      apply big_sepS_mono; eauto using equiv_entails, equiv_entails_sym.
496
  Qed.
497
498
499
500

  Lemma big_sepS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
  Proof.
501
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
502
    apply Forall_Forall2, Forall_true=> x; apply HΦ.
503
  Qed.
504
  Lemma big_sepS_proper' X :
505
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
506
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
507
  Lemma big_sepS_mono' X :
508
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
509
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
510

511
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
512
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
513

514
  Lemma big_sepS_insert Φ X x :
515
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
516
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
517
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
518
    x  X 
519
520
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
     (Ψ x b  [ set] y  X, Ψ y (f y)).
521
522
523
524
525
  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.
526
  Lemma big_sepS_fn_insert' Φ X x P :
527
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
528
  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
529

530
  Lemma big_sepS_delete Φ X x :
531
    x  X  ([ set] y  X, Φ y)  Φ x  [ set] y  X  {[ x ]}, Φ y.
532
  Proof.
533
534
    intros. rewrite -big_sepS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
535
  Qed.
536

537
538
539
  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.

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

543
  Lemma big_sepS_sepS Φ Ψ X :
544
    ([ set] y  X, Φ y  Ψ y)  ([ set] y  X, Φ y)  ([ set] y  X, Ψ y).
545
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
546
547
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
548
    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _  _)%I]comm -!assoc.
549
550
  Qed.

551
  Lemma big_sepS_later Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
552
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
553
554
555
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
    by rewrite later_sep IH.
556
  Qed.
557

558
  Lemma big_sepS_always Φ X :  ([ set] y  X, Φ y)  ([ set] y  X,  Φ y).
559
560
  Proof.
    rewrite /uPred_big_sepS.
561
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_pure.
562
563
564
565
    by rewrite always_sep IH.
  Qed.

  Lemma big_sepS_always_if q Φ X :
566
    ?q ([ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
567
  Proof. destruct q; simpl; auto using big_sepS_always. Qed.
568
569
570
571
572
573

  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.
574
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
575
576
577
    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.
578
    - rewrite (forall_elim x) pure_equiv; last by left. by rewrite True_impl.
579
    - rewrite -IH. apply forall_mono=> y.
580
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
581
582
583
584
      by rewrite True_impl.
  Qed.

  Lemma big_sepS_impl Φ Ψ X :
585
       ( x,  (x  X)  Φ x  Ψ x)  ([ set] x  X, Φ x)  [ set] x  X, Ψ x.
586
587
  Proof.
    rewrite always_and_sep_l always_forall.
588
    setoid_rewrite always_impl; setoid_rewrite always_pure.
589
590
591
    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
592

593
594
595
  Global Instance big_sepS_persistent Φ X :
    ( x, PersistentP (Φ x))  PersistentP ([ set] x  X, Φ x).
  Proof. rewrite /uPred_big_sepS. apply _. Qed.
596

597
598
599
600
  Global Instance big_sepS_timeless Φ X :
    ( x, TimelessP (Φ x))  TimelessP ([ set] x  X, Φ x).
  Proof. rewrite /uPred_big_sepS. apply _. Qed.
End gset.
601
End big_op.