cmra_big_op.v 14.2 KB
Newer Older
1
From iris.algebra Require Export cmra list.
2
From iris.prelude Require Import functions gmap.
3

4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
(** The operator [ [⋅] Ps ] folds [⋅] over the list [Ps]. This operator is not a
quantifier, so it binds strongly.

Apart from that, we define the following big operators with binders build in:

- The operator [ [⋅ list] k ↦ x ∈ l, P ] folds over a list [l]. The binder [x]
  refers to each element at index [k].
- The operator [ [⋅ map] k ↦ x ∈ m, P ] folds over a map [m]. The binder [x]
  refers to each element at index [k].
- The operator [ [⋅ set] x ∈ X, P ] folds over a set [m]. The binder [x] refers
  to each element.

Since these big operators are like quantifiers, they have the same precedence as
[∀] and [∃]. *)

(** * Big ops over lists *)
(* This is the basic building block for other big ops *)
Fixpoint big_op {M : ucmraT} (xs : list M) : M :=
22
  match xs with [] =>  | x :: xs => x  big_op xs end.
23
24
Arguments big_op _ !_ /.
Instance: Params (@big_op) 1.
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
Notation "'[⋅]' xs" := (big_op xs) (at level 20) : C_scope.

(** * Other big ops *)
Definition big_opL {M : ucmraT} {A} (l : list A) (f : nat  A  M) : M :=
  [] (imap f l).
Instance: Params (@big_opL) 2.
Typeclasses Opaque big_opL.
Notation "'[⋅' 'list' ] k ↦ x ∈ l , P" := (big_opL l (λ k x, P))
  (at level 200, l at level 10, k, x at level 1, right associativity,
   format "[⋅  list ]  k ↦ x  ∈  l ,  P") : C_scope.
Notation "'[⋅' 'list' ] x ∈ l , P" := (big_opL l (λ _ x, P))
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[⋅  list ]  x  ∈  l ,  P") : C_scope.

Definition big_opM {M : ucmraT} `{Countable K} {A}
    (m : gmap K A) (f : K  A  M) : M :=
  [] (curry f <$> map_to_list m).
Instance: Params (@big_opM) 6.
Typeclasses Opaque big_opM.
Notation "'[⋅' 'map' ] k ↦ x ∈ m , P" := (big_opM m (λ k x, P))
  (at level 200, m at level 10, k, x at level 1, right associativity,
   format "[⋅  map ]  k ↦ x  ∈  m ,  P") : C_scope.

Definition big_opS {M : ucmraT} `{Countable A}
  (X : gset A) (f : A  M) : M := [] (f <$> elements X).
Instance: Params (@big_opS) 5.
Typeclasses Opaque big_opS.
Notation "'[⋅' 'set' ] x ∈ X , P" := (big_opS X (λ x, P))
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[⋅  set ]  x  ∈  X ,  P") : C_scope.
55
56
57

(** * Properties about big ops *)
Section big_op.
58
59
Context {M : ucmraT}.
Implicit Types xs : list M.
60
61

(** * Big ops *)
62
63
64
65
66
Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op M).
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
Global Instance big_op_proper : Proper (() ==> ()) (@big_op M) := ne_proper _.

Lemma big_op_nil : [] (@nil M) = .
67
Proof. done. Qed.
68
Lemma big_op_cons x xs : [] (x :: xs) = x  [] xs.
69
Proof. done. Qed.
70
71
72
73
74
75
76
77
78
79
Lemma big_op_app xs ys : [] (xs ++ ys)  [] xs  [] ys.
Proof.
  induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
  by rewrite IH assoc.
Qed.

Lemma big_op_mono xs ys : Forall2 () xs ys  [] xs  [] ys.
Proof. induction 1 as [|x y xs ys Hxy ? IH]; simpl; eauto using cmra_mono. Qed.

Global Instance big_op_permutation : Proper (() ==> ()) (@big_op M).
80
81
Proof.
  induction 1 as [|x xs1 xs2 ? IH|x y xs|xs1 xs2 xs3]; simpl; auto.
82
83
  - by rewrite IH.
  - by rewrite !assoc (comm _ x).
84
  - by trans (big_op xs2).
85
Qed.
86
87

Lemma big_op_contains xs ys : xs `contains` ys  [] xs  [] ys.
88
Proof.
89
90
  intros [xs' ->]%contains_Permutation.
  rewrite big_op_app; apply cmra_included_l.
91
Qed.
92
93

Lemma big_op_delete xs i x : xs !! i = Some x  x  [] delete i xs  [] xs.
94
95
Proof. by intros; rewrite {2}(delete_Permutation xs i x). Qed.

96
Lemma big_sep_elem_of xs x : x  xs  x  [] xs.
97
Proof.
98
99
  intros [i ?]%elem_of_list_lookup. rewrite -big_op_delete //.
  apply cmra_included_l.
100
Qed.
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
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
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
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369

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

  Lemma big_opL_mono f g l :
    ( k y, l !! k = Some y  f k y  g k y) 
    ([ list] k  y  l, f k y)  [ list] k  y  l, g k y.
  Proof.
    intros Hf. apply big_op_mono.
    revert f g Hf. induction l as [|x l IH]=> f g Hf; first constructor.
    rewrite !imap_cons; constructor; eauto.
  Qed.
  Lemma big_opL_proper f g l :
    ( k y, l !! k = Some y  f k y  g k y) 
    ([ list] k  y  l, f k y)  ([ list] k  y  l, g k y).
  Proof.
    intros Hf; apply big_op_proper.
    revert f g Hf. induction l as [|x l IH]=> f g Hf; first constructor.
    rewrite !imap_cons; constructor; eauto.
  Qed.

  Global Instance big_opL_ne l n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (big_opL (M:=M) l).
  Proof.
    intros f g Hf. apply big_op_ne.
    revert f g Hf. induction l as [|x l IH]=> f g Hf; first constructor.
    rewrite !imap_cons; constructor. by apply Hf. apply IH=> n'; apply Hf.
  Qed.
  Global Instance big_opL_proper' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
           (big_opL (M:=M) l).
  Proof. intros f1 f2 Hf. by apply big_opL_proper; intros; last apply Hf. Qed.
  Global Instance big_opL_mono' l :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
           (big_opL (M:=M) l).
  Proof. intros f1 f2 Hf. by apply big_opL_mono; intros; last apply Hf. Qed.

  Lemma big_opL_nil f : ([ list] ky  nil, f k y) = .
  Proof. done. Qed.

  Lemma big_opL_cons f x l :
    ([ list] ky  x :: l, f k y) = f 0 x  [ list] ky  l, f (S k) y.
  Proof. by rewrite /big_opL imap_cons. Qed.

  Lemma big_opL_singleton f x : ([ list] ky  [x], f k y)  f 0 x.
  Proof. by rewrite big_opL_cons big_opL_nil right_id. Qed.

  Lemma big_opL_app f l1 l2 :
    ([ list] ky  l1 ++ l2, f k y)
     ([ list] ky  l1, f k y)  ([ list] ky  l2, f (length l1 + k) y).
  Proof. by rewrite /big_opL imap_app big_op_app. Qed.

  Lemma big_opL_lookup f l i x :
    l !! i = Some x  f i x  [ list] ky  l, f k y.
  Proof.
    intros. rewrite -(take_drop_middle l i x) // big_opL_app big_opL_cons.
    rewrite Nat.add_0_r take_length_le; eauto using lookup_lt_Some, Nat.lt_le_incl.
    eapply transitivity, cmra_included_r; eauto using cmra_included_l.
  Qed.

  Lemma big_opL_elem_of (f : A  M) l x : x  l  f x  [ list] y  l, f y.
  Proof.
    intros [i ?]%elem_of_list_lookup; eauto using (big_opL_lookup (λ _, f)).
  Qed.

  Lemma big_opL_fmap {B} (h : A  B) (f : nat  B  M) l :
    ([ list] ky  h <$> l, f k y)  ([ list] ky  l, f k (h y)).
  Proof. by rewrite /big_opL imap_fmap. Qed.

  Lemma big_opL_opL f g l :
    ([ list] kx  l, f k x  g k x)
     ([ list] kx  l, f k x)  ([ list] kx  l, g k x).
  Proof.
    revert f g; induction l as [|x l IH]=> f g.
    { by rewrite !big_opL_nil left_id. }
    rewrite !big_opL_cons IH.
    by rewrite -!assoc (assoc _ (g _ _)) [(g _ _  _)]comm -!assoc.
  Qed.
End list.


(** ** Big ops over finite maps *)
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
  Implicit Types f g : K  A  M.

  Lemma big_opM_mono f g m1 m2 :
    m1  m2  ( k x, m2 !! k = Some x  f k x  g k x) 
    ([ map] k  x  m1, f k x)  [ map] k  x  m2, g k x.
  Proof.
    intros HX Hf. trans ([ map] kx  m2, f k x).
    - by apply big_op_contains, fmap_contains, map_to_list_contains.
    - apply big_op_mono, Forall2_fmap, Forall_Forall2.
      apply Forall_forall=> -[i x] ? /=. by apply Hf, elem_of_map_to_list.
  Qed.
  Lemma big_opM_proper f g m :
    ( k x, m !! k = Some x  f k x  g k x) 
    ([ map] k  x  m, f k x)  ([ map] k  x  m, g k x).
  Proof.
    intros Hf. apply big_op_proper, equiv_Forall2, Forall2_fmap, Forall_Forall2.
    apply Forall_forall=> -[i x] ? /=. by apply Hf, elem_of_map_to_list.
  Qed.

  Global Instance big_opM_ne m n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (big_opM (M:=M) m).
  Proof.
    intros f1 f2 Hf. apply big_op_ne, Forall2_fmap.
    apply Forall_Forall2, Forall_true=> -[i x]; apply Hf.
  Qed.
  Global Instance big_opM_proper' m :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
           (big_opM (M:=M) m).
  Proof. intros f1 f2 Hf. by apply big_opM_proper; intros; last apply Hf. Qed.
  Global Instance big_opM_mono' m :
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
           (big_opM (M:=M) m).
  Proof. intros f1 f2 Hf. by apply big_opM_mono; intros; last apply Hf. Qed.

  Lemma big_opM_empty f : ([ map] kx  , f k x) = .
  Proof. by rewrite /big_opM map_to_list_empty. Qed.

  Lemma big_opM_insert f m i x :
    m !! i = None 
    ([ map] ky  <[i:=x]> m, f k y)  f i x  [ map] ky  m, f k y.
  Proof. intros ?. by rewrite /big_opM map_to_list_insert. Qed.

  Lemma big_opM_delete f m i x :
    m !! i = Some x 
    ([ map] ky  m, f k y)  f i x  [ map] ky  delete i m, f k y.
  Proof.
    intros. rewrite -big_opM_insert ?lookup_delete //.
    by rewrite insert_delete insert_id.
  Qed.

  Lemma big_opM_lookup f m i x :
    m !! i = Some x  f i x  [ map] ky  m, f k y.
  Proof. intros. rewrite big_opM_delete //. apply cmra_included_l. Qed.

  Lemma big_opM_singleton f i x : ([ map] ky  {[i:=x]}, f k y)  f i x.
  Proof.
    rewrite -insert_empty big_opM_insert/=; last auto using lookup_empty.
    by rewrite big_opM_empty right_id.
  Qed.

  Lemma big_opM_fmap {B} (h : A  B) (f : K  B  M) m :
    ([ map] ky  h <$> m, f k y)  ([ map] ky  m, f k (h y)).
  Proof.
    rewrite /big_opM map_to_list_fmap -list_fmap_compose.
    f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
  Qed.

  Lemma big_opM_insert_override (f : K  M) m i x y :
    m !! i = Some x 
    ([ map] k_  <[i:=y]> m, f k)  ([ map] k_  m, f k).
  Proof.
    intros. rewrite -insert_delete big_opM_insert ?lookup_delete //.
    by rewrite -big_opM_delete.
  Qed.

  Lemma big_opM_fn_insert {B} (g : K  A  B  M) (f : K  B) m i (x : A) b :
    m !! i = None 
      ([ map] ky  <[i:=x]> m, g k y (<[i:=b]> f k))
     (g i x b  [ map] ky  m, g k y (f k)).
  Proof.
    intros. rewrite big_opM_insert // fn_lookup_insert.
    apply cmra_op_proper', big_opM_proper; auto=> k y ?.
    by rewrite fn_lookup_insert_ne; last set_solver.
  Qed.
  Lemma big_opM_fn_insert' (f : K  M) m i x P :
    m !! i = None 
    ([ map] ky  <[i:=x]> m, <[i:=P]> f k)  (P  [ map] ky  m, f k).
  Proof. apply (big_opM_fn_insert (λ _ _, id)). Qed.

  Lemma big_opM_opM f g m :
       ([ map] kx  m, f k x  g k x)
     ([ map] kx  m, f k x)  ([ map] kx  m, g k x).
  Proof.
    rewrite /big_opM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
    by rewrite IH -!assoc (assoc _ (g _ _)) [(g _ _  _)]comm -!assoc.
  Qed.
End gmap.


(** ** Big ops over finite sets *)
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
  Implicit Types f : A  M.

  Lemma big_opS_mono f g X Y :
    X  Y  ( x, x  Y  f x  g x) 
    ([ set] x  X, f x)  [ set] x  Y, g x.
  Proof.
    intros HX Hf. trans ([ set] x  Y, f x).
    - by apply big_op_contains, fmap_contains, elements_contains.
    - apply big_op_mono, Forall2_fmap, Forall_Forall2.
      apply Forall_forall=> x ? /=. by apply Hf, elem_of_elements.
  Qed.
  Lemma big_opS_proper f g X Y :
    X  Y  ( x, x  X  x  Y  f x  g x) 
    ([ set] x  X, f x)  ([ set] x  Y, g x).
  Proof.
    intros HX Hf. trans ([ set] x  Y, f x).
    - apply big_op_permutation. by rewrite HX.
    - apply big_op_proper, equiv_Forall2, Forall2_fmap, Forall_Forall2.
      apply Forall_forall=> x ? /=.
      apply Hf; first rewrite HX; by apply elem_of_elements.
  Qed.

  Lemma big_opS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (big_opS (M:=M) X).
  Proof.
    intros f1 f2 Hf. apply big_op_ne, Forall2_fmap.
    apply Forall_Forall2, Forall_true=> x; apply Hf.
  Qed.
  Lemma big_opS_proper' X :
    Proper (pointwise_relation _ () ==> ()) (big_opS (M:=M) X).
  Proof. intros f1 f2 Hf. apply big_opS_proper; naive_solver. Qed.
  Lemma big_opS_mono' X :
    Proper (pointwise_relation _ () ==> ()) (big_opS (M:=M) X).
  Proof. intros f1 f2 Hf. apply big_opS_mono; naive_solver. Qed.

  Lemma big_opS_empty f : ([ set] x  , f x) = .
  Proof. by rewrite /big_opS elements_empty. Qed.

  Lemma big_opS_insert f X x :
    x  X  ([ set] y  {[ x ]}  X, f y)  (f x  [ set] y  X, f y).
  Proof. intros. by rewrite /big_opS elements_union_singleton. Qed.
  Lemma big_opS_fn_insert {B} (f : A  B  M) h X x b :
    x  X 
       ([ set] y  {[ x ]}  X, f y (<[x:=b]> h y))
     (f x b  [ set] y  X, f y (h y)).
  Proof.
    intros. rewrite big_opS_insert // fn_lookup_insert.
    apply cmra_op_proper', big_opS_proper; auto=> y ??.
    by rewrite fn_lookup_insert_ne; last set_solver.
  Qed.
  Lemma big_opS_fn_insert' f X x P :
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> f y)  (P  [ set] y  X, f y).
  Proof. apply (big_opS_fn_insert (λ y, id)). Qed.

  Lemma big_opS_delete f X x :
    x  X  ([ set] y  X, f y)  f x  [ set] y  X  {[ x ]}, f y.
  Proof.
    intros. rewrite -big_opS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
  Qed.

  Lemma big_opS_elem_of f X x : x  X  f x  [ set] y  X, f y.
  Proof. intros. rewrite big_opS_delete //. apply cmra_included_l. Qed.

  Lemma big_opS_singleton f x : ([ set] y  {[ x ]}, f y)  f x.
  Proof. intros. by rewrite /big_opS elements_singleton /= right_id. Qed.

  Lemma big_opS_opS f g X :
    ([ set] y  X, f y  g y)  ([ set] y  X, f y)  ([ set] y  X, g y).
  Proof.
    rewrite /big_opS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
    by rewrite IH -!assoc (assoc _ (g _)) [(g _  _)]comm -!assoc.
  Qed.
End gset.
370
End big_op.