Ver el código de «Tema 4: Polimorfismo y funciones de orden superior en Coq» - Razonamiento automático (2018-19)

<source lang="coq">
Require Export T3_EstructurasNat.

(* El contenido del tema es
   1. Polimorfismo
      1. Listas polimórficas  
         1. Inferencia de tipos
         2. Síntesis de los tipos de los argumentos  
         3. Argumentos implícitos  
         4. Explicitación de argumentos  
         5. Ejercicios  
      2. Polimorfismo de pares  
      3. Resultados opcionales polimórficos  
   2. Funciones como datos
      1. Funciones de orden superior 
      2. Filtrado  
      3. Funciones anónimas  
      4. Aplicación a todos los elementos (map)
      5. Plegados (fold)  
      6. Funciones que construyen funciones  
   3. Bibliografía
*)

(* =====================================================================
   § 1. Polimorfismo
   ================================================================== *)

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

(* ---------------------------------------------------------------------
   Nota. Se suprimen algunos avisos.
   ------------------------------------------------------------------ *)

Set Warnings "-notation-overridden,-parsing".

(* ---------------------------------------------------------------------
   Ejemplo 1.1.1. Definir el tipo (list X) para representar las listas
   de elementos de tipo X 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 1.1.2. Calcular el tipo de list.
   ------------------------------------------------------------------ *)

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

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

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

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

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

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

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

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

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

(* ---------------------------------------------------------------------
   Ejemplo 1.1.7. 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 1.1.8. Definir la función
      repite (X : Type) (x : X) (n : nat) : list X
   tal que (repite X x n) es la lista, de elementos de tipo X, obtenida
   repitiendo n veces el elemento x. Por ejemplo,
      repite nat 4 2 = cons nat 4 (cons nat 4 (nil nat)).
      repite bool false 1 = cons bool false (nil bool).
   ------------------------------------------------------------------ *)

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

Example prop_repite1 :
  repite nat 4 2 = cons nat 4 (cons nat 4 (nil nat)).
Proof. reflexivity.  Qed.

Example prop_repite2 :
  repite bool false 1 = cons bool false (nil bool).
Proof. reflexivity.  Qed.

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

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

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

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

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

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

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

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

(* ---------------------------------------------------------------------
   Ejemplo 1.1.12. 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 _))).

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

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

Arguments nil {X}.
Arguments cons {X} _ _.
Arguments repite {X} x n.

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

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

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

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

Example prop_repite'''1 :
  repite''' 4 2 = cons 4 (cons 4 nil).
Proof. reflexivity.  Qed.

Example prop_repite'''2 :
  repite false 1 = cons false nil.
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo 1.1.16. Definir el tipo (list' {X}) para representar las
   listas de elementos de tipo X 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 1.1.17. Definir la función
      conc {X : Type} (xs ys : list X) : (list X)
   tal que (conc xs ys) es la concatenación de xs e ys.
   ------------------------------------------------------------------ *)

Fixpoint conc {X : Type} (xs ys : list X) : (list X) :=
  match xs with
  | nil        => ys
  | cons x xs' => cons x (conc xs' ys)
  end.

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

Fixpoint inversa {X : Type} (xs : list X) : list X :=
  match xs with
  | nil        => nil
  | cons x xs' => conc (inversa xs') (cons x nil)
  end.

Example prop_inversa1 :
  inversa (cons 1 (cons 2 nil)) = (cons 2 (cons 1 nil)).
Proof. reflexivity.  Qed.

Example prop_inversa2:
  inversa (cons true nil) = cons true nil.
Proof. reflexivity.  Qed.

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

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

Example prop_longitud1:
  longitud (cons 1 (cons 2 (cons 3 nil))) = 3.
Proof. reflexivity.  Qed.

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

(* ---------------------------------------------------------------------
   Ejemplo 1.1.20. Evaluar la siguiente expresión
      Fail Definition n_nil := nil.
   ------------------------------------------------------------------ *)

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

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

(* 1ª solución *)
Definition n_nil : list nat := nil.

(* 2ª solución *)
Definition n_nil' := @nil nat.

(* ---------------------------------------------------------------------
   Ejemplo 1.1.22. Definir las siguientes abreviaturas
   + "x :: y"         para (cons x y)
   + "[ ]"            para nil
   + "[ x ; .. ; y ]" para (cons x .. (cons y []) ..).
   + "x ++ y"         para (conc 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"         := (conc x y)
                              (at level 60, right associativity).

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

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

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

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

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

Arguments par {X} {Y} _ _.

(* ---------------------------------------------------------------------
   Ejemplo 1.2.2. Definir la abreviaturas
      "( x , y )" para (par x y).
   ------------------------------------------------------------------ *)

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

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

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

(* ---------------------------------------------------------------------
   Ejemplo 1.2.4. Definir la función
      fst {X Y : Type} (p : X * Y) : X
   tal que (fst p) es la primera componente del par p. Por ejemplo,
      fst (par 3 5) = 3
   ------------------------------------------------------------------ *)

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

Example prop_fst: fst (par 3 5) = 3.
Proof. reflexivity. Qed.

(* ---------------------------------------------------------------------
   Ejemplo 2.2.5. Definir la función
      snd {X Y : Type} (p : X * Y) 
   tal que (snd p) es la segunda componente del par p. Por ejemplo,
      snd (par 3 5) = 5 
   ------------------------------------------------------------------ *)

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

Example prop_snd: snd (par 3 5) = 5.
Proof. reflexivity. Qed.


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

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

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

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

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

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

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

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

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

Example prop_aplica3veces:
  aplica3veces menosDos 9 = 3.
Proof. reflexivity.  Qed.

Example prop_aplica3veces':
  aplica3veces negacion true = false.
Proof. reflexivity.  Qed.

(* =====================================================================
   §§ 2.2. Filtrado  
   ================================================================== *)

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

Fixpoint filtra {X : Type} (p : X -> bool) (xs : list X) : (list X) :=
  match xs with
  | []       => []
  | x :: xs' => if p x
               then x :: (filtra p xs')
               else filtra p xs'
  end.

Example prop_filtra1:
  filtra esPar [1;2;3;4] = [2;4].
Proof. reflexivity.  Qed.

(* ---------------------------------------------------------------------
   Ejemplo 2.2.2. Definir la función
      unitarias {X : Type} (xss : list (list X)) : list (list X) :=
   tal que (unitarias xss) es la lista de listas unitarias de xss. Por
   ejemplo, 
      unitarias [[1;2];[3];[4];[5;6;7];[];[8]] = [[3];[4];[8]]
   ------------------------------------------------------------------ *)

Definition esUnitaria {X : Type} (xs : list X) : bool :=
  iguales_nat (longitud xs) 1.

Definition unitarias {X : Type} (xss : list (list X)) : list (list X) :=
  filtra esUnitaria xss.
  
Compute (unitarias [[1; 2]; [3]; [4]; [5;6;7]; []; [8]]).
(* = [[3]; [4]; [8]] : list (list nat)*)

Example prop_unitarias:
  unitarias [[1; 2]; [3]; [4]; [5;6;7]; []; [8]]
  = [[3]; [4]; [8]].
Proof. reflexivity.  Qed.

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

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

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

(* ---------------------------------------------------------------------
   Ejemplo 2.3.2. Calcular
      filtra (fun xs => iguales_nat (longitud xs) 1)
             [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
   ------------------------------------------------------------------ *)

Compute (filtra (fun xs => iguales_nat (longitud xs) 1)
                [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]).
(* = [[3]; [4]; [8]] : list (list nat)*)

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

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

Fixpoint map {X Y:Type} (f : X -> Y) (xs : list X) : list Y :=
  match xs with
  | []       => []
  | x :: xs' => f x :: map f xs'
  end.

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

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

Example prop_map3:
  map (fun n => [esPar n ; esImpar n]) [2;1;2;5]
  = [[true;false];[false;true];[true;false];[false;true]].
Proof. reflexivity.  Qed.

(* =====================================================================
   §§ 2.5. Plegados (fold)  
   ================================================================== *)

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

Fixpoint fold {X Y:Type} (f: X -> Y -> Y) (xs : list X) (b : Y) : Y :=
  match xs with
  | nil      => b
  | x :: xs' => f x (fold f xs' b)
  end.

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

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

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

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

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

(* ---------------------------------------------------------------------
   Ejemplo 2.6.1. Definir la función
      constante {X : Type} (x : X) : nat -> X
   tal que (constante x) es la función que a todos los naturales le
   asigna el x. Por ejemplo, 
      (constante 5) 99 = 5.
   ------------------------------------------------------------------ *)

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

Example prop_constante:
  (constante 5) 99 = 5.
Proof. reflexivity. Qed.

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

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

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

Definition plus3 := plus 3.

Example prop_plus3a:
  plus3 4 = 7.
Proof. reflexivity.  Qed.

Example prop_plus3b:
  aplica3veces plus3 0 = 9.
Proof. reflexivity.  Qed.

Example prop_plus3c:
  aplica3veces (plus 3) 0 = 9.
Proof. reflexivity.  Qed.

(* =====================================================================
   § Bibliografía
   ================================================================== *)

(*
 + "Polymorphism and higher-order functions" de Peirce et als. 
   http://bit.ly/2Mj5gMf *)
</source>