upred_big_op.v 11 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
(** * Big ops over lists *)
(* These are the basic building blocks for other big ops *)
7
8
9
10
11
12
13
14
Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M:=
  match Ps with [] => True | P :: Ps => P  uPred_big_and Ps end%I.
Instance: Params (@uPred_big_and) 1.
Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
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.
Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
15

16
17
(** * Other big ops *)
(** We use a type class to obtain overloaded notations *)
18
Definition uPred_big_sepM {M} `{Countable K} {A}
19
20
    (m : gmap K A) (Φ : K  A  uPred M) : uPred M :=
  uPred_big_sep (curry Φ <$> map_to_list m).
21
Instance: Params (@uPred_big_sepM) 6.
22
23
Notation "'Π★{map' m } Φ" := (uPred_big_sepM m Φ)
  (at level 20, m at level 10, format "Π★{map  m }  Φ") : uPred_scope.
24

25
Definition uPred_big_sepS {M} `{Countable A}
26
  (X : gset A) (Φ : A  uPred M) : uPred M := uPred_big_sep (Φ <$> elements X).
27
Instance: Params (@uPred_big_sepS) 5.
28
29
Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
  (at level 20, X at level 10, format "Π★{set  X }  Φ") : uPred_scope.
30

31
(** * Persistence of lists of uPreds *)
32
Class PersistentL {M} (Ps : list (uPred M)) :=
33
  persistentL : Forall PersistentP Ps.
34
Arguments persistentL {_} _ {_}.
35

36
(** * Properties *)
37
38
39
40
41
Section big_op.
Context {M : cmraT}.
Implicit Types Ps Qs : list (uPred M).
Implicit Types A : Type.

42
(** ** Big ops over lists *)
43
Global Instance big_and_proper : Proper (() ==> ()) (@uPred_big_and M).
44
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
45
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
46
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
47

48
Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
49
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
50
Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
51
52
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

53
Global Instance big_and_mono' : Proper (Forall2 () ==> ()) (@uPred_big_and M).
54
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
55
Global Instance big_sep_mono' : Proper (Forall2 () ==> ()) (@uPred_big_sep M).
56
57
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.

58
Global Instance big_and_perm : Proper (() ==> ()) (@uPred_big_and M).
59
60
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
61
62
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
63
  - etrans; eauto.
64
Qed.
65
Global Instance big_sep_perm : Proper (() ==> ()) (@uPred_big_sep M).
66
67
Proof.
  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
68
69
  - by rewrite IH.
  - by rewrite !assoc (comm _ P).
70
  - etrans; eauto.
71
Qed.
72

73
Lemma big_and_app Ps Qs : Π (Ps ++ Qs)  (Π Ps  Π Qs).
74
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
75
Lemma big_sep_app Ps Qs : Π★ (Ps ++ Qs)  (Π★ Ps  Π★ Qs).
76
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
77

78
Lemma big_and_contains Ps Qs : Qs `contains` Ps  Π Ps  Π Qs.
79
Proof.
80
  intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
81
Qed.
82
Lemma big_sep_contains Ps Qs : Qs `contains` Ps  Π★ Ps  Π★ Qs.
83
Proof.
84
  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
85
86
Qed.

87
Lemma big_sep_and Ps : Π★ Ps  Π Ps.
88
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
89

90
Lemma big_and_elem_of Ps P : P  Ps  Π Ps  P.
91
Proof. induction 1; simpl; auto with I. Qed.
92
Lemma big_sep_elem_of Ps P : P  Ps  Π★ Ps  P.
93
94
Proof. induction 1; simpl; auto with I. Qed.

95
(** ** Big ops over finite maps *)
96
97
98
Section gmap.
  Context `{Countable K} {A : Type}.
  Implicit Types m : gmap K A.
99
  Implicit Types Φ Ψ : K  A  uPred M.
100

101
  Lemma big_sepM_mono Φ Ψ m1 m2 :
102
    m2  m1  ( x k, m2 !! k = Some x  Φ k x  Ψ k x) 
103
    Π★{map m1} Φ  Π★{map m2} Ψ.
104
  Proof.
105
    intros HX HΦ. trans (Π★{map m2} Φ)%I.
106
    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
107
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
108
      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
109
  Qed.
110
111
112
113
  Lemma big_sepM_proper Φ Ψ m1 m2 :
    m1  m2  ( x k, m1 !! k = Some x  m2 !! k = Some x  Φ k x  Ψ k x) 
    Π★{map m1} Φ  Π★{map m2} Ψ.
  Proof.
114
115
116
    (* 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. *)
117
    intros [??] ?; apply (anti_symm ()); apply big_sepM_mono;
118
      eauto using equiv_entails, equiv_entails_sym, @lookup_weaken.
119
  Qed.
120
121
122
123
124

  Global Instance big_sepM_ne m n :
    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
           (uPred_big_sepM (M:=M) m).
  Proof.
125
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
126
    apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ.
127
  Qed.
128
  Global Instance big_sepM_proper' m :
129
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
130
           (uPred_big_sepM (M:=M) m).
131
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
132
  Global Instance big_sepM_mono' m :
133
    Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
134
           (uPred_big_sepM (M:=M) m).
135
  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
136

137
  Lemma big_sepM_empty Φ : Π★{map } Φ  True.
138
  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
139
  Lemma big_sepM_insert Φ (m : gmap K A) i x :
140
    m !! i = None  Π★{map <[i:=x]> m} Φ  (Φ i x  Π★{map m} Φ).
141
  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
144
  Lemma big_sepM_delete Φ (m : gmap K A) i x :
    m !! i = Some x  Π★{map m} Φ  (Φ i x  Π★{map delete i m} Φ).
  Proof. intros. by rewrite -big_sepM_insert ?lookup_delete // insert_delete. Qed.
145
  Lemma big_sepM_singleton Φ i x : Π★{map {[i := x]}} Φ  (Φ i x).
146
147
148
149
  Proof.
    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
    by rewrite big_sepM_empty right_id.
  Qed.
150

151
  Lemma big_sepM_sepM Φ Ψ m :
152
    Π★{map m} (λ i x, Φ i x  Ψ i x)  (Π★{map m} Φ  Π★{map m} Ψ).
153
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
155
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
156
    by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _  _)%I]comm -!assoc.
157
  Qed.
158
  Lemma big_sepM_later Φ m :  Π★{map m} Φ  Π★{map m} (λ i x,  Φ i x).
159
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
160
161
162
    rewrite /uPred_big_sepM.
    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
    by rewrite later_sep IH.
163
  Qed.
164
165
End gmap.

166
(** ** Big ops over finite sets *)
167
168
169
Section gset.
  Context `{Countable A}.
  Implicit Types X : gset A.
170
  Implicit Types Φ : A  uPred M.
171

172
  Lemma big_sepS_mono Φ Ψ X Y :
173
    Y  X  ( x, x  Y  Φ x  Ψ x)  Π★{set X} Φ  Π★{set Y} Ψ.
174
  Proof.
175
    intros HX HΦ. trans (Π★{set Y} Φ)%I.
176
    - by apply big_sep_contains, fmap_contains, elements_contains.
177
    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
178
      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
179
  Qed.
180
181
182
183
184
185
  Lemma big_sepS_proper Φ Ψ X Y :
    X  Y  ( x, x  X  x  Y  Φ x  Ψ x)  Π★{set X} Φ  Π★{set Y} Ψ.
  Proof.
    intros [??] ?; apply (anti_symm ()); apply big_sepS_mono;
      eauto using equiv_entails, equiv_entails_sym.
  Qed.
186
187
188
189

  Lemma big_sepS_ne X n :
    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
  Proof.
190
    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
191
    apply Forall_Forall2, Forall_true=> x; apply HΦ.
192
  Qed.
193
  Lemma big_sepS_proper' X :
194
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
195
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_proper; naive_solver. Qed.
196
  Lemma big_sepS_mono' X :
197
    Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
198
  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
199

200
  Lemma big_sepS_empty Φ : Π★{set } Φ  True.
201
  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
202

203
  Lemma big_sepS_insert Φ X x :
204
    x  X  Π★{set {[ x ]}  X} Φ  (Φ x  Π★{set X} Φ).
205
  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
206
207
208
209
210
211
212
213
214
215
216
217
218
  Lemma big_sepS_insert' (Ψ : A  uPred M  uPred M) Φ X x P :
    x  X 
    Π★{set {[ x ]}  X} (λ y, Ψ y (<[x:=P]> Φ y))
     (Ψ x P  Π★{set X} (λ y, Ψ y (Φ y))).
  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.
  Lemma big_sepS_insert'' Φ X x P :
    x  X  Π★{set {[ x ]}  X} (<[x:=P]> Φ)  (P  Π★{set X} Φ).
  Proof. apply (big_sepS_insert' (λ y, id)). Qed.

219
  Lemma big_sepS_delete Φ X x :
220
    x  X  Π★{set X} Φ  (Φ x  Π★{set X  {[ x ]}} Φ).
221
  Proof.
222
223
    intros. rewrite -big_sepS_insert; last set_solver.
    by rewrite -union_difference_L; last set_solver.
224
  Qed.
225

226
  Lemma big_sepS_singleton Φ x : Π★{set {[ x ]}} Φ  (Φ x).
227
  Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
228

229
  Lemma big_sepS_sepS Φ Ψ X :
230
    Π★{set X} (λ x, Φ x  Ψ x)  (Π★{set X} Φ  Π★{set X} Ψ).
231
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
232
233
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
234
    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _  _)%I]comm -!assoc.
235
236
  Qed.

237
  Lemma big_sepS_later Φ X :  Π★{set X} Φ  Π★{set X} (λ x,  Φ x).
238
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
239
240
241
    rewrite /uPred_big_sepS.
    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
    by rewrite later_sep IH.
242
  Qed.
243
End gset.
244

245
(** ** Persistence *)
246
Global Instance big_and_persistent Ps : PersistentL Ps  PersistentP (Π Ps).
247
Proof. induction 1; apply _. Qed.
248
Global Instance big_sep_persistent Ps : PersistentL Ps  PersistentP (Π★ Ps).
249
250
Proof. induction 1; apply _. Qed.

251
Global Instance nil_persistent : PersistentL (@nil (uPred M)).
252
Proof. constructor. Qed.
253
Global Instance cons_persistent P Ps :
254
  PersistentP P  PersistentL Ps  PersistentL (P :: Ps).
255
Proof. by constructor. Qed.
256
257
Global Instance app_persistent Ps Ps' :
  PersistentL Ps  PersistentL Ps'  PersistentL (Ps ++ Ps').
258
Proof. apply Forall_app_2. Qed.
259
Global Instance zip_with_persistent {A B} (f : A  B  uPred M) xs ys :
260
  ( x y, PersistentP (f x y))  PersistentL (zip_with f xs ys).
261
262
263
Proof.
  unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
Qed.
264
End big_op.