{"id":4928,"date":"2015-06-01T19:39:45","date_gmt":"2015-06-01T17:39:45","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4928"},"modified":"2015-06-02T19:40:46","modified_gmt":"2015-06-02T17:40:46","slug":"i1m2014-demostracion-de-propiedades-por-induccion-sobre-numeros-y-listas","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/i1m2014-demostracion-de-propiedades-por-induccion-sobre-numeros-y-listas\/","title":{"rendered":"I1M2014: Demostraci\u00f3n de propiedades por inducci\u00f3n sobre n\u00fameros y listas"},"content":{"rendered":"<p>En la primera parte de la clase de hoy de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-14\">Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas<\/a> hemos comentado las soluciones a los ejercicios de la relaci\u00f3n 39 sobre demostraci\u00f3n de propiedades por inducci\u00f3n sobre n\u00fameros y listas<\/p>\n<p>Los ejercicios y su soluci\u00f3n se muestran a continuaci\u00f3n<br \/>\n<!--more--><\/p>\n<pre lang=\"haskell\">\n-- ---------------------------------------------------------------------\n-- Introducci\u00f3n                                                       --\n-- ---------------------------------------------------------------------\n\n-- En esta relaci\u00f3n se plantean ejercicios de demostraci\u00f3n por inducci\u00f3n\n-- de propiedades de programas. La inducci\u00f3n se realiza sobre n\u00fameros\n-- naturales y sobre listas.\n--\n-- Las transparencias del tema correspondiente se encuentran en \n--    http:\/\/www.cs.us.es\/~jalonso\/cursos\/i1m-14\/temas\/tema-8.pdf\n\n-- ---------------------------------------------------------------------\n-- Importaci\u00f3n de librer\u00edas                                           --\n-- ---------------------------------------------------------------------\n\nimport Data.List\nimport Test.QuickCheck\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 1.1. Definir, por recursi\u00f3n, la funci\u00f3n\n--    sumaImpares :: Int -> Int\n-- tal que (sumaImpares n) es la suma de los n primeros n\u00fameros\n-- impares. Por ejemplo,\n--    sumaImpares 5  ==  25\n-- ---------------------------------------------------------------------\n\nsumaImpares :: Int -> Int\nsumaImpares 0 = 0\nsumaImpares n = sumaImpares (n-1) + (2*n-1) \n\n-- ---------------------------------------------------------------------\n-- Ejercicio 1.2. Definir, sin usar recursi\u00f3n, la funci\u00f3n\n--    sumaImpares' :: Int -> Int\n-- tal que (sumaImpares' n) es la suma de los n primeros n\u00fameros\n-- impares. Por ejemplo,\n--    sumaImpares' 5  ==  25\n-- ---------------------------------------------------------------------\n\nsumaImpares' :: Int -> Int\nsumaImpares' n = sum [1,3..2*n-1]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 1.3. Definir la funci\u00f3n\n--    sumaImparesIguales :: Int -> Int -> Bool\n-- tal que (sumaImparesIguales m n) se verifica si para todo x entre m y\n-- n se tiene que (sumaImpares x) y (sumaImpares' x) son iguales.\n-- \n-- Comprobar que (sumaImpares x) y (sumaImpares' x) son iguales para\n-- todos los n\u00fameros x entre 1 y 100.\n-- ---------------------------------------------------------------------\n\n-- La definici\u00f3n es\nsumaImparesIguales :: Int -> Int -> Bool\nsumaImparesIguales m n = \n    and [sumaImpares x == sumaImpares' x | x <- [m..n]]\n\n-- La comprobaci\u00f3n es\n--    ghci> sumaImparesIguales 1 100\n--    True\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 1.4. Definir la funci\u00f3n \n--    grafoSumaImpares :: Int -> Int -> [(Int,Int)]\n-- tal que (grafoSumaImpares m n) es la lista formadas por los n\u00fameros x\n-- entre m y n y los valores de (sumaImpares x).\n--\n-- Calcular (grafoSumaImpares 1 9).\n-- ---------------------------------------------------------------------\n\n-- La definici\u00f3n es\ngrafoSumaImpares :: Int -> Int -> [(Int,Int)]\ngrafoSumaImpares m n =\n    [(x,sumaImpares x) | x <- [m..n]]\n\n-- El c\u00e1lculo es\n--    ghci> grafoSumaImpares 1 9\n--    [(1,1),(2,4),(3,9),(4,16),(5,25),(6,36),(7,49),(8,64),(9,81)]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 1e. Demostrar por inducci\u00f3n que para todo n, \n-- (sumaImpares n) es igual a n^2.\n-- ---------------------------------------------------------------------\n\n{-\n Caso base: Hay que demostrar que\n    sumaImpares 0 = 0^2 \n En efecto,\n    sumaImpares 0   [por hip\u00f3tesis]  \n    = 0               [por sumaImpares.1]\n    = 0^2             [por aritm\u00e9tica]\n \n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n (H.I.)\n     sumaImpares n = n^2\n  Hay que demostrar que\n     sumaImpares (n+1) = (n+1)^2\n  En efecto,\n     sumaImpares (n+1) = \n     = (sumaImpares n) + (2*n+1    )    [por sumaImpares.2]\n     = n^2 + (2*n+1)                    [por H.I.]\n     = (n+1)^2                          [por \u00e1lgebra]\n-} \n\n-- ---------------------------------------------------------------------\n-- Ejercicio 2.1. Definir, por recursi\u00f3n, la funci\u00f3n\n--    sumaPotenciasDeDosMasUno :: Int -> Int\n-- tal que \n--    (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. \n-- Por ejemplo, \n--    sumaPotenciasDeDosMasUno 3  ==  16\n-- ---------------------------------------------------------------------\n\nsumaPotenciasDeDosMasUno :: Int -> Int\nsumaPotenciasDeDosMasUno 0 = 2\nsumaPotenciasDeDosMasUno n = sumaPotenciasDeDosMasUno (n-1) + 2^n\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 2.2. Definir, por comprensi\u00f3n, la funci\u00f3n\n--    sumaPotenciasDeDosMasUno' :: Int -> Int\n-- tal que \n--    (sumaPotenciasDeDosMasUno' n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. \n-- Por ejemplo, \n--    sumaPotenciasDeDosMasUno' 3  ==  16\n-- ---------------------------------------------------------------------\n\nsumaPotenciasDeDosMasUno' :: Int -> Int\nsumaPotenciasDeDosMasUno' n = 1 + sum [2^x | x <- [0..n]]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 2.3. Demostrar por inducci\u00f3n que\n--    sumaPotenciasDeDosMasUno n = 2^(n+1)\n-- ---------------------------------------------------------------------\n\n{-\n  Caso base: Hay que demostrar que \n     sumaPotenciasDeDosMasUno 0 = 2^(0+1)\n  En efecto,\n       sumaPotenciasDeDosMasUno 0 \n     = 2                              [por sumaPotenciasDeDosMasUno.1]\n     = 2^(0+1)                        [por aritm\u00e9tica]\n\n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n (H.I.)\n     sumaPotenciasDeDosMasUno n = 2^(n+1)\n  Hay que demostrar que \n     sumaPotenciasDeDosMasUno (n+1) = 2^((n+1)+1)\n  En efecto, \n       sumaPotenciasDeDosMasUno (n+1)\n     = (sumaPotenciasDeDosMasUno n) + 2^(n+1)  [por sumaPotenciasDeDosMasUno.2]\n     = 2^(n+1) + 2^(n+1)                       [por H.I.]\n     = 2^((n+1)+1)                             [por aritm\u00e9tica]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 3.1. Definir, por recursi\u00f3n, la funci\u00f3n\n--    copia :: Int -> a -> [a]\n-- tal que (copia n x) es la lista formado por n copias del elemento\n-- x. Por ejemplo, \n--    copia 3 2  ==  [2,2,2]\n-- ---------------------------------------------------------------------\n \ncopia :: Int -> a -> [a]\ncopia 0 _ = []                  -- copia.1\ncopia n x = x : copia (n-1) x   -- copia.2\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 3.2. Definir, por recursi\u00f3n, la funci\u00f3n \n--    todos :: (a -> Bool) -> [a] -> Bool\n-- tal que (todos p xs) se verifica si todos los elementos de xs cumplen\n-- la propiedad p. Por ejemplo,\n--    todos even [2,6,4]  ==  True\n--    todos even [2,5,4]  ==  False\n-- ---------------------------------------------------------------------\n\ntodos :: (a -> Bool) -> [a] -> Bool\ntodos p []       = True                -- todos.1\ntodos p (x : xs) = p x && todos p xs   -- todos.2\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 3.3. Comprobar con QuickCheck que todos los elementos de \n-- (copia n x) son iguales a x.\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_copia :: Eq a => Int -> a -> Bool\nprop_copia n x =\n    todos (==x) (copia n' x)\n    where n' = abs n\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_copia\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 3.4. Demostrar, por inducci\u00f3n en n, que todos los elementos\n-- de (copia n x) son iguales a x.\n-- ---------------------------------------------------------------------\n\n{-\n  Hay que demostrar que para todo n y todo x,\n     todos (==x) (copia n x)\n\n  Caso base: Hay que demostrar que\n     todos (==x) (copia 0 x) = True \n  En efecto, \n       todos (== x) (copia 0 x)\n     = todos (== x) []            [por copia.1] \n     = True                       [por todos.1] \n\n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n (H.I.)\n     todos (==x) (copia n x) = True\n  Hay que demostrar que\n     todos (==x) (copia (n+1) x) = True\n  En efecto, \n       todos (==x) (copia (n+1) x)\n     = todos (==x) (x : copia n x )         [por copia.2]\n     = x == x && todos (==x) (copia n x )   [por todos.2] \n     = True && todos (==x) (copia n x )     [por def. de ==] \n     = todos (==x) (copia n x )             [por def. de &&] \n     = True                                 [por H.I.]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 3.5. Definir, por plegado, la funci\u00f3n \n--    todos' :: (a -> Bool) -> [a] -> Bool\n-- tal que (todos' p xs) se verifica si todos los elementos de xs cumplen\n-- la propiedad p. Por ejemplo,\n--    todos' even [2,6,4]  ==>  True\n--    todos' even [2,5,4]  ==>  False\n-- ---------------------------------------------------------------------\n\ntodos' :: (a -> Bool) -> [a] -> Bool\ntodos' p = foldr ((&&) . p) True \n\n-- ---------------------------------------------------------------------\n-- Ejercicio 5.1. Definir, por recursi\u00f3n, la funci\u00f3n \n--   factR :: Integer -> Integer\n-- tal que (factR n) es el factorial de n. Por ejemplo,\n--   factR 4  ==  24\n-- ---------------------------------------------------------------------\n\nfactR :: Integer -> Integer\nfactR 0 = 1\nfactR n = n * factR (n-1)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 5.2. Definir, por comprensi\u00f3n, la funci\u00f3n \n--   factC :: Integer -> Integer\n-- tal que (factR n) es el factorial de n. Por ejemplo,\n--   factC 4  ==  24\n-- ---------------------------------------------------------------------\n\nfactC :: Integer -> Integer\nfactC n = product [1..n]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 1.3. Comprobar con QuickCheck que las funciones factR y\n-- factC son equivalentes sobre los n\u00fameros naturales.\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_factR_factC :: Integer -> Bool\nprop_factR_factC n = \n    factR n' == factC n'\n    where n' = abs n\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_factR_factC\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 5.4. Comprobar con QuickCheck si las funciones factR y\n-- factC son equivalentes sobre los n\u00fameros enteros.\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_factR_factC_Int :: Integer -> Bool\nprop_factR_factC_Int n = \n    factR n == factC n\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_factR_factC_Int\n--    *** Exception: Non-exhaustive patterns in function factR\n\n-- No son iguales ya que factR no est\u00e1 definida para los n\u00fameros\n-- negativos y factC de cualquier n\u00famero negativo es 0.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 5.5. Se considera la siguiente definici\u00f3n iterativa de la\n-- funci\u00f3n factorial \n--    factI :: Integer -> Integer\n--    factI n = factI' n 1\n--    \n--    factI' :: Integer -> Integer -> Integer\n--    factI' 0 x = x                  -- factI'.1\n--    factI' n x = factI' (n-1) n*x   -- factI'.2\n-- Comprobar con QuickCheck que factI y factR son equivalentes sobre los\n-- n\u00fameros naturales.\n-- ---------------------------------------------------------------------\n\nfactI :: Integer -> Integer\nfactI n = factI' n 1\n\nfactI' :: Integer -> Integer -> Integer\nfactI' 0 x = x\nfactI' n x = factI' (n-1) n*x \n\n-- La propiedad es\nprop_factI_factR n = \n    factI n' == factR n'\n    where n' = abs n\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_factI_factR\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 5.6. Comprobar con QuickCheck que para todo n\u00famero natural\n-- n, (factI' n x) es igual al producto de x y (factR n).\n-- --------------------------------------------------------------------- \n\n-- La propiedad es\nprop_factI' :: Integer -> Integer -> Bool\nprop_factI' n  x =\n    factI' n' x == x * factR n'\n    where n' = abs n\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_factI'\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 5.7. Demostrar por inducci\u00f3n que para todo n\u00famero natural\n-- n, (factI' n x) es igual x*n!\n-- --------------------------------------------------------------------- \n\n{-\n  Demostraci\u00f3n (por inducci\u00f3n en n)\n\n  Caso base: Hay que demostrar que factI' 0 x = x*0!\n  En efecto,\n     factI' 0 x \n     = x           [por factI'.1]\n     = x*0!        [por \u00e1lgebra]\n\n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n: para todo x,\n     factI' n x = x*n!\n  hay que demostrar que para todo x\n     factI' (n+1) x = x*(n+1)!\n  En efecto,\n     factI' (n+1) x\n     = factI' n (n+1)*x    [por factI'.2]\n     = (n+1)*x*n!          [por hip\u00f3tesis de inducci\u00f3n]\n     = x*(n+1)!            [por \u00e1lgebra]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 6.1. Definir, recursivamente y sin usar (++). la funci\u00f3n\n--    amplia :: [a] -> a -> [a]\n-- tal que (amplia xs y) es la lista obtenida a\u00f1adiendo el elemento y al\n-- final de la lista xs. Por ejemplo,\n--    amplia [2,5] 3  ==  [2,5,3]\n-- ---------------------------------------------------------------------\n\namplia :: [a] -> a -> [a]\namplia []     y = [y]               -- amplia.1\namplia (x:xs) y = x : amplia xs y   -- amplia.2\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 6.2. Definir, mediante plegado. la funci\u00f3n\n--    ampliaF :: [a] -> a -> [a]\n-- tal que (ampliaF xs y) es la lista obtenida a\u00f1adiendo el elemento y al\n-- final de la lista xs. Por ejemplo,\n--    ampliaF [2,5] 3  ==  [2,5,3]\n-- ---------------------------------------------------------------------\n\nampliaF :: [a] -> a -> [a]\nampliaF xs y = foldr (:) [y] xs\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 6.3. Comprobar con QuickCheck que amplia y ampliaF son\n-- equivalentes. \n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_amplia_ampliaF :: Eq a => [a] -> a -> Bool\nprop_amplia_ampliaF xs y =\n    amplia xs y == ampliaF xs y\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_amplia_ampliaF\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 6.4. Comprobar con QuickCheck que\n--    amplia xs y = xs ++ [y]\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_amplia :: Eq a => [a] -> a -> Bool\nprop_amplia xs y =\n    amplia xs y == xs ++ [y]\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_amplia\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 6.5. Demostrar por inducci\u00f3n que\n--    amplia xs y = xs ++ [y]\n-- ---------------------------------------------------------------------\n\n{-\n  Demostraci\u00f3n: Por inducci\u00f3n en xs.\n\n  Caso base: Hay que demostrar que \n     amplia [] y = [] ++ [y]\n  En efecto,\n     amplia [] y \n     = [y]         [por amplia.1]\n     = [] ++ [y]   [por (++).1]\n\n  Caso inductivo: Se supone la hip\u00f3tesis de inducci\u00f3n\n     amplia xs y = xs ++ [y]\n  Hay que demostrar que\n     amplia (x:xs) y = (x:xs) ++ [y]\n  En efecto,\n     amplia (x:xs) y\n     = x : amplia xs y    [por amplia.2]\n     = x : (xs ++ [y])    [por hip\u00f3tesis de inducci\u00f3n]\n     = (x:xs) ++ [y]      [por (++).2]\n-}\n\n-- ----------------------------------------------------------------------\n-- Ejercicio 7.1. Definir la funci\u00f3n \n--    listaConSuma :: Int -> [[Int]] \n-- que, dado un n\u00famero natural n, devuelve todas las listas de enteros\n-- positivos (esto es, enteros mayores o iguales que 1) cuya suma sea\n-- n. Por ejemplo,\n--    Main> listaConSuma 4\n--    [[1,1,1,1],[1,1,2],[1,2,1],[1,3],[2,1,1],[2,2],[3,1],[4]]\n-- ---------------------------------------------------------------------\n\nlistaConSuma :: Int -> [[Int]]\nlistaConSuma 0 = [[]]\nlistaConSuma n = [x:xs | x <- [1..n], xs <- listaConSuma (n-x)]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 7.2. Definir la funci\u00f3n\n--    numeroDeListasConSuma :: Int -> Int\n-- tal que (numeroDeListasConSuma n) es el n\u00famero de elementos de\n-- (listaConSuma n). Por ejemplo,\n--    numeroDeListasConSuma 10  =  512\n-- ---------------------------------------------------------------------\n\nnumeroDeListasConSuma :: Int -> Int\nnumeroDeListasConSuma = length . listaConSuma\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 7.3. Definir la constante\n--    numerosDeListasConSuma :: [(Int,Int)]\n-- tal que numerosDeListasConSuma es la lista de los pares formado por un\n-- n\u00famero natural n mayor que 0 y el n\u00famero de elementos de \n-- (listaConSuma n). \n--\n-- Calcular el valor de\n--    take 10 numerosDeListasConSuma\n-- ---------------------------------------------------------------------\n\n-- La constante es\nnumerosDeListasConSuma :: [(Int,Int)]\nnumerosDeListasConSuma = [(n,numeroDeListasConSuma n) | n <- [1..]] \n\n-- El c\u00e1lculo es\n--    ghci> take 10 numerosDeListasConSuma\n--    [(1,1),(2,2),(3,4),(4,8),(5,16),(6,32),(7,64),(8,128),(9,256),(10,512)]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 7.4. A partir del ejercicio anterior, encontrar una f\u00f3rmula\n-- para calcular el valor de (numeroDeListasConSuma n) paras los\n-- n\u00fameros n mayores que 0. \n-- \n-- Demostrar dicha f\u00f3rmula por inducci\u00f3n fuerte.\n-- ---------------------------------------------------------------------\n\n{-\n La f\u00f3rmula es\n    numeroDeListasConSuma n = 2^(n-1)\n La demostraci\u00f3n, por inducci\u00f3n fuerte en n, es la siguiente:\n\n Caso base (n=1):\n    numeroDeListasConSuma 1 \n    = length (listaConSuma 1)    \n         [por numeroDeListasConSuma]\n    = length [[x:xs | x <- [1..1], xs <- listaConSuma [[]]]\n         [por listaConSuma.2]\n    = length [[1]]\n         [por def. de listas de comprensi\u00f3n]\n    = 1\n         [por def. de length] \n    = 2^(1-1)\n         [por aritm\u00e9tica] \n\n Paso de inducci\u00f3n: Se supone que\n    para todo x en [1..n-1], \n       numeroDeListasConSuma x = 2^(x-1)\n Hay que demostrar que\n    numeroDeListasConSuma n = 2^(n-1)\n En efecto,\n    numeroDeListasConSuma n\n    = length (listaConSuma n)   \n         [por numeroDeListasConSuma]\n    = length [x:xs | x <- [1..n], xs <- listaConSuma (n-x)]\n         [por listaConSuma.2]\n    = sum [numeroDeListasConSuma (n-x) | x <- [1..n]]\n         [por length y listas de comprensi\u00f3n]\n    = sum [2^(n-x-1) | x <- [1..n-1]] + 1\n         [por hip. de inducci\u00f3n y numeroDeListasConSuma]\n    = 2^(n-2) + 2^(n-3) + ... + 2^1 + 2^0 + 1\n    = 2^(n-1)\n         [por el ejercicio 2c de la relaci\u00f3n 15]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 7.5. A partir del ejercicio anterior, definir de manera m\u00e1s\n-- eficiente la funci\u00f3n numeroDeListasConSuma.\n-- ---------------------------------------------------------------------\n\nnumeroDeListasConSuma' :: Int -> Int\nnumeroDeListasConSuma' 0 = 1\nnumeroDeListasConSuma' n = 2^(n-1)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 7.6. Comparar la eficiencia de las dos definiciones\n-- comparando el tiempo y el espacio usado para calcular \n-- (numeroDeListasConSuma 20) y (numeroDeListasConSuma' 20).\n-- ---------------------------------------------------------------------\n\n-- La comparaci\u00f3n es\n--    ghci> :set +s\n--    ghci> numeroDeListasConSuma 20\n--    524288\n--    (9.99 secs, 519419824 bytes)\n--    ghci> numeroDeListasConSuma' 20\n--    524288\n--    (0.01 secs, 0 bytes)\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8.0. La sucesi\u00f3n de Fibonacci \n--    0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, ...\n-- puede definirse por recursi\u00f3n como\n--    fib :: Int -> Int\n--    fib 0     = 0                      -- fib.1\n--    fib 1     = 1                      -- fib.2\n--    fib (n+2) = (fib (n+1)) + fib n    -- fib.3\n-- Tambi\u00e9n puede definirse por recursici\u00f3n iterativa como\n--    fibIt :: Int -> Int\n--    fibIt n = fibItAux n 0 1\n-- donde la funci\u00f3n auxiliar se define por\n--    fibItAux :: Int -> Int -> Int -> Int\n--    fibItAux 0     a b = a                    -- fibItAux.1\n--    fibItAux (n+1) a b = fibItAux n b (a+b)   -- fibItAux.2 \n-- ---------------------------------------------------------------------\n\nfib :: Int -> Int\nfib 0 = 0\nfib 1 = 1\nfib n = fib (n-1) + fib (n-2) \n\nfibIt :: Int -> Int\nfibIt n = fibItAux n 0 1\n\nfibItAux :: Int -> Int -> Int -> Int\nfibItAux 0 a b = a\nfibItAux n a b = fibItAux (n-1) b (a+b) \n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8.1. Comprobar con QuickCheck que para todo n\u00famero natural\n-- n tal que n <= 20, se tiene que\n--    fib n = fibIt n\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_fib :: Int -> Property\nprop_fib n =\n    n >= 0 && n <= 20 ==> fib n == fibIt n\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_fib\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8.2. Sea f la funci\u00f3n definida por\n--    f :: Int -> Int -> Int\n--    f n k = fibItAux n (fib k) (fib (k+1))\n-- Definir la funci\u00f3n \n--    grafoDeF :: Int -> [(Int,Int)]\n-- tal que (grafoDeF n) es la lista de los pares formados por un n\u00famero\n-- natural k y el valor de (f n k), para k >= 1. Por ejemplo,\n--    ghci> take 7 (grafoDeF 3)\n--    [(1,3),(2,5),(3,8),(4,13),(5,21),(6,34),(7,55)]\n--    ghci> take 7 (grafoDeF 5)\n--    [(1,8),(2,13),(3,21),(4,34),(5,55),(6,89),(7,144)]\n-- ---------------------------------------------------------------------\n\nf :: Int -> Int -> Int\nf n k = fibItAux n (fib k) (fib (k+1))\n\ngrafoDeF :: Int -> [(Int,Int)]\ngrafoDeF n = [(k, f n k) | k <- [1..]]\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8.3. Comprobar con QuickCheck que para todo par de n\u00fameros\n-- naturales n, k tales que n+k <= 20, se tiene que\n--    fibItAux n (fib k) (fib (k+1)) = fib (k+n)\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_fibItAux :: Int -> Int -> Property\nprop_fibItAux n k =\n    n >= 0 && k >= 0 && n+k <= 20 ==>\n    fibItAux n (fib k) (fib (k+1)) == fib (k+n)\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_fibItAux\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8.4. Demostrar por inducci\u00f3n que para todo n y todo k,\n--    fibItAux n (fib k) (fib (k+1)) = fib (k+n)\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n: Por inducci\u00f3n en n se prueba que\n    para todo k, fibItAux n (fib k) (fib (k+1)) = fib (k+n)\n\n Caso base (n=0): Hay que demostrar que\n    para todo k, fibItAux 0 (fib k) (fib (k+1)) = fib k\n En efecto, sea k un n\u00famero natural. Se tiene\n    fibItAux 0 (fib k) (fib (k+1))\n    = fib k                          [por fibItAux.1]\n\n Paso de inducci\u00f3n: Se supone la hip\u00f3tesis de inducci\u00f3n\n    para todo k, fibItAux n (fib k) (fib (k+1)) = fib (k+n)\n Hay que demostrar que\n    para todo k, fibItAux (n+1) (fib k) (fib (k+1)) = fib (k+n+1)\n En efecto. Sea k un n\u00famero natural,\n    fibItAux (n+1) (fib k) (fib (k+1))\n    = fibItAux n (fib (k+1)) ((fib k) + (fib (k+1)))\n         [por fibItAux.2]\n    = fibItAux n (fib (k+1)) (fib (k+2))\n         [por fib.3]\n    = fib (n+k+1)\n         [por hip\u00f3tesis de inducci\u00f3n]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8.5. Demostrar que para todo n,\n--    fibIt n = fib n\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n\n    fibIt n \n    = fibItAux n 0 1               [por fibIt]\n    = fibItAux n (fib 0) (fib 1)   [por fib.1 y fib.2]\n    = fib n                        [por ejercicio 8.4]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8.1. La funci\u00f3n potencia puede definirse por\n--    potencia :: Int -> Int -> Int\n--    potencia x 0 = 1\n--    potencia x n | even n    = potencia (x*x) (div n 2)\n--                 | otherwise = x * potencia (x*x) (div n 2)\n-- Comprobar con QuickCheck que para todo n\u00famero natural n y todo\n-- n\u00famero entero x, (potencia x n) es x^n.\n-- ---------------------------------------------------------------------\n\npotencia :: Integer -> Integer -> Integer\npotencia x 0 = 1\npotencia x n | even n    = potencia (x*x) (div n 2)\n             | otherwise = x * potencia (x*x) (div n 2)\n\n-- La propiedad es\nprop_potencia :: Integer -> Integer -> Property\nprop_potencia x n =\n    n >= 0 ==> potencia x n == x^n\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_potencia\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 8.2. Demostrar por inducci\u00f3n que que para todo n\u00famero\n-- natural n y todo n\u00famero entero x, (potencia x n) es x^n\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n: Por inducci\u00f3n en n.\n\n Caso base: Hay que demostrar que \n    para todo x, potencia x 0 = 2^0\n Sea x un n\u00famero entero, entonces\n    potencia x 0 \n    = 1              [por potencia.1]\n    = 2^0            [por aritm\u00e9tica]\n\n Paso de inducci\u00f3n: Se supone que n>0 y la hip\u00f3tesis de inducci\u00f3n: \n    para todo m<n y para todo x, potencia x (n-1) = x^(n-1)\n Tenemos que demostrar que \n    para todo x, potencia x n = x^n\n Lo haremos distinguiendo casos seg\u00fan la paridad de n.\n\n Caso 1: Supongamos que n es par. Entonces, existe un k tal que \n    n = 2*k.                    (1)\n Por tanto, \n    potencia  n \n    = potencia (x*x) (div n 2)  [por potencia.2]\n    = potencia (x*x) k          [por (1)]\n    = (x*x)^k                   [por hip. de inducci\u00f3n]\n    = x^(2*k)                   [por aritm\u00e9tica]\n    = x^n                       [por (1)]\n\n Caso 2: Supongamos que n es impar. Entonces, existe un k tal que \n    n = 2*k+1.                       (2)\n Por tanto, \n    potencia  n \n    = x * potencia (x*x) (div n 2)   [por potencia.3]\n    = x * potencia (x*x) k           [por (1)]\n    = x * (x*x)^k                    [por hip. de inducci\u00f3n]\n    = x^(2*k+1)                      [por aritm\u00e9tica]\n    = x^n                            [por (1)]\n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 9.1. Comprobar con QuickCheck que para todo par de listas\n-- xs, ys se tiene que\n--    reverse (xs ++ ys) == reverse ys ++ reverse xs\n-- ---------------------------------------------------------------------\n\n-- La propiedad es\nprop_reverse_conc :: [Int] -> [Int] -> Bool\nprop_reverse_conc xs ys =\n    reverse (xs ++ ys) == reverse ys ++ reverse xs\n\n-- La comprobaci\u00f3n es\n--    ghci> quickCheck prop_reverse_conc\n--    OK, passed 100 tests.\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 9.2. Demostrar por inducci\u00f3n que para todo par de listas\n-- xs, ys se tiene que\n--    reverse (xs ++ ys) == reverse ys ++ reverse xs\n-- \n-- Las definiciones de reverse y (++) son\n--    reverse [] = []                      -- reverse.1\n--    reverse (x:xs) = reverse xs ++ [x]   -- reverse.2\n-- \n--    [] ++ ys     = ys                    -- ++.1\n--    (x:xs) ++ ys = x : (xs ++ ys)        -- ++.2\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n por inducci\u00f3n en xs.\n\n Caso base: Hay que demostrar que para toda ys,\n    reverse ([] ++ ys) == reverse ys ++ reverse []\n En efecto,\n    reverse ([] ++ ys)\n    = reverse ys                  [por ++.1] \n    = reverse ys ++ []            [por propiedad de ++]\n    = reverse ys ++ reverse []    [por reverse.1]\n\n Paso de inducci\u00f3n: Se supone que para todo ys,\n    reverse (xs ++ ys) == reverse ys ++ reverse xs\n Hay que demostrar que para todo ys,   \n    reverse ((x:xs) ++ ys) == reverse ys ++ reverse (x:xs)\n En efecto,\n    reverse ((x:xs) ++ ys)\n    = reverse (x:(xs ++ ys))               [por ++.2]\n    = reverse (xs ++ ys) ++ [x]            [por reverse.2]\n    = (reverse ys ++ reverse xs) ++ [x]    [por hip. de inducci\u00f3n]\n    = reverse ys ++ (reverse xs ++ [x])    [por asociativa de ++]\n    = reverse ys ++ reverse (x:xs)         [por reverse.2]  \n-}\n\n-- ---------------------------------------------------------------------\n-- Ejercicio 9.3. Demostrar por inducci\u00f3n que para toda lista xs,\n--    reverse (reverse xs) = xs\n-- ---------------------------------------------------------------------\n\n{-\n Demostraci\u00f3n por inducci\u00f3n en xs.\n\n Caso Base: Hay que demostrar que \n    reverse (reverse []) = []\n En efecto, \n    reverse (reverse [])\n    = reverse []           [por reverse.1]\n    = []                   [por reverse.1]\n\n Paso de inducci\u00f3n: Se supone que\n    reverse (reverse xs) = xs\n Hay que demostrar que\n    reverse (reverse (x:xs)) = x:xs\n En efecto,\n    reverse (reverse (x:xs))\n    = reverse (reverse xs ++ [x])           [por reverse.2]\n    = reverse [x] ++ reverse (reverse xs)   [por ejercicio 9.2]\n    = [x] ++ reverse (reverse xs)           [por reverse]\n    = [x] ++ xs                             [por hip. de inducci\u00f3n]\n    = x:xs                                  [por ++.2]\n-}\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy de Inform\u00e1tica de 1\u00ba del Grado en Matem\u00e1ticas hemos comentado las soluciones a los ejercicios de la relaci\u00f3n 39 sobre demostraci\u00f3n de propiedades por inducci\u00f3n sobre n\u00fameros y listas Los ejercicios y su soluci\u00f3n se muestran a continuaci\u00f3n<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[270,305,126],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4928"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4928"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4928\/revisions"}],"predecessor-version":[{"id":4929,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4928\/revisions\/4929"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4928"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4928"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4928"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}