bbb, code d'accès 394787
17 June 2021 - 14h00
[FormalProofs] Dealing with ugly proof environment.
by Pierre Courtieu from CNAM-CEDRIC
Abstract: This is an informal presentation, mainly a demo. I will show several small enhancements of both coq and proofgeneral to deal with big and/or ugly proof environments. The main feature on which most of these enhancements rely on is a simple new tactical ";;" that applies a tactic to any "new" hypothesis generated by another tactic. From there a small set of "cleaning" tactics was developed, comparable to ssreflect "administrative" postfix operators, but in a more Ltac-ish fashion.
I will describe these tactics and especially among them a prototype of "automatic naming of new hypothesis" tactical. Its purpose is to discharge the user from the tedious task of naming his hypothesis and, more importantly, RE-naming them when updating/maintaining a proof.
I will also describe a few small proofgeneral enhancements that also take advantage of this features.
