From mathcomp Require Import all_ssreflect.

(* 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 *)


(* 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.

(* 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.
 *)
Fixpoint depth (t : tree) : nat :=  (* your definition here *)

(* Test your depth function *)

(* State and prove that the size of a binary_tree is always positive. *)
Lemma lt0_size (t : tree) :  (* your statement here *).
Proof.
(* your proof here *)
Qed.

(* 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.