The Coq mailing list

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

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