(* MGS 08 : COQ 4th exercise *) Section BT. Inductive BT : Set := | L : BT | N : BT -> BT -> BT. (* implement a certified decision procedure for equality of binary trees. *) Program Fixpoint eqBT (t u: BT) : {t = u} + { t <> u } := End BT. Section Fin. Inductive Fin : nat -> Set := | fz : forall n:nat,Fin (S n) | fs : forall n:nat,Fin n -> Fin (S n). Set Implicit Arguments. (* Implement the following functions on finite sets: fmax : returns the maximal element femb : embes Fin n into Fin (S n) without changing the value. finv : mirrors the elements, mapping i to n-i in Fin n. *) Program Fixpoint fmax (n:nat) : Fin (S n) := Program Fixpoint femb (n:nat) (i:Fin n) {struct i} : Fin (S n) := Program Fixpoint finv (n:nat) (i:Fin n) {struct i} : Fin n := End Fin. Section vec. Set Implicit Arguments. Variable A:Set. Inductive Vec : nat -> Set := | vnil : Vec 0 | vcons : forall n:nat,A -> Vec n -> Vec (S n). End vec. Section vapp. Variables A B : Set. (* Implement vectorized application (vapp) and the cretaion of constant vectors (vreturn) this establishing that Vec - n is a applicative functor. *) Set Implicit Arguments. Program Fixpoint vapp (n:nat) (fs : Vec (A -> B) n) (bs : Vec A n) {struct fs}: Vec B n := Program Fixpoint vreturn (n:nat) (a:A) : Vec A n := End vapp. Section vtransp. Set Implicit Arguments. Program Definition vmap (A B:Set) (n:nat) (f : A -> B) (v : Vec A n) : Vec B n := vapp (vreturn n f) v. (* Implement vtransp which transposes a matrix represented as a vector of vectors. *) Program Fixpoint vtransp (A:Set) (n m:nat) (vs : Vec (Vec A n) m) {struct vs} : Vec (Vec A m) n :=