Pruebas de equivalencia de definiciones de inversa

En Lean, está definida la función

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

Su definición es

Una definición alternativa es

Demostrar que las dos definiciones son equivalentes; es decir,

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

[expand title=»Soluciones con Lean»]

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»]

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 take n xs ++ drop n xs = xs

En Lean están definidas las funciones

tales que

  • (take n xs) es la lista formada por los n primeros elementos de xs. Por ejemplo,

  • (drop n xs) es la lista formada eliminando los n primeros elementos de xs. Por ejemplo,

  • (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.

Dichas funciones están caracterizadas por los siguientes lemas:

Demostrar que

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

[expand title=»Soluciones con Lean»]

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»]

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

tales que

  • (length xs) es la longitud de xs. Por ejemplo,

  • (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.

Dichas funciones están caracterizadas por los siguientes lemas:

Demostrar que

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

[expand title=»Soluciones con Lean»]

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»]

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]

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

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

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

[expand title=»Soluciones con Lean»]

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»]

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 (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,

  • (repeat x n) es la lista que tiene el elemento x n veces. Por ejemplo,

Demostrar que

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

[expand title=»Soluciones con Lean»]

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»]

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]

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

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

que a es un límite de u por

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

que la sucesión u es de Cauchy por

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:

[expand title=»Soluciones con Lean»]

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»]

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]

La suma de los n primeros impares es n^2

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

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

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:

[expand title=»Soluciones con Lean»]