Notons tout de même que l'automatisation se développe énormément, d'abord la théorie des types en contient intrinsèquement une dose (l'égalité définitionnelle), ensuite Rocq comme Lean (et sûrement Agda, mais je connais moins bien) ont des tactiques qui font de la recherche automatique de preuve, et Lean a une tactique « simpl » très appréciée pour simplifier toutes sortes de buts. De manière plus générale, Rocq et Lean ont de grosses bibliothèques de tactiques (voir p.ex. https://rocq-prover.org/doc/V8.20.0/refman/coq-tacindex.html) pour faire plein d'étapes de preuve à la fois.
Par exemple, la preuve de 2+2=4 en Lean est triviale (c'est un exemple d'égalité définitionnelle) :
[^] # Re: Preuves de programme et preuves de théorèmes
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 2. Dernière modification le 24 mars 2025 à 17:45.
Notons tout de même que l'automatisation se développe énormément, d'abord la théorie des types en contient intrinsèquement une dose (l'égalité définitionnelle), ensuite Rocq comme Lean (et sûrement Agda, mais je connais moins bien) ont des tactiques qui font de la recherche automatique de preuve, et Lean a une tactique « simpl » très appréciée pour simplifier toutes sortes de buts. De manière plus générale, Rocq et Lean ont de grosses bibliothèques de tactiques (voir p.ex. https://rocq-prover.org/doc/V8.20.0/refman/coq-tacindex.html) pour faire plein d'étapes de preuve à la fois.
Par exemple, la preuve de 2+2=4 en Lean est triviale (c'est un exemple d'égalité définitionnelle) :