162 lines
5.3 KiB
Plaintext
162 lines
5.3 KiB
Plaintext
import Mathlib.Tactic
|
||
|
||
|
||
open Finset Nat
|
||
|
||
|
||
/-
|
||
# Números naturales
|
||
|
||
Vamos a hacer algunos ejercicios sobre propiedades de los naturales.
|
||
La principal herramienta que vamos a usar es la inducción. Para ello aplicaremos la
|
||
táctica `induction`.
|
||
|
||
Usaremos la notación de sumatorios. Por ejemplo, la expresión `∑ i in range (n), i^2`
|
||
representa la suma de los cuadrados de los números `0,1,..,(n-1)`. De hecho, puede aplicarse
|
||
a cualquier `finset` (de momento, quedémonos con que es otra noción de conjunto finito).
|
||
La función `range` devuelve el finset correspondiente al número que se le pase
|
||
|
||
Lo que vamos a usar fundamentalmente es un lema llamado `sum_range_succ` que permite separar
|
||
el último término de una suma. Otros resultados que pueden ser útiles son `sum_range_one` y
|
||
`sum_range_zero`.
|
||
|
||
Tamién es útil, cuando queremos demostrar igualdades que se obtienen símplemente
|
||
manipulando sumas y productos en un anillo, usar la táctica `ring`.
|
||
-/
|
||
|
||
-- Demostremos la fórmula para la suma de los cubos de los primeros números
|
||
lemma ejer1 ( n : ℕ ) : (∑ i ∈ range (n + 1), i ^3) * 4 = ((n * (n + 1) ))^2 := by
|
||
induction' n with n hind -- aplicamos inducción sobre n
|
||
· rfl -- caso n = 0 se cumple por definición ·
|
||
· rw [sum_range_succ] -- separamos el último sumando del sumatorio
|
||
rw [add_mul] -- aplicamos la distributiva, para tener exactamente
|
||
-- la misma expresión que en la hipótesis de inducción
|
||
rw [hind] -- aplicamos la hipótesis de inducción
|
||
ring -- y operamos en la expresión
|
||
-- Ahora podemos usar el anterior ejercicio para despejar el `4`
|
||
lemma ejer1' ( n : ℕ ) : (∑ i ∈ range (n.succ), i ^3) = (n *(n + 1)) ^ 2 / 4 := by
|
||
have h1 := ejer1 n
|
||
have h4m : 4 > 0
|
||
· linarith
|
||
rw [← h1]
|
||
simp
|
||
|
||
-- Dar esta vuelta puede parecer distinto a lo que haríamos normalmente con papel
|
||
-- y lápiz. Esto es porque nos estamos restringiendo a operaciones entre números
|
||
-- naturales, y en este contexto la divión `/` es la división con resto.
|
||
|
||
-- Si quisiéramos hacerlo en el espíritu usual de las matemáticas, debemos llevarnos
|
||
-- el problema al contexto de los racionales
|
||
|
||
lemma ejer1_racional (n : ℕ ) : ((∑ i ∈ range (n.succ), i ^3): ℚ) = (n *(n + 1)) ^ 2 / 4 := by
|
||
induction' n with n hind
|
||
· simp
|
||
· rw [sum_range_succ] -- separar el último término de la suma
|
||
rw [hind] -- aplicar la hipótesis de inducción
|
||
simp -- convertimos los sucesores en sumas
|
||
ring -- para poder aplicar la simplificación de expresiones en un anillo
|
||
|
||
-- # Ejercicios
|
||
|
||
-- demuestra que el producto de dos números consecutivos es par
|
||
-- puedes usar el hecho de que todo natural es par o impar (`nat.even_or_odd`)
|
||
-- también se puede hacer por inducción
|
||
|
||
lemma prod_consec_par (n : ℕ ) : 2 ∣ (n * (n + 1)) := by
|
||
sorry,
|
||
|
||
/-
|
||
Demostrar la fórmula para la suma de los primeros números naturales.
|
||
Primero como igualdad en los racionales:
|
||
|
||
-/
|
||
|
||
lemma suma_primeros_en_Q ( n : ℕ ) : (∑ i ∈ range n, i : ℚ ) = n * (n - 1) / 2 := by
|
||
sorry
|
||
|
||
/-
|
||
Ahora como igualdad en los naturales, igual es más fácil hacerlo primero quitando
|
||
denominadores.
|
||
-/
|
||
|
||
lemma suma_primeros_en_N_2 ( n : ℕ ) : 2 * (∑ i ∈ range n, i) = n * (n - 1) := by
|
||
sorry
|
||
|
||
/-
|
||
y luego usar lo anterior para obtener la fórmula con fracciones
|
||
-/
|
||
|
||
lemma suma_primeros_en_N (n : ℕ ) : (∑ i ∈ range n, i) = n * (n - 1) / 2 := by
|
||
sorry
|
||
|
||
|
||
/-
|
||
# Ejemplos con Fibonaci
|
||
|
||
Demostremos ahora algunas propiedades de la sucesión de Fibonaci. Empezamos definiendola
|
||
recursivamente:
|
||
-/
|
||
def Fib : ℕ → ℕ
|
||
| 0 => 0
|
||
| 1 => 1
|
||
| (n + 2) => Fib n + Fib (n +1)
|
||
|
||
|
||
/-
|
||
Veamos que dos términos consecutivos son coprimos
|
||
-/
|
||
lemma cons_fib_coprimos (n : ℕ ) : Nat.gcd (Fib n) (Fib (n + 1)) = 1 := by
|
||
induction' n with n h
|
||
· simp [Fib]
|
||
· cases' n with n
|
||
· simp [Fib]
|
||
· simp [Fib] at *
|
||
rw [Nat.gcd_comm]
|
||
exact h
|
||
/-
|
||
Marcamos los siguientes resultados como `@[simp]` para que la táctica `simp` los use.
|
||
-/
|
||
|
||
@[simp]
|
||
lemma fib0 : Fib 0 = 0 := by rfl
|
||
|
||
@[simp]
|
||
lemma fib1 : Fib 1 = 1 := by rfl
|
||
|
||
@[simp]
|
||
lemma fib2 : Fib 2 = 1 := by rfl
|
||
|
||
@[simp]
|
||
lemma fib2a (n : ℕ) : Fib (2 + n) = Fib (n) + Fib (1 + n) := by
|
||
rw [add_comm,Fib]
|
||
ring_nf
|
||
|
||
@[simp]
|
||
lemma fib_suma (m n : ℕ) :
|
||
Fib (m + n + 1) = Fib m * Fib n + Fib (m + 1) * Fib (n + 1) := by
|
||
induction' n with n ih generalizing m
|
||
· simp
|
||
· specialize ih (m+1)
|
||
ring_nf at *
|
||
rw [ih]
|
||
simp
|
||
ring
|
||
|
||
/-
|
||
Aquí podemos ver un ejemplo de usar la táctica `calc`
|
||
Veamos que la función de fibonacci respeta divisibilidad
|
||
(notar que el símbolo de dividir `∣` es distinto del que
|
||
se usa para definir conjuntos: `\|` frente a `|` )
|
||
-/
|
||
lemma fib_div (n r : ℕ ) : Fib n ∣ Fib (n * r) := by
|
||
cases' n with n
|
||
· simp
|
||
· induction' r with r ih
|
||
· simp
|
||
· choose a1 ha1 using ih
|
||
use (a1 * Fib (n ) + Fib ((n + 1) * r + 1))
|
||
calc Fib ((n + 1) * (r + 1)) = Fib ((n + 1) * r + n + 1) := by ring_nf
|
||
_ = Fib ((n + 1) * r) * Fib n + Fib ((n + 1) * r + 1) * Fib (n + 1) := by rw [fib_suma]
|
||
_ = Fib (n + 1) * a1 * Fib n + Fib ((n + 1) * r + 1) * Fib (n + 1) := by rw [ha1]
|
||
_ = Fib (n + 1) * (a1 * Fib n + Fib ((n + 1) * r + 1)) := by ring
|