Nesting eqv_gen inside con_gen

Stream: general

[Eric Wieser]

In the implementation notes of https://leanprover-community.github.io/mathlib_docs/group_theory/congruence.html, there's some vague note that if you try to do it in a nested way, "the recursor generated does not work".

I've tried to understand this comment by means of assuming it is incorrect, in #4158. As expected, I've run into something I'm not sure how to prove with that structure. Would anyone be able to take a look and rule whether it looks possible, or if I've missed something obvious?

[Chris Hughes]

Nested inductives are supported by reducing them to normal inductives. However the automatically generated recursors are not strong enough to actually characterise the type without unfolding the definitions. nested inductives are basically useless in Lean for this reason.

[Chris Hughes]

As a quick example, take the following nested inductive.

inductive T : Type
| mk : list T → T

This will be implemented as something a bit like this where T' ff is isomorphic to list T and T' tt is isomorphic to T.

inductive T' : bool → Type
| nil : T' ff
| cons : T' tt → T' ff → T' ff
| mk : T' ff → T' tt

The recursor for the nested inductive T should look something like the recursor for T' I think, i.e. you should be able to induct on the list at the same time. However this is not what it does look like.

[Chris Hughes]

So you should always use something like T' instead of the nested inductive, and this is basically how con_gen is already implemented.

[Eric Wieser]

Is obtaining the stronger recursor on the nested type something that needs to be done in lean core, or can it be done within mathlib?

[Chris Hughes]

The code for nested inductives is in core.

[Eric Wieser]

As lean or C++?

[Eric Wieser]

Looks like rec_on comes from https://github.com/leanprover-community/lean/blob/ec1613aef1eee72e601f192b16740629c6d49690/src/library/constructions/rec_on.cpp, I can't work out where rec comes from.

[Jannis Limperg]

The recursor is probably in kernel/inductive/inductive.cpp. The mutual/nested inductive stuff might be in library/inductive_compiler/ginductive*.cpp.

[Eric Wieser]

Is it deliberate that for T above, only rec and not rec_on is generated?

[Jannis Limperg]

I don't see why that should be the case, but maybe there's a reason. @Gabriel Ebner is probably the one most likely to know the answer. (Actually, now that I think about it, this might break one of my tactics...)

[Gabriel Ebner]

Jannis Limperg said:

I don't see why that should be the case, but maybe there's a reason. Gabriel Ebner is probably the one most likely to know the answer. (Actually, now that I think about it, this might break one of my tactics...)

This is interesting. I can guess a few possible reasons:

• You should never use nested inductives (unless you're in meta land)
• If you still use nested inductives, you're supposed to use well-founded recursion. That's why there is a cases_on and no rec_on.
• Most importantly, this is going to change in Lean 4, so don't spend too much time on nested inductives in Lean 3.

[Eric Wieser]

My understanding was that the difference between .rec and .rec_on was only argument order, so I don't understand why the former would be present but not the latter, as is the case for the T type above.