Room 206 (2nd floor, badged access)
17 June 2024 - 16h00
Small Inversions in Coq
by Basile GROS from Verimag, UGA
Abstract: The inversion tactic is one of the most powerful reasoning technique in the Coq proof assistant.
However, it produces proof terms that are clunky and unpredictable.
J-F Monin has proposed a lightweight approach to inversion by defining intermediate data structures and using the destruct tactic. This new technique is more transparent and produces readable proof terms.
We propose a mechanized version of the technique by leveraging the MetaCoq TemplateMonad tool to manipulate the inductive definitions that are used for small inversions. The talk will present the small inversions methods as well as demonstrate our generation tool, then we will discuss its current limitations and planned extensions.
Séminaire dans le cadre de la visite de M. Sozeau et Y. Forster à Verimag.
