recursion over list-nested inductives

Stream: general

[Sebastian Ullrich]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

I think inductive types have a sizeof

[Chris Hughes]

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

[Kevin Buzzard]

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

[Chris Hughes]

It's 2

[Sebastian Ullrich]

obviously

[Chris Hughes]

Turns out Type has sizeof as well.

[Reid Barton]

is it interesting?

[Chris Hughes]

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

[Sebastian Ullrich]

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]

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

[Reid Barton]

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

[Chris Hughes]

For some reason sizeof [] is 1 not 0

[Sebastian Ullrich]

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]

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

[Chris Hughes]

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]

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

[Mario Carneiro]

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]

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]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

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

[Mario Carneiro]

something like total size would work pretty well

[Mario Carneiro]

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

[Sebastian Ullrich]

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]

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]

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.