Need to use Coq functional programming language to solve below question:

Problem 6 (34 points). Binary Trees: Bring in the inductive definition of binary trees, and accomplish

the following:

(a) Define mytree2 of type tree nat depicted in Figure 2. (1 points)

(b) Define the function pre_order that returns the list of values within the binary tree, using pre-order

traversal. (4 points)

(c) As a unit test, show that pre-order traversal of mytree2 is [1;2;4;5;3]. (1 points)

(d) Define the function in_order that returns the list of values within the binary tree, using in-order

traversal. (4 points)

(e) As a unit test, show that in-order traversal of mytree2 is [4;2;5;1;3]. (1 points)

(f) Define the function post_order that returns the list of values within the binary tree, using post-order

traversal. (4 points)

(g) As a unit test, show that post-order traversal of mytree2 is [4;5;2;3;1]. (1 points)

(h) Prove that for any arbitrary binary tree t, the length of the list generated by pre-order traversal of t is

the same as the length of the list generated by the post-order traversal of t. (4 points)

(i) Bring in the function that counts the number of nodes within a binary tree. Prove that for any arbitrary

binary tree, count of the nodes of that tree is the same as the length of the list generated by pre-order

traversal of that tree. (4 points)

(j) Consider the following definition for the height of binary trees.

Fixpoint height_btr {X: Type} (btr : btree X) : nat :=

match btr with

| emp_btr => 0

| node_btr _ t1 t2 => 1 + max (height_btr t1) (height_btr t2)

end.

Show that for any arbitrary binary tree t, height_btr of t is less-than-or-equal-to (leb) the number

of nodes within t. (10 points) Hint: You may need to define lemmas to prove intermediary properties

in relation to max and leb.

2 3 5 Figure 2: mytree2 2 3 5 Figure 2: mytree2