Require Import List. Import ListNotations. (* Define a class "Finite A" for finite types A. This can be done by requiring that there is a list of all elements. So, the class should have a list "elements : list A" of all elements of A and a proof that "elements" indeed contains (use In) all elements of A. *) (* Make the following types an instance of "Finite" *) Instance Unit_Finite : Finite unit := ... Instance Bool_Finite : Finite bool := ... Instance Unit_Empty : Finite Empty_set:= ... (* Now, make the disjoint union of two finite types and instance of "Finite" *) Instance Sum_Finite {A B : Type} {FA : Finite A} {FB : Finite B} : Finite (A + B) := ... (* Define the following function that returns a list of all pairs where the first component comes from l1 and the second from l2. *) Fixpoint listProd {A B : Type} (l1 : list A) (l2 : list B) : list (A * B) := ... (* Prove the following two lemmas by induction on l (resp l1). The first lemma should also give you a hint how to implement the previous function. *) Lemma inProd' {A B : Type} : forall (a : A) (b : B) (l : list B), In b l -> In (a,b) (map (fun b => (a,b)) l). Lemma inProd {A B : Type} : forall (l1 : list A) (l2 : list B) (a : A) (b : B) , In a l1 -> In b l2 -> In (a,b) (listProd l1 l2). (* Now, you use listProd and inProd to make A*B an instance of "Finite" if A and B are. *) Instance Prod_Finite {A B : Type} {FA : Finite A} {FB : Finite B} : Finite (A * B) := ... (* Prove the following two lemmas for finite types. *) Lemma all_correct {A : Type} {FA : Finite A} (p : A -> bool) : forallb p elements = true <-> forall (x : A), p x = true. Lemma ex_correct {A : Type} {FA : Finite A} (p : A -> bool) : existsb p elements = true <-> exists (x : A), p x = true.