The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

You may be interested in the experience that we have acquired formalizing 
various complex mathematical concepts. Writing “flat” definitions where all 
components are put linearly in one record leads to very slow processing time. 
Building definitions in the form of roughly balanced binary trees using only 
dependent sums, while it requires more care and thinking at the beginning 
leads to code that compiles very fast.

I do not know if it applies to your case since there may be fewer internal 
structures in the list of  ARMv7 instructions than in the mathematical 
definitions but maybe its’ worth a try.

Vladimir.

PS The speed-up comes from the fact that in many cases there is no need to 
unfold the definitions on the branches away from the path from the node that 
you need to the root.



> On Sep 9, 2015, at 5:46 PM, 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

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail