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.
