upred_big_op.v 14.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
9
10
11
12
13
14
15
(** 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.
- 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 [∃]. *)

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

27
28
(** * Other big ops *)
(** We use a type class to obtain overloaded notations *)
29
Definition uPred_big_sepM {M} `{Countable K} {A}
30
    (m : gmap K A) (Φ : K  A  uPred M) : uPred M :=
31
  [] (curry Φ <$> map_to_list m).
32
Instance: Params (@uPred_big_sepM) 6.
33
34
35
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.
36

37
Definition uPred_big_sepS {M} `{Countable A}
38
  (X : gset A) (Φ : A  uPred M) : uPred M := [] (Φ <$> elements X).
39
Instance: Params (@uPred_big_sepS) 5.
40
41
42
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.
43

44
(** * Persistence of lists of uPreds *)
45
Class PersistentL {M} (Ps : list (uPred M)) :=
46
  persistentL : Forall PersistentP Ps.
47
Arguments persistentL {_} _ {_}.
48

49
(** * Properties *)
50
Section big_op.
51
Context {M : ucmraT}.
52
53
54
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

55
(** ** Big ops over lists *)
56
Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M).
57
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
58
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
59
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
60

61
Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
62
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
63
Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
64
65
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

66
Global Instance big_and_mono' : Proper (Forall2 () ==> ()) (@uPred_big_and M).
67
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
68
Global Instance big_sep_mono' : Proper (Forall2 () ==> ()) (@uPred_big_sep M).
69
70
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

71
Global Instance big_and_perm : Proper (() ==> ()) (@uPred_big_and M).
72
73
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
74
75
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
76
  - etrans; eauto.
77
Qed.
78
Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M).
79
80
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
81
82
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
83
  - etrans; eauto.
84
Qed.
85

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

91
Lemma big_and_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
92
Proof.
93
  intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
94
Qed.
95
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  [] Ps  [] Qs.
96
Proof.
97
  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
98
99
Qed.

100
Lemma big_sep_and Ps : [] Ps  [] Ps.
101
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
102

103
Lemma big_and_elem_of Ps P : P  Ps  [] Ps  P.
104
Proof. induction 1; simpl; auto with I. Qed.
105
Lemma big_sep_elem_of Ps P : P  Ps  [] Ps  P.
106
107
Proof. induction 1; simpl; auto with I. Qed.

108
(** ** Big ops over finite maps *)
109
110
111
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
112
  Implicit Types Φ Ψ : K  A  uPred M.
113

114
  Lemma big_sepM_mono Φ Ψ m1 m2 :
115
    m2  m1  ( k x, m2 !! k = Some x  Φ k x  Ψ k x) 
116
    ([ map] k  x  m1, Φ k x)  ([ map] k  x  m2, Ψ k x).
117
  Proof.
118
    intros HX HΦ. trans ([ map] kx  m2, Φ k x)%I.
119
    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
120
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
121
      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
122
  Qed.
123
  Lemma big_sepM_proper Φ Ψ m1 m2 :
124
    m1  m2  ( k x, m1 !! k = Some x  m2 !! k = Some x  Φ k x  Ψ k x) 
125
    ([ map] k  x  m1, Φ k x)  ([ map] k  x  m2, Ψ k x).
126
  Proof.
127
128
129
    (* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives
    File "./algebra/upred_big_op.v", line 114, characters 4-131:
    Anomaly: Uncaught exception Univ.AlreadyDeclared. Please report. *)
130
    intros [??] ?; apply (anti_symm ()); apply big_sepM_mono;
131
      eauto using equiv_entails, equiv_entails_sym, @lookup_weaken.
132
  Qed.
133
134
135
136
137

  Global Instance big_sepM_ne m n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (uPred_big_sepM (M:=M) m).
  Proof.
138
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
139
    apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ.
140
  Qed.
141
  Global Instance big_sepM_proper' m :
142
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
143
           (uPred_big_sepM (M:=M) m).
144
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
145
  Global Instance big_sepM_mono' m :
146
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
147
           (uPred_big_sepM (M:=M) m).
148
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
149

150
  Lemma big_sepM_empty Φ : ([ map] kx  , Φ k x)  True.
151
  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
152

153
  Lemma big_sepM_insert Φ (m : gmap K A) i x :
154
155
    m !! i = None 
    ([ map] ky  <[i:=x]> m, Φ k y)  (Φ i x  [ map] ky  m, Φ k y).
156
  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
157

Robbert Krebbers's avatar
Robbert Krebbers committed
158
  Lemma big_sepM_delete Φ (m : gmap K A) i x :
159
160
    m !! i = Some x 
    ([ map] ky  m, Φ k y)  (Φ i x  [ map] ky  delete i m, Φ k y).
161
162
163
164
  Proof.
    intros. rewrite -big_sepM_insert ?lookup_delete //.
    by rewrite insert_delete insert_id.
  Qed.
165

166
  Lemma big_sepM_singleton Φ i x : ([ map] ky  {[i:=x]}, Φ k y)  Φ i x.
167
168
169
170
  Proof.
    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
    by rewrite big_sepM_empty right_id.
  Qed.
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
  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.

  Lemma big_sepM_insert_override (Φ : K  uPred M) (m : gmap K A) i x :
    m !! i = Some x 
    ([ map] k_  <[i:=x]> m, Φ k)  ([ map] k_  m, Φ k).
  Proof.
    intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
    by rewrite -big_sepM_delete.
  Qed.

  Lemma big_sepM_fn_insert (Ψ : K  A  uPred M  uPred M) (Φ : K  uPred M) m i x P :
    m !! i = None 
       ([ map] ky  <[i:=x]> m, Ψ k y (<[i:=P]> Φ k))
     (Ψ i x P  [ map] ky  m, Ψ k y (Φ k)).
  Proof.
    intros. rewrite big_sepM_insert // fn_lookup_insert.
    apply sep_proper, big_sepM_proper; auto=> k y ??.
    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.

201
  Lemma big_sepM_sepM Φ Ψ m :
202
203
       ([ map] kx  m, Φ k x  Ψ k x)
     (([ map] kx  m, Φ k x)  ([ map] kx  m, Ψ k x)).
204
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
205
206
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
207
    by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _  _)%I]comm -!assoc.
208
  Qed.
209

210
211
  Lemma big_sepM_later Φ m :
    ( [ map] kx  m, Φ k x)  ([ map] kx  m,  Φ k x).
212
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
215
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
    by rewrite later_sep IH.
216
  Qed.
217
218
219
220
221
222
223
224
225
226
227
228

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

  Lemma big_sepM_always_if p Φ m :
    (?p [ map] kx  m, Φ k x)  ([ map] kx  m, ?p Φ k x).
  Proof. destruct p; simpl; auto using big_sepM_always. Qed.
229
230
End gmap.

231
(** ** Big ops over finite sets *)
232
233
234
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
235
  Implicit Types Φ : A  uPred M.
236

237
  Lemma big_sepS_mono Φ Ψ X Y :
238
239
    Y  X  ( x, x  Y  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  ([ set] x  Y, Ψ x).
240
  Proof.
241
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
242
    - by apply big_sep_contains, fmap_contains, elements_contains.
243
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
244
      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
245
  Qed.
246
  Lemma big_sepS_proper Φ Ψ X Y :
247
248
    X  Y  ( x, x  X  x  Y  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  ([ set] x  Y, Ψ x).
249
250
251
252
  Proof.
    intros [??] ?; apply (anti_symm ()); apply big_sepS_mono;
      eauto using equiv_entails, equiv_entails_sym.
  Qed.
253
254
255
256

  Lemma big_sepS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
  Proof.
257
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
258
    apply Forall_Forall2, Forall_true=> x; apply HΦ.
259
  Qed.
260
  Lemma big_sepS_proper' X :
261
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
262
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
263
  Lemma big_sepS_mono' X :
264
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
265
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
266

267
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x)  True.
268
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
269

270
  Lemma big_sepS_insert Φ X x :
271
    x  X  ([ set] y  {[ x ]}  X, Φ y)  (Φ x  [ set] y  X, Φ y).
272
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
273
  Lemma big_sepS_fn_insert (Ψ : A  uPred M  uPred M) Φ X x P :
274
    x  X 
275
276
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=P]> Φ y))
     (Ψ x P  [ set] y  X, Ψ y (Φ y)).
277
278
279
280
281
  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.
282
  Lemma big_sepS_fn_insert' Φ X x P :
283
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y)  (P  [ set] y  X, Φ y).
284
  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
285

286
  Lemma big_sepS_delete Φ X x :
287
    x  X  ([ set] y  X, Φ y)  (Φ x  [ set] y  X  {[ x ]}, Φ y).
288
  Proof.
289
290
    intros. rewrite -big_sepS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
291
  Qed.
292

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

296
  Lemma big_sepS_sepS Φ Ψ X :
297
    ([ set] y  X, Φ y  Ψ y)  (([ set] y  X, Φ y)  [ set] y  X, Ψ y).
298
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
300
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
301
    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _  _)%I]comm -!assoc.
302
303
  Qed.

304
  Lemma big_sepS_later Φ X : ( [ set] y  X, Φ y)  ([ set] y  X,  Φ y).
305
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
306
307
308
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
    by rewrite later_sep IH.
309
  Qed.
310
311
312
313
314
315
316
317
318
319
320

  Lemma big_sepS_always Φ X : ( [ set] y  X, Φ y)  ([ set] y  X,  Φ y).
  Proof.
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_const.
    by rewrite always_sep IH.
  Qed.

  Lemma big_sepS_always_if q Φ X :
    (?q [ set] y  X, Φ y)  ([ set] y  X, ?q Φ y).
  Proof. destruct q; simpl; auto using big_sepS_always. Qed.
321
End gset.
322

323
(** ** Persistence *)
324
Global Instance big_and_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
325
Proof. induction 1; apply _. Qed.
326
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
327
328
Proof. induction 1; apply _. Qed.

329
Global Instance nil_persistent : PersistentL (@nil (uPred M)).
330
Proof. constructor. Qed.
331
Global Instance cons_persistent P Ps :
332
  PersistentP P  PersistentL Ps  PersistentL (P :: Ps).
333
Proof. by constructor. Qed.
334
335
Global Instance app_persistent Ps Ps' :
  PersistentL Ps  PersistentL Ps'  PersistentL (Ps ++ Ps').
336
Proof. apply Forall_app_2. Qed.
337
Global Instance zip_with_persistent {A B} (f : A  B  uPred M) xs ys :
338
  ( x y, PersistentP (f x y))  PersistentL (zip_with f xs ys).
339
340
341
Proof.
  unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
342
End big_op.