Zulip Chat Archive

Stream: general

Topic: Nesting eqv_gen inside con_gen


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Chris Hughes (Sep 15 2020 at 19:09):

The code for nested inductives is in core.

view this post on Zulip Eric Wieser (Sep 15 2020 at 19:47):

As lean or C++?

view this post on Zulip Eric Wieser (Sep 15 2020 at 20:04):

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.

view this post on Zulip 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 library/inductive_compiler/ginductive*.cpp.

view this post on Zulip Eric Wieser (Sep 15 2020 at 20:47):

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

view this post on Zulip 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...)

view this post on Zulip 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 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.

view this post on Zulip Eric Wieser (Sep 21 2020 at 21:19):

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.


Last updated: May 06 2021 at 21:09 UTC