fin_collections.v 8.02 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 14 15 `````` Section fin_collection. Context `{FinCollection A C}. `````` Robbert Krebbers committed Nov 18, 2015 16 ``````Implicit Types X Y : C. `````` Robbert Krebbers committed Jun 11, 2012 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 Jun 11, 2012 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 Jun 11, 2012 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 Oct 19, 2012 53 ``````Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. `````` Robbert Krebbers committed Nov 12, 2012 54 ``````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 12, 2012 56 ``````Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅. `````` Robbert Krebbers committed Jun 11, 2012 57 ``````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 Jun 11, 2012 60 ``````Qed. `````` Robbert Krebbers committed Nov 12, 2012 61 ``````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 Jan 05, 2013 63 64 ``````Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅. Proof. by rewrite size_empty_iff. Qed. `````` Robbert Krebbers committed Nov 12, 2012 65 ``````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 Jun 11, 2012 67 68 ``````Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y. Proof. `````` Robbert Krebbers committed Jun 05, 2014 69 `````` 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 Jun 11, 2012 72 ``````Qed. `````` Robbert Krebbers committed Jun 05, 2014 73 ``````Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅. `````` Robbert Krebbers committed Oct 19, 2012 74 ``````Proof. `````` Robbert Krebbers committed Jun 05, 2014 75 `````` 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 Oct 19, 2012 78 ``````Qed. `````` Robbert Krebbers committed Jun 05, 2014 79 80 81 82 ``````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 83 ``````Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X. `````` Robbert Krebbers committed Aug 29, 2012 84 ``````Proof. `````` Robbert Krebbers committed Jun 05, 2014 85 86 `````` intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|]. contradict Hsz. rewrite HX, size_empty; lia. `````` Robbert Krebbers committed Jun 11, 2012 87 ``````Qed. `````` Robbert Krebbers committed May 11, 2013 88 ``````Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}. `````` Robbert Krebbers committed Jun 11, 2012 89 ``````Proof. `````` Robbert Krebbers committed May 11, 2013 90 91 `````` 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 Jun 11, 2012 94 95 96 ``````Qed. Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y. Proof. `````` Robbert Krebbers committed Nov 12, 2012 97 `````` intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length. `````` Robbert Krebbers committed Jun 11, 2012 98 `````` 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 Jun 11, 2012 103 ``````Qed. `````` Robbert Krebbers committed Oct 19, 2012 104 105 ``````Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. Proof. `````` Robbert Krebbers committed Nov 12, 2012 106 `````` refine (cast_if (decide_rel (∈) x (elements X))); `````` Robbert Krebbers committed Jun 05, 2014 107 `````` by rewrite <-(elem_of_elements _). `````` Robbert Krebbers committed Oct 19, 2012 108 109 110 ``````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 Oct 19, 2012 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 May 11, 2013 116 `````` apply (size_empty_inv _ E1). by rewrite elem_of_difference. `````` Robbert Krebbers committed Oct 19, 2012 117 118 ``````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 May 11, 2013 120 `````` rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3. `````` Robbert Krebbers committed Oct 19, 2012 121 ``````Qed. `````` Robbert Krebbers committed Jun 11, 2012 122 ``````Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). `````` Robbert Krebbers committed Aug 29, 2012 123 ``````Proof. `````` Robbert Krebbers committed Jan 05, 2013 124 `````` 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 Jun 11, 2012 127 128 ``````Qed. Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y. `````` Robbert Krebbers committed May 11, 2013 129 ``````Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed. `````` Robbert Krebbers committed Jan 05, 2013 130 ``````Lemma subset_size X Y : X ⊂ Y → size X < size Y. `````` Robbert Krebbers committed Jun 11, 2012 131 ``````Proof. `````` Robbert Krebbers committed Jan 05, 2013 132 133 134 135 `````` 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. `````` Robbert Krebbers committed Jun 11, 2012 136 ``````Qed. `````` Robbert Krebbers committed Aug 12, 2013 137 ``````Lemma collection_wf : wf (strict (@subseteq C _)). `````` Robbert Krebbers committed Aug 21, 2013 138 ``````Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed. `````` Robbert Krebbers committed Jun 11, 2012 139 ``````Lemma collection_ind (P : C → Prop) : `````` Robbert Krebbers committed Aug 29, 2012 140 `````` Proper ((≡) ==> iff) P → `````` Robbert Krebbers committed May 11, 2013 141 `````` P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X. `````` Robbert Krebbers committed Jun 11, 2012 142 ``````Proof. `````` Robbert Krebbers committed Jan 05, 2013 143 144 `````` intros ? Hemp Hadd. apply well_founded_induction with (⊂). { apply collection_wf. } `````` Robbert Krebbers committed Jun 05, 2014 145 `````` 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 Jun 11, 2012 149 150 151 ``````Qed. Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) : Proper ((=) ==> (≡) ==> iff) P → `````` Robbert Krebbers committed Jun 17, 2013 152 `````` P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) → `````` Robbert Krebbers committed Aug 21, 2012 153 `````` ∀ X, P (collection_fold f b X) X. `````` Robbert Krebbers committed Jun 11, 2012 154 155 ``````Proof. intros ? Hemp Hadd. `````` Robbert Krebbers committed Nov 12, 2012 156 `````` cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X). `````` Robbert Krebbers committed Jun 05, 2014 157 158 `````` { intros help ?. apply help; [apply NoDup_elements|]. symmetry. apply elem_of_elements. } `````` Robbert Krebbers committed Jan 05, 2013 159 `````` 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 Jun 11, 2012 165 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 166 167 ``````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 168 `````` (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 May 11, 2013 170 ``````Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed. `````` Robbert Krebbers committed May 07, 2013 171 172 ``````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 173 174 ``````Proof. refine (cast_if (decide (Forall P (elements X)))); `````` Robbert Krebbers committed Jun 05, 2014 175 `````` abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements; `````` Robbert Krebbers committed Nov 12, 2012 176 `````` by rewrite <-Forall_forall). `````` Robbert Krebbers committed Oct 19, 2012 177 ``````Defined. `````` Robbert Krebbers committed May 07, 2013 178 179 ``````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 180 181 ``````Proof. refine (cast_if (decide (Exists P (elements X)))); `````` Robbert Krebbers committed Jun 05, 2014 182 `````` abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements; `````` Robbert Krebbers committed Nov 12, 2012 183 `````` by rewrite <-Exists_exists). `````` Robbert Krebbers committed Oct 19, 2012 184 ``````Defined. `````` Robbert Krebbers committed Aug 21, 2012 185 ``````Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X : `````` Robbert Krebbers committed May 07, 2013 186 `````` Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X). `````` Robbert Krebbers committed Jun 11, 2012 187 ``End fin_collection.``