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]

Escribe un comentario