Eric Wieser (Sep 15 2020 at 16:13):
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 (Sep 15 2020 at 17:46):
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 (Sep 15 2020 at 17:48):
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
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 (Sep 15 2020 at 17:51):
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 (Sep 15 2020 at 19:00):
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 (Sep 15 2020 at 19:09):
The code for nested inductives is in core.
Eric Wieser (Sep 15 2020 at 19:47):
As lean or C++?
Eric Wieser (Sep 15 2020 at 20:04):
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 (Sep 15 2020 at 20:40):
The recursor is probably in
kernel/inductive/inductive.cpp. The mutual/nested inductive stuff might be in
Eric Wieser (Sep 15 2020 at 20:47):
Is it deliberate that for
T above, only
rec and not
rec_on is generated?
Jannis Limperg (Sep 15 2020 at 21:06):
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 (Sep 21 2020 at 08:05):
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
- 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 (Sep 21 2020 at 21:19):
My understanding was that the difference between
.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.
Last updated: Aug 03 2023 at 10:10 UTC