finite.v 12.1 KB
 Robbert Krebbers committed Feb 08, 2015 1 ``````(* Copyright (c) 2012-2015, Robbert Krebbers. *) `````` Robbert Krebbers committed May 02, 2014 2 ``````(* This file is distributed under the terms of the BSD license. *) `````` Robbert Krebbers committed Jun 17, 2013 3 4 5 6 7 ``````Require Export countable list. Obligation Tactic := idtac. Class Finite A `{∀ x y : A, Decision (x = y)} := { enum : list A; `````` Robbert Krebbers committed Jun 05, 2014 8 `````` NoDup_enum : NoDup enum; `````` Robbert Krebbers committed Jun 17, 2013 9 10 11 `````` elem_of_enum x : x ∈ enum }. Arguments enum _ {_ _} : clear implicits. `````` Robbert Krebbers committed Jun 05, 2014 12 ``````Arguments NoDup_enum _ {_ _} : clear implicits. `````` Robbert Krebbers committed Jun 17, 2013 13 14 ``````Definition card A `{Finite A} := length (enum A). Program Instance finite_countable `{Finite A} : Countable A := {| `````` Robbert Krebbers committed Feb 08, 2015 15 16 `````` encode := λ x, Pos.of_nat \$ S \$ from_option 0 \$ fst <\$> list_find (x =) (enum A); `````` Robbert Krebbers committed Jun 17, 2013 17 18 19 20 21 `````` 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. `````` Robbert Krebbers committed Feb 08, 2015 22 23 24 `````` 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. `````` Robbert Krebbers committed Jun 17, 2013 25 26 ``````Qed. Definition find `{Finite A} P `{∀ x, Decision (P x)} : option A := `````` Robbert Krebbers committed Feb 08, 2015 27 `````` list_find P (enum A) ≫= decode_nat ∘ fst. `````` Robbert Krebbers committed Jun 17, 2013 28 29 30 31 `````` 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. `````` Robbert Krebbers committed Feb 08, 2015 32 33 34 `````` rewrite Nat2Pos.id by done; simpl. destruct (list_find _ xs) as [[i y]|] eqn:?; simpl. * destruct (list_find_Some (x =) xs i y); eauto using lookup_lt_Some. `````` Robbert Krebbers committed Jun 17, 2013 35 36 37 38 39 40 41 42 43 `````` * destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia. 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. `````` Robbert Krebbers committed Feb 08, 2015 44 45 46 `````` 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. `````` Robbert Krebbers committed Jun 17, 2013 47 48 49 50 51 ``````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 08, 2015 52 `````` intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_equality'. `````` Robbert Krebbers committed Jun 17, 2013 53 `````` rewrite !Nat2Pos.id in Hx by done. `````` Robbert Krebbers committed Feb 08, 2015 54 `````` destruct (list_find_Some P xs i y); naive_solver. `````` Robbert Krebbers committed Jun 17, 2013 55 56 57 58 59 ``````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. `````` Robbert Krebbers committed Feb 08, 2015 60 61 62 `````` intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto. rewrite Hi. destruct (list_find_Some P xs i y); simplify_equality'; auto. exists y. by rewrite !Nat2Pos.id by done. `````` Robbert Krebbers committed Jun 17, 2013 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 ``````Qed. Lemma card_0_inv P `{finA: Finite A} : card A = 0 → A → P. Proof. intros ? x. destruct finA as [[|??] ??]; simplify_equality. by destruct (not_elem_of_nil x). Qed. Lemma finite_inhabited A `{finA: Finite A} : 0 < card A → Inhabited A. Proof. unfold card. destruct finA as [[|x ?] ??]; simpl; auto with lia. constructor; exact x. Qed. Lemma finite_injective_contains `{finA: Finite A} `{finB: Finite B} (f: A → B) `{!Injective (=) (=) f} : f <\$> enum A `contains` enum B. Proof. `````` Robbert Krebbers committed Jun 05, 2014 78 `````` intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2. `````` Robbert Krebbers committed Jun 17, 2013 79 80 81 82 ``````Qed. Lemma finite_injective_Permutation `{Finite A} `{Finite B} (f : A → B) `{!Injective (=) (=) f} : card A = card B → f <\$> enum A ≡ₚ enum B. Proof. `````` Robbert Krebbers committed Aug 15, 2013 83 `````` intros. apply contains_Permutation_length_eq. `````` Robbert Krebbers committed Jun 17, 2013 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 `````` * by rewrite fmap_length. * by apply finite_injective_contains. Qed. Lemma finite_injective_surjective `{Finite A} `{Finite B} (f : A → B) `{!Injective (=) (=) f} : card A = card B → Surjective (=) f. Proof. intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto. rewrite finite_injective_Permutation; auto using elem_of_enum. Qed. Lemma finite_surjective A `{Finite A} B `{Finite B} : 0 < card A ≤ card B → ∃ g : B → A, Surjective (=) g. 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. Lemma finite_injective A `{Finite A} B `{Finite B} : card A ≤ card B ↔ ∃ f : A → B, Injective (=) (=) f. Proof. split. * intros. destruct (decide (card A = 0)) as [HA|?]. { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). } destruct (finite_surjective A B) as (g&?); auto with lia. destruct (surjective_cancel g) as (f&?). exists f. apply cancel_injective. * intros [f ?]. unfold card. rewrite <-(fmap_length f). by apply contains_length, (finite_injective_contains f). Qed. Lemma finite_bijective A `{Finite A} B `{Finite B} : card A = card B ↔ ∃ f : A → B, Injective (=) (=) f ∧ Surjective (=) f. Proof. split. * intros; destruct (proj1 (finite_injective A B)) as [f ?]; auto with lia. exists f; auto using (finite_injective_surjective f). * intros (f&?&?). apply (anti_symmetric (≤)); apply finite_injective. + by exists f. + destruct (surjective_cancel f) as (g&?); eauto using cancel_injective. Qed. Lemma injective_card `{Finite A} `{Finite B} (f : A → B) `{!Injective (=) (=) f} : card A ≤ card B. Proof. apply finite_injective. eauto. Qed. Lemma surjective_card `{Finite A} `{Finite B} (f : A → B) `{!Surjective (=) f} : card B ≤ card A. Proof. destruct (surjective_cancel f) as (g&?). apply injective_card with g, cancel_injective. Qed. Lemma bijective_card `{Finite A} `{Finite B} (f : A → B) `{!Injective (=) (=) f} `{!Surjective (=) f} : card A = card B. Proof. apply finite_bijective. eauto. Qed. `````` Robbert Krebbers committed Aug 27, 2013 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 ``````(** 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. `````` Robbert Krebbers committed Jun 17, 2013 158 159 160 161 162 163 164 165 166 167 168 169 ``````(** 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 Sep 30, 2014 170 `````` (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_equality'. `````` Robbert Krebbers committed Jun 17, 2013 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. `````` Robbert Krebbers committed Nov 15, 2014 183 184 `````` Context `{Finite A, ∀ x y : B, Decision (x = y)} (f : A → B) (g : B → A). Context `{!Injective (=) (=) f, !Cancel (=) f g}. `````` Robbert Krebbers committed Jun 17, 2013 185 186 `````` Program Instance bijective_finite: Finite B := {| enum := f <\$> enum A |}. `````` Robbert Krebbers committed Jun 05, 2014 187 `````` Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed. `````` Robbert Krebbers committed Jun 17, 2013 188 189 190 191 192 193 194 195 196 197 `````` 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. * rewrite elem_of_list_fmap. by intros (?&?&?). `````` Robbert Krebbers committed Jun 05, 2014 198 `````` * apply (NoDup_fmap_2 _); auto using NoDup_enum. `````` Robbert Krebbers committed Jun 17, 2013 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 ``````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. `````` Robbert Krebbers committed Nov 15, 2014 221 ``````Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type := `````` Robbert Krebbers committed Jun 17, 2013 222 223 224 `````` {| enum := (inl <\$> enum A) ++ (inr <\$> enum B) |}. Next Obligation. intros. apply NoDup_app; split_ands. `````` Robbert Krebbers committed Jun 05, 2014 225 `````` * apply (NoDup_fmap_2 _). by apply NoDup_enum. `````` Robbert Krebbers committed Jun 17, 2013 226 `````` * intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence. `````` Robbert Krebbers committed Jun 05, 2014 227 `````` * apply (NoDup_fmap_2 _). by apply NoDup_enum. `````` Robbert Krebbers committed Jun 17, 2013 228 229 230 231 232 ``````Qed. Next Obligation. intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap; eauto using @elem_of_enum. Qed. `````` Robbert Krebbers committed Nov 15, 2014 233 ``````Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B. `````` Robbert Krebbers committed Jun 17, 2013 234 235 ``````Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed. `````` Robbert Krebbers committed Nov 15, 2014 236 ``````Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type := `````` Robbert Krebbers committed Jun 17, 2013 237 238 `````` {| enum := foldr (λ x, (pair x <\$> enum B ++)) [] (enum A) |}. Next Obligation. `````` Robbert Krebbers committed Jun 05, 2014 239 `````` intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl. `````` Robbert Krebbers committed Jun 17, 2013 240 241 `````` { constructor. } apply NoDup_app; split_ands. `````` Robbert Krebbers committed Jun 05, 2014 242 `````` * by apply (NoDup_fmap_2 _), NoDup_enum. `````` Robbert Krebbers committed Jun 17, 2013 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 `````` * intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_equality. clear IH. induction Hxs as [|x' xs ?? IH]; simpl. { rewrite elem_of_nil. tauto. } rewrite elem_of_app, elem_of_list_fmap. intros [(?&?&?)|?]; simplify_equality. + destruct Hx. by left. + destruct IH. by intro; destruct Hx; right. auto. * done. Qed. Next Obligation. intros ?????? [x y]. induction (elem_of_enum x); simpl. * rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum. * rewrite elem_of_app; eauto. 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. `````` Robbert Krebbers committed Jun 05, 2014 274 `````` induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |]. `````` Robbert Krebbers committed Jun 17, 2013 275 `````` apply NoDup_app; split_ands. `````` Robbert Krebbers committed Jun 05, 2014 276 `````` * by apply (NoDup_fmap_2 _). `````` Robbert Krebbers committed Jun 17, 2013 277 `````` * intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap. `````` Robbert Krebbers committed Sep 30, 2014 278 `````` intros ([k2 Hk2]&?&?) Hxk2; simplify_equality'. destruct Hx. revert Hxk2. `````` Robbert Krebbers committed Jun 17, 2013 279 280 `````` 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 Sep 30, 2014 281 `````` intros [([??]&?&?)|?]; simplify_equality'; auto. `````` Robbert Krebbers committed Jun 17, 2013 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 `````` * apply IH. Qed. Next Obligation. intros ???? [l Hl]. revert l Hl. induction n as [|n IH]; intros [|x l] ?; simpl; simplify_equality. { 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 *. * rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'. eexists (l↾Hl'). split. by apply (sig_eq_pi _). done. * rewrite elem_of_app. eauto. 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.``````