First steps with Coq

Assia Mahboubi

From mathcomp Require Import all_ssreflect.

Exercise 1: booleans

Implement the exclusive disjunction on booleans

Definition xorb b := (* your definition here *) Lemma xorTb b : xorb true b = ~~ b. Proof. admit. (* your proof here *) Admitted. (* turn into Qed once done *) Lemma xorbN a b : xorb a (negb b) = negb (xorb a b). Proof. admit. (* your proof here *) Admitted. (* turned into Qed once done *)

Exercise 2: natural numbers

Implement a boolean equality test on natural numbers

Fixpoint eqn (m n : nat) : bool := (* your definition here *) Lemma eq_eqn (n m : nat) : n = m -> eqn n m = true. Admitted. Lemma eqn_eq (n m : nat) : eqn n m = true -> n = m. Admitted.

Exercise 3: Save the trees

Define an inductive type for binary trees (without labels)

Inductive tree : Set := (* your definition here *)

Define a function counting the number of nodes in a tree

Fixpoint size (t : tree) : nat := (* your definition here *)

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

Definition one_tree : tree := (* your definition here *) Definition three_tree : tree := (* your definition here *) Eval compute in size one_tree. Eval compute in size three_tree.

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.

Print maxn. Fixpoint depth (t : tree) : nat := (* your definition here *) (* Don't forget to test your function! *)

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

Lemma leq_depth_size (t : tree) : (* your statement here *). Proof. (* your proof here *) Qed.