{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "<span style=\"font-size:2em; color:blue\">\n",
    "    Tema 8: Razonamiento sobre programas\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, 4 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-08.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": [
    "**Librería auxiliares**\n",
    "\n",
    "+ En este tema se usarán las siguientes librerías:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "import Test.QuickCheck\n",
    "import Test.QuickCheck.Function"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Razonamiento ecuacional"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Cálculo con longitud\n",
    "\n",
    "+ Programa:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "longitud []     = 0                 -- longitud.1\n",
    "longitud (_:xs) = 1 + longitud xs   -- longitud.2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Propiedad: `longitud [2,3,1] = 3`\n",
    "\n",
    "+ Demostración:\n",
    "\n",
    "```sesion\n",
    "longitud [2,3,1]\n",
    "= 1 + longitud [2,3]          [por longitud.2]\n",
    "= 1 + (1 + longitud [3])      [por longitud.2]\n",
    "= 1 + (1 + (1 + longitud [])) [por longitud.2]\n",
    "= 1 + (1 + (1 + 0)            [por longitud.1]\n",
    "= 3\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Propiedad de intercambia\n",
    "\n",
    "+ Programa:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "intercambia :: (a,b) -> (b,a)\n",
    "intercambia (x,y) = (y,x)       -- intercambia"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Propiedad:\n",
    "\n",
    "```sesion\n",
    "intercambia (intercambia (x,y)) = (x,y)\n",
    "```\n",
    "\n",
    "+ Demostración:\n",
    "\n",
    "```sesion\n",
    "intercambia (intercambia (x,y))\n",
    "= intercambia (y,x)      [por intercambia] \n",
    "= (x,y)                  [por intercambia]\n",
    "```\n",
    "\n",
    "+ Propiedad en QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_intercambia :: Eq a => a -> a -> Bool\n",
    "prop_intercambia x y = \n",
    "    intercambia (intercambia (x,y)) == (x,y)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_intercambia"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Inversa de listas unitarias\n",
    "\n",
    "+ Inversa de una lista:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [],
   "source": [
    "inversa :: [a] -> [a]\n",
    "inversa []     = []                  -- inversa.1\n",
    "inversa (x:xs) = inversa xs ++ [x]   -- inversa.2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Prop.: `inversa [x] = [x]`\n",
    "\n",
    "```sesion\n",
    "inversa [x] \n",
    "= inversa (x:[])      [notación de lista] \n",
    "= (inversa []) ++ [x] [inversa.2] \n",
    "= [] ++ [x]           [inversa.1] \n",
    "= [x]                 [def. de ++] \n",
    "```\n",
    "\n",
    "+ Propiedad en QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_inversa_unitaria :: Eq a => a -> Bool\n",
    "prop_inversa_unitaria x =\n",
    "    inversa [x] == [x]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_inversa_unitaria"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Razonamiento ecuacional con análisis de casos\n",
    "\n",
    "+ Negación lógica:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "not :: Bool -> Bool\n",
    "not False = True\n",
    "not True  = False"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Prop.: `not (not x) = x`\n",
    "\n",
    "+ Demostración por casos: Caso 1: `x = True`:\n",
    "\n",
    "```sesion\n",
    "not (not True) \n",
    "= not False      [not.2] \n",
    "= True           [not.1]\n",
    "```\n",
    "\n",
    "+ Demostración por casos: Caso 2: `x = False`:\n",
    "\n",
    "```sesion\n",
    "not (not False) \n",
    "= not True      [not.1] \n",
    "= False         [not.2]  \n",
    "```\n",
    "\n",
    "+ Propiedad con QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_doble_negacion :: Bool -> Bool\n",
    "prop_doble_negacion x =\n",
    "  not (not x) == x"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_doble_negacion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Razonamiento por inducción sobre los naturales"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Esquema de inducción sobre los naturales \n",
    "\n",
    "Para demostrar que todos los números naturales tienen una propiedad `P`\n",
    "basta probar:\n",
    "\n",
    "+ Caso base `n=0`:  `P(0)`.\n",
    "+ Caso inductivo `n=(m+1)`:   Suponiendo `P(m)` demostrar `P(m+1)`.\n",
    "\n",
    "En el caso inductivo, la propiedad `P(n)` se llama la hipótesis de inducción."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Ejemplo de inducción sobre los naturales\n",
    "\n",
    "+ `(replicate n x)` es la lista formda por `n` elementos iguales a `x`. Por\n",
    "  ejemplo,\n",
    "\n",
    "```sesion\n",
    "replicate 3 5  ==  [5,5,5]  \n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [],
   "source": [
    "replicate :: Int -> a -> [a]\n",
    "replicate 0 _ = []\n",
    "replicate n x = x : replicate (n-1) x"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[5,5,5]"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "replicate 3 5"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Prop.: `length (replicate n x) = n`\n",
    "\n",
    "\n",
    "+ Demostracion del caso base (`n=0`):\n",
    "\n",
    "```sesion\n",
    "length (replicate 0 x) \n",
    "= length []            [por replicate.1]\n",
    "= 0                    [por def. length]\n",
    "```\n",
    "\n",
    "+ Demostración del caso inductivo (`n=m+1`):\n",
    "\n",
    "```sesion\n",
    "length (replicate (m+1) x) \n",
    "= length (x:(replicate m x))  [por replicate.2] \n",
    "= 1 + length (replicate m x)  [por def. length] \n",
    "= 1 + m                       [por hip. ind.] \n",
    "= m + 1                       [por conmutativa de +]\n",
    "```\n",
    "\n",
    "+ Especificación de la propiedad en QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_length_replicate :: Int -> Int -> Bool\n",
    "prop_length_replicate n xs =\n",
    "    length (replicate m xs) == m\n",
    "    where m = abs n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación de la propiedad:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_length_replicate"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Razonamiento por inducción sobre listas"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Esquema de inducción sobre listas \n",
    "\n",
    "Para demostrar que todas las listas finitas tienen una propiedad `P` basta\n",
    "probar:\n",
    "\n",
    "+ Caso base `xs=[]`: `P([])`.\n",
    "+ Caso inductivo `xs=(y:ys)`: Suponiendo `P(ys)` demostrar `P(y:ys)`.\n",
    "\n",
    "En el caso inductivo, la propiedad `P(ys)` se llama la hipótesis de inducción."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Asociatividad de ++\n",
    "\n",
    "+ Programa:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [],
   "source": [
    "(++) :: [a] -> [a] -> [a]\n",
    "[]     ++ ys = ys             -- ++.1\n",
    "(x:xs) ++ ys = x : (xs ++ ys) -- ++.2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Propiedad: `xs ++ (ys ++ zs)=(xs ++ ys) ++ zs`\n",
    "\n",
    "+ Especificación con QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_asociativa_conc :: [Int] -> [Int] -> [Int] -> Bool\n",
    "prop_asociativa_conc xs ys zs = \n",
    "    xs ++ (ys ++ zs)==(xs ++ ys) ++ zs"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_asociativa_conc"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Demostración por inducción en `xs`:\n",
    "\n",
    "+ Caso base `xs=[]`: Reduciendo el lado izquierdo\n",
    "\n",
    "```sesion\n",
    "xs ++ (ys ++ zs) \n",
    "= [] ++ (ys ++ zs)   [por hipótesis] \n",
    "= ys ++ zs           [por  ++ .1]\n",
    "= ([] ++ ys) ++ zs   [por  ++ .1]\n",
    "= (xs ++ ys) ++ zs   [por hipótesis] \n",
    "```\n",
    "\n",
    "+ Caso inductivo `xs = a:as`: Suponiendo la hipótesis de inducción  \n",
    "  `as ++ (ys ++ zs) = (as ++ ys) ++ zs`   \n",
    "  hay que demostrar que  \n",
    "  `(a:as) ++ (ys ++ zs) = ((a:as) ++ ys) ++ zs`\n",
    "\n",
    "```sesion\n",
    "(a:as) ++ (ys ++ zs) \n",
    "= a:(as ++ (ys ++ zs))  [por  ++ .2] \n",
    "= a:((as ++ ys) ++ zs)  [por hip. ind.] \n",
    "= (a:(as ++ ys)) ++ zs  [por ++.2] \n",
    "= ((a:as) ++ ys) ++ zs  [por ++.2] \n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## [] es la identidad para ++ por la derecha\n",
    "\n",
    "+ Propiedad: `xs ++ []=xs`\n",
    "\n",
    "+ Especificación con QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_identidad_concatenacion :: [Int] -> Bool\n",
    "prop_identidad_concatenacion xs = xs ++ [] == xs  "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_identidad_concatenacion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Demostración por inducción en `xs`:\n",
    "\n",
    "+ Caso base `xs = []`:\n",
    "\n",
    "```sesion\n",
    "xs ++ [] \n",
    "= [] ++ [] \n",
    "= []         [por ++.1] \n",
    "```\n",
    "\n",
    "+ Caso inductivo `xs = a:as`: Suponiendo la hipótesis de inducción  \n",
    "  `as ++ [] = as`  \n",
    "  hay que demostrar que\n",
    "  `(a:as) ++ []=(a:as)`\n",
    "\n",
    "```sesion\n",
    "(a:as) ++ [] \n",
    "= a:(as ++ [])   [por ++.2] \n",
    "= a:as           [por hip. ind.]\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Relación entre length y ++\n",
    "\n",
    "+ Programas:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [],
   "source": [
    "length :: [a] -> Int\n",
    "length []     = 0               -- length.1\n",
    "length (x:xs) = 1 + length xs   -- length.2\n",
    "\n",
    "(++) :: [a] -> [a] -> [a]\n",
    "[]     ++ ys = ys                 -- ++.1\n",
    "(x:xs) ++ ys = x : (xs ++ ys)     -- ++.2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Propiedad: `length(xs ++ ys) = (length xs)+(length ys)`\n",
    "\n",
    "+ Especificación con QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_length_append :: [Int] -> [Int] -> Bool\n",
    "prop_length_append xs ys = \n",
    "   length(xs ++ ys)==(length xs)+(length ys) "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_length_append"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Demostración por inducción en `xs`:\n",
    "\n",
    "+ Caso base `xs = []`:\n",
    "\n",
    "```sesion\n",
    "length([] ++ ys)\n",
    "= length ys                [por ++.1] \n",
    "= 0+(length ys)            [por aritmética] \n",
    "= (length [])+(length ys)  [por length.1]\n",
    "```\n",
    "\n",
    "+ Caso inductivo `xs = a:as`: Suponiendo la hipótesis de inducción  \n",
    "  `length(as ++ ys) = (length as)+(length ys)`  \n",
    "  hay que demostrar que  \n",
    "  `length((a:as) ++ ys) = (length (a:as))+(length ys)`\n",
    "  \n",
    "```sesion\n",
    "length((a:as) ++ ys)\n",
    "= length(a:(as ++ ys))              [por ++.2] \n",
    "= 1 + length(as ++ ys)              [por length.2] \n",
    "= 1 + ((length as) + (length ys))   [por hip. ind.] \n",
    "= (1 + (length as)) + (length ys)   [por aritmética] \n",
    "= (length (a:as)) + (length ys)     [por length.2]\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Relación entre take y drop\n",
    "\n",
    "+ Programas:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "metadata": {},
   "outputs": [],
   "source": [
    "take :: Int -> [a] -> [a]\n",
    "take 0 _       = []                  -- take.1\n",
    "take _ []      = []                  -- take.2\n",
    "take n (x:xs)  = x : take (n-1) xs   -- take.3\n",
    "\n",
    "drop :: Int -> [a] -> [a]\n",
    "drop 0 xs      = xs                  -- drop.1\n",
    "drop _ []      = []                  -- drop,2\n",
    "drop n (_:xs)  = drop (n-1) xs       -- drop.3\n",
    "\n",
    "(++) :: [a] -> [a] -> [a]\n",
    "[]     ++ ys = ys                    -- ++.1\n",
    "(x:xs) ++ ys = x : (xs ++ ys)        -- ++.2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Propiedad: `take n xs ++ drop n xs = xs`\n",
    "\n",
    "+ Especificación con QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_take_drop :: Int -> [Int] -> Property\n",
    "prop_take_drop n xs = \n",
    "    n >= 0 ==> take n xs ++ drop n xs == xs"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests; 85 discarded."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_take_drop"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Demostración por inducción en `n`:\n",
    "\n",
    "+ Caso base `n = 0`:\n",
    "\n",
    "```sesion\n",
    "take 0 xs ++ drop 0 xs \n",
    "= [] ++ xs              [por take.1 y drop.1] \n",
    "= xs                    [por ++.1]\n",
    "```\n",
    "\n",
    "+ Caso inductivo `n = m+1`: Suponiendo la hipótesis de inducción 1  \n",
    "  $(\\forall xs::[a])$`take m xs ++ drop m xs = xs`  \n",
    "  hay que demostrar que  \n",
    "  $(\\forall xs::[a])$`take (m+1) xs ++ drop (m+1) xs = xs` \n",
    "\n",
    "+ Lo demostraremos por inducción en `xs`:\n",
    "\n",
    "+ Caso base `xs = []`:\n",
    "\n",
    "```sesion\n",
    "take (m+1) [] ++ drop (m+1) [] \n",
    "= [] ++ []                        [por take.2 y drop.2]\n",
    "= []                              [por ++.1]\n",
    "``` \n",
    "\n",
    "+ Caso inductivo `xs = a:as`: Suponiendo la hip. de inducción 2  \n",
    "  `take (m+1) as ++ drop (m+1) as = as`  \n",
    "  hay que demostrar que  \n",
    "  `take (m+1) (a:as) ++ drop (m+1) (a:as) = (a:as)`\n",
    "\n",
    "```sesion\n",
    "take (m+1) (a:as) ++ drop (m+1) (a:as) \n",
    "= (a:(take m as)) ++ (drop m as)     [take.3 y drop.3] \n",
    "= (a:((take m as) ++ (drop m as))    [por ++.2] \n",
    "= a:as                               [por hip. de ind. 1]\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## La concatenación de listas vacías es vacía\n",
    "\n",
    "+ Programas:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [],
   "source": [
    "null :: [a] -> Bool\n",
    "null []           = True            -- null.1\n",
    "null (_:_)        = False           -- null.2\n",
    "\n",
    "(++) :: [a] -> [a] -> [a]\n",
    "[]     ++ ys      = ys              -- (++).1\n",
    "(x:xs) ++ ys      = x : (xs ++ ys)  -- (++).2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Propiedad: `null xs = null (xs ++ xs)`.\n",
    "\n",
    "+ Demostración por inducción en `xs`:\n",
    "\n",
    "+ Caso 1: `xs = []`: Reduciendo ambos lados:\n",
    "\n",
    "```sesion\n",
    "null xs \n",
    "= null []          [por hipótesis] \n",
    "= True             [por null.1] \n",
    "\n",
    "null (xs ++ xs) \n",
    "= null ([] ++ [])  [por hipótesis]\n",
    "= null []          [por (++).1]\n",
    "= True             [por null.1] \n",
    "```\n",
    "\n",
    "\n",
    "+ Caso `xs = y:ys`: Reduciendo ambos lados:\n",
    "\n",
    "```sesion\n",
    "null xs \n",
    "= null (y:ys)              [por hipótesis] \n",
    "= False                    [por null.2\n",
    "\n",
    "null (xs ++ xs) \n",
    "= null ((y:ys) ++ (y:ys))  [por hipótesis]\n",
    "= null (y:(ys ++ (y:ys))   [por (++).2]\n",
    "= False                    [por null.2\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Equivalencia de funciones\n",
    "\n",
    "+ Programas:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [],
   "source": [
    "inversa1, inversa2 :: [a] -> [a]\n",
    "inversa1 []     = []                                      -- inversa1.1\n",
    "inversa1 (x:xs) = inversa1 xs ++ [x]                      -- inversa1.2\n",
    "\n",
    "inversa2 xs = inversa2Aux xs []                           -- inversa2.1\n",
    "    where inversa2Aux []     ys = ys                      -- inversa2Aux.1\n",
    "          inversa2Aux (x:xs) ys = inversa2Aux xs (x:ys)   -- inversa2Aux.2"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Propiedad: `inversa1 xs = inversa2 xs`\n",
    "\n",
    "+ Especificación con QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_equiv_inversa :: [Int] -> Bool\n",
    "prop_equiv_inversa xs = inversa1 xs == inversa2 xs"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_equiv_inversa "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Demostración: Es consecuencia del siguiente lema:  \n",
    "  `inversa1 xs ++ ys = inversa2Aux xs ys`  \n",
    "  En efecto,\n",
    "\n",
    "```sesion\n",
    "inversa1 xs \n",
    "= inversa1 xs ++ []     [por identidad de ++] \n",
    "= inversa2Aux xs ++ []  [por el lema] \n",
    "= inversa2 xs           [por el inversa2.1] \n",
    "```\n",
    "\n",
    "+ Demostración del lema: Por inducción en `xs`:\n",
    "\n",
    "+ Caso base `xs = []`:\n",
    "\n",
    "```sesion\n",
    "inversa1 [] ++ ys\n",
    "= [] ++ ys              [por inversa1.1] \n",
    "= ys                    [por ++.1] \n",
    "= inversa2Aux [] ys     [por inversa2Aux.1]\n",
    "```\n",
    "\n",
    "+ Caso inductivo `xs=(a:as)`: La hipótesis de inducción es  \n",
    "  $(\\forall ys::[a])$`inversa1 as ++ ys = inversa2Aux as ys`  \n",
    "  Por tanto,\n",
    "\n",
    "```sesion\n",
    "inversa1 (a:as) ++ ys\n",
    "= (inversa1 as ++ [a]) ++ ys    [por inversa1.2] \n",
    "= (inversa1 as) ++ ([a] ++ ys)  [por asociativa de ++]\n",
    "= (inversa1 as) ++ (a:ys)       [por ley unitaria] \n",
    "= (inversa2Aux as (a:ys)        [por hip. de inducción] \n",
    "= inversa2Aux (a:as) ys         [por inversa2Aux.2]\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Propiedades de funciones de orden superior\n",
    "\n",
    "**Relación entre sum y map**\n",
    "\n",
    "+ La función `sum`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "metadata": {},
   "outputs": [],
   "source": [
    "sum :: [Int] -> Int\n",
    "sum []     = 0                \n",
    "sum (x:xs) = x + sum xs       "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Propiedad: `sum (map (2*) xs) = 2 * sum xs`\n",
    "\n",
    "+ Especificación con QuickCheck:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_sum_map :: [Int] -> Bool\n",
    "prop_sum_map xs = sum (map (2*) xs) == 2 * sum xs"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_sum_map"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Demostración de la propiedad por inducción en `xs`\n",
    "\n",
    "+ Caso `[]`:\n",
    "\n",
    "```sesion\n",
    "sum (map (2*) xs)  \n",
    "= sum (map (2*) [])  [por hipótesis] \n",
    "= sum []             [por map.1] \n",
    "= 0                  [por sum.1] \n",
    "= 2 * 0              [por aritmética] \n",
    "= 2 * sum []         [por sum.1] \n",
    "= 2 * sum xs         [por hipótesis] \n",
    "```\n",
    "\n",
    "+ Caso `xs = y:ys`: Entonces,\n",
    "\n",
    "```sesion\n",
    "sum (map (2*) xs)  \n",
    "= sum (map (2*) (y:ys))         [por hipótesis]  \n",
    "= sum ((2*) y : (map (2*) ys))  [por map.2]  \n",
    "= (2*) y + (sum (map (2*) ys))  [por sum.2]  \n",
    "= (2*) y + (2 * sum ys)         [por hip. de inducción]  \n",
    "= (2 * y) + (2 * sum ys)        [por (2*)] \n",
    "= 2 * (y + sum ys)              [por aritmética] \n",
    "= 2 * sum (y:ys)                [por sum.2] \n",
    "= 2 * sum xs                    [por hipótesis]\n",
    "```\n",
    "\n",
    "**Comprobación de propiedades con argumentos funcionales**\n",
    "\n",
    "+ La aplicación de una función a los elementos de una lista conserva su\n",
    "  longitud:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 35,
   "metadata": {},
   "outputs": [],
   "source": [
    "prop_map_length (Fun _ f) xs =\n",
    "    length (map f xs) == length xs"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ En el inicio del fichero hay que escribir\n",
    "\n",
    "```haskell\n",
    "import Test.QuickCheck.Function\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "+ Comprobación"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 36,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "+++ OK, passed 100 tests."
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "quickCheck prop_map_length"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Bibliografía\n",
    "\n",
    "+ H.C. Cunningham. *Notes on Functional Programming with Haskell*.\n",
    "\n",
    "+ J. Fokker. *Programación funcional*.\n",
    "\n",
    "+ G. Hutton. *Programming in Haskell*. Cambridge University Press, 2007.\n",
    "    + Cap. 13: Reasoning about programs.\n",
    "\n",
    "+ B.C. Ruiz, F. Gutiérrez, P. Guerrero y J.E. Gallardo. *Razonando con\n",
    "  Haskell*. Thompson, 2004.\n",
    "    + Cap. 6: Programación con listas.\n",
    "\n",
    "+ S. Thompson. *Haskell: The Craft of Functional Programming*, Second\n",
    "  Edition. Addison-Wesley, 1999. \n",
    "    + Cap. 8: Reasoning about programs.\n",
    "\n",
    "+ E.P. Wentworth. *Introduction to funcional programming*."
   ]
  }
 ],
 "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
}