The Coq mailing list

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

I am trying to get the plugin running, but I'm experiencing various
difficulties. How exactly am I supposed to use it?

Cheers,
Petar

On 10 September 2015 at 23:46, Jean-Francois Monin
<jean-francois.monin AT imag.fr>
 wrote:
> As far as I can see on
> https://github.com/jscert/jscert/blob/master/coq/JsPrettyRules.v
> there is nothing complicated.
>
> Clauses look like:
> Inductive red_stat : state -> execution_ctx -> ext_stat -> out -> Prop :=
>  ...
>  | red_stat_while_2_true : forall S0 S C labs e1 t2 rv o1 o,
>       red_stat S C t2 o1 ->
>       red_stat S C (stat_while_3 labs e1 t2 rv o1) o ->
>       red_stat S0 C (stat_while_2 labs e1 t2 rv (vret S true)) o
>   ...
>
> JF
>
> On Thu, Sep 10, 2015 at 10:21:23PM +0200, Thomas Braibant wrote:
>>    The plugin has not been maintained too much. However, if your inductive
>>    falls into the scope of what it can handle [1], you should get a much
>>    faster/smaller inversion principle out of the box.
>>    [1] That is, it does not support completely type families with dependent
>>    types.
>>    On Wed, Sep 9, 2015 at 6:09 PM, Robbert Krebbers
>>    
>> <[1]mailinglists AT robbertkrebbers.nl>
>>  wrote:
>>
>>      Pierre Boutillier and Thomas Braibant developed a plugin to automate
>>      Monin's approach. See:
>>
>>        [2]https://github.com/braibant/invert
>>
>>      I do not know whether there is a newer (and maintained) version.
>>
>>      On 09/09/2015 04:57 PM, 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 
>> <[3]xavier.leroy AT inria.fr>
>>        wrote:
>>
>>            2015-09-07 16:58 GMT+02:00 Petar Maksimovic
>>            
>> <[4]petar.maksimovic AT gmail.com
>>            
>> <mailto:[5]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":
>>          
>> [6]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