ch6.v

Require Import Nat.
Require Import Arith.
Require Import ZArith.
Require Import FunctionalExtensionality.
Require Import List.
Import ListNotations.

Open Scope nat_scope.

(* Exercise 6.1 *)
(* Define an inductive type for seasons and then
  use the function month_rec to define a function
  that maps every month to the season that contains
  most of its days. *)

Inductive month : Set :=
  | January
  | February
  | March
  | April
  | May
  | June
  | July
  | August
  | September
  | October
  | November
  | December.

Inductive season : Set :=
  | Winter
  | Spring
  | Summer
  | Autumn.

Definition month_season_rec :=
  month_rec (fun _ => season)
    Winter Winter Spring
    Spring Spring Summer
    Summer Summer Autumn
    Autumn Autumn Winter.

(* Exercise 6.2 *)
(* What are the types of bool_ind and bool_rec
  that are generated by the Coq system for the type bool? *)

Check bool_ind.
(* forall P : bool -> Prop, P true -> P false -> forall b : bool, P b *)
Check bool_rec.
(* forall P : bool -> Set, P true -> P false -> forall b : bool, P b *)

(* Exercise 6.3 *)
(* Prove in two different ways the following theorem: *)

Definition bool_equal := forall b : bool, b = true \/ b = false.

(* 1. By directly building a proof term with the right type,
  with the help of theorems or_introl, or_intror,
  and refl_equal *)

Definition bool_eq_term : bool_equal :=
  fun b => bool_ind (fun b => b = true \/ b = false)
    (or_introl refl_equal) (or_intror refl_equal) b.

(* 2. By using pattern, apply, left, right, and reflexivity.*)

Definition bool_eq_proof : bool_equal.
Proof.
  intro.
  pattern b.
  apply bool_ind.
  - apply or_introl. reflexivity.
  - apply or_intror. reflexivity.
Qed.

(* Exercise 6.4 *)
(* Using the type introduced for seasons in Exercise 6.1
  page 139, write the function that maps any month to the season
  that contains most of its days, this time using the pattern
  matching construct. *)

Definition month_season (m : month) : season := 
  match m with
  | December | January | February => Winter
  | March | April | May => Spring
  | June | July | August => Summer
  | September | October | November => Autumn
  end.

(* Exercise 6.5 *)
(* Write the function that maps every month that has an even
  number of days to the boolean value true and the others to false. *)

Definition month_length (leap : bool) (m : month) : nat :=
  match m with
  | February => if leap then 29 else 28
  | April | June | September | November => 30
  | _ => 31
  end.

Definition even_days (leap : bool) : month -> bool :=
  fun m : month => even (month_length leap m).

(* Exercise 6.6 *)
(* Define the functions bool_xor, bool_and, bool_or, bool_eq
  of type bool -> bool -> bool, and the function bool_not of
  type bool -> bool. Prove the following theorems: *)

Definition bool_xor (a b : bool) := 
  match a, b with
  | true, true | false, false => false
  | _, _ => true
  end.

Definition bool_and (a b : bool) :=
  match a, b with
  | true, true => true
  | _, _ => false
  end.

Definition bool_or (a b : bool) :=
  match a, b with
  | false, false => false
  | _, _ => true
  end.

Definition bool_eq (a b : bool) :=
  match a, b with
  | true, true | false, false => true
  | _, _ => false
  end.

Definition bool_not (b : bool) :=
  match b with
  | false => true
  | true => false
  end.

Goal forall b1 b2 : bool, bool_xor b1 b2 = bool_not (bool_eq b1 b2).
Proof. intros; elim b1; elim b2; simpl; reflexivity. Qed.

Goal forall b1 b2 : bool,
  bool_not (bool_and b1 b2) = bool_or (bool_not b1) (bool_not b2).
Proof. intros; elim b1; elim b2; simpl; reflexivity. Qed.

Goal forall b : bool, bool_not (bool_not b) = b.
Proof. apply bool_ind; simpl; reflexivity. Qed.

Goal forall b : bool, bool_or b (bool_not b) = true.
Proof. apply bool_ind; simpl; reflexivity. Qed.

Goal forall b1 b2 : bool, bool_eq b1 b2 = true -> b1 = b2.
Proof.
  intros b1 b2; elim b1; elim b2; simpl;
  try reflexivity;
  intros H; rewrite H; reflexivity.
Qed.

Goal forall b1 b2 : bool, b1 = b2 -> bool_eq b1 b2 = true.
Proof.
  intros b1 b2; elim b1; elim b2; simpl;
  try reflexivity;
  intros H; rewrite H; reflexivity.
Qed.
  
Goal forall b1 b2 : bool,
  bool_not (bool_or b1 b2) = bool_and (bool_not b1) (bool_not b2).
Proof.
  intros b1 b2; elim b1; elim b2; simpl; reflexivity.
Qed.

Goal forall b1 b2 b3 : bool,
  bool_or (bool_and b1 b3) (bool_and b2 b3) = bool_and (bool_or b1 b2) b3.
Proof.
  intros; elim b1; elim b2; elim b3; simpl; reflexivity.
Qed.

(* Exercise 6.7 *)
(* What is the type of plane_rec? *)

Inductive plane' : Set := point' : Z -> Z -> plane'.
Check plane'_rec.

(* forall P : plane -> Set, 
    (forall z z0 : Z, P (point z z0)) -> forall p : plane, P p *)

(* Note: There is a discrepancy between the book and output seen here *)

Record plane : Set := point {abscissa: Z; ordinate: Z}.

(* Note (cont.): 
  In the book, it states that this definition yields the same 
  printout as the defintion above:
    Inductive plane : Set := point : Z -> Z -> plane
  
  However, using Coq 8.17, this is not the case.
  As a result, there is no _plane_rec_ generated for
  the Record definition.

  It seems Records have distinguished themselves from their
  behaviourally adjacent inductive types.

  If this is an actual chnage in Coq's implmentation, a
  possible motivation could be the integration of
  typeclasses, which is presumably a fairly new feature.

  Further investigation would involve checking versions
  in between the textbook realease version and 8.17 to 
  discover how record types may have changed.
*)

(* Exercise 6.8 *)
(* Define a function that computes the "Manhattan" distance
  for points of the plane (the Manhattan distance is the sum
  of the absolute values of differences of coordinates *)

Open Scope Z_scope.
Definition manhattan : plane -> plane -> Z :=
  fun p1 p2 => 
    let (x1, y1) := p1 in 
    let (x2, y2) := p2 in
    (Z.abs (x1 - x2)) + (Z.abs (y1 - y2)).
Close Scope Z_scope.

(* Exercise 6.9 *)
(* What is the type of vehicle_rec? Use this function to define
  an equivalent to nb_seats. *)

Inductive vehicle : Set :=
  bicycle : nat -> vehicle | motorized : nat -> nat -> vehicle.

Check vehicle_rec.
(* 
  forall P : vehicle -> Set 
    (forall n : nat, P (bicycle n)) ->
    (forall n n0 : nat, P (motorized n n0)) ->
    forall v : vehicle, P v
*)

Definition nb_seats (v : vehicle) : nat :=
  match v with
  | bicycle x => x
  | motorized x _ => x
  end.

Definition nb_seats' (v : vehicle) : nat :=
  vehicle_rec (fun _ => nat)
    (fun n => n)
    (fun n _ => n) v.

Goal forall v, nb_seats v = nb_seats' v.
Proof.
  unfold nb_seats, nb_seats'.
  intros. elim v; simpl; auto.
Qed.

(* Exercise 6.10 *)
(* Define a function is_January that maps January
  to True and any other month to False, using the
  function month_rect *)

Definition is_January : month -> Prop :=
  month_rect _
    True False False False False False
    False False False False False False.

(* Exercise 6.11 *)
(* Use the same technique to build a proof of true =/= false. *)

Goal (true <> false).
Proof.
  unfold not; intros H.
  change ((fun b : bool =>
    match b with | true => True | false => False end) false).
  rewrite <- H.
  trivial.
Qed.

(* Exercise 6.12 *)
(* For the vehicle type (see Sect. 6.1.6), use the same
  technique to build a proof that no bicycle is equal to a
  motorized vehicle. *)

Goal forall a b c, (bicycle a) <> (motorized b c).
Proof.
  unfold not; intros a b c H.
  change ((fun v => match v with
    | bicycle _ => True 
    | motorized _ _ => False
    end) (motorized b c)).
  rewrite <- H.
  trivial.
Qed.

(* Exercise 6.13 *)
(* This exercise shows a use of discriminate and underlines
  the danger of adding axioms to the system. The "theory"
  introduced here proposes a description of rational numbers
  as fractions with a non-zero denominator. An axiom is added
  to indicate that two rational numbers are equal as soon as they
  satisfy a classical arithmetic condition. *)
Section RatPlusTemp.

Record RatPlus : Set :=
  mkRat {top : nat; bottom : nat; bottom_condition : bottom <> O}.

Axiom eq_RatPlus : forall r r' : RatPlus,
  top r * bottom r' = top r' * bottom r -> r = r'.

(* Prove that this theory is inconsistent (just construct a
  proof of False). When this exercise is solved, you should
  remove this construction from the environment, using the command
  Reset eq_RatPlus. *)

Goal False.
Proof.
  assert (H1: 1 <> 0); auto.
  assert (H2: 2 <> 0); auto.
  cut ((mkRat 1 1 H1) = (mkRat 2 2 H2)).
  - discriminate.
  - apply eq_RatPlus; simpl; reflexivity.
Qed.

End RatPlusTemp.

(* Exercise 6.14 *)
(* Reproduce the above discussion for the function
  mult: compile a table describing convertibility
  for simple patterns of the two arguments. *)

Fixpoint mult (n m : nat) {struct n} : nat :=
  match n with
  | O   => O
  | S p => (plus m (mult p m))
  end.

(* 
  mult 0 0              => 0
  mult 0 m              => m
  mult (S p) 0          => 0 + (mult p 0)
  mult (S p) m          => m + (mult p m)
  mult (S (S p)) (S m)  => (S m) + (mult (S p) (S m))
*)

(* Exercise 6.15 *)
(* Define a function of type nat->bool that only
  returns true for numbers smaller than 3, in other
  terms "S (S (S 0))." *)

Definition lt3 n :=
  match n with
  | S (S (S n)) => false
  | _ => true
  end.

(* Exercise 6.16 *)
(* Define an addition function so that the principal
  argument is second instead of first argument. *)

Fixpoint plus' (n m : nat) {struct m} : nat :=
  match m with
  | O   => n
  | S p => S (plus' n p)
  end.
    
(* Exercise 6.17 *)
(* Define a function sum_f that takes as arguments
  a number n and a function f of type nat->Z and returns
  the sum of all values of f for the natural numbers that
  are strictly smaller than n. *)

Fixpoint sum_f (n : nat) (f : nat->nat) : nat :=
  match n with
  | O   => O
  | S n => (f n) + (sum_f n f)
  end.

(* Exercise 6.18 *)
(* Define two_power:nat->nat so that "two_power n" is 2^n. *)

Fixpoint two_power (n : nat) : nat :=
  match n with
  | O   => 1
  | S n => 2 * (two_power n)
  end.

(* Exercise 6.19 *)
(* What is the representation in the type _positive_
  for numbers 1000, 25, 512? *)

(* 1000 = 1111101000_b*)
Check xO (xO (xO (xI (xO (xI (xI (xI (xI (xH))))))))).

(* 25 = 11001_b *)
Check xI (xO (xO (xI xH))).

(* 512 = 100000000_b *)
Check xO (xO (xO (xO (xO (xO (xO (xO xH))))))).

(* Exercise 6.20 *)
(* Build the function pos_even_bool of type _positive->bool_
that returns the value true exactly when the argument is even. *)
Definition pos_even_bool (p : positive) : bool :=
  match p with
  | xO _ => true
  | _    => false
  end.

SearchPattern (positive->Z).

(* Exercise 6.21 *)
(* Build the function pos_div4 of type positive->Z that
  maps any number z to the integer part of z/4. *)
Definition pos_div4 (p : positive) : Z :=
  match p with
  | xO (xO p') | xO (xI p')
  | xI (xO p') | xI (xI p') =>  Zpos p' 
  | _ => 0
  end.

(* Exercise 6.22 *)
(* Assuming there exists a function pos_mult that
  describes the multiplication of two positive
  representations and returns a positive representation,
  use this function to build a function that multiplies
  numbers of type Z and returns a value of type Z. *)

Definition Zmult : Z->Z->Z := fun a b =>
  match a, b with
  | Zpos p, Zpos q | Zneg p, Zneg q => Zpos (Pos.mul p q)
  | Zneg p, Zpos q | Zpos p, Zneg q => Zneg (Pos.mul p q)
  | _, _ => 0%Z
  end.

(* Exercise 6.23 *)
(* Build the inductive type that represents the language
  of propositional logic without variables:
    L = L/\L | L\/L | ~L | L => L | L_True | L_False *)

Inductive prop :=
  | L_And : prop->prop->prop
  | L_Or : prop->prop->prop
  | L_Not : prop->prop
  | L_Imp : prop->prop->prop
  | L_True : prop
  | L_False : prop.

(* Exercise 6.24 *)
(* Every strictly positive rational number can be
  obtained in a unique manner by a succession of
  applications of functions N and D on the number one,
  where N and D are defined by the following equations:

    N(x) = 1 + x, D(x) = 1 / (1 + (1 / x)) 
  
  We can associate any strictly positive rational number
  with an element of an inductive type with one constructor
  for one, and two other constructors representing the
  functions N and D. Define this inductive type (see
  the related exercise 6.44).
*)

Inductive rational :=
  | rI : rational
  | rN : rational->rational
  | rD : rational->rational.

(* Exercise 6.25 *)
(* The Coq library ZArith provides a function
    Zeq_bool : Z -> Z -> bool
  to compare two integer values and return a boolean
  value expressing the result. Using this function define
  a function value_present with the type
    value_present : Z -> Z_btree -> bool
  that determines whether an integer appears
  in a binary tree. *)

Inductive Z_btree : Set :=
  Z_bleaf : Z_btree | Z_bnode : Z->Z_btree->Z_btree->Z_btree.

Fixpoint value_present (z : Z) (t : Z_btree) : bool :=
  match t with
  | Z_bleaf => false
  | Z_bnode x l r => (Zeq_bool x z) || value_present z l || value_present z r
  end.

(* Exercise 6.26 *)
(* Define a function power: Z->nat->Z to compute the power
  of an integer and a function discrete_log:
  positive->nat that maps any number p
  to the number n such that 2^n =< p < 2^(n+1). *)

Fixpoint discrete_log (p : positive) : nat :=
  match p with
  | xH => 0
  | xO p' | xI p' => 1 + discrete_log p'
  end.

(* Exercise 6.27 *)
(* Define a function zero_present: Z_fbtree->bool that 
  maps any tree x to true if and only ifa contains the
  value zero. *)

Inductive Z_fbtree : Set :=
 | Z_fleaf : Z_fbtree
 | Z_fnode : Z -> (bool->Z_fbtree) -> Z_fbtree.

Fixpoint zero_present (t : Z_fbtree) : bool :=
  match t with
  | Z_fleaf => false
  | Z_fnode x f => (Z.eqb x 0)
    || zero_present (f true) || zero_present (f false)
  end.

(* Exercise 6.28 *)
(* Define a function that checks whether the zero value
  occurs in an infinitely branching tree at a node 
  reachable only by indices smaller than a number n. *)

Inductive Z_inf_branch_tree: Set :=
  | Z_inf_leaf : Z_inf_branch_tree
  | Z_inf_node : Z -> (nat->Z_inf_branch_tree) -> Z_inf_branch_tree.

Fixpoint or_f (n : nat) (f : nat -> bool) : bool :=
  match n with
  | O => false
  | S n' => f n' || or_f n' f
  end. 

Fixpoint zero_present_inf (n : nat) (t : Z_inf_branch_tree) : bool :=
  match t with
  | Z_inf_leaf => false
  | Z_inf_node x f => (Z.eqb x 0) 
    || or_f n (fun i => zero_present_inf n (f i)) 
  end.

(* Exercise 6.29 *)
(* Redo the proof of theorem plus_n_0, using only the tactics
  intro, assumption, elim, simpl, apply, and reflexivity. *)

Goal forall n:nat, n = n + 0.
Proof.
  intro.
  elim n.
  - reflexivity.
  - intro m; intro H.
    simpl. rewrite <- H; reflexivity.
Qed.

(* Exercise 6.30 *)
(* This exercise uses the types Z_btree and Z_fbtree
  introduced in Sects. 6.3.4 and 6.3.5.1. Define functions
    f1: Z_btree -> Z_fbtree and f2: Z_fbtree -> Z_btree
  that establish the most natural bijection between the
  two types (see Sects. 6.3.4 and 6.3.5.1). Prove the 
  following lemma:
    forall t:Z_btree, f2 (f1 t) = t.
  What is missing to prove the following statement?
    forall t:Z_fbtree, f1 (f2 t) = t. 
*)

Print Z_btree.

Fixpoint f1 (t : Z_btree) : Z_fbtree :=
  match t with
  | Z_bleaf => Z_fleaf
  | Z_bnode x l r => Z_fnode x (fun b => if b then f1 l else f1 r)
  end.

Fixpoint f2 (t : Z_fbtree) : Z_btree :=
  match t with
  | Z_fleaf => Z_bleaf
  | Z_fnode x f => Z_bnode x (f2 (f true)) (f2 (f false))
  end.

Goal forall t:Z_btree, f2 (f1 t) = t.
Proof.
  intros.
  elim t; simpl.
  - reflexivity.
  - intros x l IHl r IHr.
    rewrite IHl, IHr.
    reflexivity.
Qed.

(* Second proof requires functional extensionality *)

Theorem f_equal : forall (A B : Type) (f: A -> B) (x y: A),
  x = y -> f x = f y.
Proof. intros A B f x y eq. rewrite eq. reflexivity. Qed.

Goal forall t:Z_fbtree, f1 (f2 t) = t.
Proof.
  intros.
  elim t; simpl.
  - reflexivity.
  - intros x f H.
    apply f_equal.
    extensionality b.
    elim b; apply H.
Qed.

(* Exercise 6.31 *)
(* Prove forall n : nat, (mult2 n) = n+n (see Sect. 6.3.3) *)

Fixpoint mult2 (n:nat) : nat :=
  match n with
  | O => O
  | S p => S (S (mult2 p))
  end.

Goal forall n : nat, (mult2 n) = n+n.
Proof.
  intros.
  elim n; simpl.
  - reflexivity.
  - intros; rewrite H.
    f_equal.
    apply plus_n_Sm.
Qed.

(* Exercise 6.32 *)
(* The sum of the first n natural numbers is defined
  with the following function: *)

Fixpoint sum_n (n:nat) : nat :=
  match n with
  | O => O
  | S p => S p + sum_n p
  end.

(* Prove the following statement: *)
Goal forall n:nat, 2 * sum_n n = n*n + n.
Proof.
  intros.
  elim n; simpl.
  - reflexivity.
  - intros m H.
    rewrite <- plus_n_O in *.
    repeat rewrite <- plus_n_Sm.
    f_equal. f_equal. 
    rewrite Nat.mul_succ_r.
    rewrite <- H.
    rewrite Nat.add_assoc, Nat.add_comm.
    repeat rewrite Nat.add_assoc.
    f_equal. f_equal.
    apply Nat.add_comm.
Qed.

(* Exercise 6.33 *)
(* Prove the following statement: *)
Goal forall n:nat, n <= sum_n n.
Proof.
  intros. elim n; simpl.
  - reflexivity.
  - intros m H.
    apply le_n_S.
    apply Nat.le_add_r.
Qed.

(* Exercise 6.34 *)
(* Build a polymorphic function that takes a list as
  argument and returns a list containing the first two
  elements when they exist. *)
(* Assumption: when one element is present, return it *)

Definition first_two {A : Set} (l : list A) : list A :=
  match l with
  | cons a l' => match l' with
    | nil => cons a nil
    | cons b l'' => cons a (cons b nil)
    end
  | _ => nil
  end.

Compute first_two [3;4;5].
Compute first_two [6].

(* Exercise 6.35 *)
(* Build a function that takes a natural number, n,
  and a list as arguments and returns the list containing
  the first n elements of the list when they exist. *)

Fixpoint first_n {A : Set} (n : nat) (l : list A) : list A :=
  match n, l with
  | S n', cons x l' => cons x (first_n n' l')
  | _, _ => nil
  end.

Compute first_n 2 [3;4;5].
Compute first_n 5 [3;4;5].

(* Exercise 6.36 *)
(* Build a function that takes a list of integers as
  argument and returns the sum of these numbers. *)

Fixpoint sum_list (l : list Z) : Z :=
  match l with
  | nil => 0
  | cons x l' => x + sum_list l'
  end.

Compute sum_list [1%Z;2%Z;3%Z;4%Z].

(* Exercise 6.37 *)
(* Build a function that takes a natural number n as
  argument and builds a list containing n occurrences of
  the number one. *)

Fixpoint n_ones (n : nat) : list nat :=
  match n with
  | O => nil
  | S n' => cons 1 (n_ones n')
  end.

Compute n_ones 6.

(* Exercise 6.38 *)
(* Build a function that takes a number n and returns the
  list containing the integers from 1 to n, in this order. *)

Fixpoint tri_list (n : nat) : list nat :=
  match n with
  | O => nil
  | S O => [1]
  | S n' => (tri_list n') ++ [n] 
  end.

Compute tri_list 7.

(* Exercise 6.39 *)
(* Define the other variant "nth_option'." The arguments
  are given in the same order, but the principal argument
  is the number n. Prove that both functions always give the
  same result when applied on the same input. *)

Fixpoint nth_option (A:Set) (n:nat) (l:list A) {struct l} : option A :=
  match n, l with
  | O , cons a tl => Some a
  | S p, cons a tl => nth_option A p tl
  | _, nil => None
  end.

Fixpoint nth_option' (A:Set) (n:nat) (l:list A) {struct n} : option A :=
  match n, l with
  | O , cons a tl => Some a
  | S p, cons a tl => nth_option' A p tl
  | _, nil => None
  end.

Goal forall A n l, nth_option A n l = nth_option' A n l.
Proof.
  intros A n.
  elim n; simpl.
  - destruct l; simpl; reflexivity.
  - intros n' Heq l.
    destruct l; simpl.
    + reflexivity.
    + apply Heq.
Qed.

(* Exercise 6.40 *)
(* Prove: *)

Goal forall (A : Set) (n : nat) (l : list A),
  nth_option A n l = None -> length l <= n.
Proof.
  intros A n l; revert n.
  elim l; simpl; intros.
  - destruct n.
    + reflexivity.
    + apply Nat.le_0_l.
  - destruct n.
    + discriminate.
    + apply le_n_S, H.
      assumption.
Qed.

(* Exercise 6.41 *)
(* Define a function that maps a type A in sort Set,
  a function f of type A->bool, and a list t to the first
  element x in l such that "f x" is true. *)

Fixpoint filter_first {A : Set} (f : A->bool) (l : list A) : option A :=
  match l with
  | nil => None
  | x :: l' => if f x then Some x else filter_first f l'
  end.

(* Exercise 6.42 *)
(* Define the functions split and combine with the
  following types and the usual behavior (transform a
  list of pairs into a pair of lists containing the same
  data, but with a different structure):
    split : forall A B : Set, list A*B -> list A * list B
    combine : forall A B : Set, list A -> list B -> list A*B
  Write and prove a theorem that relates these two functions.
*)

Definition split : forall A B : Set, list (A*B) -> list A * list B :=
  fun (A B : Set) =>
  let cons_pair p l := (fst p :: fst l, snd p :: snd l) in
  fix f (l : list (A*B)) :=
    match l with
    | nil => (nil, nil)
    | p :: l' => cons_pair p (f l')
    end.

(* Assumption for combine:
  Since there is no known default for types A and B,
  the most reasonable action to take when combining
  lists of unequal length is to truncate the longer
  of the two.
*)
    
Definition combine : forall A B : Set, list A -> list B -> list (A*B) :=
  fun (A B : Set) =>
  fix f (la : list A) (lb : list B) : list (A*B) :=
    match la, lb with
    | xa :: la', xb :: lb' => (xa, xb) :: f la' lb'
    | _, _ => nil
    end.

Goal forall A B l, 
  combine A B (fst (split A B l)) (snd (split A B l)) = l.
Proof.
  intros.
  elim l; simpl; intros.
  - reflexivity.
  - destruct a as (ax, ay); simpl.
    rewrite H.
    reflexivity.
Qed.

(* Exercise 6.43 *)
(* Build the type btree of polymorphic binary trees.
  Define translation functions from Z_btree to (btree Z)
  and vice versa. Prove that they are inverse to each other. *)

Inductive btree (A : Set) : Set :=
  bleaf : btree A | bnode : A -> btree A -> btree A -> btree A.
    
Fixpoint bt_Zbt (t : btree Z) : Z_btree :=
  match t with
  | bleaf _ => Z_bleaf
  | bnode _ x l r => Z_bnode x (bt_Zbt l) (bt_Zbt r)
  end.

Fixpoint Zbt_bt (t : Z_btree) : btree Z :=
  match t with
  | Z_bleaf => bleaf Z
  | Z_bnode x l r => bnode Z x (Zbt_bt l) (Zbt_bt r)
  end.

Goal forall t, bt_Zbt (Zbt_bt t) = t.
Proof.
  intros t.
  elim t; simpl.
  - reflexivity.
  - intros x l IHl r IHr.
    rewrite IHl, IHr.
    reflexivity.
Qed.

Goal forall t, Zbt_bt (bt_Zbt t) = t.
Proof.
  intros t.
  elim t; simpl.
  - reflexivity.
  - intros x l IHl r IHr.
    rewrite IHl, IHr.
    reflexivity.
Qed.

(* Exercise 6.44 *)
(* This exercise continues Exercise 6.24 page 169. Build
  the function that takes an element of the type defined
  to represent rational numbers and returns the numerator
  and denominator of the corresponding reduced fraction. *)

(*
  N(a/b) = 1 + a/b = b/b + a/b 
    = (a + b) / b
  D(a/b) = 1 / 1 + (1 / (a/b)) = 1 / 1 + (b/a)
    = 1 / (a + b / b)
    = b / (a + b)
*)

Fixpoint r_eval (r : rational) : nat*nat :=
  match r with
  | rI => (1, 1)
  | rN r' => let (n, d) := (r_eval r') in (n + d, d)
  | rD r' => let (n, d) := (r_eval r') in (n, n + d)
  end.

(* Exercise 6.45 *)
(* The aim of this exercise is to implement a sieve
  function that computes all the prime numbers that are
  less than a given number. The first step is to define
  a type of comparison values: *)

Inductive cmp: Set :=
  Less : cmp | Equal : cmp | Greater : cmp.

(* Then three functions must be defined:
  1. three_way_compare: nat->nat->cmp,
    to compare two natural numbers.
  2. update_primes: nat->(list nat*nat)->(list nat*nat)*bool, 
    with a number k and a list of pairs (p,m) as arguments,
    such that m is the smallest multiple of p greater than
    or equal to k and returns the list of pairs (p, m') 
    where m' is the smallest multiple of p strictly greater 
    than k and a boolean value that is true if one of the m 
    was equal to k.
  3. prime_sieve: nat->(list nat*nat),
    to map a number k to the list of pairs (p, m) where
    p is a prime number smaller than or equal to k and
    m is the smallest multiple of p greater than or
    equal to k+1.

  Prove that prime_sieve can be used to compute all the 
  prime numbers smaller than a given k. *)

Definition three_way_compare (a b : nat) : cmp :=
  if a <? b then Less else if b <? a then Greater else Equal.

Fixpoint update_primes (k : nat) (l : list (nat*nat)) : list(nat*nat) * bool :=
  match l with
  | nil => (nil, false)
  | (p, m) :: l' => 
      let (lx, b) := update_primes k l' in
      match three_way_compare m k with
      | Equal => ((p, m+p) :: lx, true)
      | _ => ((p, m) :: lx, b)
      end
  end.

Fixpoint prime_sieve (k : nat) : list (nat*nat) :=
  match k with 
  | 0 | 1 => nil
  | S k' => 
    let (l', b) := update_primes k (prime_sieve k') in
    if b then l' else l' ++ [(k, 2*k)]
  end.

Definition divides (x y : nat) : Prop := exists z, x * z = y.

Definition prime (n : nat) : Prop :=
  0 < n /\ forall k, divides k n -> k = 1 \/ k = n.

Definition primes (n : nat) := map fst (prime_sieve n).

(* It is very difficult to prove this generates all primes.
  I've decided that, for this question, it is sufficient
  to show an example.
*)

Compute (primes 100).

(* Exercise 6.46 *)
(* Prove one of the injection lemmas for the hnode construct: *)

Inductive htree (A:Set) : nat -> Set :=
  | hleaf: A -> htree A 0
  | hnode: forall n:nat, A -> htree A n -> htree A n -> htree A (S n).

(* The injection tactic is useless for this exercise; you
  need to study and adapt the method from Sect. 6.2.3.2. *)

(* Note: in the text, new syntax for pattern matching
  is given, which allows for more constrained arguments.
  The return type here is redundant, but can likely
  serve as a type enforcement while troubleshooting. *)
Definition right {A : Set} {n : nat} (h : htree A n) :=
  match h in htree _ (S x) return htree A x with
  | hnode _ p v t1 t2 => t2
  end.

(* A simpler implementation moves the contraint to the 
  header. Note that in both cases, the hleaf case need
  not apply, because the pattern matching knows hleaf
  does not exists for all (S n) aka n > 0. The return
  type can also now be defined in the header as
  htree A n. For brevity, I've kept it out *)
Definition left {A : Set} {n : nat} (h : htree A (S n)) :=
  match h with
  | hnode _ p v t1 t2 => t1
  end.

Goal forall (n:nat) (t1 t2 t3 t4 : htree nat n),
  hnode nat n 0 t1 t2 = hnode nat n 0 t3 t4 -> t1 = t3.
Proof.
  intros.
  change (
    left (hnode nat n 0 t1 t2) = left (hnode nat n 0 t3 t4)).
  rewrite H.
  reflexivity.
Qed.

(* Exercise 6.47 *)
(* Define a function that takes a number n and builds a
  fixed-height tree of height n containing integer values. *)
Fixpoint blank_htree (n : nat) : htree Z n :=
  match n with
  | O => hleaf Z 0%Z
  | S n' => hnode Z n' 0%Z (blank_htree n') (blank_htree n')
  end.

(* Exercise 6.48 *)
(* Define inductively the type binary_word used in
  section 4.1.1.2 and define recursively the function
  binary_word_concat. *)

Inductive binary_word : nat -> Set := 
  | be : binary_word 0
  | bx {n : nat} : bool -> binary_word n -> binary_word (S n).

Notation "0_ b" := (bx false b) (at level 0, right associativity).
Notation "1_ b" := (bx true b) (at level 0, right associativity).

Fixpoint concat {n m : nat} (b : binary_word n) (c : binary_word m) : binary_word (n + m) :=
  match b in binary_word n return binary_word m -> binary_word (n + m) with
  | be => fun _ => c
  | @bx n' v b' => fun _ => bx v (concat b' c)
  end c.

Compute concat (bx true be) (bx false (bx true be)).

(* Exercise 6.49 *)
(* Define the function binary_word_or that computes the
  bit-wise "or" operation of two words of the same length
  (like the "|" operator in the C language). *)

Definition hd {n : nat} (b : binary_word (S n)) : bool :=
  match b with
  | bx v _ => v
  end.

Definition tl {n : nat} (b : binary_word (S n)) : binary_word n :=
  match b with
  | bx _ b' => b'
  end.

Fixpoint binary_word_or {n : nat} (b c : binary_word n) : binary_word n :=
  match b in binary_word n return binary_word n -> binary_word n with
  | be => fun _ => be
  | bx x b' => fun c' => bx (x || hd c') (binary_word_or b' (tl c'))
  end c.

Compute binary_word_or (0_ 0_ 1_ 1_ be) (0_ 1_ 0_ 1_ be).

(* Exercise 6.50 *)
(* Define a function with a dependent type that returns true
  for natural numbers of the form 4n+1, false for numbers
  of the form 4n+3, and n for numbers of the form 2n. *)

(* The sequence of returns for 0 to n is: 
    0 true 1 false 2 true 3 false ....
  An alternating sequence of nat and bool. *)

(* The return type depends on whether n is even or not *)
Fixpoint bizzare_type (n : nat) : Set :=
  match n with 
  | 0 => nat 
  | 1 => bool
  | S (S n') => bizzare_type n'
  end.
(* Note: bizzare_type (S (S n)) = bizzare_type n *)

(* The function must have the return type (bizzare type n)
  Considering each half of the alternating sequence
  seperately, we find two recursive relationships:
  
  For even n : f (S (S n)) -> S (f n)
  For odd n : f (S (S n)) -> negb (f n)
  
  The function that acts upon the recursive case must
  also be defined using a similar pattern to the typing
*)

Fixpoint bizzare_func (n : nat) : bizzare_type n -> bizzare_type n :=
  match n with
  | 0 => S
  | 1 => negb
  | S (S n) => bizzare_func n
  end.

(* Now, with a dependent type and recursive step function,
  we can define the main function. This is effectively
  two different recurrence relations zipped together on
  the odds and evens. Every component built has abided
  by this separation.
*)
Fixpoint bizzare (n : nat) : bizzare_type n :=
  match n with
  | 0 => 0
  | 1 => true
  | S (S n') => bizzare_func n' (bizzare n')
  end.

(* Exercise 6.51 *)
(* Prove the following two propositions, which only
  apparently contradict each other: *)
  
Goal forall x y: Empty_set, x=y.
Proof. intros; elim x. Qed.

Goal forall x y: Empty_set, ~x=y.
Proof. intros; elim x. Qed.