finite.v 11.8 KB
 Robbert Krebbers committed Nov 11, 2015 1 2 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) (* This file is distributed under the terms of the BSD license. *) `````` Robbert Krebbers committed Feb 13, 2016 3 ``````From prelude Require Export countable list. `````` Robbert Krebbers committed Nov 11, 2015 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 `````` Class Finite A `{∀ x y : A, Decision (x = y)} := { enum : list A; NoDup_enum : NoDup enum; elem_of_enum x : x ∈ enum }. Arguments enum _ {_ _} : clear implicits. Arguments NoDup_enum _ {_ _} : clear implicits. Definition card A `{Finite A} := length (enum A). Program Instance finite_countable `{Finite A} : Countable A := {| encode := λ x, Pos.of_nat \$ S \$ from_option 0 \$ fst <\$> list_find (x =) (enum A); decode := λ p, enum A !! pred (Pos.to_nat p) |}. Arguments Pos.of_nat _ : simpl never. Next Obligation. intros ?? [xs Hxs HA] x; unfold encode, decode; simpl. destruct (list_find_elem_of (x =) xs x) as [[i y] Hi]; auto. rewrite Nat2Pos.id by done; simpl; rewrite Hi; simpl. destruct (list_find_Some (x =) xs i y); naive_solver. Qed. Definition find `{Finite A} P `{∀ x, Decision (P x)} : option A := list_find P (enum A) ≫= decode_nat ∘ fst. Lemma encode_lt_card `{finA: Finite A} x : encode_nat x < card A. Proof. destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl. rewrite Nat2Pos.id by done; simpl. destruct (list_find _ xs) as [[i y]|] eqn:?; simpl. `````` Robbert Krebbers committed Feb 17, 2016 33 34 `````` - destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some. - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia. `````` Robbert Krebbers committed Nov 11, 2015 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 ``````Qed. Lemma encode_decode A `{finA: Finite A} i : i < card A → ∃ x, decode_nat i = Some x ∧ encode_nat x = i. Proof. destruct finA as [xs Hxs HA]. unfold encode_nat, decode_nat, encode, decode, card; simpl. intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx]. exists x. rewrite !Nat2Pos.id by done; simpl. destruct (list_find_elem_of (x =) xs x) as [[j y] Hj]; auto. destruct (list_find_Some (x =) xs j y) as [? ->]; auto. rewrite Hj; csimpl; eauto using NoDup_lookup. Qed. Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x : find P = Some x → P x. Proof. destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl. `````` Robbert Krebbers committed Feb 17, 2016 51 `````` intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_eq/=. `````` Robbert Krebbers committed Nov 11, 2015 52 53 54 55 56 57 58 59 `````` rewrite !Nat2Pos.id in Hx by done. destruct (list_find_Some P xs i y); naive_solver. Qed. Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x : P x → ∃ y, find P = Some y ∧ P y. Proof. destruct finA as [xs Hxs HA]; unfold find, decode; simpl. intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto. `````` Robbert Krebbers committed Feb 17, 2016 60 `````` rewrite Hi. destruct (list_find_Some P xs i y); simplify_eq/=; auto. `````` Robbert Krebbers committed Nov 11, 2015 61 62 63 64 65 `````` exists y. by rewrite !Nat2Pos.id by done. Qed. Lemma card_0_inv P `{finA: Finite A} : card A = 0 → A → P. Proof. `````` Robbert Krebbers committed Feb 17, 2016 66 `````` intros ? x. destruct finA as [[|??] ??]; simplify_eq. `````` Robbert Krebbers committed Nov 11, 2015 67 68 69 70 `````` by destruct (not_elem_of_nil x). Qed. Lemma finite_inhabited A `{finA: Finite A} : 0 < card A → Inhabited A. Proof. `````` Robbert Krebbers committed Nov 17, 2015 71 `````` unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|]. `````` Robbert Krebbers committed Nov 11, 2015 72 73 `````` constructor; exact x. Qed. `````` Robbert Krebbers committed Feb 11, 2016 74 75 ``````Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A → B) `{!Inj (=) (=) f} : f <\$> enum A `contains` enum B. `````` Robbert Krebbers committed Nov 11, 2015 76 77 78 ``````Proof. intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2. Qed. `````` Robbert Krebbers committed Feb 11, 2016 79 80 ``````Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A → B) `{!Inj (=) (=) f} : card A = card B → f <\$> enum A ≡ₚ enum B. `````` Robbert Krebbers committed Nov 11, 2015 81 82 ``````Proof. intros. apply contains_Permutation_length_eq. `````` Robbert Krebbers committed Feb 17, 2016 83 84 `````` - by rewrite fmap_length. - by apply finite_inj_contains. `````` Robbert Krebbers committed Nov 11, 2015 85 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 86 87 ``````Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A → B) `{!Inj (=) (=) f} : card A = card B → Surj (=) f. `````` Robbert Krebbers committed Nov 11, 2015 88 89 ``````Proof. intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto. `````` Robbert Krebbers committed Feb 11, 2016 90 `````` rewrite finite_inj_Permutation; auto using elem_of_enum. `````` Robbert Krebbers committed Nov 11, 2015 91 92 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 93 94 ``````Lemma finite_surj A `{Finite A} B `{Finite B} : 0 < card A ≤ card B → ∃ g : B → A, Surj (=) g. `````` Robbert Krebbers committed Nov 11, 2015 95 96 97 98 99 100 101 ``````Proof. intros [??]. destruct (finite_inhabited A) as [x']; auto with lia. exists (λ y : B, from_option x' (decode_nat (encode_nat y))). intros x. destruct (encode_decode B (encode_nat x)) as (y&Hy1&Hy2). { pose proof (encode_lt_card x); lia. } exists y. by rewrite Hy2, decode_encode_nat. Qed. `````` Robbert Krebbers committed Feb 11, 2016 102 103 ``````Lemma finite_inj A `{Finite A} B `{Finite B} : card A ≤ card B ↔ ∃ f : A → B, Inj (=) (=) f. `````` Robbert Krebbers committed Nov 11, 2015 104 105 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 106 `````` - intros. destruct (decide (card A = 0)) as [HA|?]. `````` Robbert Krebbers committed Nov 11, 2015 107 `````` { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). } `````` Robbert Krebbers committed Feb 11, 2016 108 109 `````` destruct (finite_surj A B) as (g&?); auto with lia. destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj. `````` Robbert Krebbers committed Feb 17, 2016 110 `````` - intros [f ?]. unfold card. rewrite <-(fmap_length f). `````` Robbert Krebbers committed Feb 11, 2016 111 `````` by apply contains_length, (finite_inj_contains f). `````` Robbert Krebbers committed Nov 11, 2015 112 113 ``````Qed. Lemma finite_bijective A `{Finite A} B `{Finite B} : `````` Robbert Krebbers committed Feb 11, 2016 114 `````` card A = card B ↔ ∃ f : A → B, Inj (=) (=) f ∧ Surj (=) f. `````` Robbert Krebbers committed Nov 11, 2015 115 116 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 117 `````` - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia. `````` Robbert Krebbers committed Feb 11, 2016 118 `````` exists f; auto using (finite_inj_surj f). `````` Robbert Krebbers committed Feb 17, 2016 119 `````` - intros (f&?&?). apply (anti_symm (≤)); apply finite_inj. `````` Robbert Krebbers committed Nov 11, 2015 120 `````` + by exists f. `````` Robbert Krebbers committed Feb 11, 2016 121 `````` + destruct (surj_cancel f) as (g&?); eauto using cancel_inj. `````` Robbert Krebbers committed Nov 11, 2015 122 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 123 124 125 126 127 ``````Lemma inj_card `{Finite A} `{Finite B} (f : A → B) `{!Inj (=) (=) f} : card A ≤ card B. Proof. apply finite_inj. eauto. Qed. Lemma surj_card `{Finite A} `{Finite B} (f : A → B) `{!Surj (=) f} : card B ≤ card A. `````` Robbert Krebbers committed Nov 11, 2015 128 ``````Proof. `````` Robbert Krebbers committed Feb 11, 2016 129 130 `````` destruct (surj_cancel f) as (g&?). apply inj_card with g, cancel_inj. `````` Robbert Krebbers committed Nov 11, 2015 131 132 ``````Qed. Lemma bijective_card `{Finite A} `{Finite B} (f : A → B) `````` Robbert Krebbers committed Feb 11, 2016 133 `````` `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B. `````` Robbert Krebbers committed Nov 11, 2015 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 ``````Proof. apply finite_bijective. eauto. Qed. (** Decidability of quantification over finite types *) Section forall_exists. Context `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)}. Lemma Forall_finite : Forall P (enum A) ↔ (∀ x, P x). Proof. rewrite Forall_forall. intuition auto using elem_of_enum. Qed. Lemma Exists_finite : Exists P (enum A) ↔ (∃ x, P x). Proof. rewrite Exists_exists. naive_solver eauto using elem_of_enum. Qed. Global Instance forall_dec: Decision (∀ x, P x). Proof. refine (cast_if (decide (Forall P (enum A)))); abstract by rewrite <-Forall_finite. Defined. Global Instance exists_dec: Decision (∃ x, P x). Proof. refine (cast_if (decide (Exists P (enum A)))); abstract by rewrite <-Exists_finite. Defined. End forall_exists. (** Instances *) Section enc_finite. Context `{∀ x y : A, Decision (x = y)}. Context (to_nat : A → nat) (of_nat : nat → A) (c : nat). Context (of_to_nat : ∀ x, of_nat (to_nat x) = x). Context (to_nat_c : ∀ x, to_nat x < c). Context (to_of_nat : ∀ i, i < c → to_nat (of_nat i) = i). Program Instance enc_finite : Finite A := {| enum := of_nat <\$> seq 0 c |}. Next Obligation. apply NoDup_alt. intros i j x. rewrite !list_lookup_fmap. intros Hi Hj. destruct (seq _ _ !! i) as [i'|] eqn:Hi', `````` Robbert Krebbers committed Feb 17, 2016 169 `````` (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=. `````` Robbert Krebbers committed Nov 11, 2015 170 171 172 173 174 175 176 177 178 179 180 181 182 `````` destruct (lookup_seq_inv _ _ _ _ Hi'), (lookup_seq_inv _ _ _ _ Hj'); subst. rewrite <-(to_of_nat i), <-(to_of_nat j) by done. by f_equal. Qed. Next Obligation. intros x. rewrite elem_of_list_fmap. exists (to_nat x). split; auto. by apply elem_of_list_lookup_2 with (to_nat x), lookup_seq. Qed. Lemma enc_finite_card : card A = c. Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed. End enc_finite. Section bijective_finite. Context `{Finite A, ∀ x y : B, Decision (x = y)} (f : A → B) (g : B → A). `````` Robbert Krebbers committed Feb 11, 2016 183 `````` Context `{!Inj (=) (=) f, !Cancel (=) f g}. `````` Robbert Krebbers committed Nov 11, 2015 184 185 186 187 188 189 190 191 192 193 194 195 `````` Program Instance bijective_finite: Finite B := {| enum := f <\$> enum A |}. Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed. Next Obligation. intros y. rewrite elem_of_list_fmap. eauto using elem_of_enum. Qed. End bijective_finite. Program Instance option_finite `{Finite A} : Finite (option A) := {| enum := None :: Some <\$> enum A |}. Next Obligation. constructor. `````` Robbert Krebbers committed Feb 17, 2016 196 197 `````` - rewrite elem_of_list_fmap. by intros (?&?&?). - apply (NoDup_fmap_2 _); auto using NoDup_enum. `````` Robbert Krebbers committed Nov 11, 2015 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 ``````Qed. Next Obligation. intros ??? [x|]; [right|left]; auto. apply elem_of_list_fmap. eauto using elem_of_enum. Qed. Lemma option_cardinality `{Finite A} : card (option A) = S (card A). Proof. unfold card. simpl. by rewrite fmap_length. Qed. Program Instance unit_finite : Finite () := {| enum := [tt] |}. Next Obligation. apply NoDup_singleton. Qed. Next Obligation. intros []. by apply elem_of_list_singleton. Qed. Lemma unit_card : card unit = 1. Proof. done. Qed. Program Instance bool_finite : Finite bool := {| enum := [true; false] |}. Next Obligation. constructor. by rewrite elem_of_list_singleton. apply NoDup_singleton. Qed. Next Obligation. intros [|]. left. right; left. Qed. Lemma bool_card : card bool = 2. Proof. done. Qed. Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type := {| enum := (inl <\$> enum A) ++ (inr <\$> enum B) |}. Next Obligation. `````` Robbert Krebbers committed Feb 19, 2016 223 `````` intros. apply NoDup_app; split_and?. `````` Robbert Krebbers committed Feb 17, 2016 224 225 226 `````` - apply (NoDup_fmap_2 _). by apply NoDup_enum. - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence. - apply (NoDup_fmap_2 _). by apply NoDup_enum. `````` Robbert Krebbers committed Nov 11, 2015 227 228 229 230 231 232 233 234 235 236 237 238 239 ``````Qed. Next Obligation. intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap; eauto using @elem_of_enum. Qed. Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B. Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed. Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type := {| enum := foldr (λ x, (pair x <\$> enum B ++)) [] (enum A) |}. Next Obligation. intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl. { constructor. } `````` Robbert Krebbers committed Feb 19, 2016 240 `````` apply NoDup_app; split_and?. `````` Robbert Krebbers committed Feb 17, 2016 241 `````` - by apply (NoDup_fmap_2 _), NoDup_enum. `````` Robbert Krebbers committed Feb 17, 2016 242 `````` - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq. `````` Robbert Krebbers committed Nov 11, 2015 243 244 245 `````` clear IH. induction Hxs as [|x' xs ?? IH]; simpl. { rewrite elem_of_nil. tauto. } rewrite elem_of_app, elem_of_list_fmap. `````` Robbert Krebbers committed Feb 17, 2016 246 `````` intros [(?&?&?)|?]; simplify_eq. `````` Robbert Krebbers committed Nov 11, 2015 247 248 `````` + destruct Hx. by left. + destruct IH. by intro; destruct Hx; right. auto. `````` Robbert Krebbers committed Feb 17, 2016 249 `````` - done. `````` Robbert Krebbers committed Nov 11, 2015 250 251 252 ``````Qed. Next Obligation. intros ?????? [x y]. induction (elem_of_enum x); simpl. `````` Robbert Krebbers committed Feb 17, 2016 253 254 `````` - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum. - rewrite elem_of_app; eauto. `````` Robbert Krebbers committed Nov 11, 2015 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 ``````Qed. Lemma prod_card `{Finite A} `{Finite B} : card (A * B) = card A * card B. Proof. unfold card; simpl. induction (enum A); simpl; auto. rewrite app_length, fmap_length. auto. Qed. Let list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n } := fix go n := match n with | 0 => [[]↾eq_refl] | S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <\$> (go n) ++)) [] l end. Program Instance list_finite `{Finite A} n : Finite { l | length l = n } := {| enum := list_enum (enum A) n |}. Next Obligation. intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |]. revert IH. generalize (list_enum (enum A) n). intros l Hl. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |]. `````` Robbert Krebbers committed Feb 19, 2016 274 `````` apply NoDup_app; split_and?. `````` Robbert Krebbers committed Feb 17, 2016 275 276 `````` - by apply (NoDup_fmap_2 _). - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap. `````` Robbert Krebbers committed Feb 17, 2016 277 `````` intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2. `````` Robbert Krebbers committed Nov 11, 2015 278 279 `````` induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |]. rewrite elem_of_app, elem_of_list_fmap, elem_of_cons. `````` Robbert Krebbers committed Feb 17, 2016 280 `````` intros [([??]&?&?)|?]; simplify_eq/=; auto. `````` Robbert Krebbers committed Feb 17, 2016 281 `````` - apply IH. `````` Robbert Krebbers committed Nov 11, 2015 282 283 284 ``````Qed. Next Obligation. intros ???? [l Hl]. revert l Hl. `````` Robbert Krebbers committed Feb 17, 2016 285 `````` induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq. `````` Robbert Krebbers committed Nov 11, 2015 286 287 288 `````` { apply elem_of_list_singleton. by apply (sig_eq_pi _). } revert IH. generalize (list_enum (enum A) n). intros k Hk. induction (elem_of_enum x) as [x xs|x xs]; simpl in *. `````` Robbert Krebbers committed Feb 17, 2016 289 `````` - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'. `````` Robbert Krebbers committed Nov 11, 2015 290 `````` eexists (l↾Hl'). split. by apply (sig_eq_pi _). done. `````` Robbert Krebbers committed Feb 17, 2016 291 `````` - rewrite elem_of_app. eauto. `````` Robbert Krebbers committed Nov 11, 2015 292 293 294 295 296 297 298 299 ``````Qed. Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n. Proof. unfold card; simpl. induction n as [|n IH]; simpl; auto. rewrite <-IH. clear IH. generalize (list_enum (enum A) n). induction (enum A) as [|x xs IH]; intros l; simpl; auto. by rewrite app_length, fmap_length, IH. Qed.``````