fin_collections.v 8.03 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 7 8 ``````From Coq Require Import Permutation. From prelude Require Import relations listset. From prelude Require Export numbers collections. `````` Robbert Krebbers committed Nov 11, 2015 9 10 11 12 13 14 15 `````` 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. Section fin_collection. Context `{FinCollection A C}. `````` Robbert Krebbers committed Nov 18, 2015 16 ``````Implicit Types X Y : C. `````` Robbert Krebbers committed Nov 11, 2015 17 `````` `````` Robbert Krebbers committed Dec 11, 2015 18 19 ``````Lemma fin_collection_finite X : set_finite X. Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed. `````` Robbert Krebbers committed Nov 18, 2015 20 ``````Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)). `````` Robbert Krebbers committed Nov 11, 2015 21 22 ``````Proof. intros ?? E. apply NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 23 24 25 `````` - apply NoDup_elements. - apply NoDup_elements. - intros. by rewrite !elem_of_elements, E. `````` Robbert Krebbers committed Nov 11, 2015 26 ``````Qed. `````` Robbert Krebbers committed Feb 17, 2016 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 ``````Lemma elements_empty : elements (∅ : C) = []. Proof. apply elem_of_nil_inv; intros x. rewrite elem_of_elements, elem_of_empty; tauto. Qed. 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]}), elements_union_singleton, elements_empty by solve_elem_of. 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 Nov 18, 2015 52 ``````Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _). `````` Robbert Krebbers committed Nov 11, 2015 53 54 ``````Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. Lemma size_empty : size (∅ : C) = 0. `````` Robbert Krebbers committed Feb 17, 2016 55 ``````Proof. unfold size, collection_size. simpl. by rewrite elements_empty. Qed. `````` Robbert Krebbers committed Nov 11, 2015 56 57 ``````Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅. Proof. `````` Robbert Krebbers committed Dec 11, 2015 58 59 `````` 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 60 61 ``````Qed. Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅. `````` Robbert Krebbers committed Dec 11, 2015 62 ``````Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed. `````` Robbert Krebbers committed Nov 11, 2015 63 64 65 ``````Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅. Proof. by rewrite size_empty_iff. Qed. Lemma size_singleton (x : A) : size {[ x ]} = 1. `````` Robbert Krebbers committed Feb 17, 2016 66 ``````Proof. unfold size, collection_size. simpl. by rewrite elements_singleton. Qed. `````` Robbert Krebbers committed Nov 11, 2015 67 68 69 ``````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. `````` Robbert Krebbers committed Feb 17, 2016 70 `````` generalize (elements X). intros [|? l]; intro; simplify_eq/=. `````` Robbert Krebbers committed Dec 11, 2015 71 `````` rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence. `````` Robbert Krebbers committed Nov 11, 2015 72 73 74 75 ``````Qed. 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 76 77 `````` - 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 78 79 80 81 82 83 84 85 86 87 88 89 90 91 ``````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. 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 92 93 `````` - rewrite elem_of_singleton. eauto using size_singleton_inv. - solve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 94 95 96 97 98 ``````Qed. Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y. Proof. intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length. apply Permutation_length, NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 99 100 `````` - apply NoDup_elements. - apply NoDup_app; repeat split; try apply NoDup_elements. `````` Robbert Krebbers committed Jan 16, 2016 101 `````` intros x; rewrite !elem_of_elements; solve_elem_of. `````` Robbert Krebbers committed Feb 17, 2016 102 `````` - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. `````` Robbert Krebbers committed Nov 11, 2015 103 104 105 106 107 108 109 110 ``````Qed. 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. Global Program Instance collection_subseteq_dec_slow (X Y : C) : Decision (X ⊆ Y) | 100 := `````` Robbert Krebbers committed Jan 12, 2016 111 112 `````` match decide_rel (=) (size (X ∖ Y)) 0 return _ with | left _ => left _ | right _ => right _ `````` Robbert Krebbers committed Nov 11, 2015 113 114 `````` end. Next Obligation. `````` Robbert Krebbers committed Jan 12, 2016 115 `````` intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)). `````` Robbert Krebbers committed Nov 11, 2015 116 117 118 `````` apply (size_empty_inv _ E1). by rewrite elem_of_difference. Qed. Next Obligation. `````` Robbert Krebbers committed Jan 12, 2016 119 `````` intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x. `````` Robbert Krebbers committed Nov 11, 2015 120 121 122 123 124 `````` rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3. Qed. Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). Proof. rewrite <-size_union by solve_elem_of. `````` Robbert Krebbers committed Jan 16, 2016 125 `````` setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by solve_elem_of. `````` Robbert Krebbers committed Feb 11, 2016 126 `````` rewrite <-union_difference, (comm (∪)); solve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 ``````Qed. 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. intros. rewrite (union_difference X Y) by solve_elem_of. rewrite size_union_alt, difference_twice. cut (size (Y ∖ X) ≠ 0); [lia |]. by apply size_non_empty_iff, non_empty_difference. Qed. 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 146 `````` - rewrite (union_difference {[ x ]} X) by solve_elem_of. `````` Robbert Krebbers committed Jan 16, 2016 147 `````` apply Hadd. solve_elem_of. apply IH; solve_elem_of. `````` Robbert Krebbers committed Feb 17, 2016 148 `````` - by rewrite HX. `````` Robbert Krebbers committed Nov 11, 2015 149 150 151 152 153 154 155 156 157 158 159 ``````Qed. 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 160 `````` - intros X HX. setoid_rewrite elem_of_nil in HX. `````` Robbert Krebbers committed Jan 16, 2016 161 `````` rewrite equiv_empty. done. solve_elem_of. `````` Robbert Krebbers committed Feb 17, 2016 162 `````` - intros X HX. setoid_rewrite elem_of_cons in HX. `````` Robbert Krebbers committed Jan 16, 2016 163 164 `````` rewrite (union_difference {[ x ]} X) by solve_elem_of. apply Hadd. solve_elem_of. apply IH. solve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 165 166 167 168 ``````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 169 `````` Proper ((≡) ==> R) (collection_fold f b : C → B). `````` Robbert Krebbers committed Nov 11, 2015 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 ``````Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed. Global Instance set_Forall_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (set_Forall P X) | 100. Proof. refine (cast_if (decide (Forall P (elements X)))); abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements; by rewrite <-Forall_forall). Defined. Global Instance set_Exists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (set_Exists P X) | 100. Proof. refine (cast_if (decide (Exists P (elements X)))); abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements; by rewrite <-Exists_exists). Defined. Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X : Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X). End fin_collection.``````