## Stream: general

### Topic: recursion over list-nested inductives

#### Sebastian Ullrich (Jun 17 2019 at 12:28):

I'm surprised that the lemma https://github.com/leanprover/lean/blob/master/tests/lean/run/term_app2.lean#L27 has never made it into mathlib (though list.attach has). Do people just avoid nested inductives in general in Lean 3? Is it ultimately easier to replace a nested occurrence list t -> with (n : nat) -> (fin n -> t) ->?

#### Chris Hughes (Jun 17 2019 at 12:56):

nested inductives don't give the best recursor right now, so I think people tend to avoid them. Also, I tend to use list.length instead of sizeof if I have to induct on a list in that way. I view sizeof as an internal thing. I don't actually know what the sizeof a list is defined to be, though I imagine it's the length.

#### Sebastian Ullrich (Jun 17 2019 at 12:59):

No, it's the sum of element sizes. You couldn't prove such recursions terminating otherwise.

#### Kevin Buzzard (Jun 17 2019 at 13:02):

Does everything have a size? Can we ask what the size of the real numbers are? Or a perfectoid space?

#### Kevin Buzzard (Jun 17 2019 at 13:03):

Like Chris, I have always regarded sizeof as some internal thing which we mortals shouldn't be fiddling with.

#### Chris Hughes (Jun 17 2019 at 13:03):

I think inductive types have a sizeof

#### Chris Hughes (Jun 17 2019 at 13:05):

I would have used list.sum for that sort of induction.

#### Kevin Buzzard (Jun 17 2019 at 13:05):

Great, we could ask what the size of [real] is

#### Chris Hughes (Jun 17 2019 at 13:07):

It's 2

obviously

#### Chris Hughes (Jun 17 2019 at 13:09):

Turns out Type has sizeof as well.

#### Reid Barton (Jun 17 2019 at 13:10):

is it interesting?

#### Chris Hughes (Jun 17 2019 at 13:11):

Non inductive types also have sizeof, but it's just always zero.

#### Sebastian Ullrich (Jun 17 2019 at 13:12):

Every type that may be used in a mutual or nested inductive should have a has_sizeof instance. As Chris said, the value only really matters for actually inductive types, on which you may want to use well-founded induction.

#### Reid Barton (Jun 17 2019 at 13:12):

Type is not an inductive type, is it? So I would have thought it would also have sizeof always zero

#### Reid Barton (Jun 17 2019 at 13:13):

Is 2 counting the two things list and real in list real?

#### Chris Hughes (Jun 17 2019 at 13:17):

For some reason sizeof [] is 1 not 0

#### Sebastian Ullrich (Jun 17 2019 at 13:17):

I wouldn't say sizeof is an implementation detail. If you want to do induction over a mutual or nested inductive, you'll want to use it as the measure, and you'll need to do proofs about it. You could define your own measure, but it would not be drastically different from the synthesized one.

#### Sebastian Ullrich (Jun 17 2019 at 13:17):

If you never do that, you don't have to care about sizeof, of course.

#### Chris Hughes (Jun 17 2019 at 13:22):

But usually I already have theorems about things like list.sum or list.length, but nothing about list.sizeof. These are also nicer definitions to prove things about since they're standard maths definitions, starting at 1 for [] is a bit odd. Also I guess the general definition of sizeof isn't published anywhere, so people aren't going to use it.

#### Reid Barton (Jun 17 2019 at 13:24):

Oh I got fooled by Haskell. [real] is not list real

#### Mario Carneiro (Jun 17 2019 at 20:02):

sizeof only works for well orders that have ordinal height <= omega, so it doesn't work for things like lex order on nat x nat

#### Mario Carneiro (Jun 17 2019 at 20:03):

The advice I give is to avoid it in any manual proof. If lean can use it to completely automate your wf recursion then that's great, but it's basically never the best wf relation for the job

#### Chris Hughes (Jun 17 2019 at 20:10):

I guess that's not @Sebastian Ullrich 's advice

#### Sebastian Ullrich (Jun 17 2019 at 20:54):

I still don't see what other measure you would use on a rose tree-like data type, or why

#### Mario Carneiro (Jun 17 2019 at 21:03):

you probably don't want to get the structure of the elements involved in a rose tree

#### Mario Carneiro (Jun 17 2019 at 21:03):

something like total size would work pretty well

#### Mario Carneiro (Jun 17 2019 at 21:04):

I don't think I want to consider [162] bigger than [0, [1, 1], 0]

#### Sebastian Ullrich (Jun 18 2019 at 07:35):

For the purpose of proving well-foundedness of recursions over the tree, the size of a leaf does not matter. Daniel(?) could have chosen to ignore them when synthesizing sizeof, but I assume it was easier to just sum up all parameters, without no apparent downside.

#### Mario Carneiro (Jun 18 2019 at 07:51):

I think it is important to have them in the instances for sizeof so that the size passes through nested inductives (i.e. you wouldn't get the right answer with nested inductives like list (list T) -> T unless the size of the inner list was represented in the size of the outer list), but it is otherwise undesirable to have parameters be counted in the size. I have had examples where this actually prevents some constructions; for example if you map a rose tree then the "size" should not change, but that's not true if the size of elements matter

#### Sebastian Ullrich (Jun 18 2019 at 08:54):

Ah, you want do a structure-preserving map over the children before recursing into them... in that case sizeof may not work and one should define their own measure, yes. But if this is not the case, I would still default to sizeof, personally.

Last updated: May 08 2021 at 09:11 UTC