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]