Zulip Chat Archive

Stream: general

Topic: recursion over list-nested inductives


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

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

view this post on Zulip Sebastian Ullrich (Jun 17 2019 at 12:59):

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

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

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

view this post on Zulip Chris Hughes (Jun 17 2019 at 13:03):

I think inductive types have a sizeof

view this post on Zulip Chris Hughes (Jun 17 2019 at 13:05):

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

view this post on Zulip Kevin Buzzard (Jun 17 2019 at 13:05):

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

view this post on Zulip Chris Hughes (Jun 17 2019 at 13:07):

It's 2

view this post on Zulip Sebastian Ullrich (Jun 17 2019 at 13:08):

obviously

view this post on Zulip Chris Hughes (Jun 17 2019 at 13:09):

Turns out Type has sizeof as well.

view this post on Zulip Reid Barton (Jun 17 2019 at 13:10):

is it interesting?

view this post on Zulip Chris Hughes (Jun 17 2019 at 13:11):

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

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

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

view this post on Zulip Reid Barton (Jun 17 2019 at 13:13):

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

view this post on Zulip Chris Hughes (Jun 17 2019 at 13:17):

For some reason sizeof [] is 1 not 0

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

view this post on Zulip Sebastian Ullrich (Jun 17 2019 at 13:17):

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

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

view this post on Zulip Reid Barton (Jun 17 2019 at 13:24):

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

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

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

view this post on Zulip Chris Hughes (Jun 17 2019 at 20:10):

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

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

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

view this post on Zulip Mario Carneiro (Jun 17 2019 at 21:03):

something like total size would work pretty well

view this post on Zulip Mario Carneiro (Jun 17 2019 at 21:04):

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

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

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

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