fin_collections.v 11.2 KB
Newer Older
1
(* Copyright (c) 2012-2017, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4 5
(* This file is distributed under the terms of the BSD license. *)
(** This file collects definitions and theorems on finite collections. Most
importantly, it implements a fold and size function and some useful induction
principles on finite collections . *)
6
From iris.prelude Require Import relations.
7
From iris.prelude Require Export numbers collections.
8
Set Default Proof Using "Type*".
Robbert Krebbers's avatar
Robbert Krebbers committed
9 10 11 12 13

Instance collection_size `{Elements A C} : Size C := length  elements.
Definition collection_fold `{Elements A C} {B}
  (f : A  B  B) (b : B) : C  B := foldr f b  elements.

14 15 16
Instance collection_filter
    `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
  of_list (filter P (elements X)).
17
Typeclasses Opaque collection_filter.
18

Robbert Krebbers's avatar
Robbert Krebbers committed
19 20
Section fin_collection.
Context `{FinCollection A C}.
21
Implicit Types X Y : C.
Robbert Krebbers's avatar
Robbert Krebbers committed
22

23 24
Lemma fin_collection_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
25 26 27 28 29 30 31 32

Instance elem_of_dec_slow (x : A) (X : C) : Decision (x  X) | 100.
Proof.
  refine (cast_if (decide_rel () x (elements X)));
    by rewrite <-(elem_of_elements _).
Defined.

(** * The [elements] operation *)
33
Global Instance elements_proper: Proper (() ==> ()) (elements (C:=C)).
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35
Proof.
  intros ?? E. apply NoDup_Permutation.
36 37 38
  - apply NoDup_elements.
  - apply NoDup_elements.
  - intros. by rewrite !elem_of_elements, E.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
Qed.
40

41 42 43 44 45
Lemma elements_empty : elements ( : C) = [].
Proof.
  apply elem_of_nil_inv; intros x.
  rewrite elem_of_elements, elem_of_empty; tauto.
Qed.
46 47 48 49 50 51 52 53 54 55 56
Lemma elements_empty_inv X : elements X = []  X  .
Proof.
  intros HX; apply elem_of_equiv_empty; intros x.
  rewrite <-elem_of_elements, HX, elem_of_nil. tauto.
Qed.
Lemma elements_empty' X : elements X = []  X  .
Proof.
  split; intros HX; [by apply elements_empty_inv|].
  by rewrite <-Permutation_nil, HX, elements_empty.
Qed.

57 58 59 60 61 62 63 64 65 66 67 68
Lemma elements_union_singleton (X : C) x :
  x  X  elements ({[ x ]}  X)  x :: elements X.
Proof.
  intros ?; apply NoDup_Permutation.
  { apply NoDup_elements. }
  { by constructor; rewrite ?elem_of_elements; try apply NoDup_elements. }
  intros y; rewrite elem_of_elements, elem_of_union, elem_of_singleton.
  by rewrite elem_of_cons, elem_of_elements.
Qed.
Lemma elements_singleton x : elements {[ x ]} = [x].
Proof.
  apply Permutation_singleton. by rewrite <-(right_id  () {[x]}),
69
    elements_union_singleton, elements_empty by set_solver.
70
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Lemma elements_submseteq X Y : X  Y  elements X + elements Y.
72
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
  intros; apply NoDup_submseteq; auto using NoDup_elements.
74 75 76
  intros x. rewrite !elem_of_elements; auto.
Qed.

77
(** * The [size] operation *)
78
Global Instance collection_size_proper: Proper (() ==> (=)) (@size C _).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
80

Robbert Krebbers's avatar
Robbert Krebbers committed
81
Lemma size_empty : size ( : C) = 0.
82
Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
83 84
Lemma size_empty_inv (X : C) : size X = 0  X  .
Proof.
85 86
  intros; apply equiv_empty; intros x; rewrite <-elem_of_elements.
  by rewrite (nil_length_inv (elements X)), ?elem_of_nil.
Robbert Krebbers's avatar
Robbert Krebbers committed
87 88
Qed.
Lemma size_empty_iff (X : C) : size X = 0  X  .
89
Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
90 91
Lemma size_non_empty_iff (X : C) : size X  0  X  .
Proof. by rewrite size_empty_iff. Qed.
92

Robbert Krebbers's avatar
Robbert Krebbers committed
93 94 95
Lemma collection_choose_or_empty X : ( x, x  X)  X  .
Proof.
  destruct (elements X) as [|x l] eqn:HX; [right|left].
96 97
  - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
  - exists x. rewrite <-elem_of_elements, HX. by left.
Robbert Krebbers's avatar
Robbert Krebbers committed
98 99 100 101 102 103 104 105 106 107
Qed.
Lemma collection_choose X : X     x, x  X.
Proof. intros. by destruct (collection_choose_or_empty X). Qed.
Lemma collection_choose_L `{!LeibnizEquiv C} X : X     x, x  X.
Proof. unfold_leibniz. apply collection_choose. Qed.
Lemma size_pos_elem_of X : 0 < size X   x, x  X.
Proof.
  intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
  contradict Hsz. rewrite HX, size_empty; lia.
Qed.
108 109 110 111 112 113 114 115 116

Lemma size_singleton (x : A) : size {[ x ]} = 1.
Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed.
Lemma size_singleton_inv X x y : size X = 1  x  X  y  X  x = y.
Proof.
  unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
  generalize (elements X). intros [|? l]; intro; simplify_eq/=.
  rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
117 118 119 120
Lemma size_1_elem_of X : size X = 1   x, X  {[ x ]}.
Proof.
  intros E. destruct (size_pos_elem_of X); auto with lia.
  exists x. apply elem_of_equiv. split.
121
  - rewrite elem_of_singleton. eauto using size_singleton_inv.
122
  - set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
123
Qed.
124

Robbert Krebbers's avatar
Robbert Krebbers committed
125
Lemma size_union X Y : X  Y  size (X  Y) = size X + size Y.
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  intros. unfold size, collection_size. simpl. rewrite <-app_length.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  apply Permutation_length, NoDup_Permutation.
129 130
  - apply NoDup_elements.
  - apply NoDup_app; repeat split; try apply NoDup_elements.
131
    intros x; rewrite !elem_of_elements; set_solver.
132
  - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
Robbert Krebbers's avatar
Robbert Krebbers committed
133 134 135
Qed.
Lemma size_union_alt X Y : size (X  Y) = size X + size (Y  X).
Proof.
136 137 138
  rewrite <-size_union by set_solver.
  setoid_replace (Y  X) with ((Y  X)  X) by set_solver.
  rewrite <-union_difference, (comm ()); set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Qed.
140

Robbert Krebbers's avatar
Robbert Krebbers committed
141 142 143 144
Lemma subseteq_size X Y : X  Y  size X  size Y.
Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
Lemma subset_size X Y : X  Y  size X < size Y.
Proof.
145
  intros. rewrite (union_difference X Y) by set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
146 147 148 149
  rewrite size_union_alt, difference_twice.
  cut (size (Y  X)  0); [lia |].
  by apply size_non_empty_iff, non_empty_difference.
Qed.
150 151

(** * Induction principles *)
Robbert Krebbers's avatar
Robbert Krebbers committed
152 153 154 155 156 157 158 159 160
Lemma collection_wf : wf (strict (@subseteq C _)).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma collection_ind (P : C  Prop) :
  Proper (() ==> iff) P 
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Proof.
  intros ? Hemp Hadd. apply well_founded_induction with ().
  { apply collection_wf. }
  intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
161 162
  - rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH; set_solver.
163
  - by rewrite HX.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
Qed.
165 166 167
Lemma collection_ind_L `{!LeibnizEquiv C} (P : C  Prop) :
  P   ( x X, x  X  P X  P ({[ x ]}  X))   X, P X.
Proof. apply collection_ind. by intros ?? ->%leibniz_equiv_iff. Qed.
168 169

(** * The [collection_fold] operation *)
Robbert Krebbers's avatar
Robbert Krebbers committed
170 171 172 173 174 175 176 177 178 179
Lemma collection_fold_ind {B} (P : B  C  Prop) (f : A  B  B) (b : B) :
  Proper ((=) ==> () ==> iff) P 
  P b   ( x X r, x  X  P r X  P (f x r) ({[ x ]}  X)) 
   X, P (collection_fold f b X) X.
Proof.
  intros ? Hemp Hadd.
  cut ( l, NoDup l   X, ( x, x  X  x  l)  P (foldr f b l) X).
  { intros help ?. apply help; [apply NoDup_elements|].
    symmetry. apply elem_of_elements. }
  induction 1 as [|x l ?? IH]; simpl.
180
  - intros X HX. setoid_rewrite elem_of_nil in HX.
181
    rewrite equiv_empty. done. set_solver.
182
  - intros X HX. setoid_rewrite elem_of_cons in HX.
183 184
    rewrite (union_difference {[ x ]} X) by set_solver.
    apply Hadd. set_solver. apply IH. set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
185 186 187 188
Qed.
Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
    (f : A  B  B) (b : B) `{!Proper ((=) ==> R ==> R) f}
    (Hf :  a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
189
  Proper (() ==> R) (collection_fold f b : C  B).
Robbert Krebbers's avatar
Robbert Krebbers committed
190
Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
191

192
(** * Minimal elements *)
193
Lemma minimal_exists R `{!Transitive R,  x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
194 195 196 197 198 199 200 201 202 203 204 205 206 207 208
  X     x, x  X  minimal R x X.
Proof.
  pattern X; apply collection_ind; clear X.
  { by intros X X' HX; setoid_rewrite HX. }
  { done. }
  intros x X ? IH Hemp. destruct (collection_choose_or_empty X) as [[z ?]|HX].
  { destruct IH as (x' & Hx' & Hmin); [set_solver|].
    destruct (decide (R x x')).
    - exists x; split; [set_solver|].
      eauto using union_minimal, singleton_minimal, minimal_weaken.
    - exists x'; split; [set_solver|].
      auto using union_minimal, singleton_minimal_not_above. }
  exists x; split; [set_solver|].
  rewrite HX, (right_id _ ()). apply singleton_minimal.
Qed.
209 210
Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R,
     x y, Decision (R x y)} (X : C) :
Robbert Krebbers's avatar
Robbert Krebbers committed
211
  X     x, x  X  minimal R x X.
212
Proof. unfold_leibniz. apply (minimal_exists R). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
213

214
(** * Filter *)
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
Section filter.
  Context (P : A  Prop) `{! x, Decision (P x)}.

  Lemma elem_of_filter X x : x  filter P X  P x  x  X.
  Proof.
    unfold filter, collection_filter.
    by rewrite elem_of_of_list, elem_of_list_filter, elem_of_elements.
  Qed.
  Global Instance set_unfold_filter X Q :
    SetUnfold (x  X) Q  SetUnfold (x  filter P X) (P x  Q).
  Proof.
    intros ??; constructor. by rewrite elem_of_filter, (set_unfold (x  X) Q).
  Qed.

  Lemma filter_empty : filter P (:C)  .
  Proof. set_solver. Qed.
  Lemma filter_union X Y : filter P (X  Y)  filter P X  filter P Y.
  Proof. set_solver. Qed.
  Lemma filter_singleton x : P x  filter P ({[ x ]} : C)  {[ x ]}.
  Proof. set_solver. Qed.
  Lemma filter_singleton_not x : ¬P x  filter P ({[ x ]} : C)  .
  Proof. set_solver. Qed.

  Section leibniz_equiv.
    Context `{!LeibnizEquiv C}.
    Lemma filter_empty_L : filter P (:C) = .
    Proof. set_solver. Qed.
    Lemma filter_union_L X Y : filter P (X  Y) = filter P X  filter P Y.
    Proof. set_solver. Qed.
    Lemma filter_singleton_L x : P x  filter P ({[ x ]} : C) = {[ x ]}.
    Proof. set_solver. Qed.
    Lemma filter_singleton_not_L x : ¬P x  filter P ({[ x ]} : C) = .
    Proof. set_solver. Qed.
  End leibniz_equiv.
End filter.
250

251
(** * Decision procedures *)
252 253 254 255 256
Lemma set_Forall_elements P X : set_Forall P X  Forall P (elements X).
Proof. rewrite Forall_forall. by setoid_rewrite elem_of_elements. Qed.
Lemma set_Exists_elements P X : set_Exists P X  Exists P (elements X).
Proof. rewrite Exists_exists. by setoid_rewrite elem_of_elements. Qed.

257
Lemma set_Forall_Exists_dec (P Q : A  Prop) (dec :  x, {P x} + {Q x}) X :
258 259
  {set_Forall P X} + {set_Exists Q X}.
Proof.
260
 refine (cast_if (Forall_Exists_dec P Q dec (elements X)));
261 262 263 264 265
   [by apply set_Forall_elements|by apply set_Exists_elements].
Defined.

Lemma not_set_Forall_Exists P `{dec :  x, Decision (P x)} X :
  ¬set_Forall P X  set_Exists (not  P) X.
266
Proof. intro. by destruct (set_Forall_Exists_dec P (not  P) dec X). Qed.
267 268 269
Lemma not_set_Exists_Forall P `{dec :  x, Decision (P x)} X :
  ¬set_Exists P X  set_Forall (not  P) X.
Proof.
270 271
  by destruct (set_Forall_Exists_dec
    (not  P) P (λ x, swap_if (decide (P x))) X).
272 273 274 275
Qed.

Global Instance set_Forall_dec (P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Forall P X) | 100.
Robbert Krebbers's avatar
Robbert Krebbers committed
276
Proof.
277 278
 refine (cast_if (decide (Forall P (elements X))));
   by rewrite set_Forall_elements.
Robbert Krebbers's avatar
Robbert Krebbers committed
279 280 281 282
Defined.
Global Instance set_Exists_dec `(P : A  Prop) `{ x, Decision (P x)} X :
  Decision (set_Exists P X) | 100.
Proof.
283 284
 refine (cast_if (decide (Exists P (elements X))));
   by rewrite set_Exists_elements.
Robbert Krebbers's avatar
Robbert Krebbers committed
285 286
Defined.
End fin_collection.