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

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

- The operators [ [] Ps ] and [ [] Ps ] fold [] and [] over the list [Ps].
  This operator is not a quantifier, so it binds strongly.
9
10
11
- The operator [ [ list] k  x  l, P ] asserts that [P] holds separately for
  each element [x] at position [x] in the list [l]. This operator is a
  quantifier, and thus has the same precedence as [] and [].
12
13
14
15
16
17
18
- The operator [ [ map] k  x  m, P ] asserts that [P] holds separately for
  each [k  x] in the map [m]. This operator is a quantifier, and thus has the
  same precedence as [] and [].
- The operator [ [ set] x  X, P ] asserts that [P] holds separately for each
  [x] in the set [X]. This operator is a quantifier, and thus has the same
  precedence as [] and []. *)

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

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

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

51
Definition uPred_big_sepS {M} `{Countable A}
52
  (X : gset A) (Φ : A  uPred M) : uPred M := [] (Φ <$> elements X).
53
Instance: Params (@uPred_big_sepS) 5.
54
Typeclasses Opaque uPred_big_sepS.
55
56
57
Notation "'[★' 'set' ] x ∈ X , P" := (uPred_big_sepS X (λ x, P))
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[★  set ]  x  ∈  X ,  P") : uPred_scope.
58

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

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

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

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

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

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

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

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

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

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

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

127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
(** ** Persistence *)
Global Instance big_and_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
Proof. induction 1; apply _. Qed.
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
Proof. induction 1; apply _. Qed.

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

Global Instance fmap_persistent {A} (f : A  uPred M) xs :
  ( x, PersistentP (f x))  PersistentL (f <$> xs).
144
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
145
146
147
148
149
Global Instance zip_with_persistent {A B} (f : A  B  uPred M) xs ys :
  ( x y, PersistentP (f x y))  PersistentL (zip_with f xs ys).
Proof.
  unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
150
151
152
153
154
Global Instance imap_persistent {A} (f : nat  A  uPred M) xs :
  ( i x, PersistentP (f i x))  PersistentL (imap f xs).
Proof.
  rewrite /PersistentL /imap=> ?. generalize 0. induction xs; constructor; auto.
Qed.
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172

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

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

Global Instance fmap_timeless {A} (f : A  uPred M) xs :
  ( x, TimelessP (f x))  TimelessL (f <$> xs).
173
Proof. intros. apply Forall_fmap, Forall_forall; auto. Qed.
174
175
176
177
178
Global Instance zip_with_timeless {A B} (f : A  B  uPred M) xs ys :
  ( x y, TimelessP (f x y))  TimelessL (zip_with f xs ys).
Proof.
  unfold TimelessL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
Global Instance imap_timeless {A} (f : nat  A  uPred M) xs :
  ( i x, TimelessP (f i x))  TimelessL (imap f xs).
Proof.
  rewrite /TimelessL /imap=> ?. generalize 0. induction xs; constructor; auto.
Qed.

(** ** Big ops over lists *)
Section list.
  Context {A : Type}.
  Implicit Types l : list A.
  Implicit Types Φ Ψ : nat  A  uPred M.

  Lemma big_sepL_mono Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y  Ψ k y) 
    ([ list] k  y  l, Φ k y)  [ list] k  y  l, Ψ k y.
  Proof.
    intros HΦ. apply big_sep_mono'.
    revert Φ Ψ HΦ. induction l as [|x l IH]=> Φ Ψ HΦ; first constructor.
    rewrite !imap_cons; constructor; eauto.
  Qed.
  Lemma big_sepL_proper Φ Ψ l :
    ( k y, l !! k = Some y  Φ k y ⊣⊢ Ψ k y) 
    ([ list] k  y  l, Φ k y) ⊣⊢ ([ list] k  y  l, Ψ k y).
  Proof.
    intros ?; apply (anti_symm ()); apply big_sepL_mono;
      eauto using equiv_entails, equiv_entails_sym, lookup_weaken.
  Qed.

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

  Lemma big_sepL_nil Φ : ([ list] ky  nil, Φ k y) ⊣⊢ True.
  Proof. done. Qed.

  Lemma big_sepL_cons Φ x l :
    ([ list] ky  x :: l, Φ k y) ⊣⊢ Φ 0 x  [ list] ky  l, Φ (S k) y.
  Proof. by rewrite /uPred_big_sepL imap_cons. Qed.

  Lemma big_sepL_singleton Φ x : ([ list] ky  [x], Φ k y) ⊣⊢ Φ 0 x.
  Proof. by rewrite big_sepL_cons big_sepL_nil right_id. Qed.

  Lemma big_sepL_app Φ l1 l2 :
    ([ list] ky  l1 ++ l2, Φ k y)
    ⊣⊢ ([ list] ky  l1, Φ k y)  ([ list] ky  l2, Φ (length l1 + k) y).
  Proof. by rewrite /uPred_big_sepL imap_app big_sep_app. Qed.

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

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

253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
  Lemma big_sepL_fmap {B} (f : A  B) (Φ : nat  B  uPred M) l :
    ([ list] ky  f <$> l, Φ k y) ⊣⊢ ([ list] ky  l, Φ k (f y)).
  Proof. by rewrite /uPred_big_sepL imap_fmap. Qed.

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

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

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

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

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

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

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

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

326

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

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

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

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

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

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

382
383
384
385
  Lemma big_sepM_lookup Φ m i x :
    m !! i = Some x  ([ map] ky  m, Φ k y)  Φ i x.
  Proof. intros. by rewrite big_sepM_delete // sep_elim_l. Qed.

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

392
393
394
395
396
397
398
  Lemma big_sepM_fmap {B} (f : A  B) (Φ : K  B  uPred M) m :
    ([ map] ky  f <$> m, Φ k y) ⊣⊢ ([ map] ky  m, Φ k (f y)).
  Proof.
    rewrite /uPred_big_sepM map_to_list_fmap -list_fmap_compose.
    f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
  Qed.

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

407
  Lemma big_sepM_fn_insert {B} (Ψ : K  A  B  uPred M) (f : K  B) m i x b :
408
    m !! i = None 
409
410
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=b]> f k))
    ⊣⊢ (Ψ i x b  [ map] ky  m, Ψ k y (f k)).
411
412
  Proof.
    intros. rewrite big_sepM_insert // fn_lookup_insert.
413
    apply sep_proper, big_sepM_proper; auto=> k y ?.
414
415
416
417
418
419
420
    by rewrite fn_lookup_insert_ne; last set_solver.
  Qed.
  Lemma big_sepM_fn_insert' (Φ : K  uPred M) m i x P :
    m !! i = None 
    ([ map] ky  <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P  [ map] ky  m, Φ k).
  Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.

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

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

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

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

  Lemma big_sepM_forall Φ m :
    ( k x, PersistentP (Φ k x)) 
    ([ map] kx  m, Φ k x) ⊣⊢ ( k x, m !! k = Some x  Φ k x).
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> k; apply forall_intro=> x.
456
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
457
458
459
    rewrite /uPred_big_sepM. setoid_rewrite <-elem_of_map_to_list.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; auto.
    rewrite -always_and_sep_l; apply and_intro.
460
    - rewrite (forall_elim i) (forall_elim x) pure_equiv; last by left.
461
462
      by rewrite True_impl.
    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
463
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
464
465
466
467
      by rewrite True_impl.
  Qed.

  Lemma big_sepM_impl Φ Ψ m :
468
     ( k x, m !! k = Some x  Φ k x  Ψ k x)  ([ map] kx  m, Φ k x)
469
470
471
     [ map] kx  m, Ψ k x.
  Proof.
    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
472
    setoid_rewrite always_impl; setoid_rewrite always_pure.
473
474
475
    rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
    by rewrite -always_wand_impl always_elim wand_elim_l.
  Qed.
476

Robbert Krebbers's avatar
Robbert Krebbers committed
477
478
479
  Global Instance big_sepM_empty_persistent Φ :
    PersistentP ([ map] kx  , Φ k x).
  Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
480
481
482
483
  Global Instance big_sepM_persistent Φ m :
    ( k x, PersistentP (Φ k x))  PersistentP ([ map] kx  m, Φ k x).
  Proof. intros. apply big_sep_persistent, fmap_persistent=>-[??] /=; auto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
484
485
486
  Global Instance big_sepM_nil_timeless Φ :
    TimelessP ([ map] kx  , Φ k x).
  Proof. rewrite /uPred_big_sepM map_to_list_empty. apply _. Qed.
487
488
489
  Global Instance big_sepM_timeless Φ m :
    ( k x, TimelessP (Φ k x))  TimelessP ([ map] kx  m, Φ k x).
  Proof. intro. apply big_sep_timeless, fmap_timeless=> -[??] /=; auto. Qed.
490
491
End gmap.

492

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

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

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

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

532
  Lemma big_sepS_insert Φ X x :
533
    x  X  ([ set] y  {[ x ]}  X, Φ y) ⊣⊢ (Φ x  [ set] y  X, Φ y).
534
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
535
  Lemma big_sepS_fn_insert {B} (Ψ : A  B  uPred M) f X x b :
536
    x  X 
537
538
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=b]> f y))
    ⊣⊢ (Ψ x b  [ set] y  X, Ψ y (f y)).
539
540
541
542
543
  Proof.
    intros. rewrite big_sepS_insert // fn_lookup_insert.
    apply sep_proper, big_sepS_proper; auto=> y ??.
    by rewrite fn_lookup_insert_ne; last set_solver.
  Qed.
544
  Lemma big_sepS_fn_insert' Φ X x P :
545
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y) ⊣⊢ (P  [ set] y  X, Φ y).
546
  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
547

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

555
556
557
  Lemma big_sepS_elem_of Φ X x : x  X  ([ set] y  X, Φ y)  Φ x.
  Proof. intros. by rewrite big_sepS_delete // sep_elim_l. Qed.

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

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

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

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

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

  Lemma big_sepS_forall Φ X :
    ( x, PersistentP (Φ x))  ([ set] x  X, Φ x) ⊣⊢ ( x,  (x  X)  Φ x).
  Proof.
    intros. apply (anti_symm _).
    { apply forall_intro=> x.
592
      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
593
594
595
    rewrite /uPred_big_sepS. setoid_rewrite <-elem_of_elements.
    induction (elements X) as [|x l IH]; csimpl; auto.
    rewrite -always_and_sep_l; apply and_intro.
596
    - rewrite (forall_elim x) pure_equiv; last by left. by rewrite True_impl.
597
    - rewrite -IH. apply forall_mono=> y.
598
      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
599
600
601
602
      by rewrite True_impl.
  Qed.

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

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

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