temas/Tema-19.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<span style=\"font-size:2em; color:blue\">\n",
    "    Tema 19: El TAD de las árboles binarios de búsqueda\n",
    "</span>  \n",
    "\n",
    "----------\n",
    "\n",
    "[José A. Alonso](https://www.cs.us.es/~jalonso)  \n",
    "[Departamento de Ciencias de la Computación e I.A.](https://www.cs.us.es)  \n",
    "[Universidad de Sevilla](http://www.us.es)  \n",
    "Sevilla, 15 de agosto de 2019"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "> __Notas:__ \n",
    "+ La versión interactiva de este tema se encuentra en [Binder](https://mybinder.org/v2/gh/jaalonso/Temas_interactivos_de_PF_con_Haskell/master?urlpath=lab/tree/temas/Tema-19.ipynb).\n",
    "+ Se desactiva el [corrector estilo de Haskell](https://github.com/gibiansky/IHaskell/wiki#opt-no-lint)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    ":opt no-lint"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Especificación del TAD de los árboles binarios de búsqueda"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Signatura del TAD de los árboles binarios de búsqueda\n",
    "\n",
    "**Descripción de los árboles binarios de búsqueda**\n",
    "\n",
    "+ Un árbol binario de búsqueda (ABB) es un árbol binario tal que el valor\n",
    "  de cada nodo es mayor que los valores de su subárbol izquierdo y es menor que\n",
    "  los valores de su subárbol derecho y, además, ambos subárboles son árboles\n",
    "  binarios de búsqueda.\n",
    "\n",
    "+ Por ejemplo, al almacenar los valores de [2,3,4,5,6,8,9] en un ABB se\n",
    "  puede obtener los siguientes ABB:\n",
    "\n",
    "```sesion\n",
    "    5                     5\n",
    "  /   \\                 /   \\\n",
    " 2     6               3     8\n",
    "  \\     \\             / \\   / \\\n",
    "   4     8           2   4 6   9\n",
    "  /       \\\n",
    " 3         9\n",
    "```\n",
    "\n",
    "+ El objetivo principal de los ABB es reducir el tiempo de acceso a los\n",
    "  valores.\n",
    "  \n",
    "**Signatura del TAD de los árboles binarios de búsqueda**\n",
    "\n",
    "```sesion\n",
    "vacio     :: ABB \n",
    "inserta   :: (Ord a,Show a) => a -> ABB a -> ABB a\n",
    "elimina   :: (Ord a,Show a) => a -> ABB a -> ABB a\n",
    "crea      :: (Ord a,Show a) => [a] -> ABB a\n",
    "menor     :: Ord a => ABB a -> a\n",
    "elementos :: (Ord a,Show a) => ABB a -> [a]\n",
    "pertenece :: (Ord a,Show a) => a -> ABB a -> Bool\n",
    "valido    :: (Ord a,Show a) => ABB a -> Bool\n",
    "```\n",
    "\n",
    "+ Descripción de las operaciones:\n",
    "    + `vacio` es el ABB vacío.\n",
    "    + `(pertenece v a)` se verifica si v es el valor de algún nodo del ABB a.\n",
    "    + `(inserta v a)` es el árbol obtenido añadiendo el valor v al ABB a, si no\n",
    "      es uno de sus valores.\n",
    "    + `(crea vs)` es el ABB cuyos valores son vs.\n",
    "    + `(elementos a)` es la lista de los valores de los nodos del ABB en el\n",
    "      recorrido inorden.\n",
    "    + `(elimina v a)` es el ABB obtenido eliminando el valor v del ABB a.\n",
    "    + `(menor a)` es el mínimo valor del ABB a.\n",
    "    + `(valido a)` se verifica si a es un ABB correcto."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Propiedades del TAD de los árboles binarios de búsqueda\n",
    "\n",
    "+ `valido vacio`\n",
    "\n",
    "+ `valido (inserta v a)`\n",
    "\n",
    "+ `inserta x a /= vacio`\n",
    "\n",
    "+ `pertenece x (inserta x a)`\n",
    "\n",
    "+ `not (pertenece x vacio)`\n",
    "\n",
    "+ `pertenece y (inserta x a) == (x == y) || pertenece y a`\n",
    "\n",
    "+ `valido (elimina v a)`\n",
    "\n",
    "+ `elimina x (inserta x a) == elimina x a`\n",
    "\n",
    "+ `valido (crea xs)`\n",
    "\n",
    "+ `elementos (crea xs) == sort (nub xs)`\n",
    "\n",
    "+ `pertenece v a == elem v (elementos a)`\n",
    "\n",
    "+ `∀x ∈ elementos a (menor a ≤ x)` \n",
    " \n",
    "# Implementación del TAD de los árboles binarios de búsqueda\n",
    "\n",
    "## Los ABB como tipo de dato algebraico"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "module ArbolBin\n",
    "  (ABB,\n",
    "   vacio,     -- ABB \n",
    "   inserta,   -- (Ord a,Show a) => a -> ABB a -> ABB a\n",
    "   elimina,   -- (Ord a,Show a) => a -> ABB a -> ABB a\n",
    "   crea,      -- (Ord a,Show a) => [a] -> ABB a\n",
    "   crea',     -- (Ord a,Show a) => [a] -> ABB a\n",
    "   menor,     -- Ord a => ABB a -> a\n",
    "   elementos, -- (Ord a,Show a) => ABB a -> [a]\n",
    "   pertenece, -- (Ord a,Show a) => a -> ABB a -> Bool\n",
    "   valido     -- (Ord a,Show a) => ABB a -> Bool\n",
    "  ) where\n",
    "\n",
    "-- Los ABB como tipo de dato algebraico.\n",
    "data ABB a = Vacio\n",
    "           | Nodo a (ABB a) (ABB a)\n",
    "  deriving Eq\n",
    "\n",
    "-- Procedimiento de escritura de árboles binarios de búsqueda.\n",
    "instance (Show a, Ord a) => Show (ABB a) where\n",
    "  show Vacio        = \" -\"\n",
    "  show (Nodo x i d) = \" (\" ++ show x ++ show i ++ show d ++ \")\"\n",
    "\n",
    "-- Ejemplos de ABB\n",
    "--    ghci> abb1\n",
    "--     (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))\n",
    "--    ghci> abb2\n",
    "--     (5 (2 - (4 (3 - -) -)) (8 (6 - (7 - -)) (10 (9 - -) (11 - -))))\n",
    "abb1, abb2 :: ABB Int\n",
    "abb1 = crea (reverse [5,2,6,4,8,3,9])\n",
    "abb2 = foldr inserta vacio (reverse [5,2,4,3,8,6,7,10,9,11])\n",
    "\n",
    "-- vacio es el ABB vacío. Por ejemplo,\n",
    "--    ghci> vacio\n",
    "--     -\n",
    "vacio :: ABB a\n",
    "vacio = Vacio\n",
    "\n",
    "-- (pertenece v' a) se verifica si v' es el valor de algún nodo del ABB\n",
    "-- a. Por ejemplo, \n",
    "--   pertenece 3 abb1  ==  True\n",
    "--   pertenece 7 abb1  ==  False\n",
    "pertenece :: (Ord a,Show a) => a -> ABB a -> Bool\n",
    "pertenece _ Vacio = False\n",
    "pertenece v' (Nodo v i d)\n",
    "  | v == v'   = True  \n",
    "  | v' < v    = pertenece v' i\n",
    "  | otherwise = pertenece v' d\n",
    "\n",
    "-- (inserta v a) es el árbol obtenido añadiendo el valor v al ABB a, si\n",
    "-- no es uno de sus valores. Por ejemplo, \n",
    "--    ghci> inserta 7 abb1\n",
    "--     (5 (2 - (4 (3 - -) -)) (6 - (8 (7 - -) (9 - -))))\n",
    "inserta :: (Ord a,Show a) => a -> ABB a -> ABB a\n",
    "inserta v' Vacio = Nodo v' Vacio Vacio\n",
    "inserta v' (Nodo v i d) \n",
    "  | v' == v   = Nodo v i d\n",
    "  | v' < v    = Nodo v (inserta v' i) d\n",
    "  | otherwise = Nodo v i (inserta v' d)\n",
    "                                        \n",
    "-- (crea1 vs) es el ABB cuyos valores son vs. Por ejemplo,\n",
    "--    ghci> crea1 [3,7,2]\n",
    "--     (7 (3 (2 - -) -) -)\n",
    "crea :: (Ord a,Show a) => [a] -> ABB a\n",
    "crea = foldr inserta Vacio\n",
    "\n",
    "-- (crea' vs) es el ABB de menor profundidad cuyos valores son los de\n",
    "-- la lista ordenada vs. Por ejemplo, \n",
    "--    ghci> crea' [2,3,7]\n",
    "--     (3 (2 - -) (7 - -))\n",
    "crea' :: (Ord a,Show a) => [a] -> ABB a\n",
    "crea' [] = Vacio\n",
    "crea' vs = Nodo x (crea' l1) (crea' l2)\n",
    "  where n      = length vs `div` 2\n",
    "        l1     = take n vs\n",
    "        (x:l2) = drop n vs \n",
    "\n",
    "-- (elementos a) es la lista de los valores de los nodos del ABB en el\n",
    "-- recorrido inorden. Por ejemplo,          \n",
    "--   elementos abb1  ==  [2,3,4,5,6,8,9]\n",
    "--   elementos abb2  ==  [2,3,4,5,6,7,8,9,10,11]\n",
    "elementos :: (Ord a,Show a) => ABB a -> [a]\n",
    "elementos Vacio        = []\n",
    "elementos (Nodo v i d) = elementos i ++ [v] ++ elementos d\n",
    "\n",
    "-- (elimina v a) es el ABB obtenido borrando el valor v del ABB a. Por\n",
    "-- ejemplo, \n",
    "--    ghci> abb1\n",
    "--     (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))\n",
    "--    ghci> elimina 3 abb1\n",
    "--     (5 (2 - (4 - -)) (6 - (8 - (9 - -))))\n",
    "--    ghci> elimina 2 abb1\n",
    "--     (5 (4 (3 - -) -) (6 - (8 - (9 - -))))\n",
    "--    ghci> elimina 5 abb1\n",
    "--     (6 (2 - (4 (3 - -) -)) (8 - (9 - -)))\n",
    "--    ghci> elimina 7 abb1\n",
    "--     (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))\n",
    "elimina  :: (Ord a,Show a) => a -> ABB a -> ABB a\n",
    "elimina _  Vacio = Vacio \n",
    "elimina v' (Nodo v i Vacio) | v'==v = i \n",
    "elimina v' (Nodo v Vacio d) | v'==v = d\n",
    "elimina v' (Nodo v i d)\n",
    "  | v' < v    = Nodo v (elimina v' i) d \n",
    "  | v' > v    = Nodo v i (elimina v' d)  \n",
    "  | otherwise = Nodo k i (elimina k d)\n",
    "  where k = menor d \n",
    "\n",
    "-- (menor a) es el mínimo valor del ABB a. Por ejemplo,\n",
    "--   menor abb1  ==  2\n",
    "menor :: Ord a => ABB a -> a\n",
    "menor (Nodo v Vacio _) = v\n",
    "menor (Nodo _ i _)        = menor i \n",
    "\n",
    "-- (menorTodos v a) se verifica si v es menor que todos los elementos\n",
    "-- del ABB a.\n",
    "menorTodos :: (Ord a, Show a) => a -> ABB a -> Bool\n",
    "menorTodos _ Vacio = True \n",
    "menorTodos v a        = v < minimum (elementos a)\n",
    "\n",
    "-- (mayorTodos v a) se verifica si v es mayor que todos los elementos\n",
    "-- del ABB a.\n",
    "mayorTodos :: (Ord a, Show a) => a -> ABB a -> Bool\n",
    "mayorTodos _ Vacio = True \n",
    "mayorTodos v a = v > maximum (elementos a)\n",
    "\n",
    "-- (valido a) se verifica si a es un ABB correcto. Por ejemplo,\n",
    "--    valido abb1 == True\n",
    "valido :: (Ord a, Show a) => ABB a -> Bool\n",
    "valido Vacio        = True\n",
    "valido (Nodo v a b) =\n",
    "  mayorTodos v a &&\n",
    "  menorTodos v b && \n",
    "  valido a &&\n",
    "  valido b"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Ejemplos"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "abb1, abb2 :: ABB Int\n",
    "abb1 = crea (reverse [5,2,6,4,8,3,9])\n",
    "abb2 = foldr inserta vacio (reverse [5,2,4,3,8,6,7,10,9,11])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " (5 (2 - (4 (3 - -) -)) (8 (6 - (7 - -)) (10 (9 - -) (11 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "abb2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " -"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "vacio"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "pertenece 3 abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "pertenece 7 abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " (5 (2 - (4 (3 - -) -)) (6 - (8 (7 - -) (9 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "inserta 7 abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " (7 (3 (2 - -) -) -)"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "crea [2,3,7]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " (3 (2 - -) (7 - -))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "crea' [2,3,7]"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[2,3,4,5,6,8,9]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "elementos abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[2,3,4,5,6,7,8,9,10,11]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "elementos abb2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       " (5 (2 - (4 - -)) (6 - (8 - (9 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "abb1\n",
    "elimina 3 abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       " (5 (4 (3 - -) -) (6 - (8 - (9 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "abb1\n",
    "elimina 2 abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       " (6 (2 - (4 (3 - -) -)) (8 - (9 - -)))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "abb1\n",
    "elimina 5 abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       " (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       " (5 (2 - (4 (3 - -) -)) (6 - (8 - (9 - -))))"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "abb1\n",
    "elimina 7 abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "2"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "menor abb1 "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "valido abb1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "valido abb2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Se elimina la implementación"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [],
   "source": [
    ":m - ArbolBin"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Comprobación de la implementación con QuickCheck"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [],
   "source": [
    "{-# LANGUAGE FlexibleInstances #-}\n",
    "\n",
    "module ArbolBinPropiedades where\n",
    "\n",
    "import ArbolBin\n",
    "\n",
    "import Data.List\n",
    "import Test.QuickCheck\n",
    "\n",
    "-- ---------------------------------------------------------------------\n",
    "-- Generador de ABB                                                   --\n",
    "-- ---------------------------------------------------------------------\n",
    "\n",
    "-- genABB es un generador de árboles binarios de búsqueda. Por ejemplo,\n",
    "--    ghci> sample genABB\n",
    "--     -\n",
    "--     (1 (-1 - -) -)\n",
    "--     (1 - -)\n",
    "--     (-1 (-3 - -) (1 - (4 - -)))\n",
    "--     -\n",
    "--     (10 (-7 - -) -)\n",
    "--     (1 (-9 - -) (7 (5 - -) (10 - -)))\n",
    "--     ...\n",
    "genABB :: Gen (ABB Int)\n",
    "genABB = do\n",
    "  xs <- listOf arbitrary\n",
    "  return (foldr inserta vacio xs)\n",
    "\n",
    "-- Los árboles binarios de búsqueda son concreciones de la clase\n",
    "-- arbitraria. \n",
    "instance Arbitrary (ABB Int) where\n",
    "  arbitrary = genABB\n",
    "\n",
    "-- Propiedad. Todo los elementos generados por genABB son árboles binarios\n",
    "-- de búsqueda.\n",
    "prop_genABB_correcto :: ABB Int -> Bool\n",
    "prop_genABB_correcto = valido \n",
    "\n",
    "-- Comprobación.\n",
    "--    ghci> quickCheck prop_genABB_correcto\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- listaOrdenada es un generador de listas ordenadas de números\n",
    "-- enteros. Por ejemplo,\n",
    "--    ghci> sample listaOrdenada\n",
    "--    [1]\n",
    "--    [1]\n",
    "--    [-2,-1,0]\n",
    "--    [-1,0,1]\n",
    "--    [-8,-5,-4,-3,3,4,8]\n",
    "--    [-6,-3,8]\n",
    "--    [-14,-13]\n",
    "--    [-31,-23,-16,-13,-11,-5,1,4,11,14,15,21,26,29]\n",
    "--    []\n",
    "--    []\n",
    "--    []\n",
    "listaOrdenada :: Gen [Int]\n",
    "listaOrdenada = \n",
    "  frequency [(1,return []),\n",
    "             (4,do xs <- orderedList\n",
    "                   n <- arbitrary\n",
    "                   return (nub ((case xs of\n",
    "                                   []  -> n\n",
    "                                   x:_ -> n `min` x)\n",
    "                                :xs)))]\n",
    "\n",
    "-- (ordenada xs) se verifica si xs es una lista ordenada creciente. Por\n",
    "-- ejemplo, \n",
    "--    ordenada [3,5,9]  ==  True\n",
    "--    ordenada [3,9,5]  ==  False\n",
    "ordenada :: [Int] -> Bool\n",
    "ordenada xs = and [x<y | (x,y) <- zip xs (tail xs)]\n",
    "\n",
    "-- Propiedad. El generador listaOrdenada produce listas ordenadas. \n",
    "prop_listaOrdenada_correcta :: [Int] -> Property\n",
    "prop_listaOrdenada_correcta _ = \n",
    "  forAll listaOrdenada ordenada\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_listaOrdenada_correcta\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedad. Al eliminar las repeticiones en las listas producidas por el\n",
    "-- generador orderedList se obtienen listas ordenadas.  \n",
    "prop_orderedList_correcta :: [Int] -> Property\n",
    "prop_orderedList_correcta _ = \n",
    "  forAll orderedList (ordenada . nub)\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_orderedList_correcta\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- ---------------------------------------------------------------------\n",
    "-- Propiedades                                                        --\n",
    "-- ---------------------------------------------------------------------\n",
    "\n",
    "-- Propiedades de vacio\n",
    "-- --------------------\n",
    "\n",
    "-- Prop. vacio es un ABB.\n",
    "prop_vacio_es_ABB :: Bool\n",
    "prop_vacio_es_ABB =\n",
    "  valido (vacio :: ABB Int)\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_vacio_es_ABB\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedades de inserta\n",
    "-- ----------------------\n",
    "\n",
    "-- Propiedad. Si a es un ABB, entonces (inserta v a) también lo es.\n",
    "prop_inserta_es_valida :: Int -> ABB Int -> Bool\n",
    "prop_inserta_es_valida v a =\n",
    "  valido (inserta v a)\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_inserta_es_valida\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedad. El árbol que resulta de añadir un elemento a un ABB es no\n",
    "-- vacío. \n",
    "prop_inserta_es_no_vacio :: Int -> ABB Int -> Bool\n",
    "prop_inserta_es_no_vacio x a =\n",
    "  inserta x a /= vacio\n",
    "\n",
    "-- Comprobación.\n",
    "--    ghci> quickCheck prop_inserta_es_no_vacio\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedad. Para todo x y a, x es un elemento de (inserta x a). \n",
    "prop_elemento_de_inserta :: Int -> ABB Int -> Bool\n",
    "prop_elemento_de_inserta x a =\n",
    "  pertenece x (inserta x a)\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_elemento_de_inserta\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedades de pertenece\n",
    "-- ------------------------\n",
    "\n",
    "-- Propiedad. En en árbol vacio no hay ningún elemento.\n",
    "prop_vacio_sin_elementos :: Int -> Bool\n",
    "prop_vacio_sin_elementos x =\n",
    "  not (pertenece x vacio)\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_vacio_sin_elementos\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedad. Los elementos de (inserta x a) son x y los elementos de\n",
    "-- a. \n",
    "prop_elementos_de_inserta :: Int -> Int -> ABB Int -> Bool\n",
    "prop_elementos_de_inserta x y a =\n",
    "  pertenece y (inserta x a) == (x == y) || pertenece y a\n",
    "\n",
    "-- Comprobación.\n",
    "--    ghci> quickCheck prop_elementos_de_inserta\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedades de elimina\n",
    "-- ----------------------\n",
    "\n",
    "-- Propiedad. Si a es un ABB, entonces (elimina v a) también lo es.\n",
    "prop_elimina_es_valida :: Int -> ABB Int -> Bool\n",
    "prop_elimina_es_valida v a = \n",
    "  valido (elimina v a)\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_elimina_es_valida\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Prop. El resultado de eliminar el elemento x en (inserta x a) es\n",
    "-- (elimina x a). \n",
    "prop_elimina_agrega :: Int -> ABB Int -> Bool\n",
    "prop_elimina_agrega x a =\n",
    "  elimina x (inserta x a) == elimina x a\n",
    "\n",
    "-- Comprobación\n",
    "--    ghci> quickCheck prop_elimina_agrega\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedades de crea\n",
    "-- -------------------\n",
    "\n",
    "-- Propiedad. (crea xs) es un ABB.\n",
    "prop_crea_es_valida :: [Int] -> Bool\n",
    "prop_crea_es_valida xs =\n",
    "  valido (crea xs)\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_crea_es_valida\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedades de crea'\n",
    "-- --------------------\n",
    "\n",
    "-- Propiedad. Para todas las listas ordenadas xs, se tiene que (crea' xs)\n",
    "-- es un ABB.\n",
    "prop_crea'_es_valida :: [Int] -> Property\n",
    "prop_crea'_es_valida _ =\n",
    "  forAll listaOrdenada (valido . crea')\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_crea'_es_valida\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedades de elementos\n",
    "-- ------------------------\n",
    "\n",
    "-- Propiedad. (elementos (crea xs)) es igual a la lista xs ordenada y\n",
    "-- sin repeticiones. \n",
    "prop_elementos_crea :: [Int] -> Bool\n",
    "prop_elementos_crea xs =\n",
    "  elementos (crea xs) == sort (nub xs)\n",
    "\n",
    "-- Comprobación\n",
    "--    ghci> quickCheck prop_elementos_crea\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedad. Si ys es una lista ordenada sin repeticiones, entonces\n",
    "-- (elementos (crea' ys)) es igual ys. \n",
    "prop_elementos_crea' :: [Int] -> Bool\n",
    "prop_elementos_crea' xs =\n",
    "  elementos (crea' ys) == ys\n",
    "  where ys = sort (nub xs)\n",
    "\n",
    "-- Comprobación\n",
    "--    ghci> quickCheck prop_elementos_crea'\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedad. Un elemento pertenece a (elementos a) syss es un valor de a.\n",
    "prop_en_elementos :: Int -> ABB Int -> Bool\n",
    "prop_en_elementos v a =\n",
    "    pertenece v a == elem v (elementos a)\n",
    "\n",
    "-- Comprobación:\n",
    "--    ghci> quickCheck prop_enElementos''\n",
    "--    +++ OK, passed 100 tests.\n",
    "\n",
    "-- Propiedades de menor\n",
    "-- --------------------\n",
    "\n",
    "-- Propiedad. (menor a) es menor o igual que todos los elementos de ABB\n",
    "-- a. \n",
    "prop_menoresMinimo ::Int -> ABB Int -> Bool\n",
    "prop_menoresMinimo _ a =\n",
    "  and [menor a <= v | v <- elementos a]\n",
    "\n",
    "-- Comprobación.\n",
    "--    ghci> quickCheck prop_menoresMinimo\n",
    "--    +++ OK, passed 100 tests."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación de las propiedades"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 1 test."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "import Test.QuickCheck\n",
    "quickCheck prop_listaOrdenada_correcta\n",
    "quickCheck prop_orderedList_correcta\n",
    "quickCheck prop_vacio_es_ABB\n",
    "quickCheck prop_inserta_es_valida\n",
    "quickCheck prop_inserta_es_no_vacio\n",
    "quickCheck prop_elemento_de_inserta\n",
    "quickCheck prop_vacio_sin_elementos\n",
    "quickCheck prop_elementos_de_inserta\n",
    "quickCheck prop_elimina_es_valida\n",
    "quickCheck prop_elimina_agrega\n",
    "quickCheck prop_crea_es_valida\n",
    "quickCheck prop_crea'_es_valida\n",
    "quickCheck prop_elementos_crea\n",
    "quickCheck prop_elementos_crea'\n",
    "quickCheck prop_en_elementos\n",
    "quickCheck prop_menoresMinimo\n",
    "quickCheck prop_genABB_correcto"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "> **Nota** Se borran los ficheros de los módulos usados"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": []
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    ":! rm -f *.hs *.hi *.o *.dyn_*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Referencias\n",
    "\n",
    "+ F. Rabhi y G. Lapalme\n",
    "  [Algorithms: A functional programming approach](https://www.iro.umontreal.ca/~lapalme/Algorithms-functional.html)\n",
    "    + Cap. 5.7 Binary search trees."
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Haskell",
   "language": "haskell",
   "name": "haskell"
  },
  "language_info": {
   "codemirror_mode": "ihaskell",
   "file_extension": ".hs",
   "name": "haskell",
   "pygments_lexer": "Haskell",
   "version": "8.6.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}