finite.v 13.7 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 vector.
4

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

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.
33 34
  rewrite Nat2Pos.id by done; simpl.
  destruct (list_find _ xs) as [[i y]|] eqn:?; simpl.
35 36
  - 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.
37 38 39 40 41 42 43 44
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.
45 46 47
  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.
48 49 50 51 52
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.
53
  intros Hx. destruct (list_find _ _) as [[i y]|] eqn:Hi; simplify_eq/=.
54
  rewrite !Nat2Pos.id in Hx by done.
55
  destruct (list_find_Some P xs i y); naive_solver.
56 57 58 59 60
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.
61
  intros Hx. destruct (list_find_elem_of P xs x) as [[i y] Hi]; auto.
62
  rewrite Hi. destruct (list_find_Some P xs i y); simplify_eq/=; auto.
63
  exists y. by rewrite !Nat2Pos.id by done.
64 65
Qed.

66 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
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.

99 100
Lemma card_0_inv P `{finA: Finite A} : card A = 0  A  P.
Proof.
101
  intros ? x. destruct finA as [[|??] ??]; simplify_eq.
102 103 104 105
  by destruct (not_elem_of_nil x).
Qed.
Lemma finite_inhabited A `{finA: Finite A} : 0 < card A  Inhabited A.
Proof.
106
  unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
107 108
  constructor; exact x.
Qed.
109 110
Lemma finite_inj_contains `{finA: Finite A} `{finB: Finite B} (f: A  B)
  `{!Inj (=) (=) f} : f <$> enum A `contains` enum B.
111
Proof.
112
  intros. destruct finA, finB. apply NoDup_contains; auto using NoDup_fmap_2.
113
Qed.
114 115
Lemma finite_inj_Permutation `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A = card B  f <$> enum A  enum B.
116
Proof.
117
  intros. apply contains_Permutation_length_eq.
118 119
  - by rewrite fmap_length.
  - by apply finite_inj_contains.
120
Qed.
121 122
Lemma finite_inj_surj `{Finite A} `{Finite B} (f : A  B)
  `{!Inj (=) (=) f} : card A = card B  Surj (=) f.
123 124
Proof.
  intros HAB y. destruct (elem_of_list_fmap_2 f (enum A) y) as (x&?&?); eauto.
125
  rewrite finite_inj_Permutation; auto using elem_of_enum.
126 127
Qed.

128 129
Lemma finite_surj A `{Finite A} B `{Finite B} :
  0 < card A  card B   g : B  A, Surj (=) g.
130 131
Proof.
  intros [??]. destruct (finite_inhabited A) as [x']; auto with lia.
132
  exists (λ y : B, from_option id x' (decode_nat (encode_nat y))).
133 134 135 136
  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.
137 138
Lemma finite_inj A `{Finite A} B `{Finite B} :
  card A  card B   f : A  B, Inj (=) (=) f.
139 140
Proof.
  split.
141
  - intros. destruct (decide (card A = 0)) as [HA|?].
142
    { exists (card_0_inv B HA). intros y. apply (card_0_inv _ HA y). }
143 144
    destruct (finite_surj A B) as (g&?); auto with lia.
    destruct (surj_cancel g) as (f&?). exists f. apply cancel_inj.
145
  - intros [f ?]. unfold card. rewrite <-(fmap_length f).
146
    by apply contains_length, (finite_inj_contains f).
147 148
Qed.
Lemma finite_bijective A `{Finite A} B `{Finite B} :
149
  card A = card B   f : A  B, Inj (=) (=) f  Surj (=) f.
150 151
Proof.
  split.
152
  - intros; destruct (proj1 (finite_inj A B)) as [f ?]; auto with lia.
153
    exists f; auto using (finite_inj_surj f).
154
  - intros (f&?&?). apply (anti_symm ()); apply finite_inj.
155
    + by exists f.
156
    + destruct (surj_cancel f) as (g&?); eauto using cancel_inj.
157
Qed.
158 159 160 161 162
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.
163
Proof.
164 165
  destruct (surj_cancel f) as (g&?).
  apply inj_card with g, cancel_inj.
166 167
Qed.
Lemma bijective_card `{Finite A} `{Finite B} (f : A  B)
168
  `{!Inj (=) (=) f} `{!Surj (=) f} : card A = card B.
169 170
Proof. apply finite_bijective. eauto. Qed.

171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191
(** 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.

192 193
(** Instances *)
Section enc_finite.
194
  Context `{EqDecision A}.
195 196 197 198 199 200 201 202 203
  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',
204
      (seq _ _ !! j) as [j'|] eqn:Hj'; simplify_eq/=.
205 206 207 208 209 210 211 212 213 214 215 216
    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.
217
  Context `{Finite A, EqDecision B} (f : A  B) (g : B  A).
218
  Context `{!Inj (=) (=) f, !Cancel (=) f g}.
219 220

  Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
221
  Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
222 223 224 225 226 227 228 229 230
  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.
231 232
  - rewrite elem_of_list_fmap. by intros (?&?&?).
  - apply (NoDup_fmap_2 _); auto using NoDup_enum.
233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
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.

255
Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
256 257
  {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
Next Obligation.
258
  intros. apply NoDup_app; split_and?.
259 260 261
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
  - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
  - apply (NoDup_fmap_2 _). by apply NoDup_enum.
262 263 264 265 266
Qed.
Next Obligation.
  intros ?????? [x|y]; rewrite elem_of_app, !elem_of_list_fmap;
    eauto using @elem_of_enum.
Qed.
267
Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
268 269
Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.

270
Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
271 272
  {| enum := foldr (λ x, (pair x <$> enum B ++)) [] (enum A) |}.
Next Obligation.
273
  intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
274
  { constructor. }
275
  apply NoDup_app; split_and?.
276
  - by apply (NoDup_fmap_2 _), NoDup_enum.
277
  - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
278 279 280
    clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
    { rewrite elem_of_nil. tauto. }
    rewrite elem_of_app, elem_of_list_fmap.
281
    intros [(?&?&?)|?]; simplify_eq.
282 283
    + destruct Hx. by left.
    + destruct IH. by intro; destruct Hx; right. auto.
284
  - done.
285 286 287
Qed.
Next Obligation.
  intros ?????? [x y]. induction (elem_of_enum x); simpl.
288 289
  - rewrite elem_of_app, !elem_of_list_fmap. eauto using @elem_of_enum.
  - rewrite elem_of_app; eauto.
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307
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.
308
  induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
309
  apply NoDup_app; split_and?.
310 311
  - by apply (NoDup_fmap_2 _).
  - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
312
    intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.
313 314
    induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
    rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
315
    intros [([??]&?&?)|?]; simplify_eq/=; auto.
316
  - apply IH.
317 318 319
Qed.
Next Obligation.
  intros ???? [l Hl]. revert l Hl.
320
  induction n as [|n IH]; intros [|x l] ?; simpl; simplify_eq.
321 322 323
  { 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 *.
324
  - rewrite elem_of_app, elem_of_list_fmap. left. injection Hl. intros Hl'.
325
    eexists (lHl'). split. by apply (sig_eq_pi _). done.
326
  - rewrite elem_of_app. eauto.
327 328 329 330 331 332 333 334
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.
335 336 337 338 339 340 341 342 343 344 345 346 347 348 349

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.