SimpleGraph.dist of disconnected vertices is zero

Stream: mathlib4

[Rida Hamadani]

I've noticed that docs#SimpleGraph.dist defaults to zero if there is no walk between the vertices pair. All the references that I've seen so far define the distance of disconnected vertices to be infinity (for example, Diestel p8, AOCP vol. 4A p7, etc).

Moreover, other parts of the SimpleGraph library seem to be following the convention of defaulting to infinity, such as docs#SimpleGraph.girth.

Is there any specific reason for that?

[Yaël Dillies]

The general reason is that ℕ is nicer to work with than ℕ∞ but that's not a very strong reason

[Rida Hamadani]

Do you think its a good idea to make it default to infinity?

[Yaël Dillies]

I don't know! It doesn't sound unreasonable. You can try :smile:

[Yaël Dillies]

However let me warn you that it's easy to fall into library housekeeping. I strongly encourage you to find a big end goal to motivate your housekeeping changes

[Rida Hamadani]

Actually I wanted to define eccentricity, radius, and diameter of a simple graph, which is why I was looking at the distance.

[Yaël Dillies]

Quite likely, it doesn't actually matter for most applications whether SimpleGraph.dist (or eccentricity, radius, and diameter) is ℕ- or ℕ∞-valued, so the easiest might be to follow whatever is in mathlib already

[Rida Hamadani]

Speaking of which, do you think it is a good idea to include these definitions in the Metric.lean file (which contains SimpleGraph.dist), or make a separate file for each one?

I was thinking that maybe at first we would include them in Metric.lean, and then move them later on to separate files once they start getting their own results.

[Yaël Dillies]

Rida Hamadani said:

I was thinking that maybe at first we would include them in Metric.lean, and then move them later on to separate files once they start getting their own results.

That's exactly what I would do

[Rida Hamadani]

Great, thank you!

[Ruben Van de Velde]

You might check first if there's already an edist that may be infinity

[Rida Hamadani]

It seems that there is no such edist for SimpleGraph, but I understand from your message that if at any point we face issues because dist doesn't default to infinity, we can define an edist and use that instead, right?

[Ruben Van de Velde]

Yeah, this is a pattern that exists in a few places in mathlib