fin_collections.v 7.38 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 Nov 16, 2015 6 7 ``````Require Import Permutation prelude.relations prelude.listset. Require Export prelude.numbers prelude.collections. `````` Robbert Krebbers committed Jun 11, 2012 8 `````` `````` Robbert Krebbers committed Nov 12, 2012 9 10 11 ``````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 12 13 14 `````` Section fin_collection. Context `{FinCollection A C}. `````` Robbert Krebbers committed Nov 18, 2015 15 ``````Implicit Types X Y : C. `````` Robbert Krebbers committed Jun 11, 2012 16 `````` `````` Robbert Krebbers committed Dec 11, 2015 17 18 ``````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 19 ``````Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)). `````` Robbert Krebbers committed Jun 11, 2012 20 21 ``````Proof. intros ?? E. apply NoDup_Permutation. `````` Robbert Krebbers committed Jun 05, 2014 22 23 24 `````` * apply NoDup_elements. * apply NoDup_elements. * intros. by rewrite !elem_of_elements, E. `````` Robbert Krebbers committed Jun 11, 2012 25 ``````Qed. `````` Robbert Krebbers committed Nov 18, 2015 26 ``````Global Instance collection_size_proper: Proper ((≡) ==> (=)) (@size C _). `````` Robbert Krebbers committed Oct 19, 2012 27 ``````Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. `````` Robbert Krebbers committed Nov 12, 2012 28 ``````Lemma size_empty : size (∅ : C) = 0. `````` Robbert Krebbers committed Jun 11, 2012 29 ``````Proof. `````` Robbert Krebbers committed Nov 12, 2012 30 `````` unfold size, collection_size. simpl. `````` Robbert Krebbers committed Dec 11, 2015 31 32 `````` rewrite (elem_of_nil_inv (elements ∅)); [done|intro]. rewrite elem_of_elements, elem_of_empty; auto. `````` Robbert Krebbers committed Jun 11, 2012 33 ``````Qed. `````` Robbert Krebbers committed Nov 12, 2012 34 ``````Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅. `````` Robbert Krebbers committed Jun 11, 2012 35 ``````Proof. `````` Robbert Krebbers committed Dec 11, 2015 36 37 `````` 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 38 ``````Qed. `````` Robbert Krebbers committed Nov 12, 2012 39 ``````Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅. `````` Robbert Krebbers committed Dec 11, 2015 40 ``````Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed. `````` Robbert Krebbers committed Jan 05, 2013 41 42 ``````Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅. Proof. by rewrite size_empty_iff. Qed. `````` Robbert Krebbers committed Nov 12, 2012 43 ``````Lemma size_singleton (x : A) : size {[ x ]} = 1. `````` Robbert Krebbers committed Jun 11, 2012 44 ``````Proof. `````` Robbert Krebbers committed Aug 21, 2012 45 `````` change (length (elements {[ x ]}) = length [x]). `````` Robbert Krebbers committed Jun 11, 2012 46 `````` apply Permutation_length, NoDup_Permutation. `````` Robbert Krebbers committed Jun 05, 2014 47 `````` * apply NoDup_elements. `````` Robbert Krebbers committed Aug 21, 2012 48 `````` * apply NoDup_singleton. `````` Robbert Krebbers committed Dec 11, 2015 49 50 `````` * intros y. by rewrite elem_of_elements, elem_of_singleton, elem_of_list_singleton. `````` Robbert Krebbers committed Jun 11, 2012 51 52 53 ``````Qed. Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y. Proof. `````` Robbert Krebbers committed Jun 05, 2014 54 `````` unfold size, collection_size. simpl. rewrite <-!elem_of_elements. `````` Robbert Krebbers committed Sep 30, 2014 55 `````` generalize (elements X). intros [|? l]; intro; simplify_equality'. `````` Robbert Krebbers committed Dec 11, 2015 56 `````` rewrite (nil_length_inv l), !elem_of_list_singleton by done; congruence. `````` Robbert Krebbers committed Jun 11, 2012 57 ``````Qed. `````` Robbert Krebbers committed Jun 05, 2014 58 ``````Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅. `````` Robbert Krebbers committed Oct 19, 2012 59 ``````Proof. `````` Robbert Krebbers committed Jun 05, 2014 60 `````` destruct (elements X) as [|x l] eqn:HX; [right|left]. `````` Robbert Krebbers committed Dec 11, 2015 61 `````` * apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil. `````` Robbert Krebbers committed Jun 05, 2014 62 `````` * exists x. rewrite <-elem_of_elements, HX. by left. `````` Robbert Krebbers committed Oct 19, 2012 63 ``````Qed. `````` Robbert Krebbers committed Jun 05, 2014 64 65 66 67 ``````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 68 ``````Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X. `````` Robbert Krebbers committed Aug 29, 2012 69 ``````Proof. `````` Robbert Krebbers committed Jun 05, 2014 70 71 `````` intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|]. contradict Hsz. rewrite HX, size_empty; lia. `````` Robbert Krebbers committed Jun 11, 2012 72 ``````Qed. `````` Robbert Krebbers committed May 11, 2013 73 ``````Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}. `````` Robbert Krebbers committed Jun 11, 2012 74 ``````Proof. `````` Robbert Krebbers committed May 11, 2013 75 76 77 78 `````` intros E. destruct (size_pos_elem_of X); auto with lia. exists x. apply elem_of_equiv. split. * rewrite elem_of_singleton. eauto using size_singleton_inv. * solve_elem_of. `````` Robbert Krebbers committed Jun 11, 2012 79 80 81 ``````Qed. Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y. Proof. `````` Robbert Krebbers committed Nov 12, 2012 82 `````` intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length. `````` Robbert Krebbers committed Jun 11, 2012 83 `````` apply Permutation_length, NoDup_Permutation. `````` Robbert Krebbers committed Jun 05, 2014 84 85 `````` * apply NoDup_elements. * apply NoDup_app; repeat split; try apply NoDup_elements. `````` Robbert Krebbers committed Jan 16, 2016 86 `````` intros x; rewrite !elem_of_elements; solve_elem_of. `````` Robbert Krebbers committed Dec 11, 2015 87 `````` * intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. `````` Robbert Krebbers committed Jun 11, 2012 88 ``````Qed. `````` Robbert Krebbers committed Oct 19, 2012 89 90 ``````Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100. Proof. `````` Robbert Krebbers committed Nov 12, 2012 91 `````` refine (cast_if (decide_rel (∈) x (elements X))); `````` Robbert Krebbers committed Jun 05, 2014 92 `````` by rewrite <-(elem_of_elements _). `````` Robbert Krebbers committed Oct 19, 2012 93 94 95 ``````Defined. Global Program Instance collection_subseteq_dec_slow (X Y : C) : Decision (X ⊆ Y) | 100 := `````` Robbert Krebbers committed Jan 12, 2016 96 97 `````` match decide_rel (=) (size (X ∖ Y)) 0 return _ with | left _ => left _ | right _ => right _ `````` Robbert Krebbers committed Oct 19, 2012 98 99 `````` end. Next Obligation. `````` Robbert Krebbers committed Jan 12, 2016 100 `````` intros X Y E1 x ?; apply dec_stable; intro. destruct (proj1(elem_of_empty x)). `````` Robbert Krebbers committed May 11, 2013 101 `````` apply (size_empty_inv _ E1). by rewrite elem_of_difference. `````` Robbert Krebbers committed Oct 19, 2012 102 103 ``````Qed. Next Obligation. `````` Robbert Krebbers committed Jan 12, 2016 104 `````` intros X Y E1 E2; destruct E1. apply size_empty_iff, equiv_empty. intros x. `````` Robbert Krebbers committed May 11, 2013 105 `````` rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3. `````` Robbert Krebbers committed Oct 19, 2012 106 ``````Qed. `````` Robbert Krebbers committed Jun 11, 2012 107 ``````Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). `````` Robbert Krebbers committed Aug 29, 2012 108 ``````Proof. `````` Robbert Krebbers committed Jan 05, 2013 109 `````` rewrite <-size_union by solve_elem_of. `````` Robbert Krebbers committed Jan 16, 2016 110 `````` setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by solve_elem_of. `````` Robbert Krebbers committed Jan 05, 2013 111 `````` rewrite <-union_difference, (commutative (∪)); solve_elem_of. `````` Robbert Krebbers committed Jun 11, 2012 112 113 ``````Qed. Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y. `````` Robbert Krebbers committed May 11, 2013 114 ``````Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed. `````` Robbert Krebbers committed Jan 05, 2013 115 ``````Lemma subset_size X Y : X ⊂ Y → size X < size Y. `````` Robbert Krebbers committed Jun 11, 2012 116 ``````Proof. `````` Robbert Krebbers committed Jan 05, 2013 117 118 119 120 `````` 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 121 ``````Qed. `````` Robbert Krebbers committed Aug 12, 2013 122 ``````Lemma collection_wf : wf (strict (@subseteq C _)). `````` Robbert Krebbers committed Aug 21, 2013 123 ``````Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed. `````` Robbert Krebbers committed Jun 11, 2012 124 ``````Lemma collection_ind (P : C → Prop) : `````` Robbert Krebbers committed Aug 29, 2012 125 `````` Proper ((≡) ==> iff) P → `````` Robbert Krebbers committed May 11, 2013 126 `````` P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X. `````` Robbert Krebbers committed Jun 11, 2012 127 ``````Proof. `````` Robbert Krebbers committed Jan 05, 2013 128 129 `````` intros ? Hemp Hadd. apply well_founded_induction with (⊂). { apply collection_wf. } `````` Robbert Krebbers committed Jun 05, 2014 130 `````` intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX]. `````` Robbert Krebbers committed Jan 05, 2013 131 `````` * rewrite (union_difference {[ x ]} X) by solve_elem_of. `````` Robbert Krebbers committed Jan 16, 2016 132 `````` apply Hadd. solve_elem_of. apply IH; solve_elem_of. `````` Robbert Krebbers committed Jan 05, 2013 133 `````` * by rewrite HX. `````` Robbert Krebbers committed Jun 11, 2012 134 135 136 ``````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 137 `````` P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) → `````` Robbert Krebbers committed Aug 21, 2012 138 `````` ∀ X, P (collection_fold f b X) X. `````` Robbert Krebbers committed Jun 11, 2012 139 140 ``````Proof. intros ? Hemp Hadd. `````` Robbert Krebbers committed Nov 12, 2012 141 `````` cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X). `````` Robbert Krebbers committed Jun 05, 2014 142 143 `````` { intros help ?. apply help; [apply NoDup_elements|]. symmetry. apply elem_of_elements. } `````` Robbert Krebbers committed Jan 05, 2013 144 `````` induction 1 as [|x l ?? IH]; simpl. `````` Robbert Krebbers committed Nov 12, 2012 145 `````` * intros X HX. setoid_rewrite elem_of_nil in HX. `````` Robbert Krebbers committed Jan 16, 2016 146 `````` rewrite equiv_empty. done. solve_elem_of. `````` Robbert Krebbers committed Nov 12, 2012 147 `````` * intros X HX. setoid_rewrite elem_of_cons in HX. `````` Robbert Krebbers committed Jan 16, 2016 148 149 `````` 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 150 ``````Qed. `````` Robbert Krebbers committed May 07, 2013 151 152 ``````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 153 `````` (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) : `````` Robbert Krebbers committed Nov 18, 2015 154 `````` Proper ((≡) ==> R) (collection_fold f b : C → B). `````` Robbert Krebbers committed May 11, 2013 155 ``````Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed. `````` Robbert Krebbers committed May 07, 2013 156 157 ``````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 158 159 ``````Proof. refine (cast_if (decide (Forall P (elements X)))); `````` Robbert Krebbers committed Jun 05, 2014 160 `````` abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements; `````` Robbert Krebbers committed Nov 12, 2012 161 `````` by rewrite <-Forall_forall). `````` Robbert Krebbers committed Oct 19, 2012 162 ``````Defined. `````` Robbert Krebbers committed May 07, 2013 163 164 ``````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 165 166 ``````Proof. refine (cast_if (decide (Exists P (elements X)))); `````` Robbert Krebbers committed Jun 05, 2014 167 `````` abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements; `````` Robbert Krebbers committed Nov 12, 2012 168 `````` by rewrite <-Exists_exists). `````` Robbert Krebbers committed Oct 19, 2012 169 ``````Defined. `````` Robbert Krebbers committed Aug 21, 2012 170 ``````Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X : `````` Robbert Krebbers committed May 07, 2013 171 `````` Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X). `````` Robbert Krebbers committed Jun 11, 2012 172 ``End fin_collection.``