fin_collections.v 9.31 KB
 Robbert Krebbers committed Feb 08, 2015 1 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) `````` Robbert Krebbers committed Aug 29, 2012 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 . *) `````` Robbert Krebbers committed Feb 13, 2016 6 7 8 ``````From Coq Require Import Permutation. From stdpp Require Import relations listset. From stdpp Require Export numbers collections. `````` Robbert Krebbers committed Jun 11, 2012 9 `````` `````` Robbert Krebbers committed Nov 12, 2012 10 11 12 ``````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 Jun 11, 2012 13 `````` `````` Robbert Krebbers committed Nov 21, 2016 14 15 16 17 ``````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 Jun 11, 2012 18 19 ``````Section fin_collection. Context `{FinCollection A C}. `````` Robbert Krebbers committed Nov 18, 2015 20 ``````Implicit Types X Y : C. `````` Robbert Krebbers committed Jun 11, 2012 21 `````` `````` Robbert Krebbers committed Dec 11, 2015 22 23 ``````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 24 25 26 27 28 29 30 31 `````` 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 32 ``````Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)). `````` Robbert Krebbers committed Jun 11, 2012 33 34 ``````Proof. intros ?? E. apply NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 35 36 37 `````` - apply NoDup_elements. - apply NoDup_elements. - intros. by rewrite !elem_of_elements, E. `````` Robbert Krebbers committed Jun 11, 2012 38 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 39 `````` `````` Robbert Krebbers committed Feb 17, 2016 40 41 42 43 44 ``````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 45 46 47 48 49 50 51 52 53 54 55 ``````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 56 57 58 59 60 61 62 63 64 65 66 67 ``````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 68 `````` elements_union_singleton, elements_empty by set_solver. `````` Robbert Krebbers committed Feb 17, 2016 69 70 71 72 73 74 75 ``````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 76 ``````(** * The [size] operation *) `````` Robbert Krebbers committed Nov 18, 2015 77 ``````Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _). `````` Robbert Krebbers committed Oct 19, 2012 78 ``````Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. `````` Robbert Krebbers committed Jul 22, 2016 79 `````` `````` Robbert Krebbers committed Nov 12, 2012 80 ``````Lemma size_empty : size (∅ : C) = 0. `````` Robbert Krebbers committed Feb 17, 2016 81 ``````Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed. `````` Robbert Krebbers committed Nov 12, 2012 82 ``````Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅. `````` Robbert Krebbers committed Jun 11, 2012 83 ``````Proof. `````` Robbert Krebbers committed Dec 11, 2015 84 85 `````` intros; apply equiv_empty; intros x; rewrite <-elem_of_elements. by rewrite (nil_length_inv (elements X)), ?elem_of_nil. `````` Robbert Krebbers committed Jun 11, 2012 86 ``````Qed. `````` Robbert Krebbers committed Nov 12, 2012 87 ``````Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅. `````` Robbert Krebbers committed Dec 11, 2015 88 ``````Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed. `````` Robbert Krebbers committed Jan 05, 2013 89 90 ``````Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅. Proof. by rewrite size_empty_iff. Qed. `````` Robbert Krebbers committed Jul 22, 2016 91 `````` `````` Robbert Krebbers committed Jun 05, 2014 92 ``````Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅. `````` Robbert Krebbers committed Oct 19, 2012 93 ``````Proof. `````` Robbert Krebbers committed Jun 05, 2014 94 `````` destruct (elements X) as [|x l] eqn:HX; [right|left]. `````` Robbert Krebbers committed Feb 17, 2016 95 96 `````` - 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 Oct 19, 2012 97 ``````Qed. `````` Robbert Krebbers committed Jun 05, 2014 98 99 100 101 ``````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. `````` Robbert Krebbers committed May 11, 2013 102 ``````Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X. `````` Robbert Krebbers committed Aug 29, 2012 103 ``````Proof. `````` Robbert Krebbers committed Jun 05, 2014 104 105 `````` intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|]. contradict Hsz. rewrite HX, size_empty; lia. `````` Robbert Krebbers committed Jun 11, 2012 106 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 107 108 109 110 111 112 113 114 115 `````` 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 May 11, 2013 116 ``````Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}. `````` Robbert Krebbers committed Jun 11, 2012 117 ``````Proof. `````` Robbert Krebbers committed May 11, 2013 118 119 `````` intros E. destruct (size_pos_elem_of X); auto with lia. exists x. apply elem_of_equiv. split. `````` Robbert Krebbers committed Feb 17, 2016 120 `````` - rewrite elem_of_singleton. eauto using size_singleton_inv. `````` Robbert Krebbers committed Feb 17, 2016 121 `````` - set_solver. `````` Robbert Krebbers committed Jun 11, 2012 122 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 123 `````` `````` Robbert Krebbers committed Mar 23, 2016 124 ``````Lemma size_union X Y : X ⊥ Y → size (X ∪ Y) = size X + size Y. `````` Robbert Krebbers committed Jun 11, 2012 125 ``````Proof. `````` Robbert Krebbers committed Mar 23, 2016 126 `````` intros. unfold size, collection_size. simpl. rewrite <-app_length. `````` Robbert Krebbers committed Jun 11, 2012 127 `````` apply Permutation_length, NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 128 129 `````` - apply NoDup_elements. - apply NoDup_app; repeat split; try apply NoDup_elements. `````` Robbert Krebbers committed Feb 17, 2016 130 `````` intros x; rewrite !elem_of_elements; set_solver. `````` Robbert Krebbers committed Feb 17, 2016 131 `````` - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. `````` Robbert Krebbers committed Jun 11, 2012 132 133 ``````Qed. Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). `````` Robbert Krebbers committed Aug 29, 2012 134 ``````Proof. `````` Robbert Krebbers committed Feb 17, 2016 135 136 137 `````` 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 Jun 11, 2012 138 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 139 `````` `````` Robbert Krebbers committed Jun 11, 2012 140 ``````Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y. `````` Robbert Krebbers committed May 11, 2013 141 ``````Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed. `````` Robbert Krebbers committed Jan 05, 2013 142 ``````Lemma subset_size X Y : X ⊂ Y → size X < size Y. `````` Robbert Krebbers committed Jun 11, 2012 143 ``````Proof. `````` Robbert Krebbers committed Feb 17, 2016 144 `````` intros. rewrite (union_difference X Y) by set_solver. `````` Robbert Krebbers committed Jan 05, 2013 145 146 147 `````` rewrite size_union_alt, difference_twice. cut (size (Y ∖ X) ≠ 0); [lia |]. by apply size_non_empty_iff, non_empty_difference. `````` Robbert Krebbers committed Jun 11, 2012 148 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 149 150 `````` (** * Induction principles *) `````` Robbert Krebbers committed Aug 12, 2013 151 ``````Lemma collection_wf : wf (strict (@subseteq C _)). `````` Robbert Krebbers committed Aug 21, 2013 152 ``````Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed. `````` Robbert Krebbers committed Jun 11, 2012 153 ``````Lemma collection_ind (P : C → Prop) : `````` Robbert Krebbers committed Aug 29, 2012 154 `````` Proper ((≡) ==> iff) P → `````` Robbert Krebbers committed May 11, 2013 155 `````` P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X. `````` Robbert Krebbers committed Jun 11, 2012 156 ``````Proof. `````` Robbert Krebbers committed Jan 05, 2013 157 158 `````` intros ? Hemp Hadd. apply well_founded_induction with (⊂). { apply collection_wf. } `````` Robbert Krebbers committed Jun 05, 2014 159 `````` intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX]. `````` Robbert Krebbers committed Feb 17, 2016 160 161 `````` - rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd. set_solver. apply IH; set_solver. `````` Robbert Krebbers committed Feb 17, 2016 162 `````` - by rewrite HX. `````` Robbert Krebbers committed Jun 11, 2012 163 ``````Qed. `````` Robbert Krebbers committed Sep 28, 2016 164 165 166 ``````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 167 168 `````` (** * The [collection_fold] operation *) `````` Robbert Krebbers committed Jun 11, 2012 169 170 ``````Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) : Proper ((=) ==> (≡) ==> iff) P → `````` Robbert Krebbers committed Jun 17, 2013 171 `````` P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) → `````` Robbert Krebbers committed Aug 21, 2012 172 `````` ∀ X, P (collection_fold f b X) X. `````` Robbert Krebbers committed Jun 11, 2012 173 174 ``````Proof. intros ? Hemp Hadd. `````` Robbert Krebbers committed Nov 12, 2012 175 `````` cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X). `````` Robbert Krebbers committed Jun 05, 2014 176 177 `````` { intros help ?. apply help; [apply NoDup_elements|]. symmetry. apply elem_of_elements. } `````` Robbert Krebbers committed Jan 05, 2013 178 `````` induction 1 as [|x l ?? IH]; simpl. `````` Robbert Krebbers committed Feb 17, 2016 179 `````` - intros X HX. setoid_rewrite elem_of_nil in HX. `````` Robbert Krebbers committed Feb 17, 2016 180 `````` rewrite equiv_empty. done. set_solver. `````` Robbert Krebbers committed Feb 17, 2016 181 `````` - intros X HX. setoid_rewrite elem_of_cons in HX. `````` Robbert Krebbers committed Feb 17, 2016 182 183 `````` rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd. set_solver. apply IH. set_solver. `````` Robbert Krebbers committed Jun 11, 2012 184 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 185 186 ``````Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R} (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f} `````` Robbert Krebbers committed Nov 12, 2012 187 `````` (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) : `````` Robbert Krebbers committed Nov 18, 2015 188 `````` Proper ((≡) ==> R) (collection_fold f b : C → B). `````` Robbert Krebbers committed May 11, 2013 189 ``````Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed. `````` Robbert Krebbers committed Jul 22, 2016 190 `````` `````` Robbert Krebbers committed Nov 21, 2016 191 ``````(** * Minimal elements *) `````` Robbert Krebbers committed Nov 20, 2016 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 ``````Lemma minimal_exists `{!StrictOrder R, ∀ x y, Decision (R x y)} (X : C) : 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. Lemma minimal_exists_L `{!LeibnizEquiv C, !StrictOrder R, ∀ x y, Decision (R x y)} (X : C) : X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X. Proof. unfold_leibniz. apply minimal_exists. Qed. `````` Robbert Krebbers committed Nov 21, 2016 213 214 215 216 217 218 219 220 ``````(** * Filter *) Lemma elem_of_filter (P : A → Prop) `{!∀ x, Decision (P x)} 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. `````` Robbert Krebbers committed Jul 22, 2016 221 ``````(** * Decision procedures *) `````` Robbert Krebbers committed May 07, 2013 222 223 ``````Global Instance set_Forall_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (set_Forall P X) | 100. `````` Robbert Krebbers committed Oct 19, 2012 224 225 ``````Proof. refine (cast_if (decide (Forall P (elements X)))); `````` Robbert Krebbers committed Jun 05, 2014 226 `````` abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements; `````` Robbert Krebbers committed Nov 12, 2012 227 `````` by rewrite <-Forall_forall). `````` Robbert Krebbers committed Oct 19, 2012 228 ``````Defined. `````` Robbert Krebbers committed May 07, 2013 229 230 ``````Global Instance set_Exists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (set_Exists P X) | 100. `````` Robbert Krebbers committed Oct 19, 2012 231 232 ``````Proof. refine (cast_if (decide (Exists P (elements X)))); `````` Robbert Krebbers committed Jun 05, 2014 233 `````` abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements; `````` Robbert Krebbers committed Nov 12, 2012 234 `````` by rewrite <-Exists_exists). `````` Robbert Krebbers committed Oct 19, 2012 235 ``````Defined. `````` Robbert Krebbers committed Jun 11, 2012 236 ``End fin_collection.``