188 lines
4.5 KiB
Plaintext
188 lines
4.5 KiB
Plaintext
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.
|
|
-/
|