The Coq mailing list

[Xavier Leroy <xavier.leroy AT inria.fr>]

> 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