# Etiqueta: IH.induct

## Pruebas de equivalencia de definiciones de inversa

En Lean, está definida la función

` reverse : list α → list α`

tal que (reverse xs) es la lista obtenida invirtiendo el orden de los elementos de xs. Por ejemplo,

` reverse [3,2,5,1] = [1,5,2,3]`

Su definición es

``` def reverse_core : list α → list α → list α | [] r := r | (a::l) r := reverse_core l (a::r)   def reverse : list α → list α := λ l, reverse_core l []```

Una definición alternativa es

``` def inversa : list α → list α | [] := [] | (x :: xs) := inversa xs ++ [x]```

Demostrar que las dos definiciones son equivalentes; es decir,

` reverse xs = inversa xs`

Para ello, completar la siguiente teoría de Lean:

```import data.list.basic open list   variable {α : Type*} variable (x : α) variables (xs ys : list α)   def inversa : list α → list α | [] := [] | (x :: xs) := inversa xs ++ [x]   example : reverse xs = inversa xs := sorry```
Soluciones con Lean
```import data.list.basic open list   variable {α : Type*} variable (x : α) variables (xs ys : list α)   -- Definición y reglas de simplificación de inversa -- ================================================   def inversa : list α → list α | [] := [] | (x :: xs) := inversa xs ++ [x]   @[simp] lemma inversa_nil : inversa ([] : list α) = [] := rfl   @[simp] lemma inversa_cons : inversa (x :: xs) = inversa xs ++ [x] := rfl   -- Reglas de simplificación de reverse_core -- ========================================   @[simp] lemma reverse_core_nil : reverse_core [] ys = ys := rfl   @[simp] lemma reverse_core_cons : reverse_core (x :: xs) ys = reverse_core xs (x :: ys) := rfl   -- Lema auxiliar: reverse_core xs ys = (inversa xs) ++ ys -- ======================================================   -- 1ª demostración del lema auxiliar example : reverse_core xs ys = (inversa xs) ++ ys := begin induction xs with a as HI generalizing ys, { calc reverse_core [] ys = ys : reverse_core_nil ys ... = [] ++ ys : (nil_append ys).symm ... = inversa [] ++ ys : congr_arg2 (++) inversa_nil.symm rfl, }, { calc reverse_core (a :: as) ys = reverse_core as (a :: ys) : reverse_core_cons a as ys ... = inversa as ++ (a :: ys) : (HI (a :: ys)) ... = inversa as ++ ([a] ++ ys) : congr_arg2 (++) rfl singleton_append ... = (inversa as ++ [a]) ++ ys : (append_assoc (inversa as) [a] ys).symm ... = inversa (a :: as) ++ ys : congr_arg2 (++) (inversa_cons a as).symm rfl}, end   -- 2ª demostración del lema auxiliar example : reverse_core xs ys = (inversa xs) ++ ys := begin induction xs with a as HI generalizing ys, { calc reverse_core [] ys = ys : by rw reverse_core_nil ... = [] ++ ys : by rw nil_append ... = inversa [] ++ ys : by rw inversa_nil }, { calc reverse_core (a :: as) ys = reverse_core as (a :: ys) : by rw reverse_core_cons ... = inversa as ++ (a :: ys) : by rw (HI (a :: ys)) ... = inversa as ++ ([a] ++ ys) : by rw singleton_append ... = (inversa as ++ [a]) ++ ys : by rw append_assoc ... = inversa (a :: as) ++ ys : by rw inversa_cons }, end   -- 3ª demostración del lema auxiliar example : reverse_core xs ys = (inversa xs) ++ ys := begin induction xs with a as HI generalizing ys, { calc reverse_core [] ys = ys : rfl ... = [] ++ ys : rfl ... = inversa [] ++ ys : rfl }, { calc reverse_core (a :: as) ys = reverse_core as (a :: ys) : rfl ... = inversa as ++ (a :: ys) : (HI (a :: ys)) ... = inversa as ++ ([a] ++ ys) : rfl ... = (inversa as ++ [a]) ++ ys : by rw append_assoc ... = inversa (a :: as) ++ ys : rfl }, end   -- 3ª demostración del lema auxiliar example : reverse_core xs ys = (inversa xs) ++ ys := begin induction xs with a as HI generalizing ys, { calc reverse_core [] ys = ys : by simp ... = [] ++ ys : by simp ... = inversa [] ++ ys : by simp }, { calc reverse_core (a :: as) ys = reverse_core as (a :: ys) : by simp ... = inversa as ++ (a :: ys) : (HI (a :: ys)) ... = inversa as ++ ([a] ++ ys) : by simp ... = (inversa as ++ [a]) ++ ys : by simp ... = inversa (a :: as) ++ ys : by simp }, end   -- 4ª demostración del lema auxiliar example : reverse_core xs ys = (inversa xs) ++ ys := begin induction xs with a as HI generalizing ys, { by simp, }, { calc reverse_core (a :: as) ys = reverse_core as (a :: ys) : by simp ... = inversa as ++ (a :: ys) : (HI (a :: ys)) ... = inversa (a :: as) ++ ys : by simp }, end   -- 5ª demostración del lema auxiliar example : reverse_core xs ys = (inversa xs) ++ ys := begin induction xs with a as HI generalizing ys, { simp, }, { simp [HI (a :: ys)], }, end   -- 6ª demostración del lema auxiliar example : reverse_core xs ys = (inversa xs) ++ ys := by induction xs generalizing ys ; simp [*]   -- 7ª demostración del lema auxiliar example : reverse_core xs ys = (inversa xs) ++ ys := begin induction xs with a as HI generalizing ys, { rw reverse_core_nil, rw inversa_nil, rw nil_append, }, { rw reverse_core_cons, rw (HI (a :: ys)), rw inversa_cons, rw append_assoc, rw singleton_append, }, end   -- 8ª demostración del lema auxiliar @[simp] lemma inversa_equiv : ∀ xs : list α, ∀ ys, reverse_core xs ys = (inversa xs) ++ ys | [] := by simp | (a :: as) := by simp [inversa_equiv as]   -- Demostraciones del lema principal -- =================================   -- 1ª demostración example : reverse xs = inversa xs := calc reverse xs = reverse_core xs [] : rfl ... = inversa xs ++ [] : by rw inversa_equiv ... = inversa xs : by rw append_nil   -- 2ª demostración example : reverse xs = inversa xs := by simp [inversa_equiv, reverse]   -- 3ª demostración example : reverse xs = inversa xs := by simp [reverse]```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory Pruebas_de_equivalencia_de_definiciones_de_inversa imports Main begin   (* Definición alternativa *) (* ====================== *)   fun inversa_aux :: "'a list ⇒ 'a list ⇒ 'a list" where "inversa_aux [] ys = ys" | "inversa_aux (x#xs) ys = inversa_aux xs (x#ys)"   fun inversa :: "'a list ⇒ 'a list" where "inversa xs = inversa_aux xs []"   (* Lema auxiliar: inversa_aux xs ys = (rev xs) @ ys *) (* ================================================ *)   (* 1ª demostración del lema auxiliar *) lemma "inversa_aux xs ys = (rev xs) @ ys" proof (induct xs arbitrary: ys) fix ys :: "'a list" have "inversa_aux [] ys = ys" by (simp only: inversa_aux.simps(1)) also have "… = [] @ ys" by (simp only: append.simps(1)) also have "… = rev [] @ ys" by (simp only: rev.simps(1)) finally show "inversa_aux [] ys = rev [] @ ys" by this next fix a ::'a and xs :: "'a list" assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys" show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys" proof - fix ys have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)" by (simp only: inversa_aux.simps(2)) also have "… = rev xs@(a#ys)" by (simp only: HI) also have "… = rev xs @ ([a] @ ys)" by (simp only: append.simps) also have "… = (rev xs @ [a]) @ ys" by (simp only: append_assoc) also have "… = rev (a # xs) @ ys" by (simp only: rev.simps(2)) finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" by this qed qed   (* 2ª demostración del lema auxiliar *) lemma "inversa_aux xs ys = (rev xs) @ ys" proof (induct xs arbitrary: ys) fix ys :: "'a list" have "inversa_aux [] ys = ys" by simp also have "… = [] @ ys" by simp also have "… = rev [] @ ys" by simp finally show "inversa_aux [] ys = rev [] @ ys" . next fix a ::'a and xs :: "'a list" assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys" show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys" proof - fix ys have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)" by simp also have "… = rev xs@(a#ys)" using HI by simp also have "… = rev xs @ ([a] @ ys)" by simp also have "… = (rev xs @ [a]) @ ys" by simp also have "… = rev (a # xs) @ ys" by simp finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" . qed qed   (* 3ª demostración del lema auxiliar *) lemma "inversa_aux xs ys = (rev xs) @ ys" proof (induct xs arbitrary: ys) fix ys :: "'a list" show "inversa_aux [] ys = rev [] @ ys" by simp next fix a ::'a and xs :: "'a list" assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys" show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys" proof - fix ys have "inversa_aux (a#xs) ys = rev xs@(a#ys)" using HI by simp also have "… = rev (a # xs) @ ys" by simp finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" . qed qed   (* 4ª demostración del lema auxiliar *) lemma "inversa_aux xs ys = (rev xs) @ ys" proof (induct xs arbitrary: ys) show "⋀ys. inversa_aux [] ys = rev [] @ ys" by simp next fix a ::'a and xs :: "'a list" assume "⋀ys. inversa_aux xs ys = rev xs@ys" then show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys" by simp qed   (* 5ª demostración del lema auxiliar *) lemma "inversa_aux xs ys = (rev xs) @ ys" proof (induct xs arbitrary: ys) case Nil then show ?case by simp next case (Cons a xs) then show ?case by simp qed   (* 6ª demostración del lema auxiliar *) lemma inversa_equiv: "inversa_aux xs ys = (rev xs) @ ys" by (induct xs arbitrary: ys) simp_all   (* Demostraciones del lema principal *) (* ================================= *)   (* 1ª demostración *) lemma "inversa xs = rev xs" proof - have "inversa xs = inversa_aux xs []" by (rule inversa.simps) also have "… = (rev xs) @ []" by (rule inversa_equiv) also have "… = rev xs" by (rule append.right_neutral) finally show "inversa xs = rev xs" by this qed   (* 2ª demostración *) lemma "inversa xs = rev xs" proof - have "inversa xs = inversa_aux xs []" by simp also have "… = (rev xs) @ []" by (rule inversa_equiv) also have "… = rev xs" by simp finally show "inversa xs = rev xs" . qed   (* 3ª demostración *) lemma "inversa xs = rev xs" by (simp add: inversa_equiv)   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## Pruebas de take n xs ++ drop n xs = xs

En Lean están definidas las funciones

``` take : nat → list α → nat drop : nat → list α → nat (++) : list α → list α → list α```

tales que

• (take n xs) es la lista formada por los n primeros elementos de xs. Por ejemplo,
` take 2 [3,5,1,9,7] = [3,5]`
• (drop n xs) es la lista formada eliminando los n primeros elementos de xs. Por ejemplo,
` drop 2 [3,5,1,9,7] = [1,9,7]`
• (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.
` [3,5] ++ [1,9,7] = [3,5,1,9,7]`

Dichas funciones están caracterizadas por los siguientes lemas:

``` take_zero : take 0 xs = [] take_nil : take n [] = [] take_cons : take (succ n) (x :: xs) = x :: take n xs drop_zero : drop 0 xs = xs drop_nil : drop n [] = [] drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys)```

Demostrar que

` take n xs ++ drop n xs = xs`

Para ello, completar la siguiente teoría de Lean:

```import data.list.basic import tactic open list nat   variable {α : Type} variable (x : α) variable (xs : list α) variable (n : ℕ)   lemma drop_zero : drop 0 xs = xs := rfl lemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl   example : take n xs ++ drop n xs = xs := sorry```
Soluciones con Lean
```import data.list.basic import tactic open list open nat   variable {α : Type} variable (n : ℕ) variable (x : α) variable (xs : list α)   lemma drop_zero : drop 0 xs = xs := rfl lemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl   -- 1ª demostración example : take n xs ++ drop n xs = xs := begin induction n with m HI1 generalizing xs, { rw take_zero, rw drop_zero, rw nil_append, }, { induction xs with a as HI2, { rw take_nil, rw drop_nil, rw nil_append, }, { rw take_cons, rw drop_cons, rw cons_append, rw (HI1 as), }, }, end   -- 2ª demostración example : take n xs ++ drop n xs = xs := begin induction n with m HI1 generalizing xs, { calc take 0 xs ++ drop 0 xs = [] ++ drop 0 xs : by rw take_zero ... = [] ++ xs : by rw drop_zero ... = xs : by rw nil_append, }, { induction xs with a as HI2, { calc take (succ m) [] ++ drop (succ m) [] = ([] : list α) ++ drop (succ m) [] : by rw take_nil ... = [] ++ [] : by rw drop_nil ... = [] : by rw nil_append, }, { calc take (succ m) (a :: as) ++ drop (succ m) (a :: as) = (a :: take m as) ++ drop (succ m) (a :: as) : by rw take_cons ... = (a :: take m as) ++ drop m as : by rw drop_cons ... = a :: (take m as ++ drop m as) : by rw cons_append ... = a :: as : by rw (HI1 as), }, }, end   -- 3ª demostración example : take n xs ++ drop n xs = xs := begin induction n with m HI1 generalizing xs, { simp, }, { induction xs with a as HI2, { simp, }, { simp [HI1 as], }, }, end   -- 4ª demostración lemma conc_take_drop_1 : ∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs | 0 xs := by calc take 0 xs ++ drop 0 xs = [] ++ drop 0 xs : by rw take_zero ... = [] ++ xs : by rw drop_zero ... = xs : by rw nil_append | (succ m) [] := by calc take (succ m) [] ++ drop (succ m) [] = ([] : list α) ++ drop (succ m) [] : by rw take_nil ... = [] ++ [] : by rw drop_nil ... = [] : by rw nil_append | (succ m) (a :: as) := by calc take (succ m) (a :: as) ++ drop (succ m) (a :: as) = (a :: take m as) ++ drop (succ m) (a :: as) : by rw take_cons ... = (a :: take m as) ++ drop m as : by rw drop_cons ... = a :: (take m as ++ drop m as) : by rw cons_append ... = a :: as : by rw conc_take_drop_1   -- 5ª demostración lemma conc_take_drop_2 : ∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs | 0 xs := by simp | (succ m) [] := by simp | (succ m) (a :: as) := by simp [conc_take_drop_2]   -- 6ª demostración lemma conc_take_drop_3 : ∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs | 0 xs := rfl | (succ m) [] := rfl | (succ m) (a :: as) := congr_arg (cons a) (conc_take_drop_3 m as)   -- 7ª demostración example : take n xs ++ drop n xs = xs := -- by library_search take_append_drop n xs   -- 8ª demostración example : take n xs ++ drop n xs = xs := by simp```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory "Pruebas_de_take_n_xs_++_drop_n_xs_Ig_xs" imports Main begin   fun take' :: "nat ⇒ 'a list ⇒ 'a list" where "take' n [] = []" | "take' 0 xs = []" | "take' (Suc n) (x#xs) = x # (take' n xs)"   fun drop' :: "nat ⇒ 'a list ⇒ 'a list" where "drop' n [] = []" | "drop' 0 xs = xs" | "drop' (Suc n) (x#xs) = drop' n xs"   (* 1ª demostración *) lemma "take' n xs @ drop' n xs = xs" proof (induct rule: take'.induct) fix n have "take' n [] @ drop' n [] = [] @ drop' n []" by (simp only: take'.simps(1)) also have "… = drop' n []" by (simp only: append.simps(1)) also have "… = []" by (simp only: drop'.simps(1)) finally show "take' n [] @ drop' n [] = []" by this next fix x :: 'a and xs :: "'a list" have "take' 0 (x#xs) @ drop' 0 (x#xs) = [] @ drop' 0 (x#xs)" by (simp only: take'.simps(2)) also have "… = drop' 0 (x#xs)" by (simp only: append.simps(1)) also have "… = x # xs" by (simp only: drop'.simps(2)) finally show "take' 0 (x#xs) @ drop' 0 (x#xs) = x#xs" by this next fix n :: nat and x :: 'a and xs :: "'a list" assume HI: "take' n xs @ drop' n xs = xs" have "take' (Suc n) (x # xs) @ drop' (Suc n) (x # xs) = (x # (take' n xs)) @ drop' n xs" by (simp only: take'.simps(3) drop'.simps(3)) also have "… = x # (take' n xs @ drop' n xs)" by (simp only: append.simps(2)) also have "… = x#xs" by (simp only: HI) finally show "take' (Suc n) (x#xs) @ drop' (Suc n) (x#xs) = x#xs" by this qed   (* 2ª demostración *) lemma "take' n xs @ drop' n xs = xs" proof (induct rule: take'.induct) case (1 n) then show ?case by simp next case (2 x xs) then show ?case by simp next case (3 n x xs) then show ?case by simp qed   (* 3ª demostración *) lemma "take' n xs @ drop' n xs = xs" by (induct rule: take'.induct) simp_all   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## Pruebas de length (xs ++ ys) = length xs + length ys

En Lean están definidas las funciones

``` length : list α → nat (++) : list α → list α → list α```

tales que

• (length xs) es la longitud de xs. Por ejemplo,
` length [2,3,5,3] = 4`
• (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.
` [1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]`

Dichas funciones están caracterizadas por los siguientes lemas:

``` length_nil : length [] = 0 length_cons : length (x :: xs) = length xs + 1 nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys)```

Demostrar que

` length (xs ++ ys) = length xs + length ys`

Para ello, completar la siguiente teoría de Lean:

```import tactic open list   variable {α : Type} variable (x : α) variables (xs ys zs : list α)   lemma length_nil : length ([] : list α) = 0 := rfl   example : length (xs ++ ys) = length xs + length ys := sorry```
Soluciones con Lean
```import tactic open list   variable {α : Type} variable (x : α) variables (xs ys zs : list α)   lemma length_nil : length ([] : list α) = 0 := rfl   -- 1ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { rw nil_append, rw length_nil, rw zero_add, }, { rw cons_append, rw length_cons, rw HI, rw length_cons, rw add_assoc, rw add_comm (length ys), rw add_assoc, }, end   -- 2ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { rw nil_append, rw length_nil, rw zero_add, }, { rw cons_append, rw length_cons, rw HI, rw length_cons, -- library_search, exact add_right_comm (length as) (length ys) 1 }, end   -- 3ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { rw nil_append, rw length_nil, rw zero_add, }, { rw cons_append, rw length_cons, rw HI, rw length_cons, -- by hint, linarith, }, end   -- 4ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { simp, }, { simp [HI], linarith, }, end   -- 5ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { simp, }, { finish [HI],}, end   -- 6ª demostración example : length (xs ++ ys) = length xs + length ys := by induction xs ; finish [*]   -- 7ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { calc length ([] ++ ys) = length ys : congr_arg length (nil_append ys) ... = 0 + length ys : (zero_add (length ys)).symm ... = length [] + length ys : congr_arg2 (+) length_nil.symm rfl, }, { calc length ((a :: as) ++ ys) = length (a :: (as ++ ys)) : congr_arg length (cons_append a as ys) ... = length (as ++ ys) + 1 : length_cons a (as ++ ys) ... = (length as + length ys) + 1 : congr_arg2 (+) HI rfl ... = (length as + 1) + length ys : add_right_comm (length as) (length ys) 1 ... = length (a :: as) + length ys : congr_arg2 (+) (length_cons a as).symm rfl, }, end   -- 8ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { calc length ([] ++ ys) = length ys : by rw nil_append ... = 0 + length ys : (zero_add (length ys)).symm ... = length [] + length ys : by rw length_nil }, { calc length ((a :: as) ++ ys) = length (a :: (as ++ ys)) : by rw cons_append ... = length (as ++ ys) + 1 : by rw length_cons ... = (length as + length ys) + 1 : by rw HI ... = (length as + 1) + length ys : add_right_comm (length as) (length ys) 1 ... = length (a :: as) + length ys : by rw length_cons, }, end   -- 9ª demostración example : length (xs ++ ys) = length xs + length ys := list.rec_on xs ( show length ([] ++ ys) = length [] + length ys, from calc length ([] ++ ys) = length ys : by rw nil_append ... = 0 + length ys : by exact (zero_add (length ys)).symm ... = length [] + length ys : by rw length_nil ) ( assume a as, assume HI : length (as ++ ys) = length as + length ys, show length ((a :: as) ++ ys) = length (a :: as) + length ys, from calc length ((a :: as) ++ ys) = length (a :: (as ++ ys)) : by rw cons_append ... = length (as ++ ys) + 1 : by rw length_cons ... = (length as + length ys) + 1 : by rw HI ... = (length as + 1) + length ys : by exact add_right_comm (length as) (length ys) 1 ... = length (a :: as) + length ys : by rw length_cons)   -- 10ª demostración example : length (xs ++ ys) = length xs + length ys := list.rec_on xs ( by simp) ( λ a as HI, by simp [HI, add_right_comm])   -- 11ª demostración lemma longitud_conc_1 : ∀ xs, length (xs ++ ys) = length xs + length ys | [] := by calc length ([] ++ ys) = length ys : by rw nil_append ... = 0 + length ys : by rw zero_add ... = length [] + length ys : by rw length_nil | (a :: as) := by calc length ((a :: as) ++ ys) = length (a :: (as ++ ys)) : by rw cons_append ... = length (as ++ ys) + 1 : by rw length_cons ... = (length as + length ys) + 1 : by rw longitud_conc_1 ... = (length as + 1) + length ys : by exact add_right_comm (length as) (length ys) 1 ... = length (a :: as) + length ys : by rw length_cons   -- 12ª demostración lemma longitud_conc_2 : ∀ xs, length (xs ++ ys) = length xs + length ys | [] := by simp | (a :: as) := by simp [longitud_conc_2 as, add_right_comm]   -- 13ª demostración example : length (xs ++ ys) = length xs + length ys := -- by library_search length_append xs ys   -- 14ª demostración example : length (xs ++ ys) = length xs + length ys := by simp```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory "Pruebas_de_length(xs_++_ys)_Ig_length_xs+length_ys" imports Main begin   (* 1ª demostración *) lemma "length (xs @ ys) = length xs + length ys" proof (induct xs) have "length ([] @ ys) = length ys" by (simp only: append_Nil) also have "… = 0 + length ys" by (rule add_0 [symmetric]) also have "… = length [] + length ys" by (simp only: list.size(3)) finally show "length ([] @ ys) = length [] + length ys" by this next fix x xs assume HI : "length (xs @ ys) = length xs + length ys" have "length ((x # xs) @ ys) = length (x # (xs @ ys))" by (simp only: append_Cons) also have "… = length (xs @ ys) + 1" by (simp only: list.size(4)) also have "… = (length xs + length ys) + 1" by (simp only: HI) also have "… = (length xs + 1) + length ys" by (simp only: add.assoc add.commute) also have "… = length (x # xs) + length ys" by (simp only: list.size(4)) then show "length ((x # xs) @ ys) = length (x # xs) + length ys" by simp qed   (* 2ª demostración *) lemma "length (xs @ ys) = length xs + length ys" proof (induct xs) show "length ([] @ ys) = length [] + length ys" by simp next fix x xs assume "length (xs @ ys) = length xs + length ys" then show "length ((x # xs) @ ys) = length (x # xs) + length ys" by simp qed   (* 3ª demostración *) lemma "length (xs @ ys) = length xs + length ys" proof (induct xs) case Nil then show ?case by simp next case (Cons a xs) then show ?case by simp qed   (* 4ª demostración *) lemma "length (xs @ ys) = length xs + length ys" by (induct xs) simp_all   (* 5ª demostración *) lemma "length (xs @ ys) = length xs + length ys" by (fact length_append)   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## Asociatividad de la concatenación de listas

En Lean la operación de concatenación de listas se representa por (++) y está caracterizada por los siguientes lemas

``` nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys)```

Demostrar que la concatenación es asociativa; es decir,

` xs ++ (ys ++ zs) = (xs ++ ys) ++ zs`

Para ello, completar la siguiente teoría de Lean:

```import data.list.basic import tactic open list   variable {α : Type} variable (x : α) variables (xs ys zs : list α)   example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := sorry```
Soluciones con Lean
```import data.list.basic import tactic open list   variable {α : Type} variable (x : α) variables (xs ys zs : list α)   -- 1ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : append.equations._eqn_1 (ys ++ zs) ... = ([] ++ ys) ++ zs : congr_arg2 (++) (append.equations._eqn_1 ys) rfl, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : append.equations._eqn_2 a as (ys ++ zs) ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI ... = (a :: (as ++ ys)) ++ zs : (append.equations._eqn_2 a (as ++ ys) zs).symm ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (append.equations._eqn_2 a as ys).symm rfl, }, end   -- 2ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : nil_append (ys ++ zs) ... = ([] ++ ys) ++ zs : congr_arg2 (++) (nil_append ys) rfl, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : cons_append a as (ys ++ zs) ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI ... = (a :: (as ++ ys)) ++ zs : (cons_append a (as ++ ys) zs).symm ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (cons_append a as ys).symm rfl, }, end   -- 3ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : by rw nil_append ... = ([] ++ ys) ++ zs : by rw nil_append, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : by rw cons_append ... = a :: ((as ++ ys) ++ zs) : by rw HI ... = (a :: (as ++ ys)) ++ zs : by rw cons_append ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append, }, end   -- 4ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : rfl ... = ([] ++ ys) ++ zs : rfl, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : rfl ... = a :: ((as ++ ys) ++ zs) : by rw HI ... = (a :: (as ++ ys)) ++ zs : rfl ... = ((a :: as) ++ ys) ++ zs : rfl, }, end   -- 5ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : by simp ... = ([] ++ ys) ++ zs : by simp, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : by simp ... = a :: ((as ++ ys) ++ zs) : congr_arg (cons a) HI ... = (a :: (as ++ ys)) ++ zs : by simp ... = ((a :: as) ++ ys) ++ zs : by simp, }, end   -- 6ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { by simp, }, { by exact (cons_inj a).mpr HI, }, end   -- 7ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { rw nil_append, rw nil_append, }, { rw cons_append, rw HI, rw cons_append, rw cons_append, }, end   -- 8ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := list.rec_on xs ( show [] ++ (ys ++ zs) = ([] ++ ys) ++ zs, from calc [] ++ (ys ++ zs) = ys ++ zs : by rw nil_append ... = ([] ++ ys) ++ zs : by rw nil_append ) ( assume a as, assume HI : as ++ (ys ++ zs) = (as ++ ys) ++ zs, show (a :: as) ++ (ys ++ zs) = ((a :: as) ++ ys) ++ zs, from calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : by rw cons_append ... = a :: ((as ++ ys) ++ zs) : by rw HI ... = (a :: (as ++ ys)) ++ zs : by rw cons_append ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append)   -- 9ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := list.rec_on xs (by simp) (by simp [*])   -- 10ª demostración lemma conc_asoc_1 : ∀ xs, xs ++ (ys ++ zs) = (xs ++ ys) ++ zs | [] := by calc [] ++ (ys ++ zs) = ys ++ zs : by rw nil_append ... = ([] ++ ys) ++ zs : by rw nil_append | (a :: as) := by calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : by rw cons_append ... = a :: ((as ++ ys) ++ zs) : by rw conc_asoc_1 ... = (a :: (as ++ ys)) ++ zs : by rw cons_append ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append   -- 11ª demostración example : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := -- by library_search append_assoc xs ys zs   -- 12ª demostración example : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by induction xs ; simp [*]   -- 13ª demostración example : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by simp```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory Asociatividad_de_la_concatenacion_de_listas imports Main begin   (* 1ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" proof (induct xs) have "[] @ (ys @ zs) = ys @ zs" by (simp only: append_Nil) also have "… = ([] @ ys) @ zs" by (simp only: append_Nil) finally show "[] @ (ys @ zs) = ([] @ ys) @ zs" by this next fix x xs assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs" have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))" by (simp only: append_Cons) also have "… = x # ((xs @ ys) @ zs)" by (simp only: HI) also have "… = (x # (xs @ ys)) @ zs" by (simp only: append_Cons) also have "… = ((x # xs) @ ys) @ zs" by (simp only: append_Cons) finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" by this qed   (* 2ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" proof (induct xs) have "[] @ (ys @ zs) = ys @ zs" by simp also have "… = ([] @ ys) @ zs" by simp finally show "[] @ (ys @ zs) = ([] @ ys) @ zs" . next fix x xs assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs" have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))" by simp also have "… = x # ((xs @ ys) @ zs)" by simp also have "… = (x # (xs @ ys)) @ zs" by simp also have "… = ((x # xs) @ ys) @ zs" by simp finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" . qed   (* 3ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" proof (induct xs) show "[] @ (ys @ zs) = ([] @ ys) @ zs" by simp next fix x xs assume "xs @ (ys @ zs) = (xs @ ys) @ zs" then show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" by simp qed   (* 4ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" proof (induct xs) case Nil then show ?case by simp next case (Cons a xs) then show ?case by simp qed   (* 5ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" by (rule append_assoc [symmetric])   (* 6ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" by (induct xs) simp_all   (* 7ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" by simp   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## Pruebas de length (repeat x n) = n

En Lean están definidas las funciones length y repeat tales que

• (length xs) es la longitud de la lista xs. Por ejemplo,
` length [1,2,5,2] = 4`
• (repeat x n) es la lista que tiene el elemento x n veces. Por ejemplo,
` repeat 7 3 = [7, 7, 7]`

Demostrar que

` length (repeat x n) = n`

Para ello, completar la siguiente teoría de Lean:

```import data.list.basic open nat open list   variable {α : Type} variable (x : α) variable (n : ℕ)   example : length (repeat x n) = n := sorry```
Soluciones con Lean
```import data.list.basic open nat open list   set_option pp.structure_projections false   variable {α : Type} variable (x : α) variable (n : ℕ)   -- 1ª demostración example : length (repeat x n) = n := begin induction n with n HI, { calc length (repeat x 0) = length [] : congr_arg length (repeat.equations._eqn_1 x) ... = 0 : length.equations._eqn_1 }, { calc length (repeat x (succ n)) = length (x :: repeat x n) : congr_arg length (repeat.equations._eqn_2 x n) ... = length (repeat x n) + 1 : length.equations._eqn_2 x (repeat x n) ... = n + 1 : congr_arg2 (+) HI rfl ... = succ n : rfl, }, end   -- 2ª demostración example : length (repeat x n) = n := begin induction n with n HI, { calc length (repeat x 0) = length [] : rfl ... = 0 : rfl }, { calc length (repeat x (succ n)) = length (x :: repeat x n) : rfl ... = length (repeat x n) + 1 : rfl ... = n + 1 : by rw HI ... = succ n : rfl, }, end   -- 3ª demostración example : length (repeat x n) = n := begin induction n with n HI, { refl, }, { dsimp, rw HI, }, end   -- 4ª demostración example : length (repeat x n) = n := begin induction n with n HI, { simp, }, { simp [HI], }, end   -- 5ª demostración example : length (repeat x n) = n := by induction n ; simp [*]   -- 6ª demostración example : length (repeat x n) = n := nat.rec_on n ( show length (repeat x 0) = 0, from calc length (repeat x 0) = length [] : rfl ... = 0 : rfl ) ( assume n, assume HI : length (repeat x n) = n, show length (repeat x (succ n)) = succ n, from calc length (repeat x (succ n)) = length (x :: repeat x n) : rfl ... = length (repeat x n) + 1 : rfl ... = n + 1 : by rw HI ... = succ n : rfl )   -- 7ª demostración example : length (repeat x n) = n := nat.rec_on n ( by simp ) ( λ n HI, by simp [HI])   -- 8ª demostración example : length (repeat x n) = n := length_repeat x n   -- 9ª demostración example : length (repeat x n) = n := by simp   -- 10ª demostración lemma length_repeat_1 : ∀ n, length (repeat x n) = n | 0 := by calc length (repeat x 0) = length ([] : list α) : rfl ... = 0 : rfl | (n+1) := by calc length (repeat x (n + 1)) = length (x :: repeat x n) : rfl ... = length (repeat x n) + 1 : rfl ... = n + 1 : by rw length_repeat_1   -- 11ª demostración lemma length_repeat_2 : ∀ n, length (repeat x n) = n | 0 := by simp | (n+1) := by simp [*]```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory "Pruebas_de_length_(repeat_x_n)_Ig_n" imports Main begin   (* 1ª demostración⁾*) lemma "length (replicate n x) = n" proof (induct n) have "length (replicate 0 x) = length ([] :: 'a list)" by (simp only: replicate.simps(1)) also have "… = 0" by (rule list.size(3)) finally show "length (replicate 0 x) = 0" by this next fix n assume HI : "length (replicate n x) = n" have "length (replicate (Suc n) x) = length (x # replicate n x)" by (simp only: replicate.simps(2)) also have "… = length (replicate n x) + 1" by (simp only: list.size(4)) also have "… = Suc n" by (simp only: HI) finally show "length (replicate (Suc n) x) = Suc n" by this qed   (* 2ª demostración⁾*) lemma "length (replicate n x) = n" proof (induct n) show "length (replicate 0 x) = 0" by simp next fix n assume "length (replicate n x) = n" then show "length (replicate (Suc n) x) = Suc n" by simp qed   (* 3ª demostración⁾*) lemma "length (replicate n x) = n" proof (induct n) case 0 then show ?case by simp next case (Suc n) then show ?case by simp qed   (* 4ª demostración⁾*) lemma "length (replicate n x) = n" by (rule length_replicate)   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Para extraer una subsucesión se aplica una función de extracción queconserva el orden; por ejemplo, la subsucesión

` uₒ, u₂, u₄, u₆, ...`

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

``` def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m```

que a es un límite de u por

``` def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε```

que a es un punto de acumulación de u por

``` def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a```

que la sucesión u es de Cauchy por

``` def suc_cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε```

Demostrar que si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u.

Para ello, completar la siguiente teoría de Lean:

```import data.real.basic open nat   variable {u : ℕ → ℝ} variables {a : ℝ} variable {φ : ℕ → ℕ}   notation `|`x`|` := abs x   def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m   def limite (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a   def suc_cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε   example (hu : suc_cauchy u) (ha : punto_acumulacion u a) : limite u a := sorry```
Soluciones con Lean
```import data.real.basic open nat   variable {u : ℕ → ℝ} variables {a : ℝ} variable {φ : ℕ → ℕ}   notation `|`x`|` := abs x   def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m   def limite (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a   def suc_cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε   lemma aux1 (h : extraccion φ) : ∀ n, n ≤ φ n := begin intro n, induction n with m HI, { exact nat.zero_le (φ 0), }, { apply nat.succ_le_of_lt, calc m ≤ φ m : HI ... < φ (succ m) : h m (m+1) (lt_add_one m), }, end   lemma aux2 (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := λ N N', ⟨max N N', ⟨le_max_right N N', le_trans (le_max_left N N') (aux1 h (max N N'))⟩⟩   lemma cerca_acumulacion (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := begin intros ε hε N, rcases h with ⟨φ, hφ1, hφ2⟩, cases hφ2 ε hε with N' hN', rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩, exact ⟨φ m, hm', hN' _ hm⟩, end   -- 1ª demostración example (hu : suc_cauchy u) (ha : punto_acumulacion u a) : limite u a := begin unfold limite, intros ε hε, unfold suc_cauchy at hu, cases hu (ε/2) (half_pos hε) with N hN, use N, have ha' : ∃ N' ≥ N, |u N' - a| < ε/2, apply cerca_acumulacion ha (ε/2) (half_pos hε), cases ha' with N' h, cases h with hNN' hN', intros n hn, calc |u n - a| = |(u n - u N') + (u N' - a)| : by ring_nf ... ≤ |u n - u N'| + |u N' - a| : abs_add (u n - u N') (u N' - a) ... < ε/2 + |u N' - a| : add_lt_add_right (hN n hn N' hNN') _ ... < ε/2 + ε/2 : add_lt_add_left hN' (ε / 2) ... = ε : add_halves ε end   -- 2ª demostración example (hu : suc_cauchy u) (ha : punto_acumulacion u a) : limite u a := begin intros ε hε, cases hu (ε/2) (by linarith) with N hN, use N, have ha' : ∃ N' ≥ N, |u N' - a| < ε/2, apply cerca_acumulacion ha (ε/2) (by linarith), rcases ha' with ⟨N', hNN', hN'⟩, intros n hn, calc |u n - a| = |(u n - u N') + (u N' - a)| : by ring_nf ... ≤ |u n - u N'| + |u N' - a| : by simp [abs_add] ... < ε : by linarith [hN n hn N' hNN'], end```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory "Si_a_es_un_punto_de_acumulacion_de_la_sucesion_de_Cauchy_u,_entonces_a_es_el_limite_de_u" imports Main HOL.Real begin   definition extraccion :: "(nat ⇒ nat) ⇒ bool" where "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"   definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"   definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool" where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"   definition suc_cauchy :: "(nat ⇒ real) ⇒ bool" where "suc_cauchy u ⟷ (∀ε>0. ∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε)"   (* Lemas auxiliares *)   lemma aux1 : assumes "extraccion φ" shows "n ≤ φ n" proof (induct n) show "0 ≤ φ 0" by simp next fix n assume HI : "n ≤ φ n" then show "Suc n ≤ φ (Suc n)" using assms extraccion_def by (metis Suc_leI lessI order_le_less_subst1) qed   lemma aux2 : assumes "extraccion φ" shows "∀ N N'. ∃ k ≥ N'. φ k ≥ N" proof (intro allI) fix N N' :: nat have "max N N' ≥ N' ∧ φ (max N N') ≥ N" by (meson assms aux1 max.bounded_iff max.cobounded2) then show "∃k ≥ N'. φ k ≥ N" by blast qed   lemma cerca_acumulacion : assumes "punto_acumulacion u a" shows "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε" proof (intro allI impI) fix ε :: real and N :: nat assume "ε > 0" obtain φ where hφ1 : "extraccion φ" and hφ2 : "limite (u ∘ φ) a" using assms punto_acumulacion_def by blast obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε" using hφ2 limite_def ‹ε > 0› by auto obtain m where "m ≥ N' ∧ φ m ≥ N" using aux2 hφ1 by blast then show "∃k≥N. ¦u k - a¦ < ε" using hN' by auto qed   (* Demostración *) lemma assumes "suc_cauchy u" "punto_acumulacion u a" shows "limite u a" proof (unfold limite_def; intro allI impI) fix ε :: real assume "ε > 0" then have "ε/2 > 0" by simp then obtain N where hN : "∀m≥N. ∀n≥N. ¦u m - u n¦ < ε/2" using assms(1) suc_cauchy_def by blast have "∀k≥N. ¦u k - a¦ < ε" proof (intro allI impI) fix k assume hk : "k ≥ N" obtain N' where hN'1 : "N' ≥ N" and hN'2 : "¦u N' - a¦ < ε/2" using assms(2) cerca_acumulacion ‹ε/2 > 0› by blast have "¦u k - a¦ = ¦(u k - u N') + (u N' - a)¦" by simp also have "… ≤ ¦u k - u N'¦ + ¦u N' - a¦" by simp also have "… < ε/2 + ¦u N' - a¦" using hk hN hN'1 by auto also have "… < ε/2 + ε/2" using hN'2 by auto also have "… = ε" by simp finally show "¦u k - a¦ < ε" . qed then show "∃N. ∀k≥N. ¦u k - a¦ < ε" by auto qed   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## La suma de los n primeros impares es n^2

En Lean, se puede definir el n-ésimo número primo por

` def impar (n : ℕ) := 2 * n + 1`

Además, en la librería finset están definidas las funciones

``` range :: ℕ → finset ℕ sum :: finset α → (α → β) → β```

tales que

+ (range n) es el conjunto de los n primeros números naturales. Por ejemplo, el valor de (range 3) es {0, 1, 2}.
+ (sum A f) es la suma del conjunto obtenido aplicando la función f a los elementos del conjunto finito A. Por ejemplo, el valor de (sum (range 3) impar) es 9.

Demostrar que la suma de los n primeros números impares es n².

Para ello, completar la siguiente teoría de Lean:

```import data.finset import tactic.ring open nat   variable (n : ℕ)   def impar (n : ℕ) := 2 * n + 1   example : finset.sum (finset.range n) impar = n ^ 2 := sorry```
Soluciones con Lean
```import data.finset import tactic.ring open nat   set_option pp.structure_projections false   variable (n : ℕ)   def impar (n : ℕ) := 2 * n + 1   -- 1ª demostración example : finset.sum (finset.range n) impar = n ^ 2 := begin induction n with m HI, { calc finset.sum (finset.range 0) impar = 0 : by simp ... = 0 ^ 2 : rfl, }, { calc finset.sum (finset.range (succ m)) impar = finset.sum (finset.range m) impar + impar m : finset.sum_range_succ impar m ... = m ^ 2 + impar m : congr_arg2 (+) HI rfl ... = m ^ 2 + 2 * m + 1 : rfl ... = (m + 1) ^ 2 : by ring_nf ... = succ m ^ 2 : rfl }, end   -- 2ª demostración example : finset.sum (finset.range n) impar = n ^ 2 := begin induction n with d hd, { refl, }, { rw finset.sum_range_succ, rw hd, change d ^ 2 + (2 * d + 1) = (d + 1) ^ 2, ring_nf, }, end```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory "La_suma_de_los_n_primeros_impares_es_n^2" imports Main begin   definition impar :: "nat ⇒ nat" where "impar n ≡ 2 * n + 1"   lemma "sum impar {i::nat. i < n} = n⇧2" proof (induct n) show "sum impar {i. i < 0} = 0⇧2" by simp next fix n assume HI : "sum impar {i. i < n} = n⇧2" have "{i. i < Suc n} = {i. i < n} ∪ {n}" by auto then have "sum impar {i. i < Suc n} = sum impar {i. i < n} + impar n" by simp also have "… = n⇧2 + (2 * n + 1)" using HI impar_def by simp also have "… = (n + 1)⇧2" by algebra also have "… = (Suc n)⇧2" by simp finally show "sum impar {i. i < Suc n} = (Suc n)⇧2" . qed   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## El punto de acumulación de las sucesiones convergente es su límite

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

` uₒ, u₂, u₄, u₆, ...`

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

``` def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m```

que a es un límite de u por

``` def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε```

que u es convergente por

``` def convergente (u : ℕ → ℝ) := ∃ a, limite u a```

que a es un punto de acumulación de u por

``` def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a```

Demostrar que si u es una sucesión convergente y a es un punto de acumulación de u, entonces a es un límite de u.

Para ello, completar la siguiente teoría de Lean:

```import data.real.basic open nat   variable {u : ℕ → ℝ} variables {a : ℝ}   def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε   def convergente (u : ℕ → ℝ) := ∃ a, limite u a   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a   example (hu : convergente u) (ha : punto_acumulacion u a) : limite u a := sorry```
Soluciones con Lean
```import data.real.basic open nat   variable {u : ℕ → ℝ} variables {a : ℝ}   def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε   def convergente (u : ℕ → ℝ) := ∃ a, limite u a   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a   -- Lemas auxiliares -- ================   lemma unicidad_limite_aux {a b: ℝ} (ha : limite u a) (hb : limite u b) : b ≤ a := begin by_contra h, set ε := b - a with hε, cases ha (ε/2) (by linarith) with A hA, cases hb (ε/2) (by linarith) with B hB, set N := max A B with hN, have hAN : A ≤ N := le_max_left A B, have hBN : B ≤ N := le_max_right A B, specialize hA N hAN, specialize hB N hBN, rw abs_lt at hA hB, linarith, end   lemma unicidad_limite {a b: ℝ} (ha : limite u a) (hb : limite u b) : a = b := le_antisymm (unicidad_limite_aux hb ha) (unicidad_limite_aux ha hb)   lemma limite_subsucesion_aux {φ : ℕ → ℕ} (h : extraccion φ) : ∀ n, n ≤ φ n := begin intro n, induction n with m HI, { exact nat.zero_le (φ 0), }, { apply nat.succ_le_of_lt, calc m ≤ φ m : HI ... < φ (succ m) : h m (m+1) (lt_add_one m), }, end   lemma limite_subsucesion {φ : ℕ → ℕ} {a : ℝ} (h : limite u a) (hφ : extraccion φ) : limite (u ∘ φ) a := begin intros ε hε, cases h ε hε with N hN, use N, intros k hk, calc |(u ∘ φ) k - a| = |u (φ k) - a| : rfl ... < ε : hN (φ k) _, calc φ k ≥ k : limite_subsucesion_aux hφ k ... ≥ N : hk, end   -- 1ª demostración example (hu : convergente u) (ha : punto_acumulacion u a) : limite u a := begin unfold convergente at hu, cases hu with b hb, convert hb, unfold punto_acumulacion at ha, rcases ha with ⟨φ, hφ₁, hφ₂⟩, have hφ₃ : limite (u ∘ φ) b, from limite_subsucesion hb hφ₁, exact unicidad_limite hφ₂ hφ₃, end   -- 1ª demostración example (hu : convergente u) (ha : punto_acumulacion u a) : limite u a := begin cases hu with b hb, convert hb, rcases ha with ⟨φ, hφ₁, hφ₂⟩, apply unicidad_limite hφ₂ _, exact limite_subsucesion hb hφ₁, end   -- 2ª demostración example (hu : convergente u) (ha : punto_acumulacion u a) : limite u a := begin cases hu with b hb, convert hb, rcases ha with ⟨φ, hφ₁, hφ₂⟩, exact unicidad_limite hφ₂ (limite_subsucesion hb hφ₁), end```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory El_punto_de_acumulacion_de_las_sucesiones_convergente_es_su_limite imports Main HOL.Real begin   definition extraccion :: "(nat ⇒ nat) ⇒ bool" where "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"   definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool" where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"   definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"   definition convergente :: "(nat ⇒ real) ⇒ bool" where "convergente u ⟷ (∃ a. limite u a)"   definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool" where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"   (* Lemas auxiliares *)   lemma unicidad_limite_aux : assumes "limite u a" "limite u b" shows "b ≤ a" proof (rule ccontr) assume "¬ b ≤ a" let ?ε = "b - a" have "0 < ?ε/2" using ‹¬ b ≤ a› by auto obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2" using assms(1) limite_def ‹0 < ?ε/2› by blast obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2" using assms(2) limite_def ‹0 < ?ε/2› by blast let ?C = "max A B" have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2" using hA by simp have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2" using hB by simp have "∀n≥?C. ¦a - b¦ < ?ε" proof (intro allI impI) fix n assume "n ≥ ?C" have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp finally show "¦a - b¦ < b - a" using hCa hCb ‹n ≥ ?C› by fastforce qed then show False by fastforce qed   lemma unicidad_limite : assumes "limite u a" "limite u b" shows "a = b" proof (rule antisym) show "a ≤ b" using assms(2) assms(1) by (rule unicidad_limite_aux) next show "b ≤ a" using assms(1) assms(2) by (rule unicidad_limite_aux) qed   lemma limite_subsucesion_aux : assumes "extraccion φ" shows "n ≤ φ n" proof (induct n) show "0 ≤ φ 0" by simp next fix n assume HI : "n ≤ φ n" then show "Suc n ≤ φ (Suc n)" using assms extraccion_def by (metis Suc_leI lessI order_le_less_subst1) qed   lemma limite_subsucesion : assumes "subsucesion v u" "limite u a" shows "limite v a" proof (unfold limite_def; intro allI impI) fix ε :: real assume "ε > 0" then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε" using assms(2) limite_def by auto obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ" using assms(1) subsucesion_def by auto have "∀k≥N. ¦v k - a¦ < ε" proof (intro allI impI) fix k assume "N ≤ k" also have "... ≤ φ k" by (simp add: limite_subsucesion_aux hφ1) finally have "N ≤ φ k" . have "¦v k - a¦ = ¦u (φ k) - a¦" using hφ2 by simp also have "… < ε" using hN ‹N ≤ φ k› by simp finally show "¦v k - a¦ < ε" . qed then show "∃N. ∀k≥N. ¦v k - a¦ < ε" by auto qed   (* Demostración *) lemma assumes "convergente u" "punto_acumulacion u a" shows "limite u a" proof - obtain b where hb : "limite u b" using assms(1) convergente_def by auto obtain φ where hφ1 : "extraccion φ" and hφ2 : "limite (u ∘ φ) a" using assms(2) punto_acumulacion_def by auto have "limite (u ∘ φ) b" using hφ1 hb limite_subsucesion subsucesion_def by blast with hφ2 have "a = b" by (rule unicidad_limite) then show "limite u a" using hb by simp qed   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## Las subsucesiones tienen el mismo límite que la sucesión

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

` uₒ, u₂, u₄, u₆, ...`

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

``` def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m```

que v es una subsucesión de u por

``` def subsucesion (v u : ℕ → ℝ) := ∃ φ, extraccion φ ∧ v = u ∘ φ```

y que a es un límite de u por

``` def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε```

Demostrar que las subsucesiones de una sucesión convergente tienen el mismo límite que la sucesión.

Para ello, completar la siguiente teoría de Lean:

```import data.real.basic open nat   variables {u v : ℕ → ℝ} variable {a : ℝ} variable {φ : ℕ → ℕ}   def extraccion (φ : ℕ → ℕ):= ∀ n m, n < m → φ n < φ m   def subsucesion (v u : ℕ → ℝ) := ∃ φ, extraccion φ ∧ v = u ∘ φ   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε   example (hv : subsucesion v u) (ha : limite u a) : limite v a := sorry```
Soluciones con Lean
```import data.real.basic open nat   variables {u v : ℕ → ℝ} variable {a : ℝ} variable {φ : ℕ → ℕ}   def extraccion (φ : ℕ → ℕ):= ∀ n m, n < m → φ n < φ m   def subsucesion (v u : ℕ → ℝ) := ∃ φ, extraccion φ ∧ v = u ∘ φ   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε   -- En la demostración se usará el siguiente lema. lemma aux (h : extraccion φ) : ∀ n, n ≤ φ n := begin intro n, induction n with m HI, { exact nat.zero_le (φ 0), }, { apply nat.succ_le_of_lt, calc m ≤ φ m : HI ... < φ (succ m) : h m (m+1) (lt_add_one m), }, end   -- 1ª demostración example (hv : subsucesion v u) (ha : limite u a) : limite v a := begin unfold limite, intros ε hε, unfold limite at ha, cases ha ε hε with N hN, use N, intros n hn, unfold subsucesion at hv, rcases hv with ⟨φ, hφ1, hφ2⟩, rw hφ2, apply hN, apply le_trans hn, exact aux hφ1 n, end   -- 2ª demostración example (hv : subsucesion v u) (ha : limite u a) : limite v a := begin intros ε hε, cases ha ε hε with N hN, use N, intros n hn, rcases hv with ⟨φ, hφ1, hφ2⟩, rw hφ2, apply hN, exact le_trans hn (aux hφ1 n), end   -- 3ª demostración example (hv : subsucesion v u) (ha : limite u a) : limite v a := begin intros ε hε, cases ha ε hε with N hN, use N, intros n hn, rcases hv with ⟨φ, hφ1, hφ2⟩, rw hφ2, exact hN (φ n) (le_trans hn (aux hφ1 n)), end   -- 4ª demostración example (hv : subsucesion v u) (ha : limite u a) : limite v a := begin intros ε hε, cases ha ε hε with N hN, rcases hv with ⟨φ, hφ1, hφ2⟩, rw hφ2, use N, exact λ n hn, hN (φ n) (le_trans hn (aux hφ1 n)), end   -- 5ª demostración example (hv : subsucesion v u) (ha : limite u a) : limite v a := begin intros ε hε, cases ha ε hε with N hN, rcases hv with ⟨φ, hφ1, hφ2⟩, rw hφ2, exact ⟨N, λ n hn, hN (φ n) (le_trans hn (aux hφ1 n))⟩, end```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory Las_subsucesiones_tienen_el_mismo_limite_que_la_sucesion imports Main HOL.Real begin   definition extraccion :: "(nat ⇒ nat) ⇒ bool" where "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"   definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool" where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"   definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"   (* En la demostración se usará el siguiente lema *) lemma aux : assumes "extraccion φ" shows "n ≤ φ n" proof (induct n) show "0 ≤ φ 0" by simp next fix n assume HI : "n ≤ φ n" then show "Suc n ≤ φ (Suc n)" using assms extraccion_def by (metis Suc_leI lessI order_le_less_subst1) qed   (* Demostración *) lemma assumes "subsucesion v u" "limite u a" shows "limite v a" proof (unfold limite_def; intro allI impI) fix ε :: real assume "ε > 0" then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε" using assms(2) limite_def by auto obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ" using assms(1) subsucesion_def by auto have "∀k≥N. ¦v k - a¦ < ε" proof (intro allI impI) fix k assume "N ≤ k" also have "... ≤ φ k" by (simp add: aux hφ1) finally have "N ≤ φ k" . have "¦v k - a¦ = ¦u (φ k) - a¦" using hφ2 by simp also have "… < ε" using hN ‹N ≤ φ k› by simp finally show "¦v k - a¦ < ε" . qed then show "∃N. ∀k≥N. ¦v k - a¦ < ε" by auto qed   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## Si a es un punto de acumulación de u, entonces ∀ε>0, ∀ N, ∃k≥N, |u(k)−a| < ε

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

` uₒ, u₂, u₄, u₆, ...`

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

``` def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m```

También se puede definir que a es un límite de u por

``` def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε```

Los puntos de acumulación de una sucesión son los límites de sus subsucesiones. En Lean se puede definir por

``` def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a```

Demostrar que si a es un punto de acumulación de u, entonces

` ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε`

Para ello, completar la siguiente teoría de Lean:

```import data.real.basic open nat   variable {u : ℕ → ℝ} variables {a : ℝ} variable {φ : ℕ → ℕ}   def extraccion (φ : ℕ → ℕ):= ∀ n m, n < m → φ n < φ m   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a   example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε := sorry```
Soluciones con Lean
```import data.real.basic open nat   variable {u : ℕ → ℝ} variables {a : ℝ} variable {φ : ℕ → ℕ}   def extraccion (φ : ℕ → ℕ):= ∀ n m, n < m → φ n < φ m   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a   -- En la demostración se usarán los siguientes lemas.   lemma aux1 (h : extraccion φ) : ∀ n, n ≤ φ n := begin intro n, induction n with m HI, { exact nat.zero_le (φ 0), }, { apply nat.succ_le_of_lt, calc m ≤ φ m : HI ... < φ (succ m) : h m (m+1) (lt_add_one m), }, end   lemma aux2 (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := λ N N', ⟨max N N', ⟨le_max_right N N', le_trans (le_max_left N N') (aux1 h (max N N'))⟩⟩   -- 1ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ k ≥ N, |u k - a| < ε := begin intros ε hε N, unfold punto_acumulacion at h, rcases h with ⟨φ, hφ1, hφ2⟩, unfold limite at hφ2, cases hφ2 ε hε with N' hN', rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩, clear hφ1 hφ2, use φ m, split, { exact hm', }, { exact hN' m hm, }, end   -- 2ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := begin intros ε hε N, rcases h with ⟨φ, hφ1, hφ2⟩, cases hφ2 ε hε with N' hN', rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩, use φ m, exact ⟨hm', hN' m hm⟩, end   -- 3ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := begin intros ε hε N, rcases h with ⟨φ, hφ1, hφ2⟩, cases hφ2 ε hε with N' hN', rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩, exact ⟨φ m, hm', hN' _ hm⟩, end   -- 4ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := begin intros ε hε N, rcases h with ⟨φ, hφ1, hφ2⟩, cases hφ2 ε hε with N' hN', rcases aux2 hφ1 N N' with ⟨m, hm, hm'⟩, use φ m ; finish, end   -- 5ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := assume ε, assume hε : ε > 0, assume N, exists.elim h ( assume φ, assume hφ : extraccion φ ∧ limite (u ∘ φ) a, exists.elim (hφ.2 ε hε) ( assume N', assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε, have h1 : ∃ n ≥ N', φ n ≥ N, from aux2 hφ.1 N N', exists.elim h1 ( assume m, assume hm : ∃ (H : m ≥ N'), φ m ≥ N, exists.elim hm ( assume hm1 : m ≥ N', assume hm2 : φ m ≥ N, have h2 : |u (φ m) - a| < ε, from hN' m hm1, show ∃ n ≥ N, |u n - a| < ε, from exists.intro (φ m) (exists.intro hm2 h2)))))   -- 6ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := assume ε, assume hε : ε > 0, assume N, exists.elim h ( assume φ, assume hφ : extraccion φ ∧ limite (u ∘ φ) a, exists.elim (hφ.2 ε hε) ( assume N', assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε, have h1 : ∃ n ≥ N', φ n ≥ N, from aux2 hφ.1 N N', exists.elim h1 ( assume m, assume hm : ∃ (H : m ≥ N'), φ m ≥ N, exists.elim hm ( assume hm1 : m ≥ N', assume hm2 : φ m ≥ N, have h2 : |u (φ m) - a| < ε, from hN' m hm1, show ∃ n ≥ N, |u n - a| < ε, from ⟨φ m, hm2, h2⟩))))   -- 7ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := assume ε, assume hε : ε > 0, assume N, exists.elim h ( assume φ, assume hφ : extraccion φ ∧ limite (u ∘ φ) a, exists.elim (hφ.2 ε hε) ( assume N', assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε, have h1 : ∃ n ≥ N', φ n ≥ N, from aux2 hφ.1 N N', exists.elim h1 ( assume m, assume hm : ∃ (H : m ≥ N'), φ m ≥ N, exists.elim hm ( assume hm1 : m ≥ N', assume hm2 : φ m ≥ N, have h2 : |u (φ m) - a| < ε, from hN' m hm1, ⟨φ m, hm2, h2⟩))))   -- 8ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := assume ε, assume hε : ε > 0, assume N, exists.elim h ( assume φ, assume hφ : extraccion φ ∧ limite (u ∘ φ) a, exists.elim (hφ.2 ε hε) ( assume N', assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε, have h1 : ∃ n ≥ N', φ n ≥ N, from aux2 hφ.1 N N', exists.elim h1 ( assume m, assume hm : ∃ (H : m ≥ N'), φ m ≥ N, exists.elim hm ( assume hm1 : m ≥ N', assume hm2 : φ m ≥ N, ⟨φ m, hm2, hN' m hm1⟩))))   -- 9ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := assume ε, assume hε : ε > 0, assume N, exists.elim h ( assume φ, assume hφ : extraccion φ ∧ limite (u ∘ φ) a, exists.elim (hφ.2 ε hε) ( assume N', assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε, have h1 : ∃ n ≥ N', φ n ≥ N, from aux2 hφ.1 N N', exists.elim h1 ( assume m, assume hm : ∃ (H : m ≥ N'), φ m ≥ N, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))   -- 10ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := assume ε, assume hε : ε > 0, assume N, exists.elim h ( assume φ, assume hφ : extraccion φ ∧ limite (u ∘ φ) a, exists.elim (hφ.2 ε hε) ( assume N', assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε, have h1 : ∃ n ≥ N', φ n ≥ N, from aux2 hφ.1 N N', exists.elim h1 (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))   -- 11ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := assume ε, assume hε : ε > 0, assume N, exists.elim h ( assume φ, assume hφ : extraccion φ ∧ limite (u ∘ φ) a, exists.elim (hφ.2 ε hε) ( assume N', assume hN' : ∀ (n : ℕ), n ≥ N' → |(u ∘ φ) n - a| < ε, exists.elim (aux2 hφ.1 N N') (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))   -- 12ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := assume ε, assume hε : ε > 0, assume N, exists.elim h ( assume φ, assume hφ : extraccion φ ∧ limite (u ∘ φ) a, exists.elim (hφ.2 ε hε) (λ N' hN', exists.elim (aux2 hφ.1 N N') (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))   -- 13ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := assume ε, assume hε : ε > 0, assume N, exists.elim h (λ φ hφ, exists.elim (hφ.2 ε hε) (λ N' hN', exists.elim (aux2 hφ.1 N N') (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))   -- 14ª demostración example (h : punto_acumulacion u a) : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| < ε := λ ε hε N, exists.elim h (λ φ hφ, exists.elim (hφ.2 ε hε) (λ N' hN', exists.elim (aux2 hφ.1 N N') (λ m hm, exists.elim hm (λ hm1 hm2, ⟨φ m, hm2, hN' m hm1⟩))))```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory "Si_a_es_un_punto_de_acumulacion_de_u,_entonces_a_tiene_puntos_cercanos" imports Main HOL.Real begin   definition extraccion :: "(nat ⇒ nat) ⇒ bool" where "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"   definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"   definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool" where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"   (* En la demostración se usarán los siguientes lemas *) lemma aux1 : assumes "extraccion φ" shows "n ≤ φ n" proof (induct n) show "0 ≤ φ 0" by simp next fix n assume HI : "n ≤ φ n" then show "Suc n ≤ φ (Suc n)" using assms extraccion_def by (metis Suc_leI lessI order_le_less_subst1) qed   lemma aux2 : assumes "extraccion φ" shows "∀ N N'. ∃ k ≥ N'. φ k ≥ N" proof (intro allI) fix N N' :: nat have "max N N' ≥ N' ∧ φ (max N N') ≥ N" by (meson assms aux1 max.bounded_iff max.cobounded2) then show "∃k ≥ N'. φ k ≥ N" by blast qed   (* 1ª demostración *) lemma assumes "punto_acumulacion u a" shows "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε" proof (intro allI impI) fix ε :: real and N :: nat assume "ε > 0" obtain φ where hφ1 : "extraccion φ" and hφ2 : "limite (u ∘ φ) a" using assms punto_acumulacion_def by blast obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε" using hφ2 limite_def ‹ε > 0› by auto obtain m where hm1 : "m ≥ N'" and hm2 : "φ m ≥ N" using aux2 hφ1 by blast have "φ m ≥ N ∧ ¦u (φ m) - a¦ < ε" using hN' hm1 hm2 by force then show "∃k≥N. ¦u k - a¦ < ε" by auto qed   (* 2ª demostración *) lemma assumes "punto_acumulacion u a" shows "∀ε>0. ∀ N. ∃k≥N. ¦u k - a¦ < ε" proof (intro allI impI) fix ε :: real and N :: nat assume "ε > 0" obtain φ where hφ1 : "extraccion φ" and hφ2 : "limite (u ∘ φ) a" using assms punto_acumulacion_def by blast obtain N' where hN' : "∀k≥N'. ¦(u ∘ φ) k - a¦ < ε" using hφ2 limite_def ‹ε > 0› by auto obtain m where "m ≥ N' ∧ φ m ≥ N" using aux2 hφ1 by blast then show "∃k≥N. ¦u k - a¦ < ε" using hN' by auto qed   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>