upred_big_op.v 13.4 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
End gmap.

219
(** ** Big ops over finite sets *)
220
221
222
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
223
  Implicit Types Φ : A  uPred M.
224

225
  Lemma big_sepS_mono Φ Ψ X Y :
226
227
    Y  X  ( x, x  Y  Φ x  Ψ x) 
    ([ set] x  X, Φ x)  ([ set] x  Y, Ψ x).
228
  Proof.
229
    intros HX HΦ. trans ([ set] x  Y, Φ x)%I.
230
    - by apply big_sep_contains, fmap_contains, elements_contains.
231
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
232
      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
233
  Qed.
234
  Lemma big_sepS_proper Φ Ψ X Y :
235
236
    X  Y  ( x, x  X  x  Y  Φ x ⊣⊢ Ψ x) 
    ([ set] x  X, Φ x) ⊣⊢ ([ set] x  Y, Ψ x).
237
238
239
240
  Proof.
    intros [??] ?; apply (anti_symm ()); apply big_sepS_mono;
      eauto using equiv_entails, equiv_entails_sym.
  Qed.
241
242
243
244

  Lemma big_sepS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
  Proof.
245
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
246
    apply Forall_Forall2, Forall_true=> x; apply HΦ.
247
  Qed.
248
  Lemma big_sepS_proper' X :
249
    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (uPred_big_sepS (M:=M) X).
250
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
251
  Lemma big_sepS_mono' X :
252
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
253
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
254

255
  Lemma big_sepS_empty Φ : ([ set] x  , Φ x) ⊣⊢ True.
256
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
257

258
  Lemma big_sepS_insert Φ X x :
259
    x  X  ([ set] y  {[ x ]}  X, Φ y) ⊣⊢ (Φ x  [ set] y  X, Φ y).
260
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
261
  Lemma big_sepS_fn_insert (Ψ : A  uPred M  uPred M) Φ X x P :
262
    x  X 
263
264
       ([ set] y  {[ x ]}  X, Ψ y (<[x:=P]> Φ y))
    ⊣⊢ (Ψ x P  [ set] y  X, Ψ y (Φ y)).
265
266
267
268
269
  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.
270
  Lemma big_sepS_fn_insert' Φ X x P :
271
    x  X  ([ set] y  {[ x ]}  X, <[x:=P]> Φ y) ⊣⊢ (P  [ set] y  X, Φ y).
272
  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
273

274
  Lemma big_sepS_delete Φ X x :
275
    x  X  ([ set] y  X, Φ y) ⊣⊢ (Φ x  [ set] y  X  {[ x ]}, Φ y).
276
  Proof.
277
278
    intros. rewrite -big_sepS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
279
  Qed.
280

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

284
  Lemma big_sepS_sepS Φ Ψ X :
285
    ([ set] y  X, Φ y  Ψ y) ⊣⊢ (([ set] y  X, Φ y)  [ set] y  X, Ψ y).
286
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
287
288
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
289
    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _  _)%I]comm -!assoc.
290
291
  Qed.

292
  Lemma big_sepS_later Φ X : ( [ set] y  X, Φ y) ⊣⊢ ([ set] y  X,  Φ y).
293
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
294
295
296
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
    by rewrite later_sep IH.
297
  Qed.
298
End gset.
299

300
(** ** Persistence *)
301
Global Instance big_and_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
302
Proof. induction 1; apply _. Qed.
303
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP ([] Ps).
304
305
Proof. induction 1; apply _. Qed.

306
Global Instance nil_persistent : PersistentL (@nil (uPred M)).
307
Proof. constructor. Qed.
308
Global Instance cons_persistent P Ps :
309
  PersistentP P  PersistentL Ps  PersistentL (P :: Ps).
310
Proof. by constructor. Qed.
311
312
Global Instance app_persistent Ps Ps' :
  PersistentL Ps  PersistentL Ps'  PersistentL (Ps ++ Ps').
313
Proof. apply Forall_app_2. Qed.
314
Global Instance zip_with_persistent {A B} (f : A  B  uPred M) xs ys :
315
  ( x y, PersistentP (f x y))  PersistentL (zip_with f xs ys).
316
317
318
Proof.
  unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
319
End big_op.