Diameter of a simple graph

Stream: mathlib4

[Rida Hamadani]

In #12058, I've defined the diameter of a simple graph using sSup, and I defined its type to be ℕ∞, mainly for two reasons:

1. Infinite graphs.
2. Distance between vertices currently is of type ℕ, giving 0 for unreachable vertices. But in all graph theory references that I'm aware of, it is defined as ∞ instead. In that case, a disconnected graph will have an infinite diameter too. With diam : ℕ∞, it is easy to replace dist with edist in the future. (Check this).

As this is my first time trying to define something (I've only stated and proved lemmas so far), I'm not sure if this is a good way to define the diameter, and would love to hear any feedback. I'm worried about this definition being wrong, and then having to reprove all the lemmas about it.

Moreover, I'm not sure if the lemmas I included in the API are appropriate, I would like to hear feedback regarding this too. (Also, any help with the sorry's is greatly appreciated!)

Note: I didn't post this in the PR reviews stream because this is a draft PR, and I'm requesting advice on a WIP instead of a review, but please let me know if that stream is more appropriate for this sort of post.

[Kevin Buzzard]

I think that the usual reason for the "if it's infinity then let's call it 0" approach is simply that people get annoyed with working with extended naturals because a bunch of standard nat tactics like omega won't work with extended nats. If working with extended nats doesn't make you want to pull your hair out then go for it! It might even be helpful if you isolate pain points and suggest tactics which will make working with $\infty$ easier.

Note that there is one situation -- order of elements and order of groups -- where making the answer 0 turns out to be an inspired idea. Elements and groups literally can't have order 0 so you know it unambiguously means infinity, and basic theorems like order of product group equals product of orders works really well with the 0 convention! This is to do with the fact that if a surjection from the integers to a cyclic group is injective then its kernel is (0) but the size of the image is infinity.

[Rida Hamadani]

Thanks for the clarification! I've noticed that the combination of a supremum and ℕ∞ is an especially annoying one, maybe if I was working with a definition involving an infremum instead, it would have been less time consuming. I'm considering renaming the current definition to ediam and defining a new diam which is in ℕ.

[Rida Hamadani]

But it feels like when we treat infinity as zero in the case of distances and diameters, some information is lost, and this is worrying to me.
For example, given two vertices with distance zero, are they unreachable, or are they equal? We may never know.

[Ruben Van de Velde]

Yeah, then you need to distinguish those in a different way

[Ruben Van de Velde]

I wonder if something like omega could work for ENat

[Kevin Buzzard]

I was also nervous about this whole "if it's supposed to be infinity then return the wrong answer" attitude for a while, but it does work. As Ruben says, you just have to interpret a return of zero as not meaning "the answer is 0" but as meaning the answer is either 0 or infinity" and so your lemmas in the zero case just have the stronger hypothesis that the vertices are the same. Once you write a bunch of API you'll see that this is not hard to deal with, the issue is a psychological one more than anything else. You can look at the API for Nat.card which has exactly the same issue (size of the empty type is 0, size of an infinite type is 0) to see that it can be made to work, and I can testify that Nat.card is sometimes exactly what you want for a cardinality function. It's swings and roundabouts here. Humans are very good at saying "well obviously adding infinity doesn't change anything" but actually adding infinity does change something a little bit, and lean rightfully demands that you keep track.

For both cardinalities and polynomial degrees we do have two functions, one which returns infinity (actually negative infinity in the deg(0) case) if the answer is "error" and one which returns zero, and both are used extensively in the library.

[Kevin Buzzard]

In particular your claim that some information is lost is false. If d(x,y)=0 then you can still ask if x=y because you didn't lose x and y. You make the API around that observation.

[Rida Hamadani]

I see, I will reattempt the definition but in the naturals. Thank you!

[Alex J. Best]

Ruben Van de Velde said:

I wonder if something like omega could work for ENat

It can, the whole first order theory is decidable just like for naturals. The proof is essentially that each element is either infinity or a natural so any formula can be split into cases and the infinite case always simplifies to something trivial. This is basically how such a tactic could be implemented too using omega (similar to https://github.com/KisaraBlue/ec-tate-lean/blob/master/ECTate/Tactic/ELinarith.lean which was an earlier version of this from before omega existed).

[Kim Morrison]

Could one write a enat_omega tactic which is a wrapper around omega (as we already have bv_omega for BitVec)?

[Kim Morrison]

You'd probably just case split all the enats at once. Probably there's a more efficient algorithm that would require integration with omega (so not happening, since it is slated for replacement) that would split one at a time, but avoiding the overhead of rebuilding the omega state each time.