# Mutual Induction Processing Slowdown

**URL:** <https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822>\
**Category:** Using Rocq\
**Created:** [May 4, 2020, 12:49am UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822 "2020-05-04T00:49:13Z")\
**Posts on this page:** 14\
**Page:** 1

<div class="post-metadata">

**Author:** ![RandomActsOfGrammar](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/randomactsofgrammar/32/326_2.png) [@RandomActsOfGrammar](https://discourse.rocq-prover.org/u/RandomActsOfGrammar)\
**Post date:** [May 4, 2020, 12:49am UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/1 "2020-05-04T00:49:13Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![ppedrot](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ppedrot/32/55_2.png) [@ppedrot](https://discourse.rocq-prover.org/u/ppedrot)\
**Post date:** [May 5, 2020, 7:38am UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/2 "2020-05-05T07:38:43Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![RandomActsOfGrammar](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/randomactsofgrammar/32/326_2.png) [@RandomActsOfGrammar](https://discourse.rocq-prover.org/u/RandomActsOfGrammar)\
**Post date:** [May 5, 2020, 8:52pm UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/3 "2020-05-05T20:52:25Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![ppedrot](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ppedrot/32/55_2.png) [@ppedrot](https://discourse.rocq-prover.org/u/ppedrot)\
**Post date:** [May 5, 2020, 9:40pm UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/4 "2020-05-05T21:40:36Z")

</div>

> [@RandomActsOfGrammar](#):
>
> 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.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [May 13, 2020, 1:36pm UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/5 "2020-05-13T13:36:26Z")

</div>

> [@RandomActsOfGrammar](#):
>
> Is there a way to reduce the processing time with the addition of a needed mutually-inductive theorem?

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).

---

<div class="post-metadata">

**Author:** ![RandomActsOfGrammar](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/randomactsofgrammar/32/326_2.png) [@RandomActsOfGrammar](https://discourse.rocq-prover.org/u/RandomActsOfGrammar)\
**Post date:** [May 15, 2020, 1:59am UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/6 "2020-05-15T01:59:23Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [May 15, 2020, 7:45am UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/7 "2020-05-15T07:45:30Z")

</div>

FWIW this is the relevant part of the reference manual: [\<no title\> — Coq 8.18.0 documentation](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:

> <https://github.com/Blaisorblade/dot-iris/blob/b70642f00f8050228a4dace8b92e16608cc28325/theories/Dot/fundamental.v#L25-L34>

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

> <https://github.com/Blaisorblade/dot-iris/blob/08792a0c5f320f7aad5a62343b75e46661ab7ca3/theories/Dot/fundamental.v#L34-L46>

---

<div class="post-metadata">

**Author:** ![ppedrot](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ppedrot/32/55_2.png) [@ppedrot](https://discourse.rocq-prover.org/u/ppedrot)\
**Post date:** [May 16, 2020, 12:28pm UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/8 "2020-05-16T12:28:39Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![RandomActsOfGrammar](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/randomactsofgrammar/32/326_2.png) [@RandomActsOfGrammar](https://discourse.rocq-prover.org/u/RandomActsOfGrammar)\
**Post date:** [May 16, 2020, 8:45pm UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/9 "2020-05-16T20:45:11Z")

</div>

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](https://github.com/RandomActsOfGrammar/public-examples/blob/master/mutual-induction-slowdown/short.v)

The modified version: [long.v](https://github.com/RandomActsOfGrammar/public-examples/blob/master/mutual-induction-slowdown/long.v)

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

---

<div class="post-metadata">

**Author:** ![ppedrot](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ppedrot/32/55_2.png) [@ppedrot](https://discourse.rocq-prover.org/u/ppedrot)\
**Post date:** [May 17, 2020, 11:08am UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/10 "2020-05-17T11:08:28Z")

</div>

This is definitely a variant of [bug #5702](https://github.com/coq/coq/issues/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.

---

<div class="post-metadata">

**Author:** ![RandomActsOfGrammar](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/randomactsofgrammar/32/326_2.png) [@RandomActsOfGrammar](https://discourse.rocq-prover.org/u/RandomActsOfGrammar)\
**Post date:** [May 17, 2020, 9:39pm UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/11 "2020-05-17T21:39:20Z")

</div>

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](https://github.com/RandomActsOfGrammar/public-examples/blob/master/mutual-induction-slowdown/fixed.v) is the fixed version.

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [May 18, 2020, 6:40am UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/12 "2020-05-18T06:40:45Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![RandomActsOfGrammar](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/randomactsofgrammar/32/326_2.png) [@RandomActsOfGrammar](https://discourse.rocq-prover.org/u/RandomActsOfGrammar)\
**Post date:** [May 18, 2020, 7:24pm UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/13 "2020-05-18T19:24:06Z")

</div>

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](https://github.com/RandomActsOfGrammar/public-examples/blob/master/mutual-induction-slowdown/fixed-faster.v) 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?

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [May 19, 2020, 6:34am UTC](https://discourse.rocq-prover.org/t/mutual-induction-processing-slowdown/822/14 "2020-05-19T06:34:21Z")

</div>

A few comments:

- 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.