From 899adc8f535b6dbadc580c7f5bb99e8757f81ab5 Mon Sep 17 00:00:00 2001 From: Miguel Marco Date: Thu, 29 Oct 2026 12:06:44 +0100 Subject: [PATCH] =?UTF-8?q?A=C3=B1adidos=20inductivos,=20finitud=20y=20nat?= =?UTF-8?q?urales?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Curso2026/Finitud.lean | 106 +++++++++++++++++++++ Curso2026/Inductivos.lean | 187 ++++++++++++++++++++++++++++++++++++++ Curso2026/Naturales.lean | 161 ++++++++++++++++++++++++++++++++ 3 files changed, 454 insertions(+) create mode 100644 Curso2026/Finitud.lean create mode 100644 Curso2026/Inductivos.lean create mode 100644 Curso2026/Naturales.lean diff --git a/Curso2026/Finitud.lean b/Curso2026/Finitud.lean new file mode 100644 index 0000000..8f84a18 --- /dev/null +++ b/Curso2026/Finitud.lean @@ -0,0 +1,106 @@ +import Mathlib.Tactic + +open Set +/- +# Conjuntos y tipos finitos + +En Lean hay varias nociones de finitud (en parte porque en las propias matemáticas también las hay): + - Tipos finitos (`Fintype`) + - Conjuntos finitos (`Finset`) + - Tipos ordinarios que tienen la propiedad de ser finitos (`Finite`) + - Conjuntos ordinarios que tienen la propiedad de ser finitos (`Set.Finite`) + - ... + +De momento vamos a centrarnos sólo en los dos últimos casos, es decir, vamos a trabajar +con conjuntos o tipos como antes, pero usaremos en ocasiones la propiedad de que son finitos + +Que un tipo sea finito quiere decir que es biyectivo con {0,1,..,n} para algún n. Que un +conjunto sea finito quiere decir que su correspondiente tipo sea finito. +-/ + + +-- un conjunto es finito si y sólo si su tipo correspondiente es finito + +lemma tipo_finito_sii_conjunto_finito (X : Type) (S : Set X) : Finite ↥S ↔ Set.Finite S := by + exact finite_coe_iff + + +-- un conjunto es finito si y sólo si es biyectivo con {0,1,...,n} para algún natural n + +lemma Set_Finite_iff_bijective_fin_n (X : Type) ( S : Set X) : Set.Finite S ↔ ∃ n : ℕ, ∃ (a : ↥S → (Fin n)), Function.Bijective a := by + rw [← tipo_finito_sii_conjunto_finito] + fconstructor + . intro h + cases' h with n hn + use n + use hn + exact Equiv.bijective hn + . intro h + cases' h with n hn + cases' hn with a ha + fconstructor + · use n + · apply Equiv.ofBijective a ha + + + +/- +Una propiedad importante es que los conjuntos finitos tienen principio de inducción: +si una propiedad es cierta para el conjunto vacío, y si es cierta para un conjunto finito +entonceses cierta para el conjunto obtenido añadiendo un elemento, entonces es cierta +para cualquier conjunto finito. + +Veamos el ejemplo de lo que ocurre con la unión de cerrados en una topología +-/ + +example + (X : Type) + (P : Set X → Prop) + (hu : ∀ A B : Set X, P A → P B → P (A ∪ B)) + (S : Set (Set X)) + (hSI : ∀ x ∈ S, P x) + (h0 : P ∅ ) + (hfin : Set.Finite S) : + P (⋃₀ S) := by + + revert hSI -- esto es necesario porque queremos "arrastrar" la hipótesis a la inducción + induction' S, hfin using Set.Finite.induction_on with a T ha hT huT hSI + . simp only [Set.sUnion_empty] + intro h + exact h0 + . simp only [Set.sUnion_insert] + intro h + apply hu + . apply h + left + rfl + · apply huT + intro x hx + apply h + right + exact hx + +-- Para ver el recíproco, símplemente hay que ver que los conjuntos de dos elementos son finitos + + +example (X : Type) (a b : X) : Set.Finite ({a, b} : Set X) := by + exact toFinite {a, b} + +-- y que la unión de dos conjuntos es lo mismo que la unión del conjunto formado por ambos + +example (X : Type) (a b : Set X) : a ∪ b = ⋃₀ ({a , b} : Set (Set X)) := by + rw [sUnion_insert] + rw [sUnion_singleton] + + +/- +# Ejercicio + +Demuestra que todo conjunto finito no vacío de los naturales tiene un elemento maximal + +(puede ser útil la ráctica `linarith`, que intenta demostrar (des)igualdades que se puedan deducir +mediante operaciones lineales) +-/ + +example ( S : Set ℕ ) (hf : Set.Finite S) : S ≠ ∅ → ∃ m ∈ S, ∀ n ∈ S, n ≤ m := by + sorry diff --git a/Curso2026/Inductivos.lean b/Curso2026/Inductivos.lean new file mode 100644 index 0000000..084edf3 --- /dev/null +++ b/Curso2026/Inductivos.lean @@ -0,0 +1,187 @@ +import Mathlib.Tactic + +/- +# Tipos inductivos + +Los tipos inductivos son tipos en los que cada objeto se obtiene mediante una o varias +funciones. Estas funciones pueden no tomar ninguna entrada (casos primitivos) o pueden tomar +como entradas otros objetos de ese mismo tipo. + +El ejemplo más habitual es el de los números naturales: cada número natural es uno (y sólo uno) +de estos casos: +- El número 0. +- El siguiente de otro número natural. + +Y además, usando estas funciones, se obtienen exactamente todos los naturales: 1 es el siguiente de 0 +2 es el siguiente de 1... + +Podemos definir el tipo de los naturales así: +-/ + + +inductive natural + | cero : natural + | siguiente : natural → natural + +open natural + +instance : Zero natural := { zero := cero } + +-- a partir de ahora, podemos usar "cero" y "siguiente" en lugar de "natural.cero" y "natural.siguiente" + + + +/- +Se pueden definir funciones (o demostrar teoremas) sobre un tipo inductivo, diciendo +como proceder en cada uno de sus casos: +-/ + +def suma : natural → natural → natural + | n, 0 => n + | n, siguiente m => siguiente (suma n m) + + + +/- +Esto lo hacemos para poder usar "a + b" en lugar de "suma a b" +-/ + +instance : Add natural := { add := suma } + +@[simp] +lemma suma_cero (n : natural) : n + 0 = n := by + rfl + +@[simp] +lemma suma_siguiente ( n m : natural) : n + (siguiente m) = siguiente ( n + m ) := by + rfl + + +/- +Con tipos inductivos, se puede usar el principio de inducción: demostrando el teorema +para cada posible forma de construir un elemento del tipo, usando la hipótesis de que +el teorema es cierto para los objetos que se usan en la construcción. + +Por definición tenemos que n + 0 = n, veamos que 0 + n = n +-/ + +@[simp] +lemma cerosuma (n : natural) : 0 + n = n := by + induction' n with n h -- como lo queremos ver para todo n, veamos los posibles casos + · rfl + · rw [suma_siguiente] -- aplicamos la definición de suma de un siguiente + rw [h] + +/- +Veamos algunas propiedades más de la suma de naturales +-/ + +@[simp] +lemma sigsuma (n m : natural) : (siguiente n) + m = siguiente (n + m) := by + induction' m with m h + · rfl + · rw [suma_siguiente] + rw [h] + rw [suma_siguiente] + + +/- +Usando lo anterior, podemos demostrar que la suma es conmutativa +-/ + +lemma sumacomm (n m : natural) : n + m = m + n := by + induction' n with n h + · change 0 + m = m + 0 + simp only [suma_cero, eq_self_iff_true, cerosuma] + · simp only [sigsuma, suma_siguiente, h ] + + +/- +Y asociativa +-/ + +@[simp] +lemma sumaasoc (a b c : natural) : a + (b + c) = a + b + c:= by + induction' c with c h + · rfl + · simp only [suma_siguiente, h] + +/- +# Ejercicios + +Define el producto de números naturales, y demuestra algunas de sus propiedades: + +- Multiplicar por cero (a derecha e izquierda) da cero. +- El uno (siguiente del cero), es elemento neutro del producto (a derecha e izquierda) +- La propuedad distributiva +-/ + + +def mul : natural → natural → natural +| n, cero => sorry +| n, (siguiente m ) => sorry + +instance : Mul natural := ⟨ mul⟩ + +@[simp] +lemma mul_cero (n : natural) : n * 0 = 0 := by + sorry + +@[simp] +lemma mul_siguiente (n m : natural) : n * siguiente m = n * m + n := by + sorry + +@[simp] +lemma mulcero (n : natural ) : 0 * n = 0 := by + sorry + +def uno := siguiente cero + +instance : One natural := ⟨ uno⟩ + +@[simp] +lemma muluno (n : natural ) : n * 1 = n := by + sorry + +@[simp] +lemma unomul (n : natural ) : 1 * n = n := by + sorry + +@[simp] +lemma mul_suma (a b c : natural) : a * (b + c) = a * b + a * c := by + sorry + +/- +Aquí puede ser útil la tática `calc`, que permite razonar (des)igualdades en varios pasos +justificando cada paso. + +Por ejemplo, si estamos en un momento en que hay que demostrar que +`a * c + b * c + a + b = a * c + a + b * c + b ` se puede hacer así: + + +calc +a * c + b * c + a + b = a * c + (b * c + a) + b := by simp +_ = a * c + (a + b * c)+ b := by rw [sumacomm a (b *c)] +_ = a * c + a + b * c + b := by simp + +-/ +@[simp] +lemma suma_mul (a b c : natural) : (a + b) * c = a * c + b * c := by + sorry + + +/- +# Nota: + +Los números naturales ya vienen definidos de serie en lean como el tipo `nat`,y muchas de sus propiedades +están demostradas en mathlib. Además, viene de serie con varias notaciones útiles, se pueden +usar los numerales habituales, etc. +-/ + + +/- +# Ejercicio extra + +Define algún otro tipo inductivo. Por ejemplo, las listas de números naturales. Piensa que una lista +es o bien la lista vacía, o bien el resultado de añadir un elemento a una lista más corta. +-/ diff --git a/Curso2026/Naturales.lean b/Curso2026/Naturales.lean new file mode 100644 index 0000000..b4bd195 --- /dev/null +++ b/Curso2026/Naturales.lean @@ -0,0 +1,161 @@ +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