Coq Call 2021 06 30 - coq/coq GitHub Wiki

Topics

  • (more or less) recent progress on small inversions. I (Jean-François Monin) will show better techniques than the one presented at Coq WS 2010 and ITP13 : a version which is simpler to write and suits many practical needs, and a less easy one which is needed in combination with the guard condition of recursive programs. Both versions are able to deal with cases which seem out of reach of Coq standard inversion.

Notes

Slides at http://www-verimag.imag.fr/~monin/Talks/sir.pdf

Differences:

  • slide 2 replaced with references to code and last paper on the Braga method
  • slide 34 added (useful for dependent data types)

Coq scripts : http://www-verimag.imag.fr/~monin/Proof/Small_inversions/2021/