Dear all,
it is our pleasure to announce that our Rocq plugin for the automation of proxy-based small inversions has received a major update.
Here is the link to its repository:
The user interface has been greatly simplified, and there is a tutorial to both use our automated tool (covering many common cases), and also to understand the basic principles behind it. The latter are not overly complicated, once you catch the idea, so that the end user can tune them to their specific situation when needed.
As a reminder, PBSI are an inversion method that results in significantly smaller and more understandable proof and definition terms compared to the Rocq tactic inversion or the Equations package, which makes PBSI interesting in the context of dependent programming. Moreover, dependent PBSI allow to conveniently reason about such functions. To achieve this, the technique uses intermediate definitions which used to be handwritten. This package allows the user to automatically build those definitions with a simple Derive InvProxy command.
Basile Gros
Pierre Corbineau
Jean-François Monin