Dear all,
we are pleased to announce the release of our Rocq plugin for the automatisation of proxy-based small inversions.
It is still prototype, remarks and suggestions are welcome.
The repository to install and use the plugin can be found here.
Proxy-based small inversions are an alternative to the Rocq tactic inversion and Equations’ tactic dependent elimination.
The size of the generated terms are significantly reduced, an especially interesting feature when defining dependently typed functions. Dependent proxy-based small inversions allow to conveniently reason about such functions. The technique uses intermediate definitions that are usually handwritten. This package allows the user to automatically perform those definitions with a simple Derive InvProxy command.
For more details on small inversions, you can refer to this preprint.
Basile Gros
Pierre Corbineau
Jean-François Monin