Instrucciones
Tu tarea es demostrar la igualdad entre una función personalizada para invertir listas y la función integrada List.reverse.
Debido a la naturaleza de este ejercicio, en lugar de depender de las pruebas tradicionales en tiempo de ejecución, la demostración se verifica con un teorema check.
Puedes considerar que la prueba pasa si este teorema pasa la verificación de tipos.
Si trabajas de forma local o en el entorno de pruebas en línea de Lean, recibirás retroalimentación instantánea sobre si un teorema tiene éxito o falla, y por qué falla, a través de Lean InfoView.
Es una herramienta invaluable, capaz de mostrar todos los valores locales que usa tu demostración y tu objetivo actual.
La táctica sorry hace que cualquier demostración parezca correcta.
Por esta razón, el teorema check podría parecer que pasa la verificación de tipos automáticamente antes de que se escriba realmente alguna demostración.
Una vez que elimines sorry de tu demostración, Lean InfoView mostrará la retroalimentación correcta.
Demostrar teoremas en Lean
La demostración de teoremas es una parte integral de Lean.
Les permite a los programadores demostrar propiedades sobre sus programas, razonar sobre su comportamiento y codificar restricciones y especificaciones a nivel de tipos.
Este capítulo ofrece una buena introducción a la demostración de teoremas en Lean.
Para profundizar, este libro figura como un recurso oficial en el sitio web de Lean.
Lean ofrece muchas tácticas que pueden automatizar demostraciones, o partes de ellas.
Quizás quieras consultar una referencia del lenguaje.
Podemos usar el atributo del compilador csimp en un teorema que demuestra la igualdad entre dos definiciones.
Este atributo le indica al compilador que use la segunda definición en lugar de la primera:
@[csimp]
theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
... -- proof here
-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.
Es particularmente útil en situaciones en las que una implementación es más eficiente pero menos clara.
Podemos escribir una especificación simple y hacer que el código compilado use la implementación más eficiente en su lugar.
Muchas funciones de List y Array usan este patrón.
