fin_collections.v 11.3 KB
 Robbert Krebbers committed Nov 11, 2015 1 2 3 4 5 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* 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 . *) `````` Robbert Krebbers committed Feb 13, 2016 6 ``````From Coq Require Import Permutation. `````` Robbert Krebbers committed Mar 10, 2016 7 8 ``````From iris.prelude Require Import relations listset. From iris.prelude Require Export numbers collections. `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Nov 21, 2016 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)). `````` Robbert Krebbers committed Nov 21, 2016 17 ``````Typeclasses Opaque collection_filter. `````` Robbert Krebbers committed Nov 21, 2016 18 `````` `````` Robbert Krebbers committed Nov 11, 2015 19 20 ``````Section fin_collection. Context `{FinCollection A C}. `````` Robbert Krebbers committed Nov 18, 2015 21 ``````Implicit Types X Y : C. `````` Robbert Krebbers committed Nov 11, 2015 22 `````` `````` Robbert Krebbers committed Dec 11, 2015 23 24 ``````Lemma fin_collection_finite X : set_finite X. Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed. `````` Robbert Krebbers committed Jul 22, 2016 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 *) `````` Robbert Krebbers committed Nov 18, 2015 33 ``````Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)). `````` Robbert Krebbers committed Nov 11, 2015 34 35 ``````Proof. intros ?? E. apply NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 36 37 38 `````` - apply NoDup_elements. - apply NoDup_elements. - intros. by rewrite !elem_of_elements, E. `````` Robbert Krebbers committed Nov 11, 2015 39 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 40 `````` `````` Robbert Krebbers committed Feb 17, 2016 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. `````` Robbert Krebbers committed Sep 27, 2016 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. `````` Robbert Krebbers committed Feb 17, 2016 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]}), `````` Robbert Krebbers committed Feb 17, 2016 69 `````` elements_union_singleton, elements_empty by set_solver. `````` Robbert Krebbers committed Feb 17, 2016 70 71 72 73 74 75 76 ``````Qed. Lemma elements_contains X Y : X ⊆ Y → elements X `contains` elements Y. Proof. intros; apply NoDup_contains; auto using NoDup_elements. intros x. rewrite !elem_of_elements; auto. Qed. `````` Robbert Krebbers committed Jul 22, 2016 77 ``````(** * The [size] operation *) `````` Robbert Krebbers committed Nov 18, 2015 78 ``````Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _). `````` Robbert Krebbers committed Nov 11, 2015 79 ``````Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. `````` Robbert Krebbers committed Jul 22, 2016 80 `````` `````` Robbert Krebbers committed Nov 11, 2015 81 ``````Lemma size_empty : size (∅ : C) = 0. `````` Robbert Krebbers committed Feb 17, 2016 82 ``````Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed. `````` Robbert Krebbers committed Nov 11, 2015 83 84 ``````Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅. Proof. `````` Robbert Krebbers committed Dec 11, 2015 85 86 `````` intros; apply equiv_empty; intros x; rewrite <-elem_of_elements. by rewrite (nil_length_inv (elements X)), ?elem_of_nil. `````` Robbert Krebbers committed Nov 11, 2015 87 88 ``````Qed. Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅. `````` Robbert Krebbers committed Dec 11, 2015 89 ``````Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed. `````` Robbert Krebbers committed Nov 11, 2015 90 91 ``````Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅. Proof. by rewrite size_empty_iff. Qed. `````` Robbert Krebbers committed Jul 22, 2016 92 `````` `````` Robbert Krebbers committed Nov 11, 2015 93 94 95 ``````Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅. Proof. destruct (elements X) as [|x l] eqn:HX; [right|left]. `````` Robbert Krebbers committed Feb 17, 2016 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 committed Nov 11, 2015 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. `````` Robbert Krebbers committed Jul 22, 2016 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 committed Nov 11, 2015 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. `````` Robbert Krebbers committed Feb 17, 2016 121 `````` - rewrite elem_of_singleton. eauto using size_singleton_inv. `````` Robbert Krebbers committed Feb 17, 2016 122 `````` - set_solver. `````` Robbert Krebbers committed Nov 11, 2015 123 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 124 `````` `````` Robbert Krebbers committed Mar 23, 2016 125 ``````Lemma size_union X Y : X ⊥ Y → size (X ∪ Y) = size X + size Y. `````` Robbert Krebbers committed Nov 11, 2015 126 ``````Proof. `````` Robbert Krebbers committed Mar 23, 2016 127 `````` intros. unfold size, collection_size. simpl. rewrite <-app_length. `````` Robbert Krebbers committed Nov 11, 2015 128 `````` apply Permutation_length, NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 129 130 `````` - apply NoDup_elements. - apply NoDup_app; repeat split; try apply NoDup_elements. `````` Robbert Krebbers committed Feb 17, 2016 131 `````` intros x; rewrite !elem_of_elements; set_solver. `````` Robbert Krebbers committed Feb 17, 2016 132 `````` - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. `````` Robbert Krebbers committed Nov 11, 2015 133 134 135 ``````Qed. Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). Proof. `````` Robbert Krebbers committed Feb 17, 2016 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 committed Nov 11, 2015 139 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 140 `````` `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Feb 17, 2016 145 `````` intros. rewrite (union_difference X Y) by set_solver. `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Jul 22, 2016 150 151 `````` (** * Induction principles *) `````` Robbert Krebbers committed Nov 11, 2015 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]. `````` Robbert Krebbers committed Feb 17, 2016 161 162 `````` - rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd. set_solver. apply IH; set_solver. `````` Robbert Krebbers committed Feb 17, 2016 163 `````` - by rewrite HX. `````` Robbert Krebbers committed Nov 11, 2015 164 ``````Qed. `````` Robbert Krebbers committed Sep 28, 2016 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. `````` Robbert Krebbers committed Jul 22, 2016 168 169 `````` (** * The [collection_fold] operation *) `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Feb 17, 2016 180 `````` - intros X HX. setoid_rewrite elem_of_nil in HX. `````` Robbert Krebbers committed Feb 17, 2016 181 `````` rewrite equiv_empty. done. set_solver. `````` Robbert Krebbers committed Feb 17, 2016 182 `````` - intros X HX. setoid_rewrite elem_of_cons in HX. `````` Robbert Krebbers committed Feb 17, 2016 183 184 `````` rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd. set_solver. apply IH. set_solver. `````` Robbert Krebbers committed Nov 11, 2015 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))) : `````` Robbert Krebbers committed Nov 18, 2015 189 `````` Proper ((≡) ==> R) (collection_fold f b : C → B). `````` Robbert Krebbers committed Nov 11, 2015 190 ``````Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed. `````` Robbert Krebbers committed Jul 22, 2016 191 `````` `````` Robbert Krebbers committed Nov 21, 2016 192 ``````(** * Minimal elements *) `````` 193 ``````Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) : `````` Robbert Krebbers committed Nov 20, 2016 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 committed Nov 20, 2016 211 `````` X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X. `````` 212 ``````Proof. unfold_leibniz. apply (minimal_exists R). Qed. `````` Robbert Krebbers committed Nov 20, 2016 213 `````` `````` Robbert Krebbers committed Nov 21, 2016 214 ``````(** * Filter *) `````` Robbert Krebbers committed Nov 21, 2016 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. `````` Robbert Krebbers committed Nov 21, 2016 250 `````` `````` Robbert Krebbers committed Jul 22, 2016 251 ``````(** * Decision procedures *) `````` Robbert Krebbers committed Nov 22, 2016 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. `````` Robbert Krebbers committed Nov 23, 2016 257 ``````Lemma set_Forall_Exists_dec (P Q : A → Prop) (dec : ∀ x, {P x} + {Q x}) X : `````` Robbert Krebbers committed Nov 22, 2016 258 259 `````` {set_Forall P X} + {set_Exists Q X}. Proof. `````` Robbert Krebbers committed Nov 23, 2016 260 `````` refine (cast_if (Forall_Exists_dec P Q dec (elements X))); `````` Robbert Krebbers committed Nov 22, 2016 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. `````` Robbert Krebbers committed Nov 23, 2016 266 ``````Proof. intro. by destruct (set_Forall_Exists_dec P (not ∘ P) dec X). Qed. `````` Robbert Krebbers committed Nov 22, 2016 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. `````` Robbert Krebbers committed Nov 23, 2016 270 271 `````` by destruct (set_Forall_Exists_dec (not ∘ P) P (λ x, swap_if (decide (P x))) X). `````` Robbert Krebbers committed Nov 22, 2016 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 committed Nov 11, 2015 276 ``````Proof. `````` Robbert Krebbers committed Nov 22, 2016 277 278 `````` refine (cast_if (decide (Forall P (elements X)))); by rewrite set_Forall_elements. `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Nov 22, 2016 283 284 `````` refine (cast_if (decide (Exists P (elements X)))); by rewrite set_Exists_elements. `````` Robbert Krebbers committed Nov 11, 2015 285 286 ``````Defined. End fin_collection.``````