The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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