Instrucciones
Tu tarea es demostrar la igualdad entre una función personalizada que invierte listas y la función integrada List.reverse.
Debido a la naturaleza de este ejercicio, en lugar de depender de las pruebas en tiempo de ejecución tradicionales, la demostración se comprueba mediante un teorema check.
Puedes dar por superada la prueba si este teorema pasa la comprobación de tipos.
Si trabajas en local o en el playground en línea de Lean, obtendrás información instantánea sobre si algún teorema se cumple 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 este motivo, puede parecer que el teorema check supera la comprobación de tipos automáticamente antes de que se escriba realmente ninguna demostración.
Una vez que elimines sorry de tu demostración, Lean InfoView mostrará la información correcta.
Demostración de teoremas en Lean
La demostración de teoremas es una parte integral de Lean.
Permite a quienes programan 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 más, este libro figura como recurso oficial en el sitio web de Lean.
Lean ofrece muchas tácticas que pueden automatizar demostraciones, o partes de ellas.
Quizá te interese consultar una referencia del lenguaje.
Podemos usar el atributo del compilador csimp en un teorema que demuestre la igualdad entre dos definiciones.
Este atributo 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`.
Resulta especialmente útil en situaciones en las que una implementación es más eficiente pero menos clara.
Podemos escribir una especificación sencilla y hacer que el código compilado use en su lugar la implementación más eficiente.
Muchas funciones de List y Array siguen este patrón.
