Do not store recursive trees anymore in inductive blocks.

[ppedrot]

This data is now useless as it can be recovered from the compiled automaton.

[yannl35133]

Why is this equivalent, or if not a correct replacement?

[ppedrot]

Who cares, this is funind.

[yannl35133]

I saw you made the same change for elpi.

[yannl35133]

I'm not against it, but you're adding nesting over arrays as recursive here, is this fine?

[ppedrot]

This was a clear oversight, there is no reason to treat array nesting any different than normal inductive nesting here.

[yannl35133]

Do we know for sure that a transition to label Mrec must have a transition back to init? Or is this not the expected meaning of mis_is_recursive.

[ppedrot]

Hmm, upon reading the code and testing some edge cases, it's not always the case. Nesting over an inductive that does not use its parameter still generates an Mrec node. But then I guess that the question is what it means for an inductive to be truly recursive. Is the following truly recursive for instance?

Inductive box (A : Type) := Box : box A -> box A.
Inductive foo := Foo : box foo -> foo.

[ppedrot]

(I think that a reasonable spec is that an inductive is truly recursive if its associated minimal automaton has a loop, but then we have to understand why the callers where using this in the first place.)

[ppedrot]

Even if it disappears by non-uniform expansion of nesting types? The following qualifies as recursive with your criterion:

Inductive box (A : Type) :=.
Inductive foo := Foo : box foo -> foo.

but it's finite, even empty, and you can prove that without recursion.

[SkySkimmer]

Inductive loop := Lopp : loop -> loop is empty but also recursive IMO, so emptiness cannot force nonrecursive

[SkySkimmer]

BTW declareInd (outside the kernel) has a syntactic check to forbid declaration of recursive (by my above definition) inductives with Variant, but even if that check is disabled Variant foo := Foo : box foo -> foo. fails:

Error:
Bad inductive definition.
Raised at Indtypes.check_positivity_one.check_constructors.check_constr_rec in file "kernel/indtypes.ml", line 365, characters 16-65

[yannl35133]

if that check is disabled

Variant t := c (x := t) : x -> x. (or simply side-stepped)

[yannl35133]

But in any case, being recursive and being barred from being a Variant should be the same imo.

(Speaking of which, you didn't answer: does the inductive type I gave above qualify as "truly recursive"?

I don't have an opinion of what should count as recursive. I looked at all use-cases and found the following:

• Rocq-elpi's coq.env.recursive? which I don't understand
• funind's business, which I don't want to understand
• firstorder's formula.ml which apparently only expects And, Or and recursive types, and that I don't understand
• indrec and allScheme, for which being recursive means the eliminator needs to be a fixpoint
• hipattern's match_with_tuple, used in descend_in_conjunctions, used to not loop into infinitely deep conjunctions.

[yannl35133]

I can accept on behalf of @rocq-prover/kernel-maintainers but real users should be the ones to comment on the changes this PR introduces.