The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-09-08 21:44 GMT+02:00 Gregory Malecha <gmalecha AT cs.harvard.edu>:

You might be able to do something with computation, but it depends on your exact of [inversion]. If you were doing equalities then you might be able to write a lemma like:

Lemma inv_my_type_eq : forall a b : my_type,

  a = b ->

  match a , b with

  | ... , ... => ....

  end.

​I would advise to be more careful if you have 400+ constructors. This kind of pattern matching expands to 1600+ cases, and is not especially wishable.

 

Then, when you apply that lemma to [a] and [b] which have head constructors reduction gives you the appropriate case for free. Whether this will be faster or not I'm not certain, but it might be. Cedric's solution is probably a better way to go though.

On Mon, Sep 7, 2015 at 7:58 AM, Petar Maksimovic <petar.maksimovic AT gmail.com> wrote:

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.

What I've done to speed it up is to 'precompile' the inversion
principles using Derive Inversion for each of the constructors and
then build a custom tactic that uses these principles; this does speed
up the proofs immensely. The compilation process for the files that
hold the Derive Inversions is still horribly slow, but that is
expected and tolerable. The problem I'm having is that when I do a
Require Import or Export of these files in Proof General & Emacs, this
takes a very long time as well. This is also the case for compilation
of such files with coqc, even with the -dont-load-proofs directive in
place.

My current solution is to take all the generated induction principles,
print them into a separate file and declare them as axioms there. That
gives me the desired speedup, but is essentially a hack.

My questions are:

- Is there another way to speed up inversion?
- Is there a way to load the compiled libraries quicker?

Thanks, cheers,
Petar

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/