The Coq mailing list

[Petar Maksimovic <petar.maksimovic AT gmail.com>]

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