upred_big_op.v 26.3 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
52
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.
53

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

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

67
68
69
70
Class TimelessL {M} (Ps : list (uPred M)) :=
  timelessL : Forall TimelessP Ps.
Arguments timelessL {_} _ {_}.

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

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

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

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

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

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

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

122
Lemma big_sep_and Ps : [] Ps  [] Ps.
123
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
124

125
Lemma big_and_elem_of Ps P : P  Ps  [] Ps  P.
126
Proof. induction 1; simpl; auto with I. Qed.
127
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
128
129
Proof. induction 1; simpl; auto with I. Qed.

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

(** ** 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).
176
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
177
178
179
180
181
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.
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
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
250
251
252
253
254
255
  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.

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
  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
314
315
316
317
318
  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).
319
320
  Proof. rewrite /uPred_big_sepL. apply _. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
321
322
323
324
325
  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).
326
327
328
  Proof. rewrite /uPred_big_sepL. apply _. Qed.
End list.

329

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

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

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

369
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
370
  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
371

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

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

385
386
387
388
  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.

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

395
396
397
398
399
400
401
  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.

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

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

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

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

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

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

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

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

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

495

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

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

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

532
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
533
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
534

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

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

558
559
560
  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.

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

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

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

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

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

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

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

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

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