# Etiqueta: L.rw

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

## Límite de sucesiones no decrecientes

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

En Lean, se define que a es el límite de la sucesión u, por

``` def limite (u: ℕ → ℝ) (a: ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε <pre lang="text"> donde se usa la notación |x| para el valor absoluto de x <pre lang="text"> notation `|`x`|` := abs x```

y que la sucesión u es no decreciente por

``` def no_decreciente (u : ℕ → ℝ) := ∀ n m, n ≤ m → u n ≤ u m```

Demostrar que si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n.

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

```import data.real.basic import tactic   variable {u : ℕ → ℝ} variable (a : ℝ)   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε   def no_decreciente (u : ℕ → ℝ) := ∀ n m, n ≤ m → u n ≤ u m   example (h : limite u a) (h' : no_decreciente u) : ∀ n, u n ≤ a := sorry```
Soluciones con Lean
```import data.real.basic import tactic   variable {u : ℕ → ℝ} variable (a : ℝ)   notation `|`x`|` := abs x   def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε   def no_decreciente (u : ℕ → ℝ) := ∀ n m, n ≤ m → u n ≤ u m   -- 1ª demostración example (h : limite u a) (h' : no_decreciente u) : ∀ n, u n ≤ a := begin intro n, by_contradiction H, push_neg at H, replace H : u n - a > 0 := sub_pos.mpr H, cases h (u n - a) H with m hm, let k := max n m, specialize hm k (le_max_right _ _), specialize h' n k (le_max_left _ _), replace hm : |u k - a| < u k - a, by calc |u k - a| < u n - a : hm ... ≤ u k - a : sub_le_sub_right h' a, rw ← not_le at hm, apply hm, exact le_abs_self (u k - a), end   -- 2ª demostración example (h : limite u a) (h' : no_decreciente u) : ∀ n, u n ≤ a := begin intro n, by_contradiction H, push_neg at H, cases h (u n - a) (by linarith) with m hm, specialize hm (max n m) (le_max_right _ _), specialize h' n (max n m) (le_max_left _ _), rw abs_lt at hm, linarith, 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 Limite_de_sucesiones_no_decrecientes imports Main HOL.Real begin   definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"   definition no_decreciente :: "(nat ⇒ real) ⇒ bool" where "no_decreciente u ⟷ (∀ n m. n ≤ m ⟶ u n ≤ u m)"   (* 1ª demostración *) lemma assumes "limite u a" "no_decreciente u" shows "∀ n. u n ≤ a" proof (rule allI) fix n show "u n ≤ a" proof (rule ccontr) assume "¬ u n ≤ a" then have "a < u n" by (rule not_le_imp_less) then have H : "u n - a > 0" by (simp only: diff_gt_0_iff_gt) then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a" using assms(1) limite_def by blast let ?k = "max n m" have "n ≤ ?k" by (simp only: assms(2) no_decreciente_def) then have "u n ≤ u ?k" using assms(2) no_decreciente_def by blast have "¦u ?k - a¦ < u n - a" by (simp only: hm) also have "… ≤ u ?k - a" using ‹u n ≤ u ?k› by (rule diff_right_mono) finally have "¦u ?k - a¦ < u ?k - a" by this then have "¬ u ?k - a ≤ ¦u ?k - a¦" by (simp only: not_le_imp_less) moreover have "u ?k - a ≤ ¦u ?k - a¦" by (rule abs_ge_self) ultimately show False by (rule notE) qed qed   (* 2ª demostración *) lemma assumes "limite u a" "no_decreciente u" shows "∀ n. u n ≤ a" proof (rule allI) fix n show "u n ≤ a" proof (rule ccontr) assume "¬ u n ≤ a" then have H : "u n - a > 0" by simp then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a" using assms(1) limite_def by blast let ?k = "max n m" have "¦u ?k - a¦ < u n - a" using hm by simp moreover have "u n ≤ u ?k" using assms(2) no_decreciente_def by simp ultimately have "¦u ?k - a¦ < u ?k - a" by simp then show False by simp qed qed   (* 3ª demostración *) lemma assumes "limite u a" "no_decreciente u" shows "∀ n. u n ≤ a" proof fix n show "u n ≤ a" proof (rule ccontr) assume "¬ u n ≤ a" then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a" using assms(1) limite_def by fastforce let ?k = "max n m" have "¦u ?k - a¦ < u n - a" using hm by simp moreover have "u n ≤ u ?k" using assms(2) no_decreciente_def by simp ultimately show False by simp qed 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>