fin_sets.v 13.2 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 Feb 20, 2019 10 11 ``````Instance set_size `{Elements A C} : Size C := length ∘ elements. Definition set_fold `{Elements A C} {B} `````` Robbert Krebbers committed Nov 12, 2012 12 `````` (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements. `````` Robbert Krebbers committed Jun 11, 2012 13 `````` `````` Robbert Krebbers committed Feb 20, 2019 14 ``````Instance set_filter `````` Robbert Krebbers committed Nov 21, 2016 15 `````` `{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X, `````` Robbert Krebbers committed Feb 20, 2019 16 17 `````` list_to_set (filter P (elements X)). Typeclasses Opaque set_filter. `````` Robbert Krebbers committed Nov 21, 2016 18 `````` `````` Robbert Krebbers committed Feb 20, 2019 19 ``````Definition set_map `{Elements A C, Singleton B D, Empty D, Union D} `````` Robbert Krebbers committed Oct 04, 2018 20 `````` (f : A → B) (X : C) : D := `````` Robbert Krebbers committed Feb 20, 2019 21 22 `````` list_to_set (f <\$> elements X). Typeclasses Opaque set_map. `````` Robbert Krebbers committed Oct 04, 2018 23 `````` `````` Robbert Krebbers committed Feb 20, 2019 24 25 ``````Section fin_set. Context `{FinSet A C}. `````` Robbert Krebbers committed Nov 18, 2015 26 ``````Implicit Types X Y : C. `````` Robbert Krebbers committed Jun 11, 2012 27 `````` `````` Robbert Krebbers committed Feb 20, 2019 28 ``````Lemma fin_set_finite X : set_finite X. `````` Robbert Krebbers committed Dec 11, 2015 29 ``````Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed. `````` Robbert Krebbers committed Jul 22, 2016 30 `````` `````` Robbert Krebbers committed Apr 05, 2018 31 ``````Instance elem_of_dec_slow : RelDecision (∈@{C}) | 100. `````` Robbert Krebbers committed Jul 22, 2016 32 ``````Proof. `````` 33 `````` refine (λ x X, cast_if (decide_rel (∈) x (elements X))); `````` Robbert Krebbers committed Jul 22, 2016 34 35 36 37 `````` by rewrite <-(elem_of_elements _). Defined. (** * The [elements] operation *) `````` Robbert Krebbers committed Feb 20, 2019 38 39 40 41 ``````Global Instance set_unfold_elements X x P : SetUnfold (x ∈ X) P → SetUnfold (x ∈ elements X) P. Proof. constructor. by rewrite elem_of_elements, (set_unfold (x ∈ X) P). Qed. `````` Robbert Krebbers committed Nov 18, 2015 42 ``````Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) (elements (C:=C)). `````` Robbert Krebbers committed Jun 11, 2012 43 44 ``````Proof. intros ?? E. apply NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 45 46 47 `````` - apply NoDup_elements. - apply NoDup_elements. - intros. by rewrite !elem_of_elements, E. `````` Robbert Krebbers committed Jun 11, 2012 48 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 49 `````` `````` Robbert Krebbers committed Feb 17, 2016 50 51 52 53 54 ``````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 55 56 57 58 59 60 61 62 63 64 65 ``````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 66 67 68 69 70 71 72 73 74 ``````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 75 ``````Lemma elements_singleton x : elements ({[ x ]} : C) = [x]. `````` Robbert Krebbers committed Feb 17, 2016 76 77 ``````Proof. apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}), `````` Robbert Krebbers committed Feb 17, 2016 78 `````` elements_union_singleton, elements_empty by set_solver. `````` Robbert Krebbers committed Feb 17, 2016 79 ``````Qed. `````` Robbert Krebbers committed Jan 31, 2017 80 ``````Lemma elements_submseteq X Y : X ⊆ Y → elements X ⊆+ elements Y. `````` Robbert Krebbers committed Feb 17, 2016 81 ``````Proof. `````` Robbert Krebbers committed Sep 17, 2017 82 `````` intros; apply NoDup_submseteq; eauto using NoDup_elements. `````` Robbert Krebbers committed Feb 17, 2016 83 84 85 `````` intros x. rewrite !elem_of_elements; auto. Qed. `````` Robbert Krebbers committed Jul 22, 2016 86 ``````(** * The [size] operation *) `````` Robbert Krebbers committed Feb 20, 2019 87 ``````Global Instance set_size_proper: Proper ((≡) ==> (=)) (@size C _). `````` Robbert Krebbers committed Oct 19, 2012 88 ``````Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed. `````` Robbert Krebbers committed Jul 22, 2016 89 `````` `````` Robbert Krebbers committed Nov 12, 2012 90 ``````Lemma size_empty : size (∅ : C) = 0. `````` Robbert Krebbers committed Feb 20, 2019 91 ``````Proof. unfold size, set_size. simpl. by rewrite elements_empty. Qed. `````` Robbert Krebbers committed Nov 12, 2012 92 ``````Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅. `````` Robbert Krebbers committed Jun 11, 2012 93 ``````Proof. `````` Robbert Krebbers committed Dec 11, 2015 94 95 `````` 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 96 ``````Qed. `````` Robbert Krebbers committed Nov 12, 2012 97 ``````Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅. `````` Robbert Krebbers committed Dec 11, 2015 98 ``````Proof. split. apply size_empty_inv. by intros ->; rewrite size_empty. Qed. `````` Robbert Krebbers committed Jan 05, 2013 99 100 ``````Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅. Proof. by rewrite size_empty_iff. Qed. `````` Robbert Krebbers committed Jul 22, 2016 101 `````` `````` Robbert Krebbers committed Feb 20, 2019 102 ``````Lemma set_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅. `````` Robbert Krebbers committed Oct 19, 2012 103 ``````Proof. `````` Robbert Krebbers committed Jun 05, 2014 104 `````` destruct (elements X) as [|x l] eqn:HX; [right|left]. `````` Robbert Krebbers committed Feb 17, 2016 105 106 `````` - 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 107 ``````Qed. `````` Robbert Krebbers committed Feb 20, 2019 108 109 110 111 ``````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 112 ``````Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X. `````` Robbert Krebbers committed Aug 29, 2012 113 ``````Proof. `````` Robbert Krebbers committed Feb 20, 2019 114 `````` intros Hsz. destruct (set_choose_or_empty X) as [|HX]; [done|]. `````` Robbert Krebbers committed Jun 05, 2014 115 `````` contradict Hsz. rewrite HX, size_empty; lia. `````` Robbert Krebbers committed Jun 11, 2012 116 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 117 `````` `````` Robbert Krebbers committed Sep 17, 2017 118 ``````Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1. `````` Robbert Krebbers committed Feb 20, 2019 119 ``````Proof. unfold size, set_size. simpl. by rewrite elements_singleton. Qed. `````` Robbert Krebbers committed Jul 22, 2016 120 121 ``````Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y. Proof. `````` Robbert Krebbers committed Feb 20, 2019 122 `````` unfold size, set_size. simpl. rewrite <-!elem_of_elements. `````` Robbert Krebbers committed Jul 22, 2016 123 124 125 `````` 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 126 ``````Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}. `````` Robbert Krebbers committed Jun 11, 2012 127 ``````Proof. `````` Robbert Krebbers committed May 11, 2013 128 129 `````` intros E. destruct (size_pos_elem_of X); auto with lia. exists x. apply elem_of_equiv. split. `````` Robbert Krebbers committed Feb 17, 2016 130 `````` - rewrite elem_of_singleton. eauto using size_singleton_inv. `````` Robbert Krebbers committed Feb 17, 2016 131 `````` - set_solver. `````` Robbert Krebbers committed Jun 11, 2012 132 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 133 `````` `````` 134 ``````Lemma size_union X Y : X ## Y → size (X ∪ Y) = size X + size Y. `````` Robbert Krebbers committed Jun 11, 2012 135 ``````Proof. `````` Robbert Krebbers committed Feb 20, 2019 136 `````` intros. unfold size, set_size. simpl. rewrite <-app_length. `````` Robbert Krebbers committed Jun 11, 2012 137 `````` apply Permutation_length, NoDup_Permutation. `````` Robbert Krebbers committed Feb 17, 2016 138 139 `````` - apply NoDup_elements. - apply NoDup_app; repeat split; try apply NoDup_elements. `````` Robbert Krebbers committed Feb 17, 2016 140 `````` intros x; rewrite !elem_of_elements; set_solver. `````` Robbert Krebbers committed Feb 17, 2016 141 `````` - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union. `````` Robbert Krebbers committed Jun 11, 2012 142 143 ``````Qed. Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X). `````` Robbert Krebbers committed Aug 29, 2012 144 ``````Proof. `````` Robbert Krebbers committed Feb 17, 2016 145 146 147 `````` 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 148 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 149 `````` `````` Robbert Krebbers committed Jun 11, 2012 150 ``````Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y. `````` Robbert Krebbers committed May 11, 2013 151 ``````Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed. `````` Robbert Krebbers committed Jan 05, 2013 152 ``````Lemma subset_size X Y : X ⊂ Y → size X < size Y. `````` Robbert Krebbers committed Jun 11, 2012 153 ``````Proof. `````` Robbert Krebbers committed Feb 17, 2016 154 `````` intros. rewrite (union_difference X Y) by set_solver. `````` Robbert Krebbers committed Jan 05, 2013 155 156 157 `````` 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 158 ``````Qed. `````` Robbert Krebbers committed Jul 22, 2016 159 160 `````` (** * Induction principles *) `````` Robbert Krebbers committed Feb 20, 2019 161 ``````Lemma set_wf : wf (⊂@{C}). `````` Robbert Krebbers committed Aug 21, 2013 162 ``````Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed. `````` Robbert Krebbers committed Feb 20, 2019 163 ``````Lemma set_ind (P : C → Prop) : `````` Robbert Krebbers committed Aug 29, 2012 164 `````` Proper ((≡) ==> iff) P → `````` Robbert Krebbers committed May 11, 2013 165 `````` P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X. `````` Robbert Krebbers committed Jun 11, 2012 166 ``````Proof. `````` Robbert Krebbers committed Jan 05, 2013 167 `````` intros ? Hemp Hadd. apply well_founded_induction with (⊂). `````` Robbert Krebbers committed Feb 20, 2019 168 169 `````` { apply set_wf. } intros X IH. destruct (set_choose_or_empty X) as [[x ?]|HX]. `````` Robbert Krebbers committed Feb 17, 2016 170 171 `````` - rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd. set_solver. apply IH; set_solver. `````` Robbert Krebbers committed Feb 17, 2016 172 `````` - by rewrite HX. `````` Robbert Krebbers committed Jun 11, 2012 173 ``````Qed. `````` Robbert Krebbers committed Feb 20, 2019 174 ``````Lemma set_ind_L `{!LeibnizEquiv C} (P : C → Prop) : `````` Robbert Krebbers committed Sep 28, 2016 175 `````` P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X. `````` Robbert Krebbers committed Feb 20, 2019 176 ``````Proof. apply set_ind. by intros ?? ->%leibniz_equiv_iff. Qed. `````` Robbert Krebbers committed Jul 22, 2016 177 `````` `````` Robbert Krebbers committed Feb 20, 2019 178 179 ``````(** * 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 180 `````` Proper ((=) ==> (≡) ==> iff) P → `````` Robbert Krebbers committed Jun 17, 2013 181 `````` P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) → `````` Robbert Krebbers committed Feb 20, 2019 182 `````` ∀ X, P (set_fold f b X) X. `````` Robbert Krebbers committed Jun 11, 2012 183 184 ``````Proof. intros ? Hemp Hadd. `````` Robbert Krebbers committed Nov 12, 2012 185 `````` cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X). `````` Robbert Krebbers committed Jun 05, 2014 186 187 `````` { intros help ?. apply help; [apply NoDup_elements|]. symmetry. apply elem_of_elements. } `````` Robbert Krebbers committed Jan 05, 2013 188 `````` induction 1 as [|x l ?? IH]; simpl. `````` Robbert Krebbers committed Feb 17, 2016 189 `````` - intros X HX. setoid_rewrite elem_of_nil in HX. `````` Robbert Krebbers committed Feb 17, 2016 190 `````` rewrite equiv_empty. done. set_solver. `````` Robbert Krebbers committed Feb 17, 2016 191 `````` - intros X HX. setoid_rewrite elem_of_cons in HX. `````` Robbert Krebbers committed Feb 17, 2016 192 193 `````` rewrite (union_difference {[ x ]} X) by set_solver. apply Hadd. set_solver. apply IH. set_solver. `````` Robbert Krebbers committed Jun 11, 2012 194 ``````Qed. `````` Robbert Krebbers committed Feb 20, 2019 195 ``````Lemma set_fold_proper {B} (R : relation B) `{!Equivalence R} `````` Robbert Krebbers committed May 07, 2013 196 `````` (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f} `````` Robbert Krebbers committed Nov 12, 2012 197 `````` (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) : `````` Robbert Krebbers committed Feb 20, 2019 198 `````` Proper ((≡) ==> R) (set_fold f b : C → B). `````` Robbert Krebbers committed May 11, 2013 199 ``````Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed. `````` Robbert Krebbers committed Jul 22, 2016 200 `````` `````` Robbert Krebbers committed Nov 21, 2016 201 ``````(** * Minimal elements *) `````` 202 ``````Lemma minimal_exists R `{!Transitive R, ∀ x y, Decision (R x y)} (X : C) : `````` Robbert Krebbers committed Nov 20, 2016 203 204 `````` X ≢ ∅ → ∃ x, x ∈ X ∧ minimal R x X. Proof. `````` Robbert Krebbers committed Feb 20, 2019 205 `````` pattern X; apply set_ind; clear X. `````` Robbert Krebbers committed Nov 20, 2016 206 207 `````` { by intros X X' HX; setoid_rewrite HX. } { done. } `````` Robbert Krebbers committed Feb 20, 2019 208 `````` intros x X ? IH Hemp. destruct (set_choose_or_empty X) as [[z ?]|HX]. `````` Robbert Krebbers committed Nov 20, 2016 209 210 211 `````` { destruct IH as (x' & Hx' & Hmin); [set_solver|]. destruct (decide (R x x')). - exists x; split; [set_solver|]. `````` Robbert Krebbers committed Sep 17, 2017 212 `````` eauto using (union_minimal (C:=C)), (singleton_minimal (C:=C)), minimal_weaken. `````` Robbert Krebbers committed Nov 20, 2016 213 `````` - exists x'; split; [set_solver|]. `````` Robbert Krebbers committed Sep 17, 2017 214 `````` eauto using (union_minimal (C:=C)), (singleton_minimal_not_above (C:=C)). } `````` Robbert Krebbers committed Nov 20, 2016 215 216 217 `````` exists x; split; [set_solver|]. rewrite HX, (right_id _ (∪)). apply singleton_minimal. Qed. `````` 218 219 ``````Lemma minimal_exists_L R `{!LeibnizEquiv C, !Transitive R, ∀ x y, Decision (R x y)} (X : C) : `````` Robbert Krebbers committed Nov 20, 2016 220 `````` X ≠ ∅ → ∃ x, x ∈ X ∧ minimal R x X. `````` 221 ``````Proof. unfold_leibniz. apply (minimal_exists R). Qed. `````` Robbert Krebbers committed Nov 20, 2016 222 `````` `````` Robbert Krebbers committed Nov 21, 2016 223 ``````(** * Filter *) `````` Robbert Krebbers committed Nov 21, 2016 224 225 226 227 228 ``````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 229 230 `````` unfold filter, set_filter. by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements. `````` Robbert Krebbers committed Nov 21, 2016 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 `````` Qed. Global Instance set_unfold_filter X Q : SetUnfold (x ∈ X) Q → SetUnfold (x ∈ filter P X) (P x ∧ Q). Proof. intros ??; constructor. by rewrite elem_of_filter, (set_unfold (x ∈ X) Q). 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 259 `````` `````` Robbert Krebbers committed Oct 04, 2018 260 261 ``````(** * Map *) Section map. `````` Robbert Krebbers committed Feb 20, 2019 262 `````` Context `{Set_ B D}. `````` Robbert Krebbers committed Oct 04, 2018 263 264 `````` Lemma elem_of_map (f : A → B) (X : C) y : `````` Robbert Krebbers committed Feb 20, 2019 265 `````` y ∈ set_map (D:=D) f X ↔ ∃ x, y = f x ∧ x ∈ X. `````` Robbert Krebbers committed Oct 04, 2018 266 `````` Proof. `````` Robbert Krebbers committed Feb 20, 2019 267 `````` unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap. `````` Robbert Krebbers committed Oct 04, 2018 268 269 270 271 `````` by setoid_rewrite elem_of_elements. Qed. Global Instance set_unfold_map (f : A → B) (X : C) (P : A → Prop) : (∀ y, SetUnfold (y ∈ X) (P y)) → `````` Robbert Krebbers committed Feb 20, 2019 272 `````` SetUnfold (x ∈ set_map (D:=D) f X) (∃ y, x = f y ∧ P y). `````` Robbert Krebbers committed Oct 04, 2018 273 274 `````` Proof. constructor. rewrite elem_of_map; naive_solver. Qed. `````` Robbert Krebbers committed Feb 20, 2019 275 276 `````` Global Instance set_map_proper : Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (set_map (C:=C) (D:=D)). `````` Robbert Krebbers committed Oct 04, 2018 277 `````` Proof. intros f g ? X Y. set_unfold; naive_solver. Qed. `````` Robbert Krebbers committed Feb 20, 2019 278 279 `````` Global Instance set_map_mono : Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (set_map (C:=C) (D:=D)). `````` Robbert Krebbers committed Oct 04, 2018 280 281 282 `````` 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 283 `````` y ∈ set_map (D:=D) f X → ∃ x, y = f x ∧ x ∈ X. `````` Robbert Krebbers committed Oct 04, 2018 284 285 `````` Proof. set_solver. Qed. Lemma elem_of_map_2 (f : A → B) (X : C) (x : A) : `````` Robbert Krebbers committed Feb 20, 2019 286 `````` x ∈ X → f x ∈ set_map (D:=D) f X. `````` Robbert Krebbers committed Oct 04, 2018 287 288 `````` 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 289 `````` x ∈ X → y = f x → y ∈ set_map (D:=D) f X. `````` Robbert Krebbers committed Oct 04, 2018 290 291 292 `````` Proof. set_solver. Qed. End map. `````` Robbert Krebbers committed Jul 22, 2016 293 ``````(** * Decision procedures *) `````` Robbert Krebbers committed Nov 22, 2016 294 295 296 297 298 ``````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 299 ``````Lemma set_Forall_Exists_dec (P Q : A → Prop) (dec : ∀ x, {P x} + {Q x}) X : `````` Robbert Krebbers committed Nov 22, 2016 300 301 `````` {set_Forall P X} + {set_Exists Q X}. Proof. `````` Robbert Krebbers committed Nov 23, 2016 302 `````` refine (cast_if (Forall_Exists_dec P Q dec (elements X))); `````` Robbert Krebbers committed Nov 22, 2016 303 304 305 306 307 `````` [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 308 ``````Proof. intro. by destruct (set_Forall_Exists_dec P (not ∘ P) dec X). Qed. `````` Robbert Krebbers committed Nov 22, 2016 309 310 311 ``````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 312 313 `````` by destruct (set_Forall_Exists_dec (not ∘ P) P (λ x, swap_if (decide (P x))) X). `````` Robbert Krebbers committed Nov 22, 2016 314 315 316 317 ``````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 318 ``````Proof. `````` Robbert Krebbers committed Nov 22, 2016 319 320 `````` refine (cast_if (decide (Forall P (elements X)))); by rewrite set_Forall_elements. `````` Robbert Krebbers committed Oct 19, 2012 321 ``````Defined. `````` Robbert Krebbers committed May 07, 2013 322 323 ``````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 324 ``````Proof. `````` Robbert Krebbers committed Nov 22, 2016 325 326 `````` refine (cast_if (decide (Exists P (elements X)))); by rewrite set_Exists_elements. `````` Robbert Krebbers committed Oct 19, 2012 327 ``````Defined. `````` Robbert Krebbers committed Feb 20, 2019 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 `````` (** 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 Feb 20, 2019 345 ``End fin_set.``