Relación 1

-- LMF 2014-15: Rel_1.hs (9 de Febrero de 2015)
-- Introducción a la programación con Haskell.
-- Departamento de Ciencias de la Computación e I.A.
-- Universidad de Sevilla
-- =====================================================================

-- ---------------------------------------------------------------------
-- Introducción                                                       --
-- ---------------------------------------------------------------------

-- En esta relación de ejercicios hacemos una introducción a Haskell, en
-- la que se recuerdan:
-- * las definiciones elementales de funciones,
-- * las definiciones de funciones por comprensión,
-- * las definiciones de funciones por recursión y
-- * los tipos de datos.

-- ---------------------------------------------------------------------
-- Importación de librerías auxiliares                                  
-- ---------------------------------------------------------------------
 
import Test.QuickCheck
import Data.Char
import Control.Monad

-- ---------------------------------------------------------------------
-- Ejercicio 1. Definir la función media3 tal que (media3 x y z) es
-- la media aritmética de los números x, y y z. Por ejemplo, 
--    media3 1 3 8     ==  4.0
--    media3 (-1) 0 7  ==  2.0
--    media3 (-3) 0 3  ==  0.0
-- ---------------------------------------------------------------------

media3 x y z = (x+y+z)/3

-- Miriam R.
-- Rocio Rodriguez 
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 2. Definir la función ultimaCifra tal que (ultimaCifra x)
-- es la última cifra del nímero x. Por ejemplo,
--    ultimaCifra 325  ==  5
-- ---------------------------------------------------------------------

ultimaCifra x = rem x 10

-- Miriam R.
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 3. Definir la función rota tal que (rota n xs) es la lista
-- obtenida poniendo los n primeros elementos de xs al final de la
-- lista. Por ejemplo, 
--    rota 1 [3,2,5,7]  ==  [2,5,7,3]
--    rota 2 [3,2,5,7]  ==  [5,7,3,2]
--    rota 3 [3,2,5,7]  ==  [7,3,2,5]
-- ---------------------------------------------------------------------

rota n xs= (drop n xs) ++ (take n xs)


-- Pablo José Gerlach Mena 
-- Rocio Rodriguez 
-- Jaime Alberto
-- Francisco Javier Carmona

-- Maria del Carmen Mesa Marquez 
rota 0 xs = xs 
rota n [] = []
rota n (x:xs) = rota (n-1) (xs ++ [x])

-- ---------------------------------------------------------------------
-- Ejercicio 4.1. La disyunción excluyente xor de dos fórmulas se
-- verifica si una es verdadera y la otra es falsa.
-- 
-- Definir la función xor_1 que calcule la disyunción excluyente a
-- partir de la tabla de verdad. Usar 4 ecuaciones, una por cada línea
-- de la tabla. 
-- ---------------------------------------------------------------------

xor_1 :: Bool -> Bool -> Bool
xor_1 True True = False
xor_1 True False = True
xor_1 False True = True
xor_1 False False = False

-- Pablo José Gerlach Mena
-- Rocio Rodriguez 

xor_1 :: Bool -> Bool -> Bool
xor_1 x y   |x== True && y== True = False 
            |x== True && y== False = True
            |x== False && y== True = True
            |x== False && y== False = False
-- Jaime Alberto 
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 4.2. Definir la función xor_2 que calcule la disyunción
-- excluyente a partir de la tabla de verdad y patrones. Usar 2
-- ecuaciones, una por cada valor del primer argumento.
-- ---------------------------------------------------------------------

xor_2 :: Bool -> Bool -> Bool
xor_2 True x = if x then False else True
xor_2 False x = if x then True else False

-- Pablo José Gerlach Mena


-- Realizado por Nikola Drousie:
-- Rocio Rodriguez 

xor_2' True x = not x
xor_2' False x = x

-- Jaime Alberto
xor_2'' :: Bool -> Bool -> Bool
xor_2'' x y |  x== True && y== True || x==False && y== False = False
          |  x== True && y== False || x== False && y== True = True  

-- Elisa Mazuelos Jiménez:

xor_2 :: Bool -> Bool -> Bool
xor_2 True x | x == True = False
             | otherwise = True
xor_2 False x | x == False = False
              | otherwise = True

-- Esta última no es correcta (10/02/2015).
-- Corregida, gracias (10/02/2015).

-- ---------------------------------------------------------------------
-- Ejercicio 4.3. Definir la función xor_3 que calcule la disyunción
-- excluyente a partir de la disyunción (||), conjunción (&&) y negación
-- (not). Usar 1 ecuación.
-- ---------------------------------------------------------------------

xor_3 :: Bool -> Bool -> Bool
xor_3 x y = (x && (not y)) || ((not x) && y)

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-----------------------------------------------------
-- Ejercicio 4.4. Definir la función xor_4 que calcule la disyunción
-- excluyente a partir de desigualdad (/=). Usar 1 ecuación.
-- ---------------------------------------------------------------------

xor_4 :: Bool -> Bool -> Bool
xor_4 x y = x /= y

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
 
-- ---------------------------------------------------------------------
-- Ejercicio 5. Definir, por comprensión, la función
--    sumaDeCuadrados :: Integer -> Integer
-- tal que (sumaDeCuadrados n) es la suma de los cuadrados de los
-- primeros n números; es decir, 1^2 + 2^2 + ... + 100^2. Por ejemplo,
--    sumaDeCuadrados 3    ==  14
--    sumaDeCuadrados 100  ==  338350
-- ---------------------------------------------------------------------

sumaDeCuadrados n = sum [x^2 | x <- [1..n]]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 6. Una terna (x,y,z) de enteros positivos es pitagórica si 
-- x^2 + y^2 = z^2. Usando una lista por comprensión, definir la función
--    pitagoricas :: Int -> [(Int, Int, Int)]
-- tal que (pitagoricas n) es la lista de todas las ternas pitagóricas
-- cuyas componentes están entre 1 y n. Por ejemplo, 
--    *Main> pitagoricas 10 
--    [(3,4,5),(4,3,5),(6,8,10),(8,6,10)]
-- ---------------------------------------------------------------------
 
pitagoricas :: Int -> [(Int, Int, Int)]
pitagoricas n = [(x,y,z) | x <- [1..n], y <- [1..n], z <- [1..n], x^2+y^2 == z^2]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto 
-- Francisco Javier Carmona
-- Luis Curquejo. Solución acotando ligeramente los elementos x e y.

pitagoricas :: Int -> [(Int, Int, Int)]
pitagoricas n = [ (x,y,z) | z <- [1..n], x <- [1..z], y <- [1..z] , x^2 + y^2 == z^2]

-- Comentario: la definición se puede mejorar.

-- ---------------------------------------------------------------------
-- Ejercicio 7. Un entero positivo es perfecto si es igual a la suma de
-- sus factores, excluyendo el propio número. Usando una lista por
-- comprensión y la función factores (del tema), definir la función 
--    perfectos :: Int -> [Int]
-- tal que (perfectos n) es la lista de todos los números perfectos
-- menores que n. Por ejemplo: 
--    *Main> perfectos 500
--    [6,28,496]
-- ---------------------------------------------------------------------
 
perfectos :: Int -> [Int]
perfectos n = [x | x <- [1..n], esPerfecto x]

-- Definimos las funciones auxiliares:

factores :: Int -> [Int]
factores n = [x | x <- [1..n], n `mod` x == 0]

esPerfecto :: Int -> Bool
esPerfecto n = sum (factores n) == 2*n

-- Comentario: la definición se puede simplificar.

-- También podríamos definirla como:

perfectos2 :: Int -> [Int]
perfectos2 n = filter (esPerfecto) [1..n]

-- Podemos comprobar que ambas definiciones son equivalentes:

prop_perfectos n = perfectos n == perfectos2 n

-- Si queremos podemos comparar ambos algoritmos:

-- *Main> perfectos 500
-- [6,28,496]
-- (1.44 secs, 15935120 bytes)

-- *Main> perfectos2 500
-- [6,28,496]
-- (0.22 secs, 14803544 bytes)

-- Es decir, el segundo es más eficiente.

-- Pablo José Gerlach Mena

-- Rocio Rodriguez 
perfectos x = [y|y<-[1..x-1], serPerfecto y]
serPerfecto x = x==sum (factores' x)
factores x = [y|y<-[1..x], rem x y == 0]
factores' x = init (factores x)

-- Luis Curquejo

perfectos :: Int -> [Int]
perfectos n = [ x | x <- [1..n], x == sum (factoresred x)]
    where factoresred x = [ y | y <- [1..x-1], rem x y == 0] 

-- Francisco Javier Carmona


perfectos1 :: Int -> [Int]
perfectos1 n = [ x | x <- [1..n], 
                x == sum (tail(reverse (factores x)))]

-- Comentario: la definición se puede simplificar.

factores1 n = [x | x <- [1..n], rem n x == 0] 

-- ---------------------------------------------------------------------
-- Ejercicio 8.1. Definir, por comprensión, la función
--    cuadradosC :: [Integer] -> [Integer]
-- tal que (cuadradosC xs) es la lista de los cuadrados de xs. Por
-- ejemplo, 
--    cuadradosC [1,2,3]  ==  [1,4,9]
-- ---------------------------------------------------------------------

cuadradosC :: [Integer] -> [Integer]
cuadradosC xs = [x^2 | x <- xs]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez 
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 8.2. Definir, por recursión, la función
--    cuadradosR :: [Integer] -> [Integer]
-- tal que (cuadradosR xs) es la lista de los cuadrados de xs. Por
-- ejemplo, 
--    cuadradosR [1,2,3]  ==  [1,4,9]
-- ---------------------------------------------------------------------

cuadradosR :: [Integer] -> [Integer]
cuadradosR [] = []
cuadradosR (x:xs) = (x^2):(cuadradosR xs)

-- Pablo José Gerlach Mena
-- Rocio Rodriguez 
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 9.1. Definir, por comprensión, la función
--    imparesC :: [Integer] -> [Integer]
-- tal que (imparesC xs) es la lista de los números impares de xs. Por
-- ejemplo, 
--    imparesC [1,2,3]  ==  [1,3]
-- ---------------------------------------------------------------------

imparesC :: [Integer] -> [Integer]
imparesC xs = [x | x <- xs, odd x]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 9.2. Definir, por recursión, la función
--    imparesR :: [Integer] -> [Integer]
-- tal que (imparesR xs) es la lista de los números impares de xs. Por
-- ejemplo, 
--    imparesR [1,2,3]  ==  [1,3]
-- ---------------------------------------------------------------------

imparesR :: [Integer] -> [Integer]
imparesR [] = []
imparesR (x:xs) | odd x = x:(imparesR xs)
                | otherwise = imparesR xs

-- Pablo José Gerlach Mena
-- Rocio Rodriguez 
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 10. Definir, por comprensión, la función
--    sumaConsecutivos :: [Int] -> [Int]
-- tal que (sumaConsecutivos xs) es la suma de los pares de elementos
-- consecutivos de la lista xs. Por ejemplo,
--    sumaConsecutivos [3,1,5,2]  ==  [4,6,7]
--    sumaConsecutivos [3]        ==  []
-- ---------------------------------------------------------------------

sumaConsecutivos :: [Int] -> [Int]
sumaConsecutivos xs = [x+y | (x,y) <- zip xs (tail xs)]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez 
-- Jaime Alberto

-- Francisco Javier Carmona

sumaConsecutivos1 :: [Int] -> [Int]
sumaConsecutivos1 (x:xs) = [ (x+y) | (x,y) <- zip (x:xs) xs]

-- ---------------------------------------------------------------------
-- Ejercicio 11.  La distancia de Hamming entre dos listas es el número
-- de posiciones en que los correspondientes elementos son
-- distintos. Por ejemplo, la distancia de Hamming entre "roma" y "loba" 
-- es 2 (porque hay 2 posiciones en las que los elementos
-- correspondientes son distintos: la 1ª y la 3ª). 
--    
-- Definir la función distancia tal que (distancia xs ys) es la 
-- distancia de Hamming entre xs e ys. Por ejemplo,
--    distancia "romano" "comino"  ==  2
--    distancia "romano" "camino"  ==  3
--    distancia "roma"   "comino"  ==  2
--    distancia "roma"   "camino"  ==  3
--    distancia "romano" "ron"     ==  1
--    distancia "romano" "cama"    ==  2
--    distancia "romano" "rama"    ==  1
-- ---------------------------------------------------------------------

distancia :: Eq a => [a] -> [a] -> Int
distancia xs ys = length (distanciaAux xs ys)

-- Definimos la función auxiliar:

distanciaAux :: Eq a => [a] -> [a] -> [Int]
distanciaAux xs [] = []
distanciaAux [] ys = []
distanciaAux (x:xs) (y:ys) | x == y = distanciaAux xs ys
                           | otherwise = [1]++(distanciaAux xs ys)

-- Comentario: la definición se puede simplificar.

-- Pablo José Gerlach Mena

-- María Dolores Mateo Ceballos 
-- Francisco Javier Carmona
-- Aunque es parecido al anterior, sin usar función auxiliar:

distancia :: Eq a => [a] -> [a] -> Int
distancia [] _ = 0
distancia _ [] = 0
distancia (x:xs) (y:ys) | x==y = distancia xs ys 
                        | otherwise = 1 + distancia xs ys 

-- Comentario: la definición se puede simplificar.

-- Realizado por Nikola Drousie:
-- Rocio Rodriguez

distancia' :: Eq a => [a] -> [a] -> Int
distancia' xs ys = sum [ 1 | (a,b)<-zip xs ys, a/=b]
-- Jaime Alberto
-- ---------------------------------------------------------------------
-- Ejercicio 12. Definir la función
--    factoriales :: [Integer]
-- tal que factoriales es la lista de los factoriales. Por ejemplo,
--    take 10 factoriales  ==  [1,1,2,6,24,120,720,5040,40320,362880]
-- ---------------------------------------------------------------------

-- Por comprensión:

factoriales1 :: [Integer]
factoriales1 = [1]++[product [1..n] | n <-[1..]]

-- Pablo José Gerlach Mena
-- Francisco Javier Carmona

-- Rocio Rodriguez 
factoriales1 = [fact x|x<-[0..]]
fact 0 = 1
fact x = x*fact (x-1)

-- Jaime Alberto
-- Usando zipWith:

factoriales2 :: [Integer]
factoriales2 = [1]++(zipWith f [1..] [2..])
               where f n y = product ([1..n]++[y])

-- Emilio Martinez

-- Por recursión:

factoriales3 :: [Integer]
factoriales3 = 1:(aux 1 [1..])
               where aux n (x:xs)= (n*x):(aux (n*x) xs)

-- Emilio Martinez

-- Usando scanl1:

factoriales4 :: [Integer]
factoriales4 = scanl  (*) 1 [1..]

-- Emilio Martinez

-- Usando iterate:
-- Fran Franco
factoriales5 :: [Integer]
factoriales5 = map snd (iterate (\(x,y)->(x+1,x*y)) (1,1))

-- Comparación de los tiempos de evaluación:

-- *Main> take 10 factoriales1
-- [1,1,2,6,24,120,720,5040,40320,362880]

-- (0.02 secs, 0 bytes)

-- *Main> take 10 factoriales2
-- [1,2,6,24,120,720,5040,40320,362880,3628800]
-- (0.00 secs, 0 bytes)

-- *Main> take 10 factoriales3
-- [1,1,2,6,24,120,720,5040,40320,362880]
-- (0.00 secs, 528020 bytes)

-- *Main> take 10 factoriales4
-- [1,1,2,6,24,120,720,5040,40320,362880]
-- (0.00 secs, 0 bytes)

-- Pablo José Gerlach Mena

-- ---------------------------------------------------------------------
-- Ejercicio 13.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)
-- Como ejemplos se usarán los árboles
-- ---------------------------------------------------------------------
 
data Arbol a = Hoja 
             | Nodo a (Arbol a) (Arbol a)
             deriving (Show, Eq)
 
arbol_1 = Nodo 9
               (Nodo 3 
                     (Nodo 2 Hoja Hoja) 
                     (Nodo 4 Hoja Hoja)) 
               (Nodo 7 Hoja Hoja)
 
-- ---------------------------------------------------------------------
-- Ejercicio 13.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_1
--    Nodo 9 
--         (Nodo 7 Hoja Hoja) 
--         (Nodo 3 
--               (Nodo 4 Hoja Hoja) 
--               (Nodo 2 Hoja Hoja))
-- ---------------------------------------------------------------------
 
espejo :: Arbol a -> Arbol a
espejo Hoja = Hoja
espejo (Nodo a i d)= Nodo a (espejo d) (espejo i)

-- Emilio Martinez
-- Rocio Rodriguez
-- Jaime Alberto 
-- Francisco Javier Carmona 
-- ---------------------------------------------------------------------
-- Ejercicio 13.2. Comprobar con QuickCheck que para todo árbol x,
--    espejo (espejo x) = x
-- ---------------------------------------------------------------------
 
prop_espejo :: Arbol Int -> Bool
prop_espejo n = (espejo . espejo) n == n
 
-- quickCheck prop_espejo
-- +++ OK passed 100 tests.

-- Emilio Martinez
-- Jaime Alberto
-- Rocio Rodriguez 
prop_espejo x = espejo (espejo x)==x
quickCheck prop_espejo
+++ OK, passed 100 tests.
-- ---------------------------------------------------------------------
-- Ejercicio 13.3. Demostrar por inducción que para todo árbol x,
--    espejo (espejo x) = x
-- ---------------------------------------------------------------------
{-
 Demostración por inducción en x

[Caso base: Hoja]

espejo (espejo Hoja) = espejo (Hoja) por definicion de espejo Hoja
espejo (Hoja) = Hoja por definicion de espejo Hoja

Luego  espejo (espejo Hoja)= Hoja 
qed

[Suponemos que espejo (espejo x) = x , para todo x arbol]

[Sea N a i d con i, d arboles]

espejo (espejo (N a i d))= espejo (N a (espejo d) (espejo i)) por def
espejo (N a (espejo d)(espejo i)) = N a (espejo (espejo i))
                                                        (espejo(espejo
                                                                d)) por def

como i, d son arboles por hipótesis de induccion

= N a (espejo (espejo i)) (espejo (espejo d))
= N a i d

Luego espejo (espejo (N a i d)) = N a i d.
qed

Emilio Martinez 
-}
 
 -- ---------------------------------------------------------------------
-- Ejercicio 13.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_1
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> preorden arbol_1
--    [9,3,2,4,7]
-- ---------------------------------------------------------------------
 
preorden :: Arbol a -> [a]
preorden Hoja = []
preorden (Nodo a i d)= [a]++(preorden i)++(preorden d)

--Emilio Martinez
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.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_1
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> postorden arbol_1
--    [2,4,3,7,9]
-- ---------------------------------------------------------------------
 
postorden :: Arbol a -> [a]
postorden Hoja = []
postorden (Nodo a i d)= postorden i ++ [a]++ postorden d

-- Comentario: la definición no es correcta. 
-- postorden arbol_1 == [2,3,4,9,7]

-- Realizado por Nikola Drousie:
-- Rocio Rodriguez 


postorden' :: Arbol a -> [a]
postorden' Hoja = []
postorden' (Nodo a i d) = postorden' i ++ postorden' d ++ [a]
 -- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.6. Comprobar con QuickCheck que para todo árbol x,
--    postorden (espejo x) = reverse (postorden x)
-- ---------------------------------------------------------------------
 
-- La propiedad es
prop_recorrido :: Arbol Int -> Bool
prop_recorrido x = (postorden . espejo) x == (reverse . postorden) x
 
-- La comprobación es
--quickCheck prop_recorrido
-- +++ OK, passed 100 tests.

--Emilio Martinez Rivero
-- Jaime Alberto 
-- ---------------------------------------------------------------------
-- Ejercicio 13.7. Demstrar por inducción que para todo árbol x,
--    postorden (espejo x) = reverse (preorden x)
-- ---------------------------------------------------------------------
 
{-
 Demostración por inducción en x.

-}
 
-- ---------------------------------------------------------------------
-- Ejercicio 13.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 =
   reverse (preorden (espejo x)) == postorden x
 
-- La comprobación es
--    *Main> quickCheck prop_reverse_preorden_espejo
--    OK, passed 100 tests.
 
-- ---------------------------------------------------------------------
-- Ejercicio 13.9. Demostrar que para todo árbol binario x, se tiene que
--    reverse (preorden (espejo x)) = preorden x
-- ---------------------------------------------------------------------
 
{-
 Demostración:
    reverse (preorden (espejo x))
    = postorden (espejo (espejo x))    [por ejercicio 13.7]
    = postorden x                      [por ejercicio 13.3]
-}
 
-- ---------------------------------------------------------------------
-- Ejercicio 13.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_1
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> nNodos arbol_1
--    5
-- ---------------------------------------------------------------------
 
nNodos :: Arbol a -> Int
nNodos Hoja = 0
nNodos (Nodo _ i d)= 1+(nNodos i)+(nNodos d)

--Emilio Martinez
 -- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.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 = nNodos x == (nNodos . espejo) x
 
-- La comprobación es

--  quickCheck prop_nNodos_espejo
-- +++ OK, passed 100 tests.

--Emilio Martinez
 
-- ---------------------------------------------------------------------
-- Ejercicio 13.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 13.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 = length (preorden x)== nNodos x
 
-- La comprobación es

--  quickCheck prop_length_preorden
-- +++ OK, passed 100 tests.

-- Adrian Guerra
-- ---------------------------------------------------------------------
-- Ejercicio 13.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 13.15. Definir la función
--    profundidad :: Arbol a -> Int
-- tal que (profundidad x) es la profundidad del árbol x. Por ejemplo,
--    *Main> arbol_1
--    Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
--    *Main> profundidad arbol_1
--    3
-- ---------------------------------------------------------------------
 
profundidad :: Arbol a -> Int
profundidad Hoja = 0
profundidad (Nodo _ i d) = 1+ max(profundidad i) (profundidad d)

--Emilio Martinez
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.16. Comprobar con QuickCheck que para todo árbol binario
-- x, se tiene que
--    nNodos x <= 2^(profundidad x) - 1
-- ---------------------------------------------------------------------
 
-- La propiedad es
prop_nNodosProfundidad :: Arbol Int -> Bool
prop_nNodosProfundidad x = nNodos x <= 2^(profundidad x) - 1

-- La comprobación es
--  quickCheck prop_nNodosProfundidad
-- +++ OK, passed 100 tests.

-- Adrian Guerra
-- ---------------------------------------------------------------------
-- Nota. Para comprobar propiedades de árboles con QuickCheck se
-- utilizará el siguiente 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)