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.
-/