This place is dedicated to small inversions for Coq and Rocq.

PBSI

The more recent development is called PBSI (proxy-based small inversions). It is largely automated in a tool mainly developed by Basile Gros, during its PhD under the supervision of Pierre Corbineau and Jean-François Monin. This tool is available here:

https://github.com/BasileGros/proxy-based-small-inversions

History (sketch)

• 2010: first version published at the Coq Workshop
• 2013: second version published at ITP, based on continuations
• 2015-now: unpublished version used in teaching, based on auxiliary algebraic types. Became basic PBSI.
• 2026: PBSI published at LPAR, including dependent PBSI that facilitate the development of Rocq programs with dependent types and of proofs over them.

Coucou