coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Speeding up inversion on large inductives

From: Petar Maksimovic <petar.maksimovic AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Speeding up inversion on large inductives
Date: Wed, 9 Sep 2015 18:10:33 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=petar.maksimovic AT gmail.com; spf=Pass smtp.mailfrom=petar.maksimovic AT gmail.com; spf=None smtp.helo=postmaster AT mail-lb0-f171.google.com
Ironport-phdr: 9a23:BblAEBYl20DOmWHLulcOqtv/LSx+4OfEezUN459isYplN5qZpci8bnLW6fgltlLVR4KTs6sC0LqK9fm8Ej1bqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7z0osGYMl4ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JamgKmwAAJgHG9xD/WYnwuWOurudh0TPcOMT1VrExXiqj5I9kTRbpjGEMMDtvozKfsdB5kK8O+EHpnBd42YOBOIw=

Hi Jean-François,

Yes, by all means. It starts here:
https://github.com/resource-reasoning/jscert_dev/blob/master/coq/JsPrettyRules.v#L739
and ends on line 4777 of the same file.

Cheers and thanks,
Petar

On 9 September 2015 at 18:03, Jean-Francois Monin
<jean-francois.monin AT imag.fr>
wrote:
> 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

[Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/07/2015
- Re: [Coq-Club] Speeding up inversion on large inductives, Cedric Auger, 09/08/2015
  - Re: [Coq-Club] Speeding up inversion on large inductives, Xavier Leroy, 09/09/2015
    - Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015
      - Re: [Coq-Club] Speeding up inversion on large inductives, Jean-Francois Monin, 09/09/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/09/2015
        
        RE: [Coq-Club] Speeding up inversion on large inductives, Soegtrop, Michael, 09/10/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Pierre Courtieu, 09/10/2015
        Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/10/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Enrico Tassi, 09/10/2015
        RE: [Coq-Club] Speeding up inversion on large inductives, Soegtrop, Michael, 09/10/2015
      - Re: [Coq-Club] Speeding up inversion on large inductives, Robbert Krebbers, 09/09/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Thomas Braibant, 09/10/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Jean-Francois Monin, 09/10/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Petar Maksimovic, 09/11/2015
        
        Re: [Coq-Club] Speeding up inversion on large inductives, Alan Schmitt, 09/15/2015