finite.v 13.8 KB
 Robbert Krebbers committed Jan 24, 2017 1 ``````(* Copyright (c) 2012-2017, Robbert Krebbers. *) `````` Robbert Krebbers committed Nov 11, 2015 2 ``````(* This file is distributed under the terms of the BSD license. *) `````` Robbert Krebbers committed Mar 11, 2016 3 ``````From iris.prelude Require Export countable vector. `````` Ralf Jung committed Jan 05, 2017 4 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Nov 11, 2015 5 `````` `````` Robbert Krebbers committed Sep 20, 2016 6 ``````Class Finite A `{EqDecision A} := { `````` Robbert Krebbers committed Nov 11, 2015 7 8 9 10 `````` enum : list A; NoDup_enum : NoDup enum; elem_of_enum x : x ∈ enum }. `````` Ralf Jung committed Nov 15, 2016 11 12 13 14 ``````Arguments enum _ _ _ : clear implicits. Arguments enum _ {_ _}. Arguments NoDup_enum _ _ _ : clear implicits. Arguments NoDup_enum _ {_ _}. `````` Robbert Krebbers committed Nov 11, 2015 15 16 17 ``````Definition card A `{Finite A} := length (enum A). Program Instance finite_countable `{Finite A} : Countable A := {| encode := λ x, `````` Robbert Krebbers committed May 27, 2016 18 `````` Pos.of_nat \$ S \$ from_option id 0 \$ fst <\$> list_find (x =) (enum A); `````` Robbert Krebbers committed Nov 11, 2015 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 `````` 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 36 37 `````` - 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 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 ``````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 54 `````` intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_eq/=. `````` Robbert Krebbers committed Nov 11, 2015 55 56 57 58 59 60 61 62 `````` 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 63 `````` rewrite Hi. destruct (list_find_Some P xs i y); simplify_eq/=; auto. `````` Robbert Krebbers committed Nov 11, 2015 64 65 66 `````` exists y. by rewrite !Nat2Pos.id by done. Qed. `````` Robbert Krebbers committed Mar 11, 2016 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 ``````Definition encode_fin `{Finite A} (x : A) : fin (card A) := Fin.of_nat_lt (encode_lt_card x). Program Definition decode_fin `{Finite A} (i : fin (card A)) : A := match Some_dec (decode_nat i) return _ with | inleft (exist x _) => x | inright _ => _ end. Next Obligation. intros A ?? i ?; exfalso. destruct (encode_decode A i); naive_solver auto using fin_to_nat_lt. Qed. Lemma decode_encode_fin `{Finite A} (x : A) : decode_fin (encode_fin x) = x. Proof. unfold decode_fin, encode_fin. destruct (Some_dec _) as [[x' Hx]|Hx]. { by rewrite fin_to_of_nat, decode_encode_nat in Hx; simplify_eq. } exfalso; by rewrite ->fin_to_of_nat, decode_encode_nat in Hx. Qed. Lemma fin_choice {n} {B : fin n → Type} (P : ∀ i, B i → Prop) : (∀ i, ∃ y, P i y) → ∃ f, ∀ i, P i (f i). Proof. induction n as [|n IH]; intros Hex. { exists (fin_0_inv _); intros i; inv_fin i. } destruct (IH _ _ (λ i, Hex (FS i))) as [f Hf], (Hex 0%fin) as [y Hy]. exists (fin_S_inv _ y f); intros i; by inv_fin i. Qed. Lemma finite_choice `{Finite A} {B : A → Type} (P : ∀ x, B x → Prop) : (∀ x, ∃ y, P x y) → ∃ f, ∀ x, P x (f x). Proof. intros Hex. destruct (fin_choice _ (λ i, Hex (decode_fin i))) as [f ?]. exists (λ x, eq_rect _ _ (f(encode_fin x)) _ (decode_encode_fin x)); intros x. destruct (decode_encode_fin x); simpl; auto. Qed. `````` Robbert Krebbers committed Nov 11, 2015 100 101 ``````Lemma card_0_inv P `{finA: Finite A} : card A = 0 → A → P. Proof. `````` Robbert Krebbers committed Feb 17, 2016 102 `````` intros ? x. destruct finA as [[|??] ??]; simplify_eq. `````` Robbert Krebbers committed Nov 11, 2015 103 104 105 106 `````` 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 107 `````` unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|]. `````` Robbert Krebbers committed Nov 11, 2015 108 109 `````` constructor; exact x. Qed. `````` Robbert Krebbers committed Jan 06, 2017 110 111 ``````Lemma finite_inj_submseteq `{finA: Finite A} `{finB: Finite B} (f: A → B) `{!Inj (=) (=) f} : f <\$> enum A ⊆+ enum B. `````` Robbert Krebbers committed Nov 11, 2015 112 ``````Proof. `````` Robbert Krebbers committed Jan 06, 2017 113 `````` intros. destruct finA, finB. apply NoDup_submseteq; auto using NoDup_fmap_2. `````` Robbert Krebbers committed Nov 11, 2015 114 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 115 116 ``````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 117 ``````Proof. `````` Robbert Krebbers committed Jan 06, 2017 118 `````` intros. apply submseteq_Permutation_length_eq. `````` Robbert Krebbers committed Feb 17, 2016 119 `````` - by rewrite fmap_length. `````` Robbert Krebbers committed Jan 06, 2017 120 `````` - by apply finite_inj_submseteq. `````` Robbert Krebbers committed Nov 11, 2015 121 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 122 123 ``````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 124 125 ``````Proof. intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto. `````` Robbert Krebbers committed Feb 11, 2016 126 `````` rewrite finite_inj_Permutation; auto using elem_of_enum. `````` Robbert Krebbers committed Nov 11, 2015 127 128 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 129 130 ``````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 131 132 ``````Proof. intros [??]. destruct (finite_inhabited A) as [x']; auto with lia. `````` Robbert Krebbers committed May 27, 2016 133 `````` exists (λ y : B, from_option id x' (decode_nat (encode_nat y))). `````` Robbert Krebbers committed Nov 11, 2015 134 135 136 137 `````` 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 138 139 ``````Lemma finite_inj A `{Finite A} B `{Finite B} : card A ≤ card B ↔ ∃ f : A → B, Inj (=) (=) f. `````` Robbert Krebbers committed Nov 11, 2015 140 141 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 142 `````` - intros. destruct (decide (card A = 0)) as [HA|?]. `````` Robbert Krebbers committed Nov 11, 2015 143 `````` { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). } `````` Robbert Krebbers committed Feb 11, 2016 144 145 `````` 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 146 `````` - intros [f ?]. unfold card. rewrite <-(fmap_length f). `````` Robbert Krebbers committed Jan 06, 2017 147 `````` by apply submseteq_length, (finite_inj_submseteq f). `````` Robbert Krebbers committed Nov 11, 2015 148 149 ``````Qed. Lemma finite_bijective A `{Finite A} B `{Finite B} : `````` Robbert Krebbers committed Feb 11, 2016 150 `````` card A = card B ↔ ∃ f : A → B, Inj (=) (=) f ∧ Surj (=) f. `````` Robbert Krebbers committed Nov 11, 2015 151 152 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 153 `````` - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia. `````` Robbert Krebbers committed Feb 11, 2016 154 `````` exists f; auto using (finite_inj_surj f). `````` Robbert Krebbers committed Feb 17, 2016 155 `````` - intros (f&?&?). apply (anti_symm (≤)); apply finite_inj. `````` Robbert Krebbers committed Nov 11, 2015 156 `````` + by exists f. `````` Robbert Krebbers committed Feb 11, 2016 157 `````` + destruct (surj_cancel f) as (g&?); eauto using cancel_inj. `````` Robbert Krebbers committed Nov 11, 2015 158 ``````Qed. `````` Robbert Krebbers committed Feb 11, 2016 159 160 161 162 163 ``````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 164 ``````Proof. `````` Robbert Krebbers committed Feb 11, 2016 165 166 `````` destruct (surj_cancel f) as (g&?). apply inj_card with g, cancel_inj. `````` Robbert Krebbers committed Nov 11, 2015 167 168 ``````Qed. Lemma bijective_card `{Finite A} `{Finite B} (f : A → B) `````` Robbert Krebbers committed Feb 11, 2016 169 `````` `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B. `````` Robbert Krebbers committed Nov 11, 2015 170 171 172 173 ``````Proof. apply finite_bijective. eauto. Qed. (** Decidability of quantification over finite types *) Section forall_exists. `````` 174 `````` Context `{Finite A} (P : A → Prop). `````` Robbert Krebbers committed Nov 11, 2015 175 176 177 178 179 180 `````` 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. `````` 181 182 `````` Context `{∀ x, Decision (P x)}. `````` Robbert Krebbers committed Nov 11, 2015 183 `````` Global Instance forall_dec: Decision (∀ x, P x). `````` Ralf Jung committed Jan 05, 2017 184 `````` Proof using Type*. `````` Robbert Krebbers committed Nov 11, 2015 185 186 187 188 `````` refine (cast_if (decide (Forall P (enum A)))); abstract by rewrite <-Forall_finite. Defined. Global Instance exists_dec: Decision (∃ x, P x). `````` Ralf Jung committed Jan 05, 2017 189 `````` Proof using Type*. `````` Robbert Krebbers committed Nov 11, 2015 190 191 192 193 194 195 196 `````` refine (cast_if (decide (Exists P (enum A)))); abstract by rewrite <-Exists_finite. Defined. End forall_exists. (** Instances *) Section enc_finite. `````` Robbert Krebbers committed Sep 20, 2016 197 `````` Context `{EqDecision A}. `````` Robbert Krebbers committed Nov 11, 2015 198 199 200 201 202 203 204 205 206 `````` 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 207 `````` (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=. `````` Robbert Krebbers committed Nov 11, 2015 208 209 210 211 212 213 214 215 216 217 218 219 `````` 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. `````` Robbert Krebbers committed Sep 20, 2016 220 `````` Context `{Finite A, EqDecision B} (f : A → B) (g : B → A). `````` Robbert Krebbers committed Feb 11, 2016 221 `````` Context `{!Inj (=) (=) f, !Cancel (=) f g}. `````` Robbert Krebbers committed Nov 11, 2015 222 223 224 225 226 227 228 229 230 231 232 233 `````` 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 234 235 `````` - rewrite elem_of_list_fmap. by intros (?&?&?). - apply (NoDup_fmap_2 _); auto using NoDup_enum. `````` Robbert Krebbers committed Nov 11, 2015 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 ``````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 261 `````` intros. apply NoDup_app; split_and?. `````` Robbert Krebbers committed Feb 17, 2016 262 263 264 `````` - 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 265 266 267 268 269 270 271 272 273 274 275 276 277 ``````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 278 `````` apply NoDup_app; split_and?. `````` Robbert Krebbers committed Feb 17, 2016 279 `````` - by apply (NoDup_fmap_2 _), NoDup_enum. `````` Robbert Krebbers committed Feb 17, 2016 280 `````` - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq. `````` Robbert Krebbers committed Nov 11, 2015 281 282 283 `````` 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 284 `````` intros [(?&?&?)|?]; simplify_eq. `````` Robbert Krebbers committed Nov 11, 2015 285 286 `````` + destruct Hx. by left. + destruct IH. by intro; destruct Hx; right. auto. `````` Robbert Krebbers committed Feb 17, 2016 287 `````` - done. `````` Robbert Krebbers committed Nov 11, 2015 288 289 290 ``````Qed. Next Obligation. intros ?????? [x y]. induction (elem_of_enum x); simpl. `````` Robbert Krebbers committed Feb 17, 2016 291 292 `````` - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum. - rewrite elem_of_app; eauto. `````` Robbert Krebbers committed Nov 11, 2015 293 294 295 296 297 298 299 ``````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. `````` Ralf Jung committed Nov 17, 2016 300 ``````Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n } := `````` Robbert Krebbers committed Nov 11, 2015 301 302 303 304 305 `````` 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. `````` Ralf Jung committed Nov 17, 2016 306 `````` `````` Robbert Krebbers committed Nov 11, 2015 307 308 309 310 311 312 ``````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 313 `````` apply NoDup_app; split_and?. `````` Robbert Krebbers committed Feb 17, 2016 314 315 `````` - by apply (NoDup_fmap_2 _). - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap. `````` Robbert Krebbers committed Feb 17, 2016 316 `````` intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2. `````` Robbert Krebbers committed Nov 11, 2015 317 318 `````` 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 319 `````` intros [([??]&?&?)|?]; simplify_eq/=; auto. `````` Robbert Krebbers committed Feb 17, 2016 320 `````` - apply IH. `````` Robbert Krebbers committed Nov 11, 2015 321 322 323 ``````Qed. Next Obligation. intros ???? [l Hl]. revert l Hl. `````` Robbert Krebbers committed Feb 17, 2016 324 `````` induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq. `````` Robbert Krebbers committed Nov 11, 2015 325 326 327 `````` { 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 328 `````` - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'. `````` Robbert Krebbers committed Nov 11, 2015 329 `````` eexists (l↾Hl'). split. by apply (sig_eq_pi _). done. `````` Robbert Krebbers committed Feb 17, 2016 330 `````` - rewrite elem_of_app. eauto. `````` Robbert Krebbers committed Nov 11, 2015 331 ``````Qed. `````` Ralf Jung committed Nov 17, 2016 332 `````` `````` Robbert Krebbers committed Nov 11, 2015 333 334 335 336 337 338 339 ``````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. `````` Robbert Krebbers committed Mar 11, 2016 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 `````` Fixpoint fin_enum (n : nat) : list (fin n) := match n with 0 => [] | S n => 0%fin :: FS <\$> fin_enum n end. Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}. Next Obligation. intros n. induction n; simpl; constructor. - rewrite elem_of_list_fmap. by intros (?&?&?). - by apply (NoDup_fmap _). Qed. Next Obligation. intros n i. induction i as [|n i IH]; simpl; rewrite elem_of_cons, ?elem_of_list_fmap; eauto. Qed. Lemma fin_card n : card (fin n) = n. Proof. unfold card; simpl. induction n; simpl; rewrite ?fmap_length; auto. Qed.``````