(* 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 :=