# Mutual Induction Processing Slowdown

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.

1 Like

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.

FWIW this is the relevant part of the reference manual: https://coq.inria.fr/refman/language/gallina-specification-language.html#coq:cmd.fixpoint

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`:

@RandomActsOfGrammar can you post your slowdown examples somewhere publicly? I’d be curious to have a look at it.

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

The modified version: long.v

The theorem is `basic_eval_unique` at the end of both files.

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.

1 Like

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.

Combined Scheme (the same as @ppedrot suggested) would likely be even faster. Taking 2 minutes for a Qed sounds still too much.

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?

• FWIW, I had never seen a Coq file take hours because of `Theorem with` (or for any reason).