The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Hello,

Interesting. Petar, could I have a look at your inductive type?

Jean-François

On Wed, Sep 09, 2015 at 04:57:18PM +0200, 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

-- 
Jean-Francois Monin
Resp. dpt RICM (Informatics)
Polytech Grenoble, Universite Joseph Fourier - Grenoble 1
http://www.polytech-grenoble.fr/ricm.html
Lab VERIMAG http://www-verimag.imag.fr