Commit b0f5f6e6 authored by Robbert Krebbers's avatar Robbert Krebbers

Type classes for finite and countable types.

parent 1c177c39
Require Export list.
Local Obligation Tactic := idtac.
Local Open Scope positive.
Class Countable A `{ x y : A, Decision (x = y)} := {
encode : A positive;
decode : positive option A;
decode_encode x : decode (encode x) = Some x
}.
Definition encode_nat `{Countable A} (x : A) : nat :=
pred (Pos.to_nat (encode x)).
Definition decode_nat `{Countable A} (i : nat) : option A :=
decode (Pos.of_nat (S i)).
Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x.
Proof.
pose proof (Pos2Nat.is_pos (encode x)).
unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia.
by rewrite Pos2Nat.id, decode_encode.
Qed.
Section choice.
Context `{Countable A} (P : A Prop) `{ x, Decision (P x)}.
Inductive choose_step: relation positive :=
| choose_step_None {p} : decode p = None choose_step (Psucc p) p
| choose_step_Some {p x} :
decode p = Some x ¬P x choose_step (Psucc p) p.
Lemma choose_step_acc : ( x, P x) Acc choose_step 1%positive.
Proof.
intros [x Hx]. cut ( i p,
i encode x 1 + encode x = p + i Acc choose_step p).
{ intros help. by apply (help (encode x)). }
induction i as [|i IH] using Pos.peano_ind; intros p ??.
{ constructor. intros j. assert (p = encode x) by lia; subst.
inversion 1 as [? Hd|?? Hd]; subst;
rewrite decode_encode in Hd; congruence. }
constructor. intros j.
inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
Qed.
Fixpoint choose_go {i} (acc : Acc choose_step i) : A :=
match Some_dec (decode i) with
| inleft (xHx) =>
match decide (P x) with
| left _ => x
| right H => choose_go (Acc_inv acc (choose_step_Some Hx H))
end
| inright H => choose_go (Acc_inv acc (choose_step_None H))
end.
Fixpoint choose_go_correct {i} (acc : Acc choose_step i) : P (choose_go acc).
Proof. destruct acc; simpl. repeat case_match; auto. Qed.
Fixpoint choose_go_pi {i} (acc1 acc2 : Acc choose_step i) :
choose_go acc1 = choose_go acc2.
Proof. destruct acc1, acc2; simpl; repeat case_match; auto. Qed.
Definition choose (H: x, P x) : A := choose_go (choose_step_acc H).
Definition choose_correct (H: x, P x) : P (choose H) := choose_go_correct _.
Definition choose_pi (H1 H2 : x, P x) :
choose H1 = choose H2 := choose_go_pi _ _.
Definition choice (HA : x, P x) : { x | P x } := _choose_correct HA.
End choice.
Lemma surjective_cancel `{Countable A} `{ x y : B, Decision (x = y)}
(f : A B) `{!Surjective (=) f} : { g : B A & Cancel (=) f g }.
Proof.
exists (λ y, choose (λ x, f x = y) (surjective f y)).
intros y. by rewrite (choose_correct _ (surjective f y)).
Qed.
(** ** Instances *)
Program Instance option_countable `{Countable A} : Countable (option A) := {|
encode o :=
match o with None => 1 | Some x => Pos.succ (encode x) end;
decode p :=
if decide (p = 1) then Some None else Some <$> decode (Pos.pred p)
|}.
Next Obligation.
intros ??? [x|]; simpl; repeat case_decide; auto with lia.
by rewrite Pos.pred_succ, decode_encode.
Qed.
Program Instance sum_countable `{Countable A} `{Countable B} :
Countable (A + B)%type := {|
encode xy :=
match xy with inl x => (encode x)~0 | inr y => (encode y)~1 end;
decode p :=
match p with
| 1 => None | p~0 => inl <$> decode p | p~1 => inr <$> decode p
end
|}.
Next Obligation. by intros ?????? [x|y]; simpl; rewrite decode_encode. Qed.
Fixpoint prod_encode_fst (p : positive) : positive :=
match p with
| 1 => 1
| p~0 => (prod_encode_fst p)~0~0
| p~1 => (prod_encode_fst p)~0~1
end.
Fixpoint prod_encode_snd (p : positive) : positive :=
match p with
| 1 => 1~0
| p~0 => (prod_encode_snd p)~0~0
| p~1 => (prod_encode_snd p)~1~0
end.
Fixpoint prod_encode (p q : positive) : positive :=
match p, q with
| 1, 1 => 1~1
| p~0, 1 => (prod_encode_fst p)~1~0
| p~1, 1 => (prod_encode_fst p)~1~1
| 1, q~0 => (prod_encode_snd q)~0~1
| 1, q~1 => (prod_encode_snd q)~1~1
| p~0, q~0 => (prod_encode p q)~0~0
| p~0, q~1 => (prod_encode p q)~1~0
| p~1, q~0 => (prod_encode p q)~0~1
| p~1, q~1 => (prod_encode p q)~1~1
end.
Fixpoint prod_decode_fst (p : positive) : option positive :=
match p with
| p~0~0 => (~0) <$> prod_decode_fst p
| p~0~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
| p~1~0 => (~0) <$> prod_decode_fst p
| p~1~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
| 1~0 => None
| 1~1 => Some 1
| 1 => Some 1
end.
Fixpoint prod_decode_snd (p : positive) : option positive :=
match p with
| p~0~0 => (~0) <$> prod_decode_snd p
| p~0~1 => (~0) <$> prod_decode_snd p
| p~1~0 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
| p~1~1 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
| 1~0 => Some 1
| 1~1 => Some 1
| 1 => None
end.
Lemma prod_decode_encode_fst p q : prod_decode_fst (prod_encode p q) = Some p.
Proof.
assert ( p, prod_decode_fst (prod_encode_fst p) = Some p).
{ intros p'. by induction p'; simplify_option_equality. }
assert ( p, prod_decode_fst (prod_encode_snd p) = None).
{ intros p'. by induction p'; simplify_option_equality. }
revert q. by induction p; intros [?|?|]; simplify_option_equality.
Qed.
Lemma prod_decode_encode_snd p q : prod_decode_snd (prod_encode p q) = Some q.
Proof.
assert ( p, prod_decode_snd (prod_encode_snd p) = Some p).
{ intros p'. by induction p'; simplify_option_equality. }
assert ( p, prod_decode_snd (prod_encode_fst p) = None).
{ intros p'. by induction p'; simplify_option_equality. }
revert q. by induction p; intros [?|?|]; simplify_option_equality.
Qed.
Program Instance prod_countable `{Countable A} `{Countable B} :
Countable (A * B)%type := {|
encode xy := let (x,y) := xy in prod_encode (encode x) (encode y);
decode p :=
x prod_decode_fst p = decode;
y prod_decode_snd p = decode; Some (x, y)
|}.
Next Obligation.
intros ?????? [x y]; simpl.
rewrite prod_decode_encode_fst, prod_decode_encode_snd.
simpl. by rewrite !decode_encode.
Qed.
Fixpoint list_encode_ (l : list positive) : positive :=
match l with [] => 1 | x :: l => prod_encode x (list_encode_ l) end.
Definition list_encode (l : list positive) : positive :=
prod_encode (Pos.of_nat (S (length l))) (list_encode_ l).
Fixpoint list_decode_ (n : nat) (p : positive) : option (list positive) :=
match n with
| O => guard (p = 1); Some []
| S n =>
x prod_decode_fst p; pl prod_decode_snd p;
l list_decode_ n pl; Some (x :: l)
end.
Definition list_decode (p : positive) : option (list positive) :=
pn prod_decode_fst p; pl prod_decode_snd p;
list_decode_ (pred (Pos.to_nat pn)) pl.
Lemma list_decode_encode l : list_decode (list_encode l) = Some l.
Proof.
cut (list_decode_ (length l) (list_encode_ l) = Some l).
{ intros help. unfold list_decode, list_encode.
rewrite prod_decode_encode_fst, prod_decode_encode_snd; simpl.
by rewrite Nat2Pos.id by done; simpl. }
induction l; simpl; auto.
by rewrite prod_decode_encode_fst, prod_decode_encode_snd;
simplify_option_equality.
Qed.
Program Instance list_countable `{Countable A} : Countable (list A) := {|
encode l := list_encode (encode <$> l);
decode p := list_decode p = mapM decode
|}.
Next Obligation.
intros ??? l. rewrite list_decode_encode. simpl.
apply mapM_fmap_Some; auto using decode_encode.
Qed.
Program Instance pos_countable : Countable positive := {|
encode := id; decode := Some; decode_encode x := eq_refl
|}.
Program Instance N_countable : Countable N := {|
encode x := match x with N0 => 1 | Npos p => Pos.succ p end;
decode p := if decide (p = 1) then Some 0%N else Some (Npos (Pos.pred p))
|}.
Next Obligation.
intros [|p]; simpl; repeat case_decide; auto with lia.
by rewrite Pos.pred_succ.
Qed.
Program Instance Z_countable : Countable Z := {|
encode x :=
match x with Z0 => 1 | Zpos p => p~0 | Zneg p => p~1 end;
decode p := Some
match p with 1 => Z0 | p~0 => Zpos p | p~1 => Zneg p end
|}.
Next Obligation. by intros [|p|p]. Qed.
Program Instance nat_countable : Countable nat := {|
encode x := encode (N.of_nat x);
decode p := N.to_nat <$> decode p
|}.
Next Obligation.
intros x. rewrite decode_encode; simpl. by rewrite Nat2N.id.
Qed.
Require Export countable list.
Obligation Tactic := idtac.
Class Finite A `{ x y : A, Decision (x = y)} := {
enum : list A;
enum_nodup : NoDup enum;
elem_of_enum x : x enum
}.
Arguments enum _ {_ _} : clear implicits.
Arguments enum_nodup _ {_ _} : 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 $ 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_eq_elem_of xs x) as [i Hi]; auto.
rewrite Nat2Pos.id by done; simpl.
rewrite Hi; eauto using list_find_eq_Some.
Qed.
Definition find `{Finite A} P `{ x, Decision (P x)} : option A :=
list_find P (enum A) = decode_nat.
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) eqn:?; simpl.
* eapply lookup_lt_Some, list_find_eq_Some; eauto.
* 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.
destruct (list_find_eq_elem_of xs x) as [j Hj]; auto.
rewrite Hj. eauto using list_find_eq_Some, 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.
intros Hx. destruct (list_find _ _) as [i|] eqn:Hi; simplify_option_equality.
rewrite !Nat2Pos.id in Hx by done.
destruct (list_find_Some P xs i) as (?&?&?); simplify_option_equality; eauto.
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 Hi]; auto.
rewrite Hi. destruct (list_find_Some P xs i) as (y&?&?); subst; auto.
exists y. simpl. by rewrite !Nat2Pos.id by done.
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.
intros. destruct finA, finB. apply NoDup_contains; auto using fmap_nodup_2.
Qed.
Lemma finite_injective_Permutation `{Finite A} `{Finite B} (f : A B)
`{!Injective (=) (=) f} : card A = card B f <$> enum A enum B.
Proof.
intros. apply contains_Permutation.
* 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.
(** 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',
(seq _ _ !! j) as [j'|] eqn:Hj'; simplify_equality.
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).
Context `{!Injective (=) (=) f} `{!Cancel (=) f g}.
Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
Next Obligation. apply (fmap_nodup _), enum_nodup. 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.
* rewrite elem_of_list_fmap. by intros (?&?&?).
* apply (fmap_nodup _); auto using enum_nodup.
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.
intros. apply NoDup_app; split_ands.
* apply (fmap_nodup _). by apply enum_nodup.
* intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
* apply (fmap_nodup _). by apply enum_nodup.
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 (enum_nodup A) as [|x xs Hx Hxs IH]; simpl.
{ constructor. }
apply NoDup_app; split_ands.
* apply (fmap_nodup _). by apply enum_nodup.
* 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.
induction (enum_nodup A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
apply NoDup_app; split_ands.
* by apply (fmap_nodup _).
* intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
intros ([k2 Hk2]&?&?) Hxk2; simplify_equality. destruct Hx. revert Hxk2.
induction xs as [|x' xs IH]; simpl in *; [by rewrite elem_of_nil |].
rewrite elem_of_app, elem_of_list_fmap, elem_of_cons.
intros [([??]&?&?)|?]; simplify_equality; auto.
* 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.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment