The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-09-07 16:58 GMT+02:00 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.

​I am curious of what would lead to such a big inductive type.

The only big inductive type I tried to make once was for the ASCII type, I believe (thus not using the one in the stdlib).

Can't you regroup many of your constructors in a more structured way?

I mean something like:

Inductive type1 :=

| T1C1 : type1

| T1C2 : type1.

Inductive type2 := …

Inductive type3 := …

Inductive my_big_type :=

| Type1 : type1 -> my_big_type

| Type2 : type2 -> my_big_type

| Type3 : type3 -> my_big_type.

​

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 the situation is the same as what it was some years ago, it might be the case (inversion produced needlessly big terms, and you end up with equalities in your context).​ There were more clever ways to do it, but were not automatized. The situation might have changed now. (still, for backward compatibility, a new name for such a tactic might have been taken).

 

- Is there a way to load the compiled libraries quicker?

​You can try to optimize your proofs, so that proof terms are smaller (but this has to be done manually, as there is no proof optimizer I know of in Coq)​.

You can do a variation of your hack:

declare a Record (or a Module, you have to decide which one is faster/more convenient) containing all your "axioms" and make your definitions depending on it.

In a separate file, you instantiate them with your Derive Inversion, so that you "prove" your axioms, and feed your main proofs with it.

This would look like:

(* File 1 *)

Module Type Inversions.

  Parameter axiom1 : …

  Parameter axiom2 : …

   …

End Inversions.

(* File 2 *)

Require Import File1.

Module PartialProofs (INV : Inversions).

  … (* use INV.axiom1, INV.axiom2, … *)

End PartialProofs.

 

​(* File 3 *)​

Require Import File1.

​Module Derivations :​ Inversions.

  Derive Inversion …

  Definition axiom1 := …

  …

End Derivations.

Module Proofs := PartialProofs(Derivations).

Thanks, cheers,
Petar