I already asked this questions on the Coq-Club mailing list, but was told it might be a good idea to try here as well.
When changing one of my inductive definitions I get the following error
when generating an induction principle using "Combined Scheme":
Error: decompose_prod_n: not enough products
What does this error mean? According to the Index of Errors and Warnings
in the reference manual (https://coq.inria.fr/refman/coq-exnindex.html)
this error doesn't even exist.
I don't know what this error means. However, note that:
So feel free to open an issue regarding this error message, to have it documented at least, or improved (even better).
Would it be fine to submit the issue even without an example? The example depends on several large files and I do not know how to reproduce the error with a smaller example yet.
see the coq bug minimizer here: https://github.com/JasonGross/coq-tools
@Jan Menz Looks like an internal issue in the tactic code generating the scheme. Maybe your inductive has a shape that is not recognized by the scheme generator.
@Pierre-Marie Pédrot I would be surprised if the shape wasn't recognised at all. A different "Combined Scheme" definition using a larger subset of the mutually inductively defined propositions works just fine.
If you have a minimal example, as e.g. generated by the minimizer, it could be scrutinized.
I'm looking at the minimizer at the moment trying to figure out how it works. It'll probably take a while. I'll probably be running into the known problem with python in Windows.
That's more like an anomaly actually, so indeed not an error but a bug in Coq likely.
Note that it is also fine to point to a large example if this is something that you have somewhere in a public branch (if you don't manage to do the minimization yourself).
I wasn't able to get the minimizer to work, but I was able to minimize the example to a reasonable size by hand. I submitted the issue here: https://github.com/coq/coq/issues/13342
Last updated: Sep 26 2023 at 12:02 UTC