Instructions
Ta tâche consiste à prouver l'égalité entre une fonction personnalisée qui renverse une liste et la fonction intégrée List.reverse.
En raison de la nature de cet exercice, plutôt que de s'appuyer sur des tests d'exécution classiques, la preuve est vérifiée par un théorème check.
Tu peux considérer que le test est réussi si ce théorème passe la vérification des types.
Si tu travailles en local ou dans le bac à sable en ligne de Lean, Lean InfoView t'indique immédiatement si un théorème réussit ou échoue, et pourquoi il échoue.
C'est un outil précieux, capable de montrer toutes les valeurs locales utilisées par ta preuve, ainsi que ton objectif actuel.
La tactique sorry donne l'impression que n'importe quelle preuve est correcte.
C'est pourquoi le théorème check peut sembler se vérifier automatiquement avant même qu'une preuve ne soit réellement écrite.
Une fois que tu as retiré sorry de ta preuve, Lean InfoView affichera le retour correct.
Démontrer des théorèmes en Lean
La démonstration de théorèmes fait partie intégrante de Lean.
Elle permet aux développeurs de démontrer des propriétés sur leurs programmes, de raisonner sur leur comportement et d'encoder des contraintes et des spécifications au niveau du type.
Ce chapitre constitue une bonne introduction à la démonstration de théorèmes en Lean.
Pour aller plus loin, ce livre est répertorié comme ressource officielle sur le site de Lean.
Lean offre de nombreuses tactiques qui peuvent automatiser des démonstrations, ou des parties de celles-ci.
Tu peux aussi jeter un œil à une référence du langage.
On peut utiliser l'attribut du compilateur csimp sur un théorème qui démontre l'égalité entre deux définitions.
Cet attribut demande au compilateur d'utiliser la seconde définition à la place de la première :
@[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`.
Il est particulièrement utile lorsqu'une implémentation est plus efficace mais moins claire.
On peut écrire une spécification simple et faire en sorte que le code compilé utilise à la place l'implémentation plus efficace.
De nombreuses fonctions de List et Array utilisent ce schéma.
