Require Import ssrmatching ssreflect.


Module ExerciseOne.

(* In fact type nat is already available *)
Print nat.

(* Program a boolean test of equality eq_nat : nat -> nat -> bool *)
Fixpoint eq_nat (n m : nat) : bool :=
  match n, m with
    |O, O => true
    |S k, S l => eq_nat k l
    |_, _ => false
  end.

(* Prove the following lemma. There is a (small) trick. *)
Lemma eq_nat_eq (n m : nat) : eq_nat n m = true -> n = m.
Proof.
elim: n m => [|n ihn].
- by case.
- case => // m /=.
  move/ihn.
  move=> ->.
  apply: eq_refl.
Qed.

(* Define a function leq : nat -> nat -> bool *)
(* such that leq n m = true iff n is smaller or equal than m *)

(* Define an inductive type nat_bintree with two constructors, representing *)
(* binary trees labelled with natural numbers *)
Inductive nat_bintree : Type :=
| Leaf : nat -> nat_bintree 
| Node : nat -> nat_bintree -> nat_bintree -> nat_bintree.

(* Define a function is_Leaf : nat_bintree -> bool which tests whether a *)
(* bin_tree has a single leaf *)
Fixpoint is_Leaf (t : nat_bintree) : bool :=
  match t with
    |Leaf _ => true
    | _ => false
  end.

(* Program a boolean test of equality *)
(* eq_nat_bintree : nat_bintree -> nat_bintree -> bool *)
(* Hint : you can use andb : bool -> bool -> bool, which is available by *)
(* default. *)
Print andb.

Fixpoint eq_nat_bintree (t1 t2 : nat_bintree) : bool :=
  match t1, t2 with
    |Leaf n1, Leaf n2 => eq_nat n1 n2
    |Node n1 tl1 tr1, Node n2 tl2 tr2 => 
     andb (eq_nat n1 n2) (andb (eq_nat_bintree tl1 tl2) (eq_nat_bintree tr1 tr2))
    |_, _ => false
  end.

(* Prove the following lemma *)
Lemma Leaf_Node_not_eq (t : nat_bintree) : 
  is_Leaf t = true -> forall n t1 t2, eq_nat_bintree t (Node n t1 t2) = false.
Proof.
case: t => [n|n t1 t2].
- simpl. move=> _ _ _ _. apply: eq_refl.
- simpl. discriminate.
Qed.

(* Define an inductive type nat_pair whose elements are pairs of *)
(* natural numbers *)
Inductive nat_pair : Type := NatPair : nat -> nat -> nat_pair.

(* Define an inductive type mono_pair whose elements are pairs of *)
(* a same but arbitrary type *)
(* Hint : look at the definition of lists *)
Print list.

Inductive mono_pair (A : Type) : Type := MonoPair : A -> A -> mono_pair A.

(* What is the type of mono_pair? *)

(* Define an inductive type my_pair  whose elements are pairs of *)
(* two a priori different types*)
Inductive my_pair (A B : Type) : Type := MyPair : A -> B -> my_pair A B.

(* What is the type of my_pair? *)

(* Define a function my_first projecting a term of type my_pair on its *)
(* first component. What is the type of my_first? *)


Definition my_first (A B : Type) (t : my_pair A B) :=
  match t with
    |MyPair a _ => a
  end.

(* Same exercise for the second component. *)

Definition my_second (A B : Type) (t : my_pair A B) :=
  match t with
    |MyPair _ b => b
  end.

(* Prove the following lemma: *)
Lemma surjective_pairing (A B : Type) (t1 t2 : my_pair A B) : 
  my_first A B t1 = my_first A B t2 -> 
  my_second A B t1 = my_second A B t2 -> t1 = t2.
Proof.
case: t1 => a1 b1 /=.
case: t2 => a2 b2 /= -> ->.
apply: eq_refl.
Qed.

(* Define the type of polymorphic lists (i.e. lists of elements in a paramter*)
(* type A. Browse file seq.v *)
End ExerciseOne.