# Etiqueta: IH.this

## 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```

[expand title=»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>
[/expand]

[expand title=»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>
[/expand]

## 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```

[expand title=»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>
[/expand]

[expand title=»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>
[/expand]

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```

[expand title=»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>
[/expand]

[expand title=»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>
[/expand]

## Las funciones de extracción no están acotadas

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```

Demostrar que las funciones de extracción no está acotadas; es decir, que si φ es una función de extracción, entonces

` ∀ N N', ∃ n ≥ N', φ n ≥ N`

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

```import tactic open nat   variable {φ : ℕ → ℕ}   def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m   example (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := sorry```

[expand title=»Soluciones con Lean»]

```import tactic open nat   variable {φ : ℕ → ℕ}   def extraccion (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m   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 (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := begin intros N N', let n := max N N', use n, split, { exact le_max_right N N', }, { calc N ≤ n : le_max_left N N' ... ≤ φ n : aux h n, }, end   -- 2ª demostración example (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := begin intros N N', let n := max N N', use n, split, { exact le_max_right N N', }, { exact le_trans (le_max_left N N') (aux h n), }, end   -- 3ª demostración example (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := begin intros N N', use max N N', split, { exact le_max_right N N', }, { exact le_trans (le_max_left N N') (aux h (max N N')), }, end   -- 4ª demostración example (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := begin intros N N', use max N N', exact ⟨le_max_right N N', le_trans (le_max_left N N') (aux h (max N N'))⟩, end   -- 5ª demostración example (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') (aux h (max N N'))⟩⟩   -- 6ª demostración example (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := assume N N', let n := max N N' in have h1 : n ≥ N', from le_max_right N N', show ∃ n ≥ N', φ n ≥ N, from exists.intro n (exists.intro h1 (show φ n ≥ N, from calc N ≤ n : le_max_left N N' ... ≤ φ n : aux h n))   -- 7ª demostración example (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := assume N N', let n := max N N' in have h1 : n ≥ N', from le_max_right N N', show ∃ n ≥ N', φ n ≥ N, from ⟨n, h1, calc N ≤ n : le_max_left N N' ... ≤ φ n : aux h n⟩   -- 8ª demostración example (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := assume N N', let n := max N N' in have h1 : n ≥ N', from le_max_right N N', show ∃ n ≥ N', φ n ≥ N, from ⟨n, h1, le_trans (le_max_left N N') (aux h (max N N'))⟩   -- 9ª demostración example (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := assume N N', let n := max N N' in have h1 : n ≥ N', from le_max_right N N', ⟨n, h1, le_trans (le_max_left N N') (aux h n)⟩   -- 10ª demostración example (h : extraccion φ) : ∀ N N', ∃ n ≥ N', φ n ≥ N := assume N N', ⟨max N N', le_max_right N N', le_trans (le_max_left N N') (aux h (max N N'))⟩   -- 11ª demostración lemma extraccion_mye (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') (aux h (max N N'))⟩```

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>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

```theory Las_funciones_de_extraccion_no_estan_acotadas imports Main begin   definition extraccion :: "(nat ⇒ nat) ⇒ bool" where "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"   (* 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" also have "φ n < φ (Suc n)" using assms extraccion_def by blast finally show "Suc n ≤ φ (Suc n)" by simp qed   (* 1ª demostración *) lemma assumes "extraccion φ" shows "∀ N N'. ∃ k ≥ N'. φ k ≥ N" proof (intro allI) fix N N' :: nat let ?k = "max N N'" have "max N N' ≤ ?k" by (rule le_refl) then have hk : "N ≤ ?k ∧ N' ≤ ?k" by (simp only: max.bounded_iff) then have "?k ≥ N'" by (rule conjunct2) moreover have "N ≤ φ ?k" proof - have "N ≤ ?k" using hk by (rule conjunct1) also have "… ≤ φ ?k" using assms by (rule aux) finally show "N ≤ φ ?k" by this qed ultimately have "?k ≥ N' ∧ φ ?k ≥ N" by (rule conjI) then show "∃k ≥ N'. φ k ≥ N" by (rule exI) qed   (* 2ª demostración *) lemma assumes "extraccion φ" shows "∀ N N'. ∃ k ≥ N'. φ k ≥ N" proof (intro allI) fix N N' :: nat let ?k = "max N N'" have "?k ≥ N'" by simp moreover have "N ≤ φ ?k" proof - have "N ≤ ?k" by simp also have "… ≤ φ ?k" using assms by (rule aux) finally show "N ≤ φ ?k" by this qed ultimately show "∃k ≥ N'. φ k ≥ N" by blast 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>
[/expand]

## Las sucesiones convergentes son sucesiones de Cauchy

Nota: El problema de hoy lo ha escrito Sara Díaz Real y es uno de los que se encuentran en su Trabajo Fin de Máster Formalización en Lean de problemas de las Olimpiadas Internacionales de Matemáticas (IMO). Concretamente, el problema se encuentra en la página 52 junto con la demostración en lenguaje natural.

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

Se define

• el valor absoluto de x por
` notation `|`x`|` := abs x`
• a es un límite de la sucesión u, por
``` def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| ≤ ε```
• la sucesión u es convergente por
``` def suc_convergente (u : ℕ → ℝ) := ∃ l, limite u l```
• la sucesión u es de Cauchy por
``` def suc_cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε```

Demostrar que las sucesiones convergentes son de Cauchy.

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

```import data.real.basic   variable {u : ℕ → ℝ }   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε   def suc_convergente (u : ℕ → ℝ) := ∃ l, limite u l   def suc_cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε   example (h : suc_convergente u) : suc_cauchy u := sorry```

[expand title=»Soluciones con Lean»]

```import data.real.basic   variable {u : ℕ → ℝ }   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε   def suc_convergente (u : ℕ → ℝ) := ∃ l, limite u l   def suc_cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε   -- 1ª demostración example (h : suc_convergente u) : suc_cauchy u := begin unfold suc_cauchy, intros ε hε, have hε2 : 0 < ε/2 := half_pos hε, cases h with l hl, cases hl (ε/2) hε2 with N hN, clear hε hl hε2, use N, intros p hp q hq, calc |u p - u q| = |(u p - l) + (l - u q)| : by ring_nf ... ≤ |u p - l| + |l - u q| : abs_add (u p - l) (l - u q) ... = |u p - l| + |u q - l| : congr_arg2 (+) rfl (abs_sub_comm l (u q)) ... ≤ ε/2 + ε/2 : add_le_add (hN p hp) (hN q hq) ... = ε : add_halves ε, end   -- 2ª demostración example (h : suc_convergente u) : suc_cauchy u := begin intros ε hε, cases h with l hl, cases hl (ε/2) (half_pos hε) with N hN, clear hε hl, use N, intros p hp q hq, calc |u p - u q| = |(u p - l) + (l - u q)| : by ring_nf ... ≤ |u p - l| + |l - u q| : abs_add (u p - l) (l - u q) ... = |u p - l| + |u q - l| : congr_arg2 (+) rfl (abs_sub_comm l (u q)) ... ≤ ε/2 + ε/2 : add_le_add (hN p hp) (hN q hq) ... = ε : add_halves ε, end   -- 3ª demostración example (h : suc_convergente u) : suc_cauchy u := begin intros ε hε, cases h with l hl, cases hl (ε/2) (half_pos hε) with N hN, clear hε hl, use N, intros p hp q hq, have cota1 : |u p - l| ≤ ε / 2 := hN p hp, have cota2 : |u q - l| ≤ ε / 2 := hN q hq, clear hN hp hq, calc |u p - u q| = |(u p - l) + (l - u q)| : by ring_nf ... ≤ |u p - l| + |l - u q| : abs_add (u p - l) (l - u q) ... = |u p - l| + |u q - l| : by rw abs_sub_comm l (u q) ... ≤ ε : by linarith, end   -- 4ª demostración example (h : suc_convergente u) : suc_cauchy u := begin intros ε hε, cases h with l hl, cases hl (ε/2) (half_pos hε) with N hN, clear hε hl, use N, intros p hp q hq, calc |u p - u q| = |(u p - l) + (l - u q)| : by ring_nf ... ≤ |u p - l| + |l - u q| : abs_add (u p - l) (l - u q) ... = |u p - l| + |u q - l| : by rw abs_sub_comm l (u q) ... ≤ ε : by linarith [hN p hp, hN q hq], end   -- 5ª demostración example (h : suc_convergente u) : suc_cauchy u := begin intros ε hε, cases h with l hl, cases hl (ε/2) (by linarith) with N hN, use N, intros p hp q hq, calc |u p - u q| = |(u p - l) + (l - u q)| : by ring_nf ... ≤ |u p - l| + |l - u q| : by simp [abs_add] ... = |u p - l| + |u q - l| : by simp [abs_sub_comm] ... ≤ ε : by linarith [hN p hp, hN q hq], 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>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

```theory Las_sucesiones_convergentes_son_sucesiones_de_Cauchy imports Main HOL.Real begin   definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u c ⟷ (∀ε>0. ∃k::nat. ∀n≥k. ¦u n - c¦ < ε)"   definition suc_convergente :: "(nat ⇒ real) ⇒ bool" where "suc_convergente u ⟷ (∃ l. limite u l)"   definition suc_cauchy :: "(nat ⇒ real) ⇒ bool" where "suc_cauchy u ⟷ (∀ε>0. ∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε)"   (* 1ª demostración *) lemma assumes "suc_convergente u" shows "suc_cauchy u" proof (unfold suc_cauchy_def; intro allI impI) fix ε :: real assume "0 < ε" then have "0 < ε/2" by simp obtain a where "limite u a" using assms suc_convergente_def by blast then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2" using ‹0 < ε / 2› limite_def by blast have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε" proof (intro allI impI) fix p q assume hp : "p ≥ k" and hq : "q ≥ k" then have hp' : "¦u p - a¦ < ε/2" using hk by blast have hq' : "¦u q - a¦ < ε/2" using hk hq by blast have "¦u p - u q¦ = ¦(u p - a) + (a - u q)¦" by simp also have "… ≤ ¦u p - a¦ + ¦a - u q¦" by simp also have "… = ¦u p - a¦ + ¦u q - a¦" by simp also have "… < ε/2 + ε/2" using hp' hq' by simp also have "… = ε" by simp finally show "¦u p - u q¦ < ε" by this qed then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε" by (rule exI) qed   (* 2ª demostración *) lemma assumes "suc_convergente u" shows "suc_cauchy u" proof (unfold suc_cauchy_def; intro allI impI) fix ε :: real assume "0 < ε" then have "0 < ε/2" by simp obtain a where "limite u a" using assms suc_convergente_def by blast then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2" using ‹0 < ε / 2› limite_def by blast have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε" proof (intro allI impI) fix p q assume hp : "p ≥ k" and hq : "q ≥ k" then have hp' : "¦u p - a¦ < ε/2" using hk by blast have hq' : "¦u q - a¦ < ε/2" using hk hq by blast show "¦u p - u q¦ < ε" using hp' hq' by argo qed then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε" by (rule exI) qed   (* 3ª demostración *) lemma assumes "suc_convergente u" shows "suc_cauchy u" proof (unfold suc_cauchy_def; intro allI impI) fix ε :: real assume "0 < ε" then have "0 < ε/2" by simp obtain a where "limite u a" using assms suc_convergente_def by blast then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2" using ‹0 < ε / 2› limite_def by blast have "∀m≥k. ∀n≥k. ¦u m - u n¦ < ε" using hk by (smt (z3) field_sum_of_halves) then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε" by (rule exI) qed   (* 3ª demostración *) lemma assumes "suc_convergente u" shows "suc_cauchy u" proof (unfold suc_cauchy_def; intro allI impI) fix ε :: real assume "0 < ε" then have "0 < ε/2" by simp obtain a where "limite u a" using assms suc_convergente_def by blast then obtain k where hk : "∀n≥k. ¦u n - a¦ < ε/2" using ‹0 < ε / 2› limite_def by blast then show "∃k. ∀m≥k. ∀n≥k. ¦u m - u n¦ < ε" by (smt (z3) field_sum_of_halves) 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>
[/expand]