Últimos dos dígitos de (1+5^(2*n+1))/6 en Haskell

Ayer Benjamin Vitale planteó el problema Últimos dos dígitos de (1+5^(2n+1))/6 que consiste en demostrar que para cualquier n ≥ 1 los últimos dos dígitos de $\frac{1+5^{2n+1}}{6}$ son 21.

A partir del problema he elaborado la siguiente relación de ejercicios para Informática (de 1º del Grado en Matemáticas).

-- ---------------------------------------------------------------------
-- Librerías auxiliares                                               --
-- ---------------------------------------------------------------------

import Test.QuickCheck

-- ---------------------------------------------------------------------
-- Ejercicio 1. Definir la función 
--    f :: Integer -> Integer
-- tal que f(n) = (1+5^(2*n+1))/6 y calcular el valor de f(n) para n
-- desde 1 hasta 6.
-- ---------------------------------------------------------------------

f :: Integer -> Integer
f n = (1+5^(2*n+1)) `div` 6

-- El cálculo es 
--    ghci> [f n | n <- [1..6]]
--    [21,521,13021,325521,8138021,203450521]

-- ---------------------------------------------------------------------
-- Ejercicio 2. Definir la función
--    dos_ultimos :: Integer -> Integer
-- tal que (dos_ultimos x) es el número formado con los últimos dígitos
-- de x. Por ejemplo,
--    dos_ultimos 53579  ==  79
-- ---------------------------------------------------------------------

dos_ultimos :: Integer -> Integer
dos_ultimos x = x `mod` 100 

-- ---------------------------------------------------------------------
-- Ejercicio 3. Comprobar con QuickCheck que para cualquier n ≥ 1 los
-- últimos dos dígitos de (1+5^(2n+1))/6 son 21.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_dos_ultimos :: Integer -> Bool
prop_dos_ultimos n = dos_ultimos (f n') == 21
    where n' = 1 + abs n

-- La comprobación es
--    ghci> quickCheck prop_dos_ultimos
--    +++ OK, passed 100 tests.

-- ---------------------------------------------------------------------
-- Ejercicio 4. Demostrar, por inducción, que para cualquier n ≥ 1 los
-- últimos dos dígitos de (1+5^(2n+1))/6 son 21.
-- ---------------------------------------------------------------------

-- Como f(n) = (1+5^(2n+1))/6, lo que hay que demostrar es que, para
-- cualquier n ≥ 1, existe un número natural x tal f(n) = 100*x+21. Lo
-- haremos por inducción en n. 
-- 
-- (Base n=1) h(1) = 21 = 100*0+21
-- 
-- (Paso n --> n+1) La hipótesis de inducción, es que existe un y tal
-- que 
--    f(n) = 100*y+21
-- Luego, por definición de f, 
--    (1+5^(2*n+1))/6 = 100*y+21              
-- y, despejando,
--    5^(2*n+1) = 600*y+125            (1)
-- Además, por definición de f,
--    f(n+1) = (1+5^(2*(n+1)+1))/6
--           = (1+5^((2*n+1)+2))/6
--           = (1+5^(2*n+1)*5^2)/6
--           = (1+(600*y+125)*25)/6    [por (1)]
--           = (1+600*25*y+125*25)/6
--           = 100*25*y+521
--           = 100*(25*y+5)+21         
--           = 100*x+21,               [con x = 25*y+5]

-- ---------------------------------------------------------------------
-- Ejercicio 5. A partir de la demostración anterior, definir por
-- recursión una función
--    g :: Integer -> Integer
-- tal que g es equivalente a f.
-- ---------------------------------------------------------------------

g :: Integer -> Integer
g 1 = 21
g (n+1) = 100*(25*x+5)+21
           where x = ((f n) - 21) `div` 100

-- ---------------------------------------------------------------------
-- Ejercicio 6. Comprobar con QuickCheck que que las funciones f y g son
-- equivalentes, para n ≥ 1. 
-- ---------------------------------------------------------------------

-- La propiedad es 
prop_equivalencia :: Integer -> Bool
prop_equivalencia n = f n' == g n' 
    where n' = 1 + abs n

-- La comprobación es
--    ghci> quickCheck prop_equivalencia
--    +++ OK, passed 100 tests.

-- ---------------------------------------------------------------------

-- Librerías auxiliares --

-- ---------------------------------------------------------------------

import Test.QuickCheck

-- ---------------------------------------------------------------------

-- Ejercicio 1. Definir la función

-- f :: Integer -> Integer

-- tal que f(n) = (1+5^(2*n+1))/6 y calcular el valor de f(n) para n

-- desde 1 hasta 6.

-- ---------------------------------------------------------------------

f :: Integer -> Integer

f n = (1+5^(2*n+1)) `div` 6

-- El cálculo es

-- ghci> [f n | n <- [1..6]]

-- [21,521,13021,325521,8138021,203450521]

-- ---------------------------------------------------------------------

-- Ejercicio 2. Definir la función

-- dos_ultimos :: Integer -> Integer

-- tal que (dos_ultimos x) es el número formado con los últimos dígitos

-- de x. Por ejemplo,

-- dos_ultimos 53579 == 79

-- ---------------------------------------------------------------------

dos_ultimos :: Integer -> Integer

dos_ultimos x = x `mod` 100

-- ---------------------------------------------------------------------

-- Ejercicio 3. Comprobar con QuickCheck que para cualquier n ≥ 1 los

-- últimos dos dígitos de (1+5^(2n+1))/6 son 21.

-- ---------------------------------------------------------------------

-- La propiedad es

prop_dos_ultimos :: Integer -> Bool

prop_dos_ultimos n = dos_ultimos (f n') == 21

where n' = 1 + abs n

-- La comprobación es

-- ghci> quickCheck prop_dos_ultimos

-- +++ OK, passed 100 tests.

-- ---------------------------------------------------------------------

-- Ejercicio 4. Demostrar, por inducción, que para cualquier n ≥ 1 los

-- últimos dos dígitos de (1+5^(2n+1))/6 son 21.

-- ---------------------------------------------------------------------

-- Como f(n) = (1+5^(2n+1))/6, lo que hay que demostrar es que, para

-- cualquier n ≥ 1, existe un número natural x tal f(n) = 100*x+21. Lo

-- haremos por inducción en n.

-- (Base n=1) h(1) = 21 = 100*0+21

-- (Paso n --> n+1) La hipótesis de inducción, es que existe un y tal

-- que

-- f(n) = 100*y+21

-- Luego, por definición de f,

-- (1+5^(2*n+1))/6 = 100*y+21

-- y, despejando,

-- 5^(2*n+1) = 600*y+125 (1)

-- Además, por definición de f,

-- f(n+1) = (1+5^(2*(n+1)+1))/6

-- = (1+5^((2*n+1)+2))/6

-- = (1+5^(2*n+1)*5^2)/6

-- = (1+(600*y+125)*25)/6 [por (1)]

-- = (1+600*25*y+125*25)/6

-- = 100*25*y+521

-- = 100*(25*y+5)+21

-- = 100*x+21, [con x = 25*y+5]

-- ---------------------------------------------------------------------

-- Ejercicio 5. A partir de la demostración anterior, definir por

-- recursión una función

-- g :: Integer -> Integer

-- tal que g es equivalente a f.

-- ---------------------------------------------------------------------

g :: Integer -> Integer

g 1 = 21

g (n+1) = 100*(25*x+5)+21

where x = ((f n) - 21) `div` 100

-- ---------------------------------------------------------------------

-- Ejercicio 6. Comprobar con QuickCheck que que las funciones f y g son

-- equivalentes, para n ≥ 1.

-- ---------------------------------------------------------------------

-- La propiedad es

prop_equivalencia :: Integer -> Bool

prop_equivalencia n = f n' == g n'

where n' = 1 + abs n

-- La comprobación es

-- ghci> quickCheck prop_equivalencia

-- +++ OK, passed 100 tests.

Nota: Otra demostración, usando aritmética modular, es la realizada por @joseanpg que se puede leer aquí.

Se puede imprimir o compartir con