The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

The plugin has not been maintained too much. However, if your inductive falls into the scope of what it can handle [1], you should get a much faster/smaller inversion principle out of the box. 

[1] That is, it does not support completely type families with dependent types. 

On Wed, Sep 9, 2015 at 6:09 PM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

Pierre Boutillier and Thomas Braibant developed a plugin to automate Monin's approach. See:

  https://github.com/braibant/invert

I do not know whether there is a newer (and maintained) version.

On 09/09/2015 04:57 PM, Petar Maksimovic wrote:

Hi Xavier - that's a good idea, and I have already tried to adapt the
work of Monin and Shi, but I was unable to automate the generation of
their principles, and writing them by hand for each of the
constructors wasn't an option.

Cheers,
Petar

On 9 September 2015 at 16:46, Xavier Leroy <xavier.leroy AT inria.fr> wrote:

2015-09-07 16:58 GMT+02:00 Petar Maksimovic <petar.maksimovic AT gmail.com
<mailto:petar.maksimovic AT gmail.com>>:

     Hello everyone,

     I'm working on a development where there's an inductive type with 400+
     constructors. Recently, it has become necessary to invert on it
     regularly, and this takes an exceedingly long time.

You might be interested in the work of Monin and Shi on "small inversions":
http://www-verimag.imag.fr/~monin/Proof/SmallInvScalesUp/paper.pdf
I'm not sure their approach solves your problems, but it could help.

On 08/09/2015 09:43, Cedric Auger wrote:

I am curious of what would lead to such a big inductive type.

One example: full modeling of the instruction set of a modern processor
architecture.  ARMv7 has 413 instructions, and don't get me
started about ARMv8...

- Xavier Leroy