The Coq mailing list

[Petar Maksimovic <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.

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