Locally finite poset

Stream: general

[Yaël Dillies]

I just read the TODO in data.list.intervals and I was indeed thinking the same thing. Defining locally finite posets isn't hard, so I would do it myself, but how should it work with the typeclass inference? Should it be a structure extending partial_order or a class taking [partial_order] as an argument? (My guts say the latter)

[Yaël Dillies]

I'm now proving that ℕ is locally finite. This will provide a list.Ico : ℕ → ℕ → list ℕ that will do the same thing as list.range'. Should we keep list.range' then?

[Yakov Pechersky]

list.range' is there to prove things about list.range and list.iota. Will your list.Ico have the same performance as list.range'? As list.range with transpose?

[Yaël Dillies]

It's not clear to me yet. I'm trying to make it have nice computability by using data fields.

[Kyle Miller]

Maybe related is how docs#simple_graph.degree works. A graph is locally finite if every neighbor set is finite, and the finiteness data is handled via typeclasses.

[Yaël Dillies]

So we talked about using (finset.Ixx a b).val in place of multiset.Ixx a b. Should I simply delete all the multiset.Ico stuff?

[Yakov Pechersky]

I think that's reasonable, because the current definition is just over nat, and just the lift into the quotient.

[Yaël Dillies]

@Anne Baanen, in your (dead?) PR about has_enum, you're defining locally finite orders from enumerating lists and then you lift that up to enumerating multisets and enumerating finsets.
The problem with that is that this assumes the order is linear while many nonlinear orders are locally finite (although I have yet to encounter one in practice).

What do you think of using your approach for lists and mine for multisets and finsets? Then you'll need some glue between lists and multisets, but that's hopefully not too bad.

[Anne Baanen]

Yes, has_enum is very much abandoned, so please go with whatever sounds good to you. From your description, splitting into a non-linear and linear part would work well.

[Yaël Dillies]

I'll ask about who to credit when the PR is ready, because that's a lot of people!

[Alex J. Best]

I was in a talk this week that used the moebius function on the intersection posets of hyperplane arrangements, so I have seen them in practice! It reminded me of my long abandoned https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Perfect.20Numbers/near/201463174 looking at incidence algebras, its cool that you are actually adding some of this @Yaël Dillies !

[Yaël Dillies]

Ouuuh, nice! I feel like I'm taking on something everybody has wanted for years :sweat_smile:

[Yaël Dillies]

Well, there are many things we've wanted for years. But this one seems rather basic.

[Kevin Buzzard]

Please do contour integrals next ;-)

[Yaël Dillies]

Anne Baanen said:

Yes, has_enum is very much abandoned, so please go with whatever sounds good to you.

Actually, what's still there to do in branch#fin_range? It looks pretty pretty good to me!