Tema 3

(* Datos estructurados en Coq *)

Require Export Induction.

Module NatList. 

(* =====================================================================
   § Pares de númenros 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. El tipo de los números naturales es natprod y su
   constructor es pair.
   ------------------------------------------------------------------ *)

Inductive natprod : Type :=
  pair : nat -> nat -> natprod.

Check (pair 3 5).

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      fst : natprod -> nat
   tal que (fst p) es la primera componente de p.
   ------------------------------------------------------------------ *)

Definition fst (p : natprod) : nat := 
  match p with
  | pair x y => x
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Evaluar la expresión 
      fst (pair 3 5)
   ------------------------------------------------------------------ *)

Eval compute in (fst (pair 3 5)).
(* ===> 3 *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      snd : natprod -> nat
   tal que (snd p) es la segunda componente de p.
   ------------------------------------------------------------------ *)

Definition snd (p : natprod) : nat := 
  match p with
  | pair x y => y
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la notación (x,y) como una abreviaura de (pair x y).
   ------------------------------------------------------------------ *)

Notation "( x , y )" := (pair x y).

(* ---------------------------------------------------------------------
   Ejemplo. Evaluar la expresión 
      fst (3,5)
   ------------------------------------------------------------------ *)

Eval compute in (fst (3,5)).
(* ===> 3 *)

(* ---------------------------------------------------------------------
   Ejemplo. Redefinir la función fst usando la abreviatura de pares.
   ------------------------------------------------------------------ *)

Definition fst' (p : natprod) : nat := 
  match p with
  | (x,y) => x
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Redefinir la función snd usando la abreviatura de pares.
   ------------------------------------------------------------------ *)

Definition snd' (p : natprod) : nat := 
  match p with
  | (x,y) => y
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      swap_pair : natprod -> natprod
   tal que (swap_pair p) es el par obtenido intercambiando las
   componentes de p.
   ------------------------------------------------------------------ *)

Definition swap_pair (p : natprod) : natprod := 
  match p with
  | (x,y) => (y,x)
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que para todos los naturales
      (n,m) = (fst (n,m), snd (n,m)).
   ------------------------------------------------------------------ *)

Theorem surjective_pairing' : forall (n m : nat),
  (n,m) = (fst (n,m), snd (n,m)).
Proof.
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que para todo par de naturales
      p = (fst p, snd p).
   ------------------------------------------------------------------ *)

Theorem surjective_pairing_stuck : forall (p : natprod),
  p = (fst p, snd p).
Proof.
  simpl. (* No reduce nada. *)
Abort.

Theorem surjective_pairing : forall (p : natprod),
  p = (fst p, snd p).
Proof.
  intros p.  destruct p as [n m].  simpl.  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio 1. Demostrar que para todo par de naturales p,
      (snd p, fst p) = swap_pair p.
   ------------------------------------------------------------------ *)

Theorem snd_fst_is_swap : forall (p : natprod),
  (snd p, fst p) = swap_pair p.
Admitted.

(* ---------------------------------------------------------------------
   Ejercicio 2. Demostrar que para todo par de naturales p,
      fst (swap_pair p) = snd p.
   ------------------------------------------------------------------ *)

Theorem fst_swap_is_snd : forall (p : natprod),
  fst (swap_pair p) = snd p.
Admitted.

(* =====================================================================
   § Listas de números 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. natlist es la lista de los números naturales y sus
   constructores son 
   + nil (la lista vacía) y 
   + cons (tal que (cons x ys) es la lista obtenida añadiéndole x a ys. 
   ------------------------------------------------------------------ *)

Inductive natlist : Type :=
  | nil  : natlist
  | cons : nat -> natlist -> natlist.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la constante 
      mylist : natlist
   que es la lista cuyos elementos son 1, 2 y 3.
   ------------------------------------------------------------------ *)

Definition mylist := cons 1 (cons 2 (cons 3 nil)).

(* ---------------------------------------------------------------------
   Ejemplo. Definir la notación (x :: ys) como una abreviatura de 
   (cons x ys).
   ------------------------------------------------------------------ *)

Notation "x :: l" := (cons x l)
                     (at level 60, right associativity).

(* ---------------------------------------------------------------------
   Ejemplo. Definir la notación de las listas finitas escribiendo sus
   elementos entre corchetes y separados por puntos y comas.
   ------------------------------------------------------------------ *)

Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

(* ---------------------------------------------------------------------
   Ejemplo. Distintas representaciones de mylist.
   ------------------------------------------------------------------ *)

Definition mylist1 := 1 :: (2 :: (3 :: nil)).
Definition mylist2 := 1 :: 2 :: 3 :: nil.
Definition mylist3 := [1;2;3].

(* =====================================================================
   §§ Repeat  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      repeat : nat -> nat -> natlist
   tal que (repeat n k) es la lista formada por k veces el número n.
   ------------------------------------------------------------------ *)

Fixpoint repeat (n count : nat) : natlist :=
  match count with
  | O        => nil
  | S count' => n :: (repeat n count')
  end.

(* =====================================================================
   §§ Length  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      length : natlist -> nat
   tal que (length xs) es el número de elementos de xs.
   ------------------------------------------------------------------ *)

Fixpoint length (l:natlist) : nat :=
  match l with
  | nil    => O
  | h :: t => S (length t)
  end.

(* =====================================================================
   §§ Append  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      append : natlist -> natlist -> natlist
   tal que (append xs ys) es la concatenación de xs e ys.
   ------------------------------------------------------------------ *)
Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil    => l2
  | h :: t => h :: (app t l2)
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la notación (xs ++ ys) como una abreviaura de 
   (append xs ys).
   ------------------------------------------------------------------ *)

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que
      [1;2;3] ++ [4;5] = [1;2;3;4;5].
      nil     ++ [4;5] = [4;5].
      [1;2;3] ++ nil   = [1;2;3].
   ------------------------------------------------------------------ *)

Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof. reflexivity.  Qed.
Example test_app2: nil ++ [4;5] = [4;5].
Proof. reflexivity.  Qed.
Example test_app3: [1;2;3] ++ nil = [1;2;3].
Proof. reflexivity.  Qed.

(* =====================================================================
   §§ Head y tail  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      hd : nat -> natlist -> natlist
   tal que (hd d xs) es el primer elemento de xs o d, si xs es la lista
   vacía. 
   ------------------------------------------------------------------ *)

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nil    => default
  | h :: t => h
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      tl : natlist -> natlist
   tal que (tl xs) es el resto de xs.
   ------------------------------------------------------------------ *)

Definition tl (l:natlist) : natlist :=
  match l with
  | nil    => nil
  | h :: t => t
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que 
       hd 0 [1;2;3] = 1.
       hd 0 []      = 0.
       tl [1;2;3]   = [2;3].
   ------------------------------------------------------------------ *)

Example test_hd1: hd 0 [1;2;3] = 1.
Proof. reflexivity.  Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity.  Qed.
Example test_tl: tl [1;2;3] = [2;3].
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejercicio 3. Definir la función
      nonzeros : natlist -> natlist
   tal que (nonzeros xs) es la lista de los elementos de xs distintos de
   cero. Por ejemplo,
      nonzeros [0;1;0;2;3;0;0] = [1;2;3].
   ------------------------------------------------------------------ *)

Fixpoint nonzeros (l:natlist) : natlist :=
  match l with
  | nil => nil
  | a::bs => match a with
            | 0 => nonzeros bs 
            | _ =>  a:: nonzeros bs end
 end.
Example test_nonzeros:
  nonzeros [0;1;0;2;3;0;0] = [1;2;3].
Proof. simpl. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 4. Definir la función
      oddmembers : natlist -> natlist
   tal que (oddmembers xs) es la lista de los elementos impares de
   xs. Por ejemplo,
      oddmembers [0;1;0;2;3;0;0] = [1;3].
   ------------------------------------------------------------------ *)

Fixpoint oddmembers (l:natlist) : natlist :=
  match l with
  | nil => nil
  | t::xs => if oddb t then t :: oddmembers xs else oddmembers xs
  end.
 
Example test_oddmembers:
  oddmembers [0;1;0;2;3;0;0] = [1;3].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 5. Definir la función
      countoddmembers : natlist -> nat
   tal que (countoddmembers xs) es el número de elementos impares de
   xs. Por ejemplo,
      countoddmembers [1;0;3;1;4;5] = 4.
      countoddmembers [0;2;4]       = 0.
      countoddmembers nil           = 0.
   ------------------------------------------------------------------ *)

Definition countoddmembers (l:natlist) : nat :=
 length (oddmembers l). 

Example test_countoddmembers1:
  countoddmembers [1;0;3;1;4;5] = 4.
  reflexivity. Qed.

Example test_countoddmembers2:
  countoddmembers [0;2;4] = 0.
  reflexivity. Qed.

Example test_countoddmembers3:
  countoddmembers nil = 0.
  reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio 6. Definir la función
      alternate : natlist -> natlist -> natlist
   tal que (alternate xs ys) es la lista obtenida intercalando los
   elementos de xs e ys. Por ejemplo,
      alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
      alternate [1] [4;5;6]     = [1;4;5;6].
      alternate [1;2;3] [4]     = [1;4;2;3].
      alternate [] [20;30]      = [20;30].
   ------------------------------------------------------------------ *)

Fixpoint alternate (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil => l2
  | t::xs => match l2 with
            | nil => t::xs
            | p::ys => t::p::alternate xs ys end
  end.

Example test_alternate1:
  alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
  reflexivity. Qed.

Example test_alternate2:
  alternate [1] [4;5;6] = [1;4;5;6].
  reflexivity. Qed.

Example test_alternate3:
  alternate [1;2;3] [4] = [1;4;2;3].
  reflexivity. Qed.

Example test_alternate4:
  alternate [] [20;30] = [20;30].
  reflexivity. Qed.

(** [] *)

(* ----------------------------------------------------------------- *)
(** *** Multiconjuntos como listas *)

(** Un multiconjunto es como un conjunto donde los elementos pueden repetirse más de una vez. Podemos implementarlos como listas. *)

Definition bag := natlist.

(** Ejercicio 7. Definir la función count v s, que te cuenta las veces que aparece el elemento v en la lista s: 
count 1 [1;2;3;1;4;1] = 3.
count 6 [1;2;3;1;4;1] = 0.
*)

Fixpoint count (v:nat) (s:bag) : nat :=
  match s with
  | nil => 0
  | t::xs => if beq_nat t v then 1 + count v xs else count v xs
  end.

Example test_count1:              count 1 [1;2;3;1;4;1] = 3.
reflexivity. Qed.
Example test_count2:              count 6 [1;2;3;1;4;1] = 0.
reflexivity. Qed. 

(** La suma de multiconjuntos es parecida a la unión de conjuntos. Ejercicio 8. Definir la suma de multiconjuntos:
  count 1 (sum [1;2;3] [1;4;1]) = 3. *)

Definition sum : bag -> bag -> bag := app.

Example test_sum1:              count 1 (sum [1;2;3] [1;4;1]) = 3.
 reflexivity. Qed.

  (* Ejercicio 9. Definir la función add v s que añade el elemento v al multiconjunto s:
 count 1 (add 1 [1;4;1]) = 3.
 count 5 (add 1 [1;4;1]) = 0.
*)

Definition add (v:nat) (s:bag) : bag :=
  v :: s .

Example test_add1:                count 1 (add 1 [1;4;1]) = 3.
 reflexivity. Qed.
Example test_add2:                count 5 (add 1 [1;4;1]) = 0.
 reflexivity. Qed.

  (* Ejercicio 10. Definir la función member v s que se verfica si v es un elemento de la lista s: 
member 1 [1;4;1] = true.
member 2 [1;4;1] = false.*)

Definition member (v:nat) (s:bag) : bool := 
 if beq_nat 0 (count v s) then false else true.

Example test_member1:             member 1 [1;4;1] = true.
 reflexivity. Qed.

Example test_member2:             member 2 [1;4;1] = false.
reflexivity. Qed.

(** [] *)
(** Definir las siguientes funciones:*)

(** Ejercicio 11. Definir la función remove_one v s que borra una vez el elemento v de la lista s:
count 5 (remove_one 5 [2;1;5;4;1]) = 0.
count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.*)

Fixpoint remove_one (v:nat) (s:bag) : bag :=
  match s with
  | nil => nil
  | t :: xs => if beq_nat t v then xs else t:: remove_one v xs
  end.

Example test_remove_one1:
  count 5 (remove_one 5 [2;1;5;4;1]) = 0.
 reflexivity. Qed.

Example test_remove_one2:
  count 5 (remove_one 5 [2;1;4;1]) = 0.
  reflexivity. Qed.

Example test_remove_one3:
  count 4 (remove_one 5 [2;1;4;5;1;4]) = 2.
  reflexivity. Qed.

Example test_remove_one4:
  count 5 (remove_one 5 [2;1;5;4;5;1;4]) = 1.
  reflexivity. Qed.

(** Ejercicio 12. Definir la función remove_all v s que borra todas las copias del elemento v en el multiconjunto s:
count 5 (remove_all 5 [2;1;5;4;1]) = 0.
count 5 (remove_all 5 [2;1;4;1]) = 0.
count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0. *)

Fixpoint remove_all (v:nat) (s:bag) : bag :=
   match s with
  | nil => nil
  | t :: xs => if beq_nat t v then remove_all v xs else t:: remove_all v xs
  end.

Example test_remove_all1:  count 5 (remove_all 5 [2;1;5;4;1]) = 0.
  reflexivity. Qed.
Example test_remove_all2:  count 5 (remove_all 5 [2;1;4;1]) = 0.
  reflexivity. Qed.
Example test_remove_all3:  count 4 (remove_all 5 [2;1;4;5;1;4]) = 2.
  reflexivity. Qed.
Example test_remove_all4:  count 5 (remove_all 5 [2;1;5;4;5;1;4;5;1;4]) = 0.
  reflexivity. Qed.

(** Ejercicio 13. Definir la función subset s1 s2 que se verifica si s1 es un submulticonjunto de s2 *)

Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match s1 with
  | nil => true
  | x::xs => member x s2 && subset xs (remove_one x s2)
  end.

Example test_subset1:              subset [1;2] [2;1;4;1] = true.
  reflexivity. Qed.
Example test_subset2:              subset [1;2;2] [2;1;4;1] = false.
  reflexivity. Qed.

(** [] *)

(** Ejercicio 14 (avanzado). Escribir un teorema sobre multiconjuntos con las funciones count y add y probarlo.*)

Theorem bag_theorem : forall s1 s2 : bag, forall n : nat,
  count n s1 + count n s2 = count n (app s1 s2).                 
Proof.
  intros s1 s2 n. induction s1 as [|s s'].
 - simpl. reflexivity.
 - simpl. destruct (beq_nat s n).
    + simpl. rewrite IHs'. reflexivity.
    + rewrite IHs'. reflexivity.
 Qed.

(** [] *)

(* ################################################################# *)
(** * Listas *)

(** El siguiente teorema se deduce directamente de la definición de app. *)

Theorem nil_app : forall l:natlist,
  [] ++ l = l.
Proof. reflexivity. Qed.

(** ... ya que esta es decreciente en la primera componenete. *)

(** Sobre listas podemos usar las técnicas de demostración ya aprendidas sobre naturales: *)

Theorem tl_length_pred : forall l:natlist,
  pred (length l) = length (tl l).
Proof.
  intros l. destruct l as [| n l'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons n l' *)
    reflexivity.  Qed.

(* ================================================================= *)
(** ** Inducción en Listas *)

(** La inducción sobre la longitud de las listas es análoga a la de los numeros naturales. *)

Theorem app_assoc : forall l1 l2 l3 : natlist,
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros l1 l2 l3. induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons n l1' *)
    simpl. rewrite -> IHl1'. reflexivity.  Qed.

(* Comentar los nombres dados en la hipotesis de inducción. *)

(* ----------------------------------------------------------------- *)
(** *** Reverse *)

(** Definición de la función rev l que devuelve una lista formada por los elementos en orden l en orden contrario. *)

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil    => nil
  | h :: t => rev t ++ [h]
  end.

Example test_rev1:            rev [1;2;3] = [3;2;1].
Proof. reflexivity.  Qed.
Example test_rev2:            rev nil = nil.
Proof. reflexivity.  Qed.

(* ----------------------------------------------------------------- *)
(** *** Propiedades de [rev] *)

(** Definición de algunos teoremas más: *)

Theorem rev_length_firsttry : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = [] *)
    reflexivity.
  - (* l = n :: l' *)
    (* Probamos simplificando *)
    simpl.
    rewrite <- IHl'.
    (* Nos encontramos sin más que hacer, así que buscamos un lema que nos ayude. *)
Abort.

Theorem app_length : forall l1 l2 : natlist,
  length (l1 ++ l2) = (length l1) + (length l2).
Proof.
  (* WORKED IN CLASS *)
  intros l1 l2. induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons *)
    simpl. rewrite -> IHl1'. reflexivity.  Qed.


(** Ahora completamos la prueba original. *)

Theorem rev_length : forall l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons *)
    simpl. rewrite -> app_length, plus_comm.
    simpl. rewrite -> IHl'. reflexivity.  Qed.

(* ================================================================= *)
(** ** Lista de ejercicios, Parte 1 *)

(** Ejercicio 15. Demostrar que la lista vacía es el elemento neutro a derechas de la suma de listas: *)

Theorem app_nil_r : forall l : natlist,
  l ++ [] = l.
Proof.
  (* FILL IN HERE *) Admitted.

(** Ejercicio 16. Demostrar la propiedad distributiva del reverso de una lista respecto a la suma: *)

Theorem rev_app_distr: forall l1 l2 : natlist,
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
(* FILL IN HERE *) Admitted.

(** Ejercicio 17. Demostrar que el inverso de la función rev es ella misma (que es involutiva): *)

Theorem rev_involutive : forall l : natlist,
  rev (rev l) = l.
Proof.
  (* FILL IN HERE *) Admitted.

(** Ejercicio 18. Demostrar la asociatividad de la suma de 4 listas: *)

Theorem app_assoc4 : forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
  (* FILL IN HERE *) Admitted.

(** Ejercicio 19. Demostrar que al sumar dos listas no aparecen ni desaparecen ceros: *)

Lemma nonzeros_app : forall l1 l2 : natlist,
  nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** Ejercicio 20. Definir beq_natlist como la igualdad de listas:
beq_natlist nil nil = true.
beq_natlist [1;2;3] [1;2;3] = true.
beq_natlist [1;2;3] [1;2;4] = false. *)

Fixpoint beq_natlist (l1 l2 : natlist) : bool
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_beq_natlist1 :
  (beq_natlist nil nil = true).
 (* FILL IN HERE *) Admitted.

Example test_beq_natlist2 :
  beq_natlist [1;2;3] [1;2;3] = true.
(* FILL IN HERE *) Admitted.

Example test_beq_natlist3 :
  beq_natlist [1;2;3] [1;2;4] = false.
 (* FILL IN HERE *) Admitted.

(** Ejercicio 21. Demostrar que la igualdad de listas cumple la propiedad reflexiva *)

Theorem beq_natlist_refl : forall l:natlist,
  true = beq_natlist l l.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(* ================================================================= *)
(** ** List Exercises, Part 2 *)

(** **** Exercise: 3 stars, advanced (bag_proofs)  *)
(** Here are a couple of little theorems to prove about your
    definitions about bags above. *)

Theorem count_member_nonzero : forall (s : bag),
  leb 1 (count 1 (1 :: s)) = true.
Proof.
  (* FILL IN HERE *) Admitted.

(** The following lemma about [leb] might help you in the next proof. *)

Theorem ble_n_Sn : forall n,
  leb n (S n) = true.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* 0 *)
    simpl.  reflexivity.
  - (* S n' *)
    simpl.  rewrite IHn'.  reflexivity.  Qed.

Theorem remove_decreases_count: forall (s : bag),
  leb (count 0 (remove_one 0 s)) (count 0 s) = true.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, optional (bag_count_sum)  *)
(** Write down an interesting theorem [bag_count_sum] about bags
    involving the functions [count] and [sum], and prove it using
    Coq.  (You may find that the difficulty of the proof depends on
    how you defined [count]!) *)
(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 4 stars, advanced (rev_injective)  *)
(** Prove that the [rev] function is injective -- that is,

    forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.

(There is a hard way and an easy way to do this.) *)

(* FILL IN HERE *)
(** [] *)

(* ################################################################# *)
(** * Options *)

(** Suppose we want to write a function that returns the [n]th
    element of some list.  If we give it type [nat -> natlist -> nat],
    then we'll have to choose some number to return when the list is
    too short... *)

Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
  match l with
  | nil => 42  (* arbitrary! *)
  | a :: l' => match beq_nat n O with
               | true => a
               | false => nth_bad l' (pred n)
               end
  end.

(** This solution is not so good: If [nth_bad] returns [42], we
    can't tell whether that value actually appears on the input
    without further processing. A better alternative is to change the
    return type of [nth_bad] to include an error value as a possible
    outcome. We call this type [natoption]. *)

Inductive natoption : Type :=
  | Some : nat -> natoption
  | None : natoption.

(** We can then change the above definition of [nth_bad] to
    return [None] when the list is too short and [Some a] when the
    list has enough members and [a] appears at position [n]. We call
    this new function [nth_error] to indicate that it may result in an
    error. *)

Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
  match l with
  | nil => None
  | a :: l' => match beq_nat n O with
               | true => Some a
               | false => nth_error l' (pred n)
               end
  end.

Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Proof. reflexivity. Qed.
Example test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.
Proof. reflexivity. Qed.
Example test_nth_error3 : nth_error [4;5;6;7] 9 = None.
Proof. reflexivity. Qed.

(** (In the HTML version, the boilerplate proofs of these
    examples are elided.  Click on a box if you want to see one.)

    This example is also an opportunity to introduce one more small
    feature of Coq's programming language: conditional
    expressions... *)


Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=
  match l with
  | nil => None
  | a :: l' => if beq_nat n O then Some a
               else nth_error' l' (pred n)
  end.

(** Coq's conditionals are exactly like those found in any other
    language, with one small generalization.  Since the boolean type
    is not built in, Coq actually supports conditional expressions over
    _any_ inductively defined type with exactly two constructors.  The
    guard is considered true if it evaluates to the first constructor
    in the [Inductive] definition and false if it evaluates to the
    second. *)

(** The function below pulls the [nat] out of a [natoption], returning
    a supplied default in the [None] case. *)

Definition option_elim (d : nat) (o : natoption) : nat :=
  match o with
  | Some n' => n'
  | None => d
  end.

(** **** Exercise: 2 stars (hd_error)  *)
(** Using the same idea, fix the [hd] function from earlier so we don't
    have to pass a default element for the [nil] case.  *)

Definition hd_error (l : natlist) : natoption
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Example test_hd_error1 : hd_error [] = None.
 (* FILL IN HERE *) Admitted.

Example test_hd_error2 : hd_error [1] = Some 1.
 (* FILL IN HERE *) Admitted.

Example test_hd_error3 : hd_error [5;6] = Some 5.
 (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 1 star, optional (option_elim_hd)  *)
(** This exercise relates your new [hd_error] to the old [hd]. *)

Theorem option_elim_hd : forall (l:natlist) (default:nat),
  hd default l = option_elim default (hd_error l).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

End NatList.

(* ################################################################# *)
(** * Partial Maps *)

(** As a final illustration of how data structures can be defined in
    Coq, here is a simple _partial map_ data type, analogous to the
    map or dictionary data structures found in most programming
    languages. *)

(** First, we define a new inductive datatype [id] to serve as the
    "keys" of our partial maps. *)

Inductive id : Type :=
  | Id : nat -> id.

(** Internally, an [id] is just a number.  Introducing a separate type
    by wrapping each nat with the tag [Id] makes definitions more
    readable and gives us the flexibility to change representations
    later if we wish. *)

(** We'll also need an equality test for [id]s: *)

Definition beq_id (x1 x2 : id) :=
  match x1, x2 with
  | Id n1, Id n2 => beq_nat n1 n2
  end.

(** **** Exercise: 1 star (beq_id_refl)  *)
Theorem beq_id_refl : forall x, true = beq_id x x.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** Now we define the type of partial maps: *)

Module PartialMap.
Export NatList.
  
Inductive partial_map : Type :=
  | empty  : partial_map
  | record : id -> nat -> partial_map -> partial_map.

(** This declaration can be read: "There are two ways to construct a
    [partial_map]: either using the constructor [empty] to represent an
    empty partial map, or by applying the constructor [record] to
    a key, a value, and an existing [partial_map] to construct a
    [partial_map] with an additional key-to-value mapping." *)

(** The [update] function overrides the entry for a given key in a
    partial map (or adds a new entry if the given key is not already
    present). *)

Definition update (d : partial_map)
                  (x : id) (value : nat)
                  : partial_map :=
  record x value d.

(** Last, the [find] function searches a [partial_map] for a given
    key.  It returns [None] if the key was not found and [Some val] if
    the key was associated with [val]. If the same key is mapped to
    multiple values, [find] will return the first one it
    encounters. *)

Fixpoint find (x : id) (d : partial_map) : natoption :=
  match d with
  | empty         => None
  | record y v d' => if beq_id x y
                     then Some v
                     else find x d'
  end.


(** **** Exercise: 1 star (update_eq)  *)
Theorem update_eq :
  forall (d : partial_map) (x : id) (v: nat),
    find x (update d x v) = Some v.
Proof.
 (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 1 star (update_neq)  *)
Theorem update_neq :
  forall (d : partial_map) (x y : id) (o: nat),
    beq_id x y = false -> find x (update d y o) = find x d.
Proof.
 (* FILL IN HERE *) Admitted.
(** [] *)
End PartialMap.

(** **** Exercise: 2 stars (baz_num_elts)  *)
(** Consider the following inductive definition: *)

Inductive baz : Type :=
  | Baz1 : baz -> baz
  | Baz2 : baz -> bool -> baz.

(** How _many_ elements does the type [baz] have?  (Answer in English
    or the natural language of your choice.)

(* FILL IN HERE *)
*)
(** [] *)

(** $Date: 2017-10-10 09:30:37 -0400 (Tue, 10 Oct 2017) $ *)