finite.v 11.8 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2
(* This file is distributed under the terms of the BSD license. *)
3
From stdpp Require Export countable list.
4 5 6

Class Finite A `{ x y : A, Decision (x = y)} := {
  enum : list A;
7
  NoDup_enum : NoDup enum;
8 9 10
  elem_of_enum x : x  enum
}.
Arguments enum _ {_ _} : clear implicits.
11
Arguments NoDup_enum _ {_ _} : clear implicits.
12 13
Definition card A `{Finite A} := length (enum A).
Program Instance finite_countable `{Finite A} : Countable A := {|
14 15
  encode := λ x,
    Pos.of_nat $ S $ from_option 0 $ fst <$> list_find (x =) (enum A);
16 17 18 19 20
  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.
21 22 23
  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.
24 25
Qed.
Definition find `{Finite A} P `{ x, Decision (P x)} : option A :=
26
  list_find P (enum A) = decode_nat  fst.
27 28 29 30

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.
31 32 33
  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.
34 35 36 37 38 39 40 41 42
  * 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.
43 44 45
  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.
46 47 48 49 50
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.
51
  intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_equality'.
52
  rewrite !Nat2Pos.id in Hx by done.
53
  destruct (list_find_Some P xs i y); naive_solver.
54 55 56 57 58
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.
59 60 61
  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.
62 63 64 65 66 67 68 69 70
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.
71
  unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
72 73
  constructor; exact x.
Qed.
74 75
Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A  B)
  `{!Inj (=) (=) f} : f <$> enum A `contains` enum B.
76
Proof.
77
  intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2.
78
Qed.
79 80
Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A = card B  f <$> enum A  enum B.
81
Proof.
82
  intros. apply contains_Permutation_length_eq.
83
  * by rewrite fmap_length.
84
  * by apply finite_inj_contains.
85
Qed.
86 87
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A = card B  Surj (=) f.
88 89
Proof.
  intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto.
90
  rewrite finite_inj_Permutation; auto using elem_of_enum.
91 92
Qed.

93 94
Lemma finite_surj A `{Finite A} B `{Finite B} :
  0 < card A  card B   g : B  A, Surj (=) g.
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.
102 103
Lemma finite_inj A `{Finite A} B `{Finite B} :
  card A  card B   f : A  B, Inj (=) (=) f.
104 105 106 107
Proof.
  split.
  * intros. destruct (decide (card A = 0)) as [HA|?].
    { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
108 109
    destruct (finite_surj A B) as (g&?); auto with lia.
    destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
110
  * intros [f ?]. unfold card. rewrite <-(fmap_length f).
111
    by apply contains_length, (finite_inj_contains f).
112 113
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
114
  card A = card B   f : A  B, Inj (=) (=) f  Surj (=) f.
115 116
Proof.
  split.
117 118 119
  * intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
    exists f; auto using (finite_inj_surj f).
  * intros (f&?&?). apply (anti_symm ()); apply finite_inj.
120
    + by exists f.
121
    + destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
122
Qed.
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.
128
Proof.
129 130
  destruct (surj_cancel f) as (g&?).
  apply inj_card with g, cancel_inj.
131 132
Qed.
Lemma bijective_card `{Finite A} `{Finite B} (f : A  B)
133
  `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B.
134 135
Proof. apply finite_bijective. eauto. Qed.

136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156
(** 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.

157 158 159 160 161 162 163 164 165 166 167 168
(** 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',
169
      (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_equality'.
170 171 172 173 174 175 176 177 178 179 180 181
    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.
182
  Context `{Finite A,  x y : B, Decision (x = y)} (f : A  B) (g : B  A).
183
  Context `{!Inj (=) (=) f, !Cancel (=) f g}.
184 185

  Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
186
  Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
187 188 189 190 191 192 193 194 195 196
  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 (?&?&?).
197
  * apply (NoDup_fmap_2 _); auto using NoDup_enum.
198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
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.

220
Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
221 222 223
  {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
Next Obligation.
  intros. apply NoDup_app; split_ands.
224
  * apply (NoDup_fmap_2 _). by apply NoDup_enum.
225
  * intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
226
  * apply (NoDup_fmap_2 _). by apply NoDup_enum.
227 228 229 230 231
Qed.
Next Obligation.
  intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
    eauto using @elem_of_enum.
Qed.
232
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
233 234
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.

235
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
236 237
  {| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
Next Obligation.
238
  intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
239 240
  { constructor. }
  apply NoDup_app; split_ands.
241
  * by apply (NoDup_fmap_2 _), NoDup_enum.
242 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
  * 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.
273
  induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
274
  apply NoDup_app; split_ands.
275
  * by apply (NoDup_fmap_2 _).
276
  * intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
277
    intros ([k2 Hk2]&?&?) Hxk2; simplify_equality'. destruct Hx. revert Hxk2.
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.
280
    intros [([??]&?&?)|?]; simplify_equality'; auto.
281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
  * 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 (lHl'). 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.