I have found that adding or removing a theorem in a set of mutually-inductive theorems can significantly affect the processing time.
For example, I had five mutually-inductive theorems. The time to compile the file was about 2 hours and 45 minutes. By modifying one definition, I was able to combine two of these into one theorem with the same proof cases. With these four mutually-inductive theorems, the time to compile the file was about 10 minutes.
In a different case, I had to modify some definitions to add a couple of cases in a proof and add a theorem to a set of mutually-inductive theorems. This changed the processing time from a few minutes to several hours.
Why does the addition or removal of a single theorem in a set of mutually-inductive theorems without other significant changes so affect the time to process a proof? Is there a way to reduce the processing time with the addition of a needed mutually-inductive theorem?
It is hard to say without further details. If you use automation a lot, it might be the case that you generate many more goals that are silently solved, but which are triggering this slowdown. A typical problem that can arise is when matching over two inductive terms at once, which is quadratic in the number of constructors.
If you have a reasonable self-contained example you can file a bug on the GitHub page, and I will have a look at it.
I’m afraid I don’t have a reasonable self-contained example. Both of the examples which inspired this question are theorems a few hundred lines long.
I don’t think the problem is automation solving hidden goals, although that is a good suggestion. My uses of automation are restricted to handling the premises of an applied theorem.
Can you elaborate on what you mean by “matching over two inductive terms at once”? My Coq terminology is rather limited, and I don’t think you’re referring to a match expression.
I am actually referring to a match expression, even though it can be generated through tactics, e.g. by using destruct or induction. The stereotypical example of a quadratic behaviour is the proof of forall x y : I, {x = y} + {x <> y} for some inductive type I := c_1 | ... | c_n. If you write something along the lines of induction x; destruct y; congruence you’ll get a O(n²) term.
Are you using Theorem ... with? Termination checking can be very slow there, so you should at least add the correct {struct ...} annotations (which IIRC requires replacing Theorem by Fixpoint).
Even better, you can define and use induction principles using Combined Scheme; that way, you pay the high cost of termination checking only once.
(I can add pointers if relevant).
I am using Theorem ... with. Can you direct me to some resource(s) about {struct ...}? I’m not familiar with it, and I couldn’t find it in the documentation. I was able to find Combined Scheme in the documentation, so I can try that.
Writing explicit annotations can also speed up type checking of large mutual fixpoints.
Here’s one usage example from my code:
and how I changed it to use a mutual induction principle (one must combine the statements and massage them so that the principle applies, then use apply mutual_principle_name:
I pulled out one of the theorems where I’m seeing the slowdown. The slowdown happened when I modified definitions, which added a mutually-inductive theorem, along with a few cases.
The original version, which compiles in less than two seconds for me: short.v
This is definitely a variant of bug #5702. The check to noccur_with_meta in Inductive.check_one_cofix is obviously quadratic in the size of the term. A workaround would be not to use Theorem ... with but instead prove this using a generated mutual scheme.
Thank you for the help. Using Blaisorblade’s suggestion of defining the theorems using Fixpoint, I was able to process the full proof in about two minutes.
For any future readers who would like to compare, here is the fixed version.
I was satisfied with two minutes because it was better than the previous time of hours without finishing. I used a combined scheme and it was able to process the Qed in less than half a second. This version is here for any future readers.
How ought one decide whether to use Theorem ... with, Fixpoint and {struct ...}, or a combined scheme? For speed, the order is combined scheme, Fixpoint and {struct ...}, and Theorem ... with, but it is reversed, in my opinion, for clarity of what is being done. Perhaps there is some way to recognize when a theorem will require a faster method for processing?
Is Combined Scheme unclear? How? That can hopefully be made clearer in easy ways, by revising docs or syntax.
Theorem/Fixpoint with is prone to producing proof scripts that seem to work, but fail at Qed.
FWIW, I had never seen a Coq file take hours because of Theorem with (or for any reason).
There’s a proposal to allow (and encourage) struct annotations for Theorem with; that should help clarity.
All uses of Theorem with can be rephrased using an induction principle, but not always the generated one. Sometimes you need to write your own principle, using Theorem with, but typically that doesn’t take so long to typecheck, because there’s less to inline.