bbb, code d'accès 394787
17 juin 2021 - 14h00
[FormalProofs] Gestion d'un environment de preuve moche
par Pierre Courtieu de CNAM-CEDRIC
Résumé : Présentation informelle, principalement une démo, de quelques petites améliorations de Coq et proofgeneral dédiées à la gestion des environnements de preuve moche. Ces améliorations se basent en grande partie sur un petit tactical ;; qui permet d'appliquer une tactique à chacune des hypothèses créées par une autre tactique. À partir de là un petit ensemble de tactiques de nettoyage d'environnement de preuve a été développé, un peu dans l'esprit de ssrefelct mais dans un style plus proche de Ltac. Je décrirait ces tactiques, et en particulier un prototype de tactique de nommage automatique des nouvelles hypothèse, dont le but est de décharger l'utilisateur de la tâche sans intérêt consistant à nommer ses hypothèses, et surtout les RE-nommer lors des mise à jour de
scripts. J'en profiterai pour signaler quelques fonctionnalités de proofgeneral qui ont le même objectif.
