First steps with Coq

Assia Mahboubi

Exercise 1: booleans

Implement the exclusive disjunction on booleans

Exercise 2: natural numbers

Implement a boolean equality test on natural numbers

Exercise 3: Save the trees

Define an inductive type for binary trees (without labels)

Define a function counting the number of nodes in a tree

Define a tree with one node, with three nodes, and test your size function

Define a function counting the depth of the tree. Hint: you can use the function maxn : nat -> nat -> nat to compute the maximum of two natural numbers. Then test your depth function.

State and prove that the height is smaller than the number of nodes.