-- I1M 2009-10: Relación 17 (2 de marzo de 2010)
-- Departamento de Ciencias de la Computación e I.A.
-- Universidad de Sevilla
-- =====================================================================

-- ---------------------------------------------------------------------
-- Importación de librerías auxiliares                                --
-- ---------------------------------------------------------------------

import Test.QuickCheck
import Control.Monad

-- ---------------------------------------------------------------------
-- Ejercicio 1. Definir la función
--    palabrasDeLongitud :: Int -> String -> [String]
-- tal que (palabrasDeLongitud n cs) es la lista de las cadenas de
-- longitud n formada con los caracteres de cs. Por ejemplo,
--    *Main> palabrasDeLongitud 3 "ab"
--    ["aaa","aab","aba","abb","baa","bab","bba","bbb"]
-- ---------------------------------------------------------------------

palabrasDeLongitud :: Int -> String -> [String]
palabrasDeLongitud = undefined

-- ----------------------------------------------------------------------
-- Ejercicio 2.1. Definir la función 
--    listaConSuma :: Int -> [[Int]] 
-- que, dado un número natural n, devuelve todas las listas de enteros
-- positivos (esto es, enteros mayores o iguales que 1) cuya suma sea
-- n. Por ejemplo,
--    Main> listaConSuma 4
--    [[1,1,1,1],[1,1,2],[1,2,1],[1,3],[2,1,1],[2,2],[3,1],[4]]
-- ---------------------------------------------------------------------

listaConSuma :: Int -> [[Int]]
listaConSuma = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 2.2. Definir la función
--    numeroDeListasConSuma :: Int -> Int
-- tal que (numeroDeListasConSuma n) es el número de elementos de
-- (listaConSuma n). Por ejemplo,
--    numeroDeListasConSuma 10  =>  512
-- ---------------------------------------------------------------------

numeroDeListasConSuma :: Int -> Int
numeroDeListasConSuma = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 2.2. Definir la constante
--    numerosDeListasConSuma :: [(Int,Int)]
-- tal que numerosDeListasConSuma es la lista de los pares formado por un
-- número natural n mayor que 0 y el número de elementos de 
-- (listaConSuma n). 
--
-- Calcular el valor de
--    take 10 numerosDeListasConSuma
-- ---------------------------------------------------------------------

-- La constante es
numerosDeListasConSuma :: [(Int,Int)]
numerosDeListasConSuma = undefined

-- El cálculo es

-- ---------------------------------------------------------------------
-- Ejercicio 2.4. A partir del ejercicio anterior, encontrar una fórmula
-- para calcular el valor de (numeroDeListasConSuma n) paras los
-- números n mayores que 0. 
-- 
-- Demostrar dicha fórmula por inducción fuerte.
-- ---------------------------------------------------------------------

{-
 La fórmula es
    

 La demostración, por inducción fuerte en n, es la siguiente:
-}

-- ---------------------------------------------------------------------
-- Ejercicio 2.4. A partir del ejercicio anterior, definir de manera más
-- eficiente la función numeroDeListasConSuma.
-- ---------------------------------------------------------------------

numeroDeListasConSuma' :: Int -> Int
numeroDeListasConSuma' = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 2.5. Comparar la eficiencia de las dos definiciones
-- comparando el tiempo y el espacio usado para calcular 
-- (numeroDeListasConSuma 20) y (numeroDeListasConSuma' 20).
-- ---------------------------------------------------------------------

-- La comparación es

-- ---------------------------------------------------------------------
-- Ejercicio 3.1. Definir la función
--    conjetura :: Int -> Bool
-- tal que (conjetura n) se verifica si n^2+n+41 es primo. Por ejemplo,
--    conjetura 20  ==>  True
-- ---------------------------------------------------------------------

conjetura :: Int -> Bool
conjetura n = undefined


-- ---------------------------------------------------------------------
-- Ejercicio 3.2. Definir la función
--    conjeturaHasta :: Int -> Bool
-- tal que (conjeturaHasta n) se verifica si x^2+x+41 es primo para todo
-- los números x de 1 a n. Por ejemplo,
--    conjeturaHasta 20  ==>  True
-- ---------------------------------------------------------------------

conjeturaHasta :: Int -> Bool
conjeturaHasta n = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 3.3. Definir la constante
--    menorContraejemplo :: Int
-- tal que menorContraejemplo es el menor número x tal que x^2+x+41 no
-- es primo.
--
-- Calcular el valor de menorContraejemplo.
-- --------------------------------------------------------------------- 

menorContraejemplo :: Int
menorContraejemplo = undefined

-- La evaluación es

-- ---------------------------------------------------------------------
-- Ejercicio 3.4. Definir la constante
--    menorC :: Int
-- tal que menorC es el c tal que x^2-79*x+c es primo para los m
-- primeros números con m mayor que 40. 
-- 
-- Calcular menorC y el mayor m tal que para todos los x entre 1 y m
-- x^2-79*x+menorC es primo.
-- ---------------------------------------------------------------------

-- La definición es
menorC = undefined

-- El cálculo de menorC es

-- Para calcular el menor m, se define
menorM = undefined

-- El cálculo del menor m es

-- ---------------------------------------------------------------------
-- Ejercicio 4.1. Definir la función
--    menorFactor :: Integer -> Integer
-- tal que (menorFactor n) es el menor factor primo de n. Por ejemplo,
--    menorFactor 15  ==  3
-- ---------------------------------------------------------------------

menorFactor :: Integer -> Integer
menorFactor n = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4.2. Definir la función
--    factorizacion :: Integer -> [Integer]
-- tal que (factorizacion n) es la lista de todos los factores primos
-- de n; es decir, es una lista de números primos cuyo producto es
-- n. Por ejemplo,
--    factorizacion 300  ==  [2,2,3,5,5]
-- ---------------------------------------------------------------------

factorizacion :: Integer -> [Integer]
factorizacion = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 4.3. Comprobar con QuickCheck que para todo número natural
-- n >= 2, todos los elementos de (factorizacion n) son números primos.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_factorizacion_primos :: Integer -> Property
prop_factorizacion_primos n = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 4.4. Comprobar con QuickCheck que para todo número natural
-- n >= 2, el producto de los elementos de (factorizacion n) es n.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_factorizacion_producto :: Integer -> Property
prop_factorizacion_producto n = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 5.0. La sucesión de Fibonacci 
--    0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, ...
-- puede definirse por recursión como
--    fib :: Int -> Int
--    fib 0     = 0                      -- fib.1
--    fib 1     = 1                      -- fib.2
--    fib (n+2) = (fib (n+1)) + fib n    -- fib.3
-- También puede definirse por recursición iterativa como
--    fibIt :: Int -> Int
--    fibIt n = fibItAux n 0 1
-- donde la función auxiliar se define por
--    fibItAux :: Int -> Int -> Int -> Int
--    fibItAux 0     a b = a                    -- fibItAux.1
--    fibItAux (n+1) a b = fibItAux n b (a+b)   -- fibItAux.2 
-- ---------------------------------------------------------------------

fib :: Int -> Int
fib 0     = 0
fib 1     = 1
fib (n+2) = fib (n+1) + fib n 

fibIt :: Int -> Int
fibIt n = fibItAux n 0 1

fibItAux :: Int -> Int -> Int -> Int
fibItAux 0     a b = a
fibItAux (n+1) a b = fibItAux n b (a+b) 

-- ---------------------------------------------------------------------
-- Ejercicio 5.1. Comprobar con QuickCheck que para todo número natural
-- n tal que n <= 20, se tiene que
--    fib n = fibIt n
-- ---------------------------------------------------------------------

-- La propiedad es
prop_fib :: Int -> Property
prop_fib n = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 5.2. Sea f la función definida por
--    f :: Int -> Int -> Int
--    f n k = fibItAux n (fib k) (fib (k+1))
-- Definir la función 
--    grafoDeF :: Int -> [(Int,Int)]
-- tal que (grafoDeF n)
--    *Main> take 7 (grafoDeF 3)
--    [(1,3),(2,5),(3,8),(4,13),(5,21),(6,34),(7,55)]
--    *Main> take 7 (grafoDeF 5)
--    [(1,8),(2,13),(3,21),(4,34),(5,55),(6,89),(7,144)]
-- ---------------------------------------------------------------------

f :: Int -> Int -> Int
f n k = fibItAux n (fib k) (fib (k+1))

grafoDeF :: Int -> [(Int,Int)]
grafoDeF n = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 5.3. Comprobar con QuickCheck que para todo par de números
-- naturales n, k tales que n+k <= 20, se tiene que
--    fibItAux n (fib k) (fib (k+1)) = fib (k+n)
-- ---------------------------------------------------------------------

-- La propiedad es
prop_fibItAux :: Int -> Int -> Property
prop_fibItAux n k = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 5.4. Demostrar por inducción que para todo n y todo k,
--    fibItAux n (fib k) (fib (k+1)) = fib (k+n)
-- ---------------------------------------------------------------------

{-
 Demostración: 
-}

-- ---------------------------------------------------------------------
-- Ejercicio 5.5. Demostrar que para todo n,
--    fibIt n = fib n
-- ---------------------------------------------------------------------

{-
 Demostración:
-}

-- ---------------------------------------------------------------------
-- Ejercicio 6.1. La función potencia puede definirse por
--    potencia :: Int -> Int -> Int
--    potencia x 0 = 1
--    potencia x n | even n    = potencia (x*x) (div n 2)
--                 | otherwise = x * potencia (x*x) (div n 2)
-- Comprobar con QuickCheck que para todo número natural n y todo
-- número entero x, (potencia x n) es x^n.
-- ---------------------------------------------------------------------

potencia :: Integer -> Integer -> Integer
potencia x 0 = 1
potencia x n | even n    = potencia (x*x) (div n 2)
               | otherwise = x * potencia (x*x) (div n 2)

-- La propiedad es
prop_potencia :: Integer -> Integer -> Property
prop_potencia x n = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 6.2. Demostrar por inducción que que para todo número
-- natural n y todo número entero x, (potencia x n) es x^n
-- ---------------------------------------------------------------------

{-
 Demostración:
-}

-- ---------------------------------------------------------------------
-- Ejercicio 7.1. Comprobar con QuickCheck que para todo par de listas
-- xs, ys se tiene que
--    reverse (xs ++ ys) == reverse ys ++ reverse xs
-- ---------------------------------------------------------------------

-- La propiedad es
prop_reverse_conc :: [Int] -> [Int] -> Bool
prop_reverse_conc xs ys = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 7.2. Demostrar por inducción que para todo par de listas
-- xs, ys se tiene que
--    reverse (xs ++ ys) == reverse ys ++ reverse xs
-- 
-- Las definiciones de reverse y (++) son
--    reverse [] = []                      -- reverse.1
--    reverse (x:xs) = reverse xs ++ [x]   -- reverse.2
-- 
--    [] ++ ys     = ys                    -- ++.1
--    (x:xs) ++ ys = x : (xs ++ ys)        -- ++.2
-- ---------------------------------------------------------------------

{-
 Demostración:
-}

-- ---------------------------------------------------------------------
-- Ejercicio 7.3. Demostrar por inducción que para toda lista xs,
--    reverse (reverse xs) = xs
-- ---------------------------------------------------------------------

{-
 Demostración:
-}

-- ---------------------------------------------------------------------
-- Ejercicio 8.0. En los siguientes ejercicios se demostrarán
-- propiedades de los árboles binarios definidos como sigue
--    data Arbol a = Hoja 
--                 | Nodo a (Arbol a) (Arbol a)
--                 deriving (Show, Eq)
-- En los ejemplos se usaráel siguiente árbol
--    arbol = Nodo 9
--                   (Nodo 3 
--                         (Nodo 2 Hoja Hoja) 
--                         (Nodo 4 Hoja Hoja)) 
--                   (Nodo 7 Hoja Hoja)
-- ---------------------------------------------------------------------

data Arbol a = Hoja 
             | Nodo a (Arbol a) (Arbol a)
             deriving (Show, Eq)

arbol = Nodo 9
               (Nodo 3 
                     (Nodo 2 Hoja Hoja) 
                     (Nodo 4 Hoja Hoja)) 
               (Nodo 7 Hoja Hoja)

-- ---------------------------------------------------------------------
-- Ejercicio 8.1. Definir la función
--    espejo :: Arbol a -> Arbol a
-- tal que (espejo x) es la imagen especular del árbol x. Por ejemplo,
--    *Main> espejo arbol
--    Nodo 9 
--         (Nodo 7 Hoja Hoja) 
--         (Nodo 3 
--               (Nodo 4 Hoja Hoja) 
--               (Nodo 2 Hoja Hoja))
-- ---------------------------------------------------------------------

espejo :: Arbol a -> Arbol a
espejo = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 8.2. Comprobar con QuickCheck que para todo árbol x,
--    espejo (espejo x) = x
-- ---------------------------------------------------------------------

prop_espejo :: Arbol Int -> Bool
prop_espejo x = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 8.3. Demostrar por inducción que para todo árbol x,
--    espejo (espejo x) = x
-- ---------------------------------------------------------------------

{-
 Demostración:
-}

-- ---------------------------------------------------------------------
-- Ejercicio 8.4. Definir la función
--    preorden :: Arbol a -> [a]
-- tal que (preorden x) es la lista correspondiente al recorrido
-- preorden del árbol x; es decir, primero visita la raíz del árbol, a
-- continuación recorre el subárbol izquierdo y, finalmente, recorre el
-- subárbol derecho. Por ejemplo,
--    *Main> arbol
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> preorden arbol
--    [9,3,2,4,7]
-- ---------------------------------------------------------------------

preorden :: Arbol a -> [a]
preorden = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 8.5. Definir la función
--    postorden :: Arbol a -> [a]
-- tal que (postorden x) es la lista correspondiente al recorrido
-- postorden del árbol x; es decir, primero recorre el subárbol
-- izquierdo, a continuación el subárbol derecho y, finalmente, la raíz
-- del árbol. Por ejemplo,
--    *Main> arbol
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> postorden arbol
--    [2,4,3,7,9]
-- ---------------------------------------------------------------------

postorden :: Arbol a -> [a]
postorden = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 8.6. Comprobar con QuickCheck que para todo árbol x,
--    postorden (espejo x) = reverse (preorden x)
-- ---------------------------------------------------------------------

-- La propiedad es
prop_recorrido :: Arbol Int -> Bool
prop_recorrido x = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 8.7. Demstrar por inducción que para todo árbol x,
--    postorden (espejo x) = reverse (preorden x)
-- ---------------------------------------------------------------------

{-
 Demostración:
-}

-- ---------------------------------------------------------------------
-- Ejercicio 8.8. Comprobar con QuickCheck que para todo árbol binario
-- x, se tiene que
--    reverse (preorden (espejo x)) = postorden x
-- ---------------------------------------------------------------------

-- La propiedad es
prop_reverse_preorden_espejo :: Arbol Int -> Bool
prop_reverse_preorden_espejo x = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 8.9. Demostrar que para todo árbol binario x, se tiene que
--    reverse (preorden (espejo x)) = preorden x
-- ---------------------------------------------------------------------

{-
 Demostración:
-}

-- ---------------------------------------------------------------------
-- Ejercicio 8.10. Definir la función
--    nNodos :: Arbol a -> Int
-- tal que (nNodos x) es el número de nodos del árbol x. Por ejemplo,
--    *Main> arbol
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> nNodos arbol
--    5
-- ---------------------------------------------------------------------

nNodos :: Arbol a -> Int
nNodos = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 8.11. Comprobar con QuickCheck que el número de nodos de la
-- imagen especular de un árbol es el mismo que el número de nodos del
-- árbol. 
-- ---------------------------------------------------------------------

-- La propiedad es
prop_nNodos_espejo :: Arbol Int -> Bool
prop_nNodos_espejo x = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 8.12. Demostrar por inducción que el número de nodos de la
-- imagen especular de un árbol es el mismo que el número de nodos del
-- árbol. 
-- ---------------------------------------------------------------------

{-
 Demostración: 
-}

-- ---------------------------------------------------------------------
-- Ejercicio 8.13. Comprobar con QuickCheck que la longitud de la lista
-- obtenida recorriendo un árbol en sentido preorden es igual al número
-- de nodos del árbol.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_length_preorden :: Arbol Int -> Bool
prop_length_preorden x = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 8.14. Demostrar por inducción que la longitud de la lista
-- obtenida recorriendo un árbol en sentido preorden es igual al número
-- de nodos del árbol.
-- ---------------------------------------------------------------------

{-
 Demostración: 
-}

-- ---------------------------------------------------------------------
-- Ejercicio 8.15. Definir la función
--    profundidad :: Arbol a -> Int
-- tal que (profundidad x) es la profundidad del árbol x. Por ejemplo,
--    *Main> arbol
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> profundidad arbol
--    3
-- ---------------------------------------------------------------------

profundidad :: Arbol a -> Int
profundidad = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 8.16. Comprobar con QuickCheck que para todo árbol biario
-- x, se tiene que
--    nNodos x <= 2^(profundidad x) - 1
-- ---------------------------------------------------------------------

-- La propiedad es
prop_nNodosProfundidad :: Arbol Int -> Bool
prop_nNodosProfundidad x = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 8.17. Demostrar por inducción que para todo árbol binario
-- x, se tiene que
--    nNodos x <= 2^(profundidad x) - 1
-- ---------------------------------------------------------------------

{-
 Demostración:
-}

-- ---------------------------------------------------------------------
-- Ejercicio 8.18. Definir la función
--    nHojas :: Arbol a -> Int
-- tal que (nHojas x) es el número de hojas del árbol x. Por ejemplo,
--    *Main> arbol
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> nHojas arbol
--    6
-- ---------------------------------------------------------------------

nHojas :: Arbol a -> Int
nHojas = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 8.19. Comprobar con QuickCheck que en todo árbol binario el
-- número de sus hojas es igual al número de sus nodos más uno.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_nHojas :: Arbol Int -> Bool
prop_nHojas x = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 8.20. Comprobar con QuickCheck que en todo árbol binario el
-- número de sus hojas es igual al número de sus nodos más uno.
-- ---------------------------------------------------------------------

{-
 Demostración: 
-}

-- ---------------------------------------------------------------------
-- Ejercicio 8.21. Definir, usando un acumulador, la función
--    preordenIt :: Arbol a -> [a]
-- tal que (preordenIt x) es la lista correspondiente al recorrido
-- preorden del árbol x; es decir, primero visita la raíz del árbol, a
-- continuación recorre el subárbol izquierdo y, finalmente, recorre el
-- subárbol derecho. Por ejemplo,
--    *Main> arbol
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> preordenIt arbol
--    [9,3,2,4,7]
-- Nota: No usar (++) en la definición
-- ---------------------------------------------------------------------

preordenIt :: Arbol a -> [a]
preordenIt x = preordenItAux x []

preordenItAux :: Arbol a -> [a] -> [a]
preordenItAux = undefined

-- ---------------------------------------------------------------------
-- Ejercicio 8.22. Comprobar con QuickCheck que preordenIt es
-- equivalente a preorden.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_preordenIt :: Arbol Int -> Bool
prop_preordenIt x = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Ejercicio 8.22. Demostrar que preordenIt es equivalente a preorden.
-- ---------------------------------------------------------------------

prop_preordenItAux :: Arbol Int -> [Int] -> Bool
prop_preordenItAux x ys = undefined

{-
 Demostración: 
-}

-- ---------------------------------------------------------------------
-- Funciones auxiliares                                               --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Nota. Para comprobar propiedades de árboles con QuickCheck se
-- utilizará el siguinete generador.
-- ---------------------------------------------------------------------

instance Arbitrary a => Arbitrary (Arbol a) where
  arbitrary = sized arbol
    where
      arbol 0       = return Hoja 
      arbol n | n>0 = oneof [return Hoja,
                             liftM3 Nodo arbitrary subarbol subarbol]
                      where subarbol = arbol (div n 2)
  coarbitrary = undefined