Détails sur le séminaire

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.




Contact | Plan du site | Site réalisé avec SPIP 3.1.15 + AHUNTSIC [CC License]

info visites 1804228