Tema 4

(* T4: Polimorfismo y funciones deo orden superior en Coq *)

Require Export T3_Listas.

(* =====================================================================
   § Polimorfismo
   ================================================================== *)

(* =====================================================================
   §§ Listas polimórficas  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo boollist para representar las listas de
   booleanos con los constructores bool_nil y bool_cons tales que 
   + bool_nil es la lista vacía y
   + (bool_cons x ys) es la lista obtenida añadiendo el booleano x a la
     lista ys.
   ------------------------------------------------------------------ *)

Inductive boollist : Type :=
  | bool_nil : boollist
  | bool_cons : bool -> boollist -> boollist.


(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo (list X) para representar las listas de
   elementos de con los constructores nil y cons tales que 
   + nil es la lista vacía y
   + (cons x ys) es la lista obtenida añadiendo el elemento x a la
     lista ys.
   ------------------------------------------------------------------ *)

Inductive list (X:Type) : Type :=
  | nil  : list X
  | cons : X -> list X -> list X.

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el tipo de list.
   ------------------------------------------------------------------ *)

Check list.
(* ===> list : Type -> Type *)

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el tipo de (nil nat).
   ------------------------------------------------------------------ *)

Check (nil nat).
(* ===> nil nat : list nat *)

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el tipo de (cons nat 3 (nil nat)).
   ------------------------------------------------------------------ *)

Check (cons nat 3 (nil nat)).
(* ===> cons nat 3 (nil nat) : list nat *)

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el tipo de nil.
   ------------------------------------------------------------------ *)

Check nil.
(* ===> nil : forall X : Type, list X *)

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el tipo de cons.
   ------------------------------------------------------------------ *)

Check cons.
(* ===> cons : forall X : Type, X -> list X -> list X *)

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el tipo de (cons nat 2 (cons nat 1 (nil nat))).
   ------------------------------------------------------------------ *)

Check (cons nat 2 (cons nat 1 (nil nat))).
(* ==> cons nat 2 (cons nat 1 (nil nat)) : list nat *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      repeat (X : Type) (x : X) (count : nat) : list X
   tal que (repeat X x n) es la lista obtenida repitiendo n veces el
   elemento x. Por ejemplo,
      repeat nat 4 2 = cons nat 4 (cons nat 4 (nil nat)).
      repeat bool false 1 = cons bool false (nil bool).
   ------------------------------------------------------------------ *)

Fixpoint repeat (X : Type) (x : X) (count : nat) : list X :=
  match count with
  | 0 => nil X
  | S count' => cons X x (repeat X x count')
  end.

Example test_repeat1 :
  repeat nat 4 2 = cons nat 4 (cons nat 4 (nil nat)).
Proof. reflexivity.  Qed.

Example test_repeat2 :
  repeat bool false 1 = cons bool false (nil bool).
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Se definen los siguientes tipos
      Inductive mumble : Type :=
        | a : mumble
        | b : mumble -> nat -> mumble
        | c : mumble.
      
      Inductive grumble (X:Type) : Type :=
        | d : mumble -> grumble X
        | e : X -> grumble X.
  
   Decidir cuáles de los siguientes expresiones son del tipo (grumble X)
   para algún X:
      - [d (b a 5)]
      - [d mumble (b a 5)]
      - [d bool (b a 5)]
      - [e bool true]
      - [e mumble (b c 0)]
      - [e bool (b c 0)]
      - [c]
   ------------------------------------------------------------------ *)

Module MumbleGrumble.

Inductive mumble : Type :=
  | a : mumble
  | b : mumble -> nat -> mumble
  | c : mumble.

Inductive grumble (X:Type) : Type :=
  | d : mumble -> grumble X
  | e : X -> grumble X.

End MumbleGrumble.

(* =====================================================================
   §§§ Inferencia de tipos
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      repeat' X x count : list X
   tal que (repeat' X x n) es la lista obtenida repitiendo n veces el
   elemento x. Por ejemplo,
      repeat' nat 4 2 = cons nat 4 (cons nat 4 (nil nat)).
      repeat' bool false 1 = cons bool false (nil bool).
   ------------------------------------------------------------------ *)

Fixpoint repeat' X x count : list X :=
  match count with
  | 0        => nil X
  | S count' => cons X x (repeat' X x count')
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Calcular los tipos de repeat' y repeat.
   ------------------------------------------------------------------ *)

Check repeat'.
(* ===> forall X : Type, X -> nat -> list X *)
Check repeat.
(* ===> forall X : Type, X -> nat -> list X *)

(* =====================================================================
   §§§ Síntesis de los tipos de los argumentos  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      repeat'' X x count : list X
   tal que (repeat'' X x n) es la lista obtenida repitiendo n veces el
   elemento x, usando argumentos implícitos. Por ejemplo,
      repeat'' nat 4 2 = cons nat 4 (cons nat 4 (nil nat)).
      repeat'' bool false 1 = cons bool false (nil bool).
   ------------------------------------------------------------------ *)

Fixpoint repeat'' X x count : list X :=
  match count with
  | 0        => nil _
  | S count' => cons _ x (repeat'' _ x count')
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la lista formada por los números naturales 1, 2 y 3.
   ------------------------------------------------------------------ *)

Definition list123 :=
  cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).

Definition list123' :=
  cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

(* =====================================================================
   §§§ Argumentos implícitos  
   ================================================================== *)


(* ---------------------------------------------------------------------
   Ejemplo. Especificar las siguientes funciones y sus argumentos
   explícitos e implícitos:
   + nil
   + constructor
   + repeat
   ------------------------------------------------------------------ *)

Arguments nil {X}.
Arguments cons {X} _ _.
Arguments repeat {X} x count.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la lista formada por los números naturales 1, 2 y 3.
   ------------------------------------------------------------------ *)

Definition list123'' := cons 1 (cons 2 (cons 3 nil)).

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      repeat''' {X : Type} (x : X) (count : nat) : list X
   tal que (repeat'' X x n) es la lista obtenida repitiendo n veces el
   elemento x, usando argumentos implícitos. Por ejemplo,
      repeat'' nat 4 2 = cons nat 4 (cons nat 4 (nil nat)).
      repeat'' bool false 1 = cons bool false (nil bool).
   ------------------------------------------------------------------ *)

Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=
  match count with
  | 0        => nil
  | S count' => cons x (repeat''' x count')
  end.

Example test_repeat'''1 :
  repeat''' 4 2 = cons 4 (cons 4 nil).
Proof. reflexivity.  Qed.

Example test_repeat'''2 :
  repeat false 1 = cons false nil.
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo (list' {X}) para representar las listas de
   elementos de con los constructores nil y cons tales que 
   + nil' es la lista vacía y
   + (cons' x ys) es la lista obtenida añadiendo el elemento x a la
     lista ys.
   ------------------------------------------------------------------ *)

Inductive list' {X:Type} : Type :=
  | nil'  : list'
  | cons' : X -> list' -> list'.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      app {X : Type} (l1 l2 : list X) : (list X)
   tal que (app xs ys) es la concatenación de xs e ys.
   ------------------------------------------------------------------ *)

Fixpoint app {X : Type} (l1 l2 : list X) : (list X) :=
  match l1 with
  | nil      => l2
  | cons h t => cons h (app t l2)
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      rev {X:Type} (l:list X) : list X
   tal que (rev xs) es la inversa de xs. Por ejemplo,
      rev (cons 1 (cons 2 nil)) = (cons 2 (cons 1 nil)).
      rev (cons true nil) = cons true nil.
   ------------------------------------------------------------------ *)

Fixpoint rev {X:Type} (l:list X) : list X :=
  match l with
  | nil      => nil
  | cons h t => app (rev t) (cons h nil)
  end.

Example test_rev1 :
  rev (cons 1 (cons 2 nil)) = (cons 2 (cons 1 nil)).
Proof. reflexivity.  Qed.

Example test_rev2:
  rev (cons true nil) = cons true nil.
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      length {X : Type} (l : list X) : nat 
   tal que (length xs) es el número de elementos de xs. Por ejemplo,
      length (cons 1 (cons 2 (cons 3 nil))) = 3.
   ------------------------------------------------------------------ *)

Fixpoint length {X : Type} (l : list X) : nat :=
  match l with
  | nil       => 0
  | cons _ l' => S (length l')
  end.

Example test_length1:
  length (cons 1 (cons 2 (cons 3 nil))) = 3.
Proof. reflexivity.  Qed.

(* =====================================================================
   §§§ Explicitación de argumentos  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Especificar que la siguiente definición es errónea
      Fail Definition mynil := nil.
   ------------------------------------------------------------------ *)

Fail Definition mynil := nil.
(* ==> Error: Cannot infer the implicit parameter X of nil. *)

(* ---------------------------------------------------------------------
   Ejemplo. Completar la definición anterior para obtener la lista
   vacía de números naturales.
   ------------------------------------------------------------------ *)

Definition mynil : list nat := nil.

(* Alternativamente *)
Definition mynil' := @nil nat.

(* ---------------------------------------------------------------------
   Ejemplo. Definir las siguientes abreviaturas
   + "x :: y"         para (cons x y)
   + "[ ]"            para nil
   + "[ x ; .. ; y ]" para (cons x .. (cons y []) ..).
   + "x ++ y"         para (app x y)
   ------------------------------------------------------------------ *)

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
                     (at level 60, right associativity).

(* ---------------------------------------------------------------------
   Ejemplo. Definir la lista cuyos elementos son 1, 2 y 3.
   ------------------------------------------------------------------ *)

Definition list123''' := [1; 2; 3].

(* =====================================================================
   §§§ Ejercicios  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejercicio. Demostrar que la lista vacía es el elemento neutro por la
   derecha de la concatenación.
   ------------------------------------------------------------------ *)

Theorem app_nil_r : forall (X:Type), forall l:list X,
  l ++ [] = l.
Proof.
  induction l.
  + reflexivity.
  + simpl. rewrite IHl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Demostrar que la concatenación es asociativa.
   ------------------------------------------------------------------ *)

Theorem app_assoc : forall A (l m n:list A),
  l ++ m ++ n = (l ++ m) ++ n.
Proof.
  intros A l m n.
  induction l.
  + reflexivity.
  + simpl. rewrite IHl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Demostrar que la longitud de una concatenación es la suma de
   las longitudes de las listas (es decir, es un homomorfismo).
   ------------------------------------------------------------------ *)

Lemma app_length : forall (X:Type) (l1 l2 : list X),
  length (l1 ++ l2) = length l1 + length l2.
Proof.
  intros X l1 l2.
  induction l1.
  + reflexivity.
  + simpl. rewrite IHl1. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Demostrar que
      rev (l1 ++ l2) = rev l2 ++ rev l1.
   ------------------------------------------------------------------ *)

Theorem rev_app_distr: forall X (l1 l2 : list X),
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros X l1 l2.
  induction l1.
  + simpl. rewrite app_nil_r. reflexivity.
  + simpl. rewrite IHl1, app_assoc. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Demostrar que
      rev (rev l) = l.
   ------------------------------------------------------------------ *)

Theorem rev_involutive : forall X : Type, forall l : list X,
  rev (rev l) = l.
Proof.
  induction l.
  + reflexivity.
  + simpl. rewrite rev_app_distr, IHl. reflexivity.
Qed.

(* =====================================================================
   §§ Polimorfismo de pares  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo prod (X Y) con el constructor pair tal que 
   (pair x y) es el par cuyas componentes son x e y.
   ------------------------------------------------------------------ *)

Inductive prod (X Y : Type) : Type :=
| pair : X -> Y -> prod X Y.

Arguments pair {X} {Y} _ _.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la abreviatura
      "( x , y )" para (pair x y).
   ------------------------------------------------------------------ *)

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

(* ---------------------------------------------------------------------
   Ejemplo. Definir la abreviatura
      "X * Y" para (prod X Y) 
   ------------------------------------------------------------------ *)

Notation "X * Y" := (prod X Y) : type_scope.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      fst {X Y : Type} (p : X * Y) : X
   tal que (fst p) es la primera componente del par p.
   ------------------------------------------------------------------ *)

Definition fst {X Y : Type} (p : X * Y) : X :=
  match p with
  | (x, y) => x
  end.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      snd {X Y : Type} (p : X * Y) 
   tal que (snd p) es la segunda componente del par p.
   ------------------------------------------------------------------ *)

Definition snd {X Y : Type} (p : X * Y) : Y :=
  match p with
  | (x, y) => y
  end.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      combine {X Y : Type} (lx : list X) (ly : list Y) : list (X*Y) 
   tal que (combine lx ly) es la lista obtenida emparejando los
   elementos de lx y ly (como zip de Haskell).
   ------------------------------------------------------------------ *)

Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y) : list (X*Y) :=
  match lx, ly with
  | []     , _       => []
  | _      , []      => []
  | x :: tx, y :: ty => (x, y) :: (combine tx ty)
  end.

(* ---------------------------------------------------------------------
   Ejercicio. Calcular el resultado de 
      Check combine
   ------------------------------------------------------------------ *)

Check @combine.
(* ==> forall X Y : Type, list X -> list Y -> list (X * Y)*)

(* ---------------------------------------------------------------------
   Ejercicio. Calcular el resultado de 
      Compute (combine [1;2] [false;false;true;true]).
   ------------------------------------------------------------------ *)

Compute (combine [1;2] [false;false;true;true]).
(* ==> [(1, false); (2, false)] : list (nat * bool) *)

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      split {X Y : Type} (l : list (X*Y)) : (list X) * (list Y)
   tal que (split l) es el par de lista (lx,ly) cuyo emparejamiento es
   l. (La función split es como unzip de Haskell). Por ejemplo,
      split [(1,false);(2,false)] = ([1;2],[false;false]).
   ------------------------------------------------------------------ *)

Fixpoint split {X Y : Type} (l : list (X*Y)) : (list X) * (list Y) :=
 match l with
 | []          => ([], [])
 | (x, y) :: t => let s := split t in (x :: fst s, y :: snd s)
end.

Example test_split:
  split [(1,false);(2,false)] = ([1;2],[false;false]).
Proof. reflexivity. Qed.

(* =====================================================================
   §§ Resultados opcionales polimórficos  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir el tipo (option X) con los constructores Some y None
   tales que 
   + (Some x) es un valor de tipo X.
   + None es el valor nulo.
   ------------------------------------------------------------------ *)

Inductive option (X:Type) : Type :=
  | Some : X -> option X
  | None : option X.

Arguments Some {X} _.
Arguments None {X}.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      nth_error {X : Type} (l : list X) (n : nat) : option X :=
   tal que (nth_error l n) es el n-ésimo elemento de l. Por ejemplo, 
      nth_error [4;5;6;7] 0 = Some 4.
      nth_error [[1];[2]] 1 = Some [2].
      nth_error [true] 2    = None.
   ------------------------------------------------------------------ *)

Fixpoint nth_error {X : Type} (l : list X) (n : nat) : option X :=
  match l with
  | []      => None
  | a :: l' => if beq_nat n O then Some a else nth_error l' (pred n)
  end.

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

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      hd_error {X : Type} (l : list X) : option X
   tal que (hd_error l) es el primer elemento de l. Por ejemplo,
      hd_error [1;2]     = Some 1.
      hd_error [[1];[2]] = Some [1].
   ------------------------------------------------------------------ *)

Definition hd_error {X : Type} (l : list X) : option X :=
 match l with 
    | []     => None
    | x :: _ => Some x
 end.

Check @hd_error.

Example test_hd_error1 : hd_error [1;2] = Some 1.
 Proof. reflexivity. Qed.
Example test_hd_error2 : hd_error  [[1];[2]]  = Some [1].
 Proof. reflexivity. Qed.

(* =====================================================================
   § Funciones como datos
   ================================================================== *)

(* =====================================================================
   § Funciones de orden superior 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función 
      doit3times {X:Type} (f:X->X) (n:X) : X 
   tal que (doit3times f) aplica 3 veces la función f. Por ejemplo,
      doit3times minustwo 9 = 3.
      doit3times negb true  = false.
   ------------------------------------------------------------------ *)

Definition doit3times {X:Type} (f:X->X) (n:X) : X :=
  f (f (f n)).

Check @doit3times.
(* ===> doit3times : forall X : Type, (X -> X) -> X -> X *)

Example test_doit3times: doit3times minustwo 9 = 3.
Proof. reflexivity.  Qed.
Example test_doit3times': doit3times negb true = false.
Proof. reflexivity.  Qed.

(* =====================================================================
   §§ Filtrado  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      filter {X:Type} (test: X->bool) (l:list X) : (list X)
   tal que (filter p l) es la lista de los elementos de l que verifican
   p. Por ejemplo,
      filter evenb [1;2;3;4] = [2;4].
   ------------------------------------------------------------------ *)


Fixpoint filter {X:Type} (test: X->bool) (l:list X)
                : (list X) :=
  match l with
  | []     => []
  | h :: t => if test h then h :: (filter test t)
                       else       filter test t
  end.

Example test_filter1: filter evenb [1;2;3;4] = [2;4].
Proof. reflexivity.  Qed.

Definition length_is_1 {X : Type} (l : list X) : bool :=
  beq_nat (length l) 1.

Example test_filter2:
    filter length_is_1
           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity.  Qed.

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

Definition countoddmembers' (l:list nat) : nat :=
  length (filter oddb l).

Example test_countoddmembers'1:   countoddmembers' [1;0;3;1;4;5] = 4.
Proof. reflexivity.  Qed.
Example test_countoddmembers'2:   countoddmembers' [0;2;4] = 0.
Proof. reflexivity.  Qed.
Example test_countoddmembers'3:   countoddmembers' nil = 0.
Proof. reflexivity.  Qed.

(* =====================================================================
   §§ Funciones anónimas  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que
      doit3times (fun n => n * n) 2 = 256.
   ------------------------------------------------------------------ *)

Example test_anon_fun':
  doit3times (fun n => n * n) 2 = 256.
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Calcular
      filter (fun l => beq_nat (length l) 1)
             [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
   ------------------------------------------------------------------ *)

Example test_filter2':
    filter (fun l => beq_nat (length l) 1)
           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      filter_even_gt7 (l : list nat) : list nat
   tal que (filter_even_gt7 l) es la lista de los elemntos de l que son
   pares y mayores que 7. Por ejemplo,
      filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
      filter_even_gt7 [5;2;6;19;129]      = [].
   ------------------------------------------------------------------ *)

Definition filter_even_gt7 (l : list nat) : list nat :=
  filter (fun x => evenb x && leb 7 x) l.

Example test_filter_even_gt7_1 :
  filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
 Proof. reflexivity. Qed.

Example test_filter_even_gt7_2 :
  filter_even_gt7 [5;2;6;19;129] = [].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      partition : forall X : Type,
                  (X -> bool) -> list X -> list X * list X
   tal que (patition p l) es el par de lista (lx,ly) tal que lx es la
   lista de los elementos de l que cumplen p y ly la de las que no lo
   cumplen. Por ejemplo,
      partition oddb [1;2;3;4;5]         = ([1;3;5], [2;4]).
      partition (fun x => false) [5;9;0] = ([], [5;9;0]).
   ------------------------------------------------------------------ *)

Definition partition {X : Type}
                     (test : X -> bool)
                     (l : list X)
                   : list X * list X :=
  (filter test l, filter (fun x => negb (test x)) l).

Example test_partition1: partition oddb [1;2;3;4;5] = ([1;3;5], [2;4]).
Proof. reflexivity. Qed.
Example test_partition2: partition (fun x => false) [5;9;0] = ([], [5;9;0]).
Proof. reflexivity. Qed.

(* =====================================================================
   §§ Aplicación a todos los elementos (map)
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      map {X Y:Type} (f:X->Y) (l:list X) : (list Y) 
   tal que (map f l) es la lista obtenida aplicando f a todos los
   elementos de l. Por ejemplo,
      map (fun x => plus 3 x) [2;0;2] = [5;3;5].
      map oddb [2;1;2;5] = [false;true;false;true].
      map (fun n => [evenb n;oddb n]) [2;1;2;5]
        = [[true;false];[false;true];[true;false];[false;true]].
   ------------------------------------------------------------------ *)

Fixpoint map {X Y:Type} (f:X->Y) (l:list X) : (list Y) :=
  match l with
  | []     => []
  | h :: t => (f h) :: (map f t)
  end.

Example test_map1: map (fun x => plus 3 x) [2;0;2] = [5;3;5].
Proof. reflexivity.  Qed.

Example test_map2:
  map oddb [2;1;2;5] = [false;true;false;true].
Proof. reflexivity.  Qed.

Example test_map3:
    map (fun n => [evenb n;oddb n]) [2;1;2;5]
  = [[true;false];[false;true];[true;false];[false;true]].
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Demostrar que
      map f (rev l) = rev (map f l).
   ------------------------------------------------------------------ *)

Lemma map_app_distr : forall (X Y : Type) (f : X -> Y) (l t : list X),
    map f (l ++ t) = map f l ++ map f t.
Proof.
  intros X Y f l t.
  induction l.
  + reflexivity.
  + simpl. rewrite IHl. reflexivity.
Qed.

Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  intros X Y f l.
  induction l.
  + reflexivity.
  + simpl. rewrite map_app_distr, IHl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      flat_map {X Y:Type} (f:X -> list Y) (l:list X) : (list Y)
   tal que (flat_map f l) es la concatenación de las listas obtenidas
   aplicando f a l. Por ejemplo,
      flat_map (fun n => [n;n;n]) [1;5;4] = [1; 1; 1; 5; 5; 5; 4; 4; 4].
   ------------------------------------------------------------------ *)

Fixpoint flat_map {X Y:Type} (f:X -> list Y) (l:list X) 
                   : (list Y) :=
   match l with
  | [] => []
  | x :: t => f x ++ flat_map f t
  end.

Example test_flat_map1:
  flat_map (fun n => [n;n;n]) [1;5;4]
  = [1; 1; 1; 5; 5; 5; 4; 4; 4].
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      option_map {X Y : Type} (f : X -> Y) (xo : option X) : option Y
   tal que (option_map f xo) es la aplicación de f a xo.
   ------------------------------------------------------------------ *)

Definition option_map {X Y : Type} (f : X -> Y) (xo : option X)
                      : option Y :=
  match xo with
    | None   => None
    | Some x => Some (f x)
  end.

(* =====================================================================
   §§ Plegados (fold)  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      fold {X Y:Type} (f: X->Y->Y) (l:list X) (b:Y) : Y
   tal que (fold f l b) es el plegado de l con la operación f a partir
   del elemento b. Por ejemplo,
      fold mult [1;2;3;4] 1                 = 24.
      fold andb [true;true;false;true] true = false.
      fold app  [[1];[];[2;3];[4]] []       = [1;2;3;4].
   ------------------------------------------------------------------ *)

Fixpoint fold {X Y:Type} (f: X->Y->Y) (l:list X) (b:Y)
                         : Y :=
  match l with
  | nil    => b
  | h :: t => f h (fold f t b)
  end.

Check (fold andb).
(* ===> fold andb : list bool -> bool -> bool *)

Example fold_example1 :
  fold mult [1;2;3;4] 1 = 24.
Proof. reflexivity. Qed.

Example fold_example2 :
  fold andb [true;true;false;true] true = false.
Proof. reflexivity. Qed.

Example fold_example3 :
  fold app  [[1];[];[2;3];[4]] [] = [1;2;3;4].
Proof. reflexivity. Qed.

(* =====================================================================
   §§ Funciones que construyen funciones  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      constfun {X: Type} (x: X) : nat->X
   tal que (constfun x) es la función que a todos los naturales le
   asigna el x. Por ejemplo, si se define 
      Definition ftrue := constfun true.
   entonces,
      ftrue 0         = true.
      (constfun 5) 99 = 5.
   ------------------------------------------------------------------ *)

Definition constfun {X: Type} (x: X) : nat->X :=
  fun (k:nat) => x.

Definition ftrue := constfun true.

Example constfun_example1 : ftrue 0 = true.
Proof. reflexivity. Qed.

Example constfun_example2 : (constfun 5) 99 = 5.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Calcular el tipo de plus.
   ------------------------------------------------------------------ *)

Check plus.
(* ==> nat -> nat -> nat *)

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      plus3 : nat -> nat
   tal que (plus3 x) es tres más x. Por ejemplo,
      plus3 4               = 7.
      doit3times plus3 0    = 9.
      doit3times (plus 3) 0 = 9.
   ------------------------------------------------------------------ *)

Definition plus3 := plus 3.

Example test_plus3 :    plus3 4 = 7.
Proof. reflexivity.  Qed.
Example test_plus3' :   doit3times plus3 0 = 9.
Proof. reflexivity.  Qed.
Example test_plus3'' :  doit3times (plus 3) 0 = 9.
Proof. reflexivity.  Qed.

(* =====================================================================
   § Ejercicios 
   ================================================================== *)

Module Exercises.

(* ---------------------------------------------------------------------
   Ejercicio. Definir, usando fold, la función
      fold_length {X : Type} (l : list X) : nat
   tal que (fold_length l) es la longitud de l. Por ejemplo,
      fold_length [4;7;0] = 3.
   ------------------------------------------------------------------ *)
  
Definition fold_length {X : Type} (l : list X) : nat :=
  fold (fun _ n => S n) l 0.

Example test_fold_length1 : fold_length [4;7;0] = 3.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que
      fold_length l = length l.
   ------------------------------------------------------------------ *)

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
  intros X l.
  unfold fold_length.
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Definir, usando fold, la función
      fold_map {X Y:Type} (f : X -> Y) (l : list X) : list Y
   tal que (fold_map f l) es la lista obtenida aplicando f a los
   elementos de l.
   ------------------------------------------------------------------ *)

Definition fold_map {X Y:Type} (f : X -> Y) (l : list X) : list Y :=
   fold (fun x t => (f x) :: t)  l [].


(* ---------------------------------------------------------------------
   Ejemplo. Demostrar que fold_map es equivalente a map.
   ------------------------------------------------------------------ *)

Theorem fold_map_correct : forall (X Y : Type) (f : X -> Y) (l : list X),
     fold_map f l = map f l.
Proof.
  intros X Y f l.
  unfold fold_map.
  induction l.
  - reflexivity.
  - simpl. rewrite IHl. reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo. Definir la función
      prod_curry {X Y Z : Type} (f : X * Y -> Z) (x : X) (y : Y) : Z
   tal que (prod_curry f x y) es la versión curryficada de f.
   ------------------------------------------------------------------ *)

Definition prod_curry {X Y Z : Type}
  (f : X * Y -> Z) (x : X) (y : Y) : Z := f (x, y).

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      prod_uncurry {X Y Z : Type} (f : X -> Y -> Z) (p : X * Y) : Z
   tal que (prod_uncurry f p) es la versión incurryficada de f.
   ------------------------------------------------------------------ *)

Definition prod_uncurry {X Y Z : Type}
  (f : X -> Y -> Z) (p : X * Y) : Z := f (fst p) (snd p).

Check @prod_curry.
Check @prod_uncurry.

(* ---------------------------------------------------------------------
   Ejercicio. Demostrar que
      prod_curry (prod_uncurry f) x y = f x y
   ------------------------------------------------------------------ *)

Theorem uncurry_curry : forall (X Y Z : Type)
                        (f : X -> Y -> Z)
                        x y,
  prod_curry (prod_uncurry f) x y = f x y.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Demostrar que
      prod_uncurry (prod_curry f) p = f p.
   ------------------------------------------------------------------ *)

Theorem curry_uncurry : forall (X Y Z : Type)
                        (f : (X * Y) -> Z) (p : X * Y),
  prod_uncurry (prod_curry f) p = f p.
Proof.
  intros.
  destruct p.
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Demostrar que
      forall X n l, length l = n -> @nth_error X l n = None
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejercicio. En los siguientes ejercicios se trabajará con la
   definición de Church de los números naturales: el número natural n es
   la función que toma como argumento una función f y devuelve como
   valor la aplicación de n veces la función f. 
   ------------------------------------------------------------------ *)

Module Church.

(* ---------------------------------------------------------------------
   Ejercicio. Definir el tipo nat para los números naturales de Church. 
   ------------------------------------------------------------------ *)
  
Definition nat := forall X : Type, (X -> X) -> X -> X.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      one : nat
   tal que one es el número uno de Church.
   ------------------------------------------------------------------ *)

Definition one : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f x.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      two : nat
   tal que two es el número dos de Church.
   ------------------------------------------------------------------ *)

Definition two : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f (f x).

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      zero : nat
   tal que zero es el número cero de Church.
   ------------------------------------------------------------------ *)

Definition zero : nat :=
  fun (X : Type) (f : X -> X) (x : X) => x.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      three : nat
   tal que three es el número tres de Church.
   ------------------------------------------------------------------ *)

Definition three : nat := @doit3times.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      succ (n : nat) : nat
   tal que (succ n) es el siguiente del número n de Church. Por ejemplo, 
      succ zero = one.
      succ one  = two.
      succ two  = three.
   ------------------------------------------------------------------ *)

Definition succ (n : nat) : nat :=
   fun (X : Type) (f : X -> X) (x : X) => f (n X f x).

Example succ_1 : succ zero = one.
Proof. reflexivity. Qed.

Example succ_2 : succ one = two.
Proof. reflexivity. Qed.

Example succ_3 : succ two = three.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      plus (n m : nat) : nat
   tal que (plus n m) es la suma de n y m. Por ejemplo,
      plus zero one             = one.
      plus two three            = plus three two.
      plus (plus two two) three = plus one (plus three three).
   ------------------------------------------------------------------ *)

Definition plus (n m : nat) : nat :=
  fun (X : Type) (f : X -> X) (x : X) => m X f (n X f x).

Example plus_1 : plus zero one = one.
Proof. reflexivity. Qed.

Example plus_2 : plus two three = plus three two.
Proof. reflexivity. Qed.

Example plus_3 :
  plus (plus two two) three = plus one (plus three three).
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      mult (n m : nat) : nat
   tal que (mult n m) es el producto de n y m. Por ejemplo,
      mult one one = one.
      mult zero (plus three three) = zero.
      mult two three = plus three three.
   ------------------------------------------------------------------ *)

Definition mult (n m : nat) : nat :=
   fun (X : Type) (f : X -> X) (x : X) => n X (m X f) x.

Example mult_1 : mult one one = one.
Proof. reflexivity. Qed.

Example mult_2 : mult zero (plus three three) = zero.
Proof. reflexivity. Qed.

Example mult_3 : mult two three = plus three three.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejercicio. Definir la función
      exp (n m : nat) : nat
   tal que (exp n m) es la potencia m-ésima de n. Por ejemplo, 
      exp two two = plus two two.
      exp three two = plus (mult two (mult two two)) one.
      exp three zero = one.
   ------------------------------------------------------------------ *)

Definition exp (n m : nat) : nat :=
  ( fun (X : Type) (f : X -> X) (x : X) => (m (X -> X) (n X) f) x).

Example exp_1 : exp two two = plus two two.
Proof. reflexivity. Qed.

Example exp_2 : exp three two = plus (mult two (mult two two)) one.
Proof. reflexivity. Qed.

Example exp_3 : exp three zero = one.
Proof. reflexivity. Qed.

End Church.

End Exercises.