(* Third assignment for the course G54DTP. *)
(*  Venanzio Capretta, March 2011.         *)
(* Each part is worth 2 points.            *)

Require Import ZArith.
Require Import List.

Set Implicit Arguments.

(* Recall the definition of vectors. *)

Inductive Vector (A:Set): nat -> Set :=
  vnull: Vector A 0
| vcons: forall n, A -> Vector A n -> Vector A (S n).

(* The function that appends two vectors. *)

Fixpoint vapp (A:Set)(n1:nat)(v1:Vector A n1)(n2:nat)(v2:Vector A n2):
  Vector A (n1+n2) :=
match v1 with
  vnull => v2
| vcons n x v1' => vcons x (vapp v1' v2)
end.


(* PART 1 *)

(* A different way of defining vectors is by a recursive tuple type. *)

Fixpoint Tuple (A:Set)(n:nat): Set :=
match n with
  O => unit
| S n' => (A*(Tuple A n'))%type
end.

(* Define functions that transform vectors to tuples and viceversa. *)

Fixpoint vector_tuple (A:Set)(n:nat)(v:Vector A n): Tuple A n := ?

Fixpoint tuple_vector (A:Set)(n:nat): Tuple A n -> Vector A n := ?

(* PART 2 *)

(* Binary trees of fixed depth with integer labels on the nodes. *)

Inductive dTree : nat -> Set :=
  dleaf : dTree O
| dnode : Z -> forall n, dTree n -> dTree n -> dTree (S n).

(* Define the function that returns the list of labels of a tree. *)

Fixpoint dflatten (n:nat)(t:dTree n): list Z := ?

(* Define the function that returns the vector of labels of a tree.
    First you need to define a function that gives the size of the vector.
*)

Fixpoint dsize (n:nat): nat := ?

Fixpoint dvector (n:nat)(t:dTree n): Vector Z (dsize n) := ?


(* PART 3 *)

(* Define the function returning the label of the root of a tree. *)

Fixpoint droot (n:nat)(t: dTree (S n)) : Z := ?

(* Define the function returning the left subtree. *)

Fixpoint dleft (n:nat)(t: dTree (S n)): dTree n := ?

(* Define the function returning the right subtree. *)

Fixpoint dright (n:nat)(t: dTree (S n)): dTree n := ?

(* Define the addition operation for trees. *)

Fixpoint dadd (n:nat): dTree n -> dTree n -> dTree n := ?


(* PART 4 *)

Require Import Min.

(* Recall the definitions of head and tail of a vector. *)

Definition vhead (A:Set)(n:nat)(v:Vector A (S n)): A :=
match v with
  vnull => tt
| vcons n x v' => x
end.

Definition vtail (A:Set)(n:nat)(v:Vector A (S n)): Vector A n :=
match v with
  vnull => tt
| vcons n x v' => v'
end.

(* Define a function that splits a vector in two parts of specified sizes. *)

Fixpoint vsplit (n m:nat): Vector Z (n+m) -> Vector Z n * Vector Z m := ?

(* Define a function that creates a tree from a vector of correct size. *)

Fixpoint vdtree (n:nat): Vector Z (dsize n) -> dTree n := ?


(* PART 5 *)

(* Define an inductive predicate on list of naturals,
   that is satisfied whenever the list is in increasing order.
*)

Inductive IncList : list nat -> Prop := ?

(* If you defined it correctly,
   you should be able to prove the following lemma.
*)

Lemma inc_example : IncList (2::5::5::6::9::nil).
Proof.
?
Qed.