Zulip Chat Archive

Stream: new members

Topic: Inductive families confusion


Andrea Delmastro (Mar 08 2022 at 11:42):

Hello, I'm trying to figure out how inductive definitions work in Lean, but I think my question may be about a more general theoretical confusion about them.
In TPL, chapter 7, section 7, inductive families are introduced. What i can't figure out is the difference with a simpler inductive definition. For example

inductive vector (α : Type u) : nat  Type u
| nil {}                              : vector zero
| cons {n : } (a : α) (v : vector n) : vector (succ n)

Why isn't alpha considered an index? Why the definition is not something like

inductive vector :  Type u   nat   Type u?

The same is valid for lists,

inductive list (α : Type*)
| nil {} : list
| cons : α  list  list

why the type α of the list is not part of the indexes? Aren't we declaring a family of inductive types ranging on α?

Jakub Kądziołka (Mar 08 2022 at 11:54):

here, for each \a you have a separate inductive type. indices may change within the recursion

Jannis Limperg (Mar 08 2022 at 12:00):

Indices indeed generalise parameters, so you could only use indices when defining your inductive types. An inductive type with parameters is isomorphic -- and therefore morally equal -- to the same inductive type with indices. However, indices give a less convenient recursor and I believe tactics which wrap the recursor, particularly induction, may work less well. So it's a good idea to use parameters where possible.

Andrea Delmastro (Mar 08 2022 at 12:30):

So it's a good idea to use parameters where possible

So, accordingly with what @Jakub Kądziołka said, it would be a good practice to use a parameter every time I do not need to change the index in recursion?

Jannis Limperg (Mar 08 2022 at 12:33):

Yes, exactly.


Last updated: Dec 20 2023 at 11:08 UTC