fin_sets.v 16.9 KB
 Robbert Krebbers committed Jan 29, 2019 1 ``````(* Copyright (c) 2012-2019, Coq-std++ developers. *) `````` Robbert Krebbers committed Aug 29, 2012 2 ``````(* This file is distributed under the terms of the BSD license. *) `````` Robbert Krebbers committed Feb 20, 2019 3 ``````(** This file collects definitions and theorems on finite sets. Most `````` Robbert Krebbers committed Aug 29, 2012 4 ``````importantly, it implements a fold and size function and some useful induction `````` Robbert Krebbers committed Feb 20, 2019 5 ``````principles on finite sets . *) `````` Robbert Krebbers committed Jan 31, 2017 6 ``````From stdpp Require Import relations. `````` Robbert Krebbers committed Feb 20, 2019 7 ``````From stdpp Require Export numbers sets. `````` Ralf Jung committed Jan 31, 2017 8 ``````Set Default Proof Using "Type*". `````` Robbert Krebbers committed Jun 11, 2012 9 `````` `````` Robbert Krebbers committed Mar 03, 2019 10 ``````(** Operations *) `````` Robbert Krebbers committed Feb 20, 2019 11 ``````Instance set_size `{Elements A C} : Size C := length ∘ elements. `````` Robbert Krebbers committed Mar 03, 2019 12 `````` `````` Robbert Krebbers committed Feb 20, 2019 13 ``````Definition set_fold `{Elements A C} {B} `````` Robbert Krebbers committed Nov 12, 2012 14 `````` (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements. `````` Robbert Krebbers committed Jun 11, 2012 15 `````` `````` Robbert Krebbers committed Feb 20, 2019 16 ``````Instance set_filter `````` Robbert Krebbers committed Nov 21, 2016 17 `````` `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X, `````` Robbert Krebbers committed Feb 20, 2019 18 19 `````` list_to_set (filter P (elements X)). Typeclasses Opaque set_filter. `````` Robbert Krebbers committed Nov 21, 2016 20 `````` `````` Robbert Krebbers committed Feb 20, 2019 21 ``````Definition set_map `{Elements A C, Singleton B D, Empty D, Union D} `````` Robbert Krebbers committed Oct 04, 2018 22 `````` (f : A → B) (X : C) : D := `````` Robbert Krebbers committed Feb 20, 2019 23 24 `````` list_to_set (f <\$> elements X). Typeclasses Opaque set_map. `````` Robbert Krebbers committed Oct 04, 2018 25 `````` `````` Robbert Krebbers committed Mar 03, 2019 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 ``````Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C := fresh ∘ elements. Typeclasses Opaque set_filter. (** We generalize the [fresh] operation on sets to generate lists of fresh elements w.r.t. a set [X]. *) Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C} (n : nat) (X : C) : list A := match n with | 0 => [] | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X) end. Instance: Params (@fresh_list) 6 := {}. (** The following inductive predicate classifies that a list of elements is in fact fresh w.r.t. a set [X]. *) Inductive Forall_fresh `{ElemOf A C} (X : C) : list A → Prop := | Forall_fresh_nil : Forall_fresh X [] | Forall_fresh_cons x xs : x ∉ xs → x ∉ X → Forall_fresh X xs → Forall_fresh X (x :: xs). (** Properties **) `````` Robbert Krebbers committed Feb 20, 2019 48 49 ``````Section fin_set. Context `{FinSet A C}. `````` Robbert Krebbers committed Nov 18, 2015 50 ``````Implicit Types X Y : C. `````` Robbert Krebbers committed Jun 11, 2012 51 `````` `````` Robbert Krebbers committed Feb 20, 2019 52 ``````Lemma fin_set_finite X : set_finite X. `````` Robbert Krebbers committed Dec 11, 2015 53 ``````Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed. `````` Robbert Krebbers committed Jul 22, 2016 54 `````` `````` Robbert Krebbers committed Apr 05, 2018 55 ``````Instance elem_of_dec_slow : RelDecision (∈@{C}) | 100. `````` Robbert Krebbers committed Jul 22, 2016 56 ``````Proof. `````` 57 `````` refine (λ x X, cast_if (decide_rel (∈) x (elements X))); `````` Robbert Krebbers committed Jul 22, 2016 58 59 60 61 `````` by rewrite <-(elem_of_elements _). Defined. (** * The [elements] operation *) `````` Robbert Krebbers committed Feb 20, 2019 62 ``````Global Instance set_unfold_elements X x P : `````` 63 64 `````` SetUnfoldElemOf x X P → SetUnfoldElemOf x (elements X) P. Proof. constructor. by rewrite elem_of_elements, (set_unfold_elem_of x X P). Qed. `````` Robbert Krebbers committed Feb 20, 2019 65 `````` `````` Robbert Krebbers committed Nov 18, 2015 66 ``````Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)). `````` Robbert Krebbers committed Jun 11, 2012 67 68 ``````Proof. intros ?? E. apply NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 69 70 71 `````` - apply NoDup_elements. - apply NoDup_elements. - intros. by rewrite !elem_of_elements, E. `````` Robbert Krebbers committed Jun 11, 2012 72 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 73 `````` `````` Robbert Krebbers committed Feb 17, 2016 74 75 76 77 78 ``````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 79 80 81 82 83 84 85 86 87 88 89 ``````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 90 91 92 93 94 95 96 97 98 ``````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. `````` Robbert Krebbers committed Sep 17, 2017 99 ``````Lemma elements_singleton x : elements ({[ x ]} : C) = [x]. `````` Robbert Krebbers committed Feb 17, 2016 100 101 ``````Proof. apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}), `````` Robbert Krebbers committed Feb 17, 2016 102 `````` elements_union_singleton, elements_empty by set_solver. `````` Robbert Krebbers committed Feb 17, 2016 103 ``````Qed. `````` Dan Frumin committed Apr 19, 2019 104 105 106 107 108 109 110 111 ``````Lemma elements_disj_union (X Y : C) : X ## Y → elements (X ∪ Y) ≡ₚ elements X ++ elements Y. Proof. intros HXY. apply NoDup_Permutation. - apply NoDup_elements. - apply NoDup_app. set_solver by eauto using NoDup_elements. - set_solver. Qed. `````` Robbert Krebbers committed Jan 31, 2017 112 ``````Lemma elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y. `````` Robbert Krebbers committed Feb 17, 2016 113 ``````Proof. `````` Robbert Krebbers committed Sep 17, 2017 114 `````` intros; apply NoDup_submseteq; eauto using NoDup_elements. `````` Robbert Krebbers committed Feb 17, 2016 115 116 117 `````` intros x. rewrite !elem_of_elements; auto. Qed. `````` Robbert Krebbers committed Jul 22, 2016 118 ``````(** * The [size] operation *) `````` Robbert Krebbers committed Feb 20, 2019 119 ``````Global Instance set_size_proper: Proper ((≡) ==> (=)) (@size C _). `````` Robbert Krebbers committed Oct 19, 2012 120 ``````Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. `````` Robbert Krebbers committed Jul 22, 2016 121 `````` `````` Robbert Krebbers committed Nov 12, 2012 122 ``````Lemma size_empty : size (∅ : C) = 0. `````` Robbert Krebbers committed Feb 20, 2019 123 ``````Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed. `````` Robbert Krebbers committed Nov 12, 2012 124 ``````Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅. `````` Robbert Krebbers committed Jun 11, 2012 125 ``````Proof. `````` Robbert Krebbers committed Dec 11, 2015 126 127 `````` 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 128 ``````Qed. `````` Robbert Krebbers committed Nov 12, 2012 129 ``````Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅. `````` Robbert Krebbers committed Dec 11, 2015 130 ``````Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed. `````` Robbert Krebbers committed Jan 05, 2013 131 132 ``````Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅. Proof. by rewrite size_empty_iff. Qed. `````` Robbert Krebbers committed Jul 22, 2016 133 `````` `````` Robbert Krebbers committed Feb 20, 2019 134 ``````Lemma set_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅. `````` Robbert Krebbers committed Oct 19, 2012 135 ``````Proof. `````` Robbert Krebbers committed Jun 05, 2014 136 `````` destruct (elements X) as [|x l] eqn:HX; [right|left]. `````` Robbert Krebbers committed Feb 17, 2016 137 138 `````` - 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 139 ``````Qed. `````` Robbert Krebbers committed Feb 20, 2019 140 141 142 143 ``````Lemma set_choose X : X ≢ ∅ → ∃ x, x ∈ X. Proof. intros. by destruct (set_choose_or_empty X). Qed. Lemma set_choose_L `{!LeibnizEquiv C} X : X ≠ ∅ → ∃ x, x ∈ X. Proof. unfold_leibniz. apply set_choose. Qed. `````` Robbert Krebbers committed May 11, 2013 144 ``````Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X. `````` Robbert Krebbers committed Aug 29, 2012 145 ``````Proof. `````` Robbert Krebbers committed Feb 20, 2019 146 `````` intros Hsz. destruct (set_choose_or_empty X) as [|HX]; [done|]. `````` Robbert Krebbers committed Jun 05, 2014 147 `````` contradict Hsz. rewrite HX, size_empty; lia. `````` Robbert Krebbers committed Jun 11, 2012 148 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 149 `````` `````` Robbert Krebbers committed Sep 17, 2017 150 ``````Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1. `````` Robbert Krebbers committed Feb 20, 2019 151 ``````Proof. unfold size, set_size. simpl. by rewrite elements_singleton. Qed. `````` Robbert Krebbers committed Jul 22, 2016 152 153 ``````Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y. Proof. `````` Robbert Krebbers committed Feb 20, 2019 154 `````` unfold size, set_size. simpl. rewrite <-!elem_of_elements. `````` Robbert Krebbers committed Jul 22, 2016 155 156 157 `````` 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 158 ``````Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}. `````` Robbert Krebbers committed Jun 11, 2012 159 ``````Proof. `````` Robbert Krebbers committed May 11, 2013 160 161 `````` intros E. destruct (size_pos_elem_of X); auto with lia. exists x. apply elem_of_equiv. split. `````` Robbert Krebbers committed Feb 17, 2016 162 `````` - rewrite elem_of_singleton. eauto using size_singleton_inv. `````` Robbert Krebbers committed Feb 17, 2016 163 `````` - set_solver. `````` Robbert Krebbers committed Jun 11, 2012 164 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 165 `````` `````` 166 ``````Lemma size_union X Y : X ## Y → size (X ∪ Y) = size X + size Y. `````` Robbert Krebbers committed Jun 11, 2012 167 ``````Proof. `````` Robbert Krebbers committed Feb 20, 2019 168 `````` intros. unfold size, set_size. simpl. rewrite <-app_length. `````` Robbert Krebbers committed Jun 11, 2012 169 `````` apply Permutation_length, NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 170 171 `````` - apply NoDup_elements. - apply NoDup_app; repeat split; try apply NoDup_elements. `````` Robbert Krebbers committed Feb 17, 2016 172 `````` intros x; rewrite !elem_of_elements; set_solver. `````` Robbert Krebbers committed Feb 17, 2016 173 `````` - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. `````` Robbert Krebbers committed Jun 11, 2012 174 175 ``````Qed. Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). `````` Robbert Krebbers committed Aug 29, 2012 176 ``````Proof. `````` Robbert Krebbers committed Feb 17, 2016 177 178 179 `````` 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 180 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 181 `````` `````` Robbert Krebbers committed Jun 11, 2012 182 ``````Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y. `````` Robbert Krebbers committed May 11, 2013 183 ``````Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed. `````` Robbert Krebbers committed Jan 05, 2013 184 ``````Lemma subset_size X Y : X ⊂ Y → size X < size Y. `````` Robbert Krebbers committed Jun 11, 2012 185 ``````Proof. `````` Robbert Krebbers committed Feb 17, 2016 186 `````` intros. rewrite (union_difference X Y) by set_solver. `````` Robbert Krebbers committed Jan 05, 2013 187 188 189 `````` 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 190 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 191 192 `````` (** * Induction principles *) `````` Robbert Krebbers committed Feb 20, 2019 193 ``````Lemma set_wf : wf (⊂@{C}). `````` Robbert Krebbers committed Aug 21, 2013 194 ``````Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed. `````` Robbert Krebbers committed Feb 20, 2019 195 ``````Lemma set_ind (P : C → Prop) : `````` Robbert Krebbers committed Aug 29, 2012 196 `````` Proper ((≡) ==> iff) P → `````` Robbert Krebbers committed May 11, 2013 197 `````` P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X. `````` Robbert Krebbers committed Jun 11, 2012 198 ``````Proof. `````` Robbert Krebbers committed Jan 05, 2013 199 `````` intros ? Hemp Hadd. apply well_founded_induction with (⊂). `````` Robbert Krebbers committed Feb 20, 2019 200 201 `````` { apply set_wf. } intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX]. `````` Robbert Krebbers committed Feb 17, 2016 202 203 `````` - rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd. set_solver. apply IH; set_solver. `````` Robbert Krebbers committed Feb 17, 2016 204 `````` - by rewrite HX. `````` Robbert Krebbers committed Jun 11, 2012 205 ``````Qed. `````` Robbert Krebbers committed Feb 20, 2019 206 ``````Lemma set_ind_L `{!LeibnizEquiv C} (P : C → Prop) : `````` Robbert Krebbers committed Sep 28, 2016 207 `````` P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X. `````` Robbert Krebbers committed Feb 20, 2019 208 ``````Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed. `````` Robbert Krebbers committed Jul 22, 2016 209 `````` `````` Robbert Krebbers committed Feb 20, 2019 210 211 ``````(** * The [set_fold] operation *) Lemma set_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) : `````` Robbert Krebbers committed Jun 11, 2012 212 `````` Proper ((=) ==> (≡) ==> iff) P → `````` Robbert Krebbers committed Jun 17, 2013 213 `````` P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) → `````` Robbert Krebbers committed Feb 20, 2019 214 `````` ∀ X, P (set_fold f b X) X. `````` Robbert Krebbers committed Jun 11, 2012 215 216 ``````Proof. intros ? Hemp Hadd. `````` Robbert Krebbers committed Nov 12, 2012 217 `````` cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X). `````` Robbert Krebbers committed Jun 05, 2014 218 219 `````` { intros help ?. apply help; [apply NoDup_elements|]. symmetry. apply elem_of_elements. } `````` Robbert Krebbers committed Jan 05, 2013 220 `````` induction 1 as [|x l ?? IH]; simpl. `````` Robbert Krebbers committed Feb 17, 2016 221 `````` - intros X HX. setoid_rewrite elem_of_nil in HX. `````` Robbert Krebbers committed Feb 17, 2016 222 `````` rewrite equiv_empty. done. set_solver. `````` Robbert Krebbers committed Feb 17, 2016 223 `````` - intros X HX. setoid_rewrite elem_of_cons in HX. `````` Robbert Krebbers committed Feb 17, 2016 224 225 `````` rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd. set_solver. apply IH. set_solver. `````` Robbert Krebbers committed Jun 11, 2012 226 ``````Qed. `````` Robbert Krebbers committed Feb 20, 2019 227 ``````Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R} `````` Robbert Krebbers committed May 07, 2013 228 `````` (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f} `````` Robbert Krebbers committed Nov 12, 2012 229 `````` (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) : `````` Robbert Krebbers committed Feb 20, 2019 230 `````` Proper ((≡) ==> R) (set_fold f b : C → B). `````` Robbert Krebbers committed May 11, 2013 231 ``````Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed. `````` Robbert Krebbers committed Jul 22, 2016 232 `````` `````` Dan Frumin committed Apr 19, 2019 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 ``````Lemma set_fold_empty {B} (f : A → B → B) (b : B) : set_fold f b (∅ : C) = b. Proof. by unfold set_fold; simpl; rewrite elements_empty. Qed. Lemma set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) : set_fold f b ({[a]} : C) = f a b. Proof. by unfold set_fold; simpl; rewrite elements_singleton. Qed. Lemma set_fold_disj_union (f : A → A → A) (b : A) X Y : Comm (=) f → Assoc (=) f → X ## Y → set_fold f b (X ∪ Y) = set_fold f (set_fold f b X) Y. Proof. intros Hcomm Hassoc Hdisj. unfold set_fold; simpl. by rewrite elements_disj_union, <- foldr_app, (comm (++)). Qed. `````` Robbert Krebbers committed Nov 21, 2016 249 ``````(** * Minimal elements *) `````` 250 ``````Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) : `````` Robbert Krebbers committed Nov 20, 2016 251 252 `````` X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X. Proof. `````` Robbert Krebbers committed Feb 20, 2019 253 `````` pattern X; apply set_ind; clear X. `````` Robbert Krebbers committed Nov 20, 2016 254 255 `````` { by intros X X' HX; setoid_rewrite HX. } { done. } `````` Robbert Krebbers committed Feb 20, 2019 256 `````` intros x X ? IH Hemp. destruct (set_choose_or_empty X) as [[z ?]|HX]. `````` Robbert Krebbers committed Nov 20, 2016 257 258 259 `````` { destruct IH as (x' & Hx' & Hmin); [set_solver|]. destruct (decide (R x x')). - exists x; split; [set_solver|]. `````` Robbert Krebbers committed Sep 17, 2017 260 `````` eauto using (union_minimal (C:=C)), (singleton_minimal (C:=C)), minimal_weaken. `````` Robbert Krebbers committed Nov 20, 2016 261 `````` - exists x'; split; [set_solver|]. `````` Robbert Krebbers committed Sep 17, 2017 262 `````` eauto using (union_minimal (C:=C)), (singleton_minimal_not_above (C:=C)). } `````` Robbert Krebbers committed Nov 20, 2016 263 264 265 `````` exists x; split; [set_solver|]. rewrite HX, (right_id _ (∪)). apply singleton_minimal. Qed. `````` 266 267 ``````Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R, ∀ x y, Decision (R x y)} (X : C) : `````` Robbert Krebbers committed Nov 20, 2016 268 `````` X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X. `````` 269 ``````Proof. unfold_leibniz. apply (minimal_exists R). Qed. `````` Robbert Krebbers committed Nov 20, 2016 270 `````` `````` Robbert Krebbers committed Nov 21, 2016 271 ``````(** * Filter *) `````` Robbert Krebbers committed Nov 21, 2016 272 273 274 275 276 ``````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. `````` Robbert Krebbers committed Feb 20, 2019 277 278 `````` unfold filter, set_filter. by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements. `````` Robbert Krebbers committed Nov 21, 2016 279 280 `````` Qed. Global Instance set_unfold_filter X Q : `````` 281 `````` SetUnfoldElemOf x X Q → SetUnfoldElemOf x (filter P X) (P x ∧ Q). `````` Robbert Krebbers committed Nov 21, 2016 282 `````` Proof. `````` 283 `````` intros ??; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q). `````` Robbert Krebbers committed Nov 21, 2016 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 `````` 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 307 `````` `````` Robbert Krebbers committed Oct 04, 2018 308 309 ``````(** * Map *) Section map. `````` Robbert Krebbers committed Feb 20, 2019 310 `````` Context `{Set_ B D}. `````` Robbert Krebbers committed Oct 04, 2018 311 312 `````` Lemma elem_of_map (f : A → B) (X : C) y : `````` Robbert Krebbers committed Feb 20, 2019 313 `````` y ∈ set_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X. `````` Robbert Krebbers committed Oct 04, 2018 314 `````` Proof. `````` Robbert Krebbers committed Feb 20, 2019 315 `````` unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap. `````` Robbert Krebbers committed Oct 04, 2018 316 317 318 `````` by setoid_rewrite elem_of_elements. Qed. Global Instance set_unfold_map (f : A → B) (X : C) (P : A → Prop) : `````` 319 320 `````` (∀ y, SetUnfoldElemOf y X (P y)) → SetUnfoldElemOf x (set_map (D:=D) f X) (∃ y, x = f y ∧ P y). `````` Robbert Krebbers committed Oct 04, 2018 321 322 `````` Proof. constructor. rewrite elem_of_map; naive_solver. Qed. `````` Robbert Krebbers committed Feb 20, 2019 323 324 `````` Global Instance set_map_proper : Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (set_map (C:=C) (D:=D)). `````` Robbert Krebbers committed Oct 04, 2018 325 `````` Proof. intros f g ? X Y. set_unfold; naive_solver. Qed. `````` Robbert Krebbers committed Feb 20, 2019 326 327 `````` Global Instance set_map_mono : Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (set_map (C:=C) (D:=D)). `````` Robbert Krebbers committed Oct 04, 2018 328 329 330 `````` Proof. intros f g ? X Y. set_unfold; naive_solver. Qed. Lemma elem_of_map_1 (f : A → B) (X : C) (y : B) : `````` Robbert Krebbers committed Feb 20, 2019 331 `````` y ∈ set_map (D:=D) f X → ∃ x, y = f x ∧ x ∈ X. `````` Robbert Krebbers committed Oct 04, 2018 332 333 `````` Proof. set_solver. Qed. Lemma elem_of_map_2 (f : A → B) (X : C) (x : A) : `````` Robbert Krebbers committed Feb 20, 2019 334 `````` x ∈ X → f x ∈ set_map (D:=D) f X. `````` Robbert Krebbers committed Oct 04, 2018 335 336 `````` Proof. set_solver. Qed. Lemma elem_of_map_2_alt (f : A → B) (X : C) (x : A) (y : B) : `````` Robbert Krebbers committed Feb 20, 2019 337 `````` x ∈ X → y = f x → y ∈ set_map (D:=D) f X. `````` Robbert Krebbers committed Oct 04, 2018 338 339 340 `````` Proof. set_solver. Qed. End map. `````` Robbert Krebbers committed Jul 22, 2016 341 ``````(** * Decision procedures *) `````` Robbert Krebbers committed Nov 22, 2016 342 343 344 345 346 ``````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 347 ``````Lemma set_Forall_Exists_dec (P Q : A → Prop) (dec : ∀ x, {P x} + {Q x}) X : `````` Robbert Krebbers committed Nov 22, 2016 348 349 `````` {set_Forall P X} + {set_Exists Q X}. Proof. `````` Robbert Krebbers committed Nov 23, 2016 350 `````` refine (cast_if (Forall_Exists_dec P Q dec (elements X))); `````` Robbert Krebbers committed Nov 22, 2016 351 352 353 354 355 `````` [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 356 ``````Proof. intro. by destruct (set_Forall_Exists_dec P (not ∘ P) dec X). Qed. `````` Robbert Krebbers committed Nov 22, 2016 357 358 359 ``````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 360 361 `````` by destruct (set_Forall_Exists_dec (not ∘ P) P (λ x, swap_if (decide (P x))) X). `````` Robbert Krebbers committed Nov 22, 2016 362 363 364 365 ``````Qed. 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 366 ``````Proof. `````` Robbert Krebbers committed Nov 22, 2016 367 368 `````` refine (cast_if (decide (Forall P (elements X)))); by rewrite set_Forall_elements. `````` Robbert Krebbers committed Oct 19, 2012 369 ``````Defined. `````` Robbert Krebbers committed May 07, 2013 370 371 ``````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 372 ``````Proof. `````` Robbert Krebbers committed Nov 22, 2016 373 374 `````` refine (cast_if (decide (Exists P (elements X)))); by rewrite set_Exists_elements. `````` Robbert Krebbers committed Oct 19, 2012 375 ``````Defined. `````` Robbert Krebbers committed Feb 20, 2019 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 `````` (** Alternative versions of finite and infinite predicates *) Lemma pred_finite_set (P : A → Prop) : pred_finite P ↔ (∃ X : C, ∀ x, P x → x ∈ X). Proof. split. - intros [xs Hfin]. exists (list_to_set xs). set_solver. - intros [X Hfin]. exists (elements X). set_solver. Qed. Lemma pred_infinite_set (P : A → Prop) : pred_infinite P ↔ (∀ X : C, ∃ x, P x ∧ x ∉ X). Proof. split. - intros Hinf X. destruct (Hinf (elements X)). set_solver. - intros Hinf xs. destruct (Hinf (list_to_set xs)). set_solver. Qed. `````` Robbert Krebbers committed Mar 03, 2019 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 `````` Section infinite. Context `{Infinite A}. (** Properties about the [fresh] operation on finite sets *) Global Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh. Proof. unfold fresh, set_fresh. solve_proper. Qed. Lemma is_fresh X : fresh X ∉ X. Proof. unfold fresh, set_fresh. rewrite <-elem_of_elements. apply infinite_is_fresh. Qed. Lemma exist_fresh X : ∃ x, x ∉ X. Proof. exists (fresh X). apply is_fresh. Qed. (** Properties about the [fresh_list] operation on finite sets *) Global Instance fresh_list_proper n : Proper ((≡@{C}) ==> (=)) (fresh_list n). Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed. Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs → NoDup xs. Proof. induction 1; by constructor. Qed. Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs → x ∈ xs → x ∉ X. Proof. intros HX; revert x; rewrite <-Forall_forall. by induction HX; constructor. Qed. Lemma Forall_fresh_alt X xs : Forall_fresh X xs ↔ NoDup xs ∧ ∀ x, x ∈ xs → x ∉ X. Proof. split; eauto using Forall_fresh_NoDup, Forall_fresh_elem_of. rewrite <-Forall_forall. intros [Hxs Hxs']. induction Hxs; decompose_Forall_hyps; constructor; auto. Qed. Lemma Forall_fresh_subseteq X Y xs : Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs. Proof. rewrite !Forall_fresh_alt; set_solver. Qed. Lemma fresh_list_length n X : length (fresh_list n X) = n. Proof. revert X. induction n; simpl; auto. Qed. Lemma fresh_list_is_fresh n X x : x ∈ fresh_list n X → x ∉ X. Proof. revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|]. rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|]. apply IH in Hin; set_solver. Qed. Lemma NoDup_fresh_list n X : NoDup (fresh_list n X). Proof. revert X. induction n; simpl; constructor; auto. intros Hin; apply fresh_list_is_fresh in Hin; set_solver. Qed. Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X). Proof. rewrite Forall_fresh_alt; eauto using NoDup_fresh_list, fresh_list_is_fresh. Qed. End infinite. `````` Robbert Krebbers committed Feb 20, 2019 447 ``End fin_set.``