# CS 6115 Problem Set 0: Basic Functional Programming in Coq

- Due: August 31 at midnight

0. Write a function length to compute the length of list.
length : forall {A:Type}, list A -> nat
1. Write a function rev that reverses a list.
rev : forall {A:Type}, list A -> list A
2. Write a function ith that returns the ith element of a list,
if the list has enough elements, and otherwise returns None.
We are working zero-based, so for instance,
ith 2 (1::2::3::4::nil) should return Some 3, whereas
ith 4 (1::2::3::4::nil) should return None.
ith : forall {A:type}, nat -> list A -> option A
3. Write a generic function comp to compose two functions.
comp : forall {A B C:Type}, (A -> B) -> (B -> C) -> (A -> C)
4. Write a function sum that adds up all of the nats in a list.
sum : list nat -> nat
5. Write a function that map that maps a function over the
elements in a list, producing a new list.
map : forall {A B:Type}, (A -> B) -> list A -> list B
6. Write a generic "fold-right" for a list such that, for instance.
fold (fun x y => x + y) 0 (1::2::3::nil) evaluates to 6.
fold : forall {A B:Type}, (A -> B -> B) -> B -> list A -> B
7. Write a function add_pairs that takes a list of pairs of nats and
returns the list of the corresponding sums. For instance,
add_pairs ((1,2)::(3,4)::nil) should return 3::7::nil.
add_pairs : list (nat * nat) -> list nat
Use one of the list functions you have defined rather than a Fixpoint
to implement this.
8. Given the following definition for trees:

Inductive tree (A:Type) : Type :=

| Leaf : tree A

| Node : tree A -> A -> tree A -> tree A.

Arguments Leaf [A]. Arguments Node [A].

| Leaf : tree A

| Node : tree A -> A -> tree A -> tree A.

Arguments Leaf [A]. Arguments Node [A].

9. Write a function which flattens the tree into a list.
For instance, flatten on the tree:
3
/ \
1 7
/ \ / \
o o o o
should yield 1::3::7::nil.
flatten : forall {A:Type}, tree A -> list A

Inductive order : Type :=

| Less

| Equal

| Greater.

10. Write a function which when given two numbers n and m,
returns Less if n < m, Equal if n = m, and otherwise
returns Greater.
nat_cmp : nat -> nat -> order
11. Write a function that determines whether a tree nat is
a valid search tree in the sense that for a given node
with value n, all elements in the left sub-tree should
be less than n and all elements in the right sub-tree
should be greater than n.
search_tree : tree nat -> bool

This page has been generated by coqdoc