Renaming SimpleGraph.{edgeSet,vertexSet}

Stream: mathlib4

[Peter Nelson]

To reduce noise, I'll bring up the second issue in this thread as well. (I'm happy to have it moved to a new thread if a moderator thinks that would be better).

For G : SimpleGraph V, the vertex set is the type V, and the edge set is a Set, referred to as G.edgeSet.

For multigraph G : Graph a b, both the vertex set and edge sets are Sets. I have called them G.V and G.E, and was thinking a good convention would be to call them edgeSet and vertexSet in lemma names.

I think the compact notation is important, mostly because the design of multigraphs will require the vertex and edge sets to be explicitly referred to a lot in hypotheses; the comparison is something like
(hx : x ∈ G.V) (hy : y ∈ G.V) (he : e ∈ G.E) vs (hx : x ∈ G.vertexSet) (hy : y ∈ G.vertexSet) (he : e ∈ G.edgeSet) in countless places.

If H is a subgraph of G, then I believe H.V ⊆ G.V looks much cleaner than H.vertexSet ⊆ G.vertexSet and I don't think any clarity is lost. I have used the same convention for mathlib's matroids (where M.E is the ground set of a matroid M, and this is called ground in lemma names) and I think it's working well.

But Eric brought up that this would cause an inconsistency between Graph and SimpleGraph, where Graph.E corresponds to SimpleGraph.edgeSet. Fixing this would involve either changing what exists for SimpleGraph, or using the long names for multigraphs.

I have a much stronger point of view on this issue than the last one - I believe the longer names will cause the multigraph API to be considerably uglier. But consistency is also good, so here's a poll anyway!

[Peter Nelson]

/poll How should the edge/vertex sets of SimpleGraph and Graph be denoted?
SimpleGraph.E and Graph.V/Graph.E, with vertexSet and edgeSet in lemma names
[Simple]Graph.vertexSet and [Simple]Graph.edgeSet,
Graph.V and [Simple]Graph.edgeSet, with vertexSet for Graph.V in lemma names

[Peter Nelson]

(To be clear, the first option would involve a commitment to eventually rename SimpleGraph.edgeSet to SimpleGraph.E, without changing existing lemma names.)

[Bhavik Mehta]

My opinion is that we should also move towards refactoring SimpleGraph to either mimic Graph or be defined in terms of it, ie eventually go even further than just renaming to match

[Notification Bot]

4 messages were moved here from #mathlib4 > Multigraph notation - naming poll by Eric Wieser.

[Eric Wieser]

Peter Nelson said:

I'm happy to have it moved to a new thread if a moderator thinks that would be better).

(I did this, I think we want visibility in the title of the rename being proposed, to make it easier to spot)

[Eric Wieser]

The proposal to use vertexSet in theorems names but V in the definition seems quite strange to me; this goes against our default symbol-reading rule (though the new preferred spelling machinery does at least give us a way to document it). I would have expected V in both places or neither, like Polynomial.X (which I guess could have been Polynomial.var instead)

[Bhavik Mehta]

I agree it goes against the default; my vote above is assuming that it's documented using recommended_spelling, in the module doc, and on the definition itself, together with the justification (as in the original post here) for the decision. Provided it is, I think the justification above makes sense

[Pim Otte]

I might be missing some context from somewhere else, but what is the case against using V/E in names too?

I'm not strongly opposed to introducing a split, but in mirroring Matroid, we might also consider verts/vertices/edges as names.

[Peter Nelson]

Single capital letters look strange with the capitalization convention in lemma names, I find. It also feels right for lemma names to correspond somewhat to how things are said, rather than written.

verts/edges isn’t bad, though. One disadvantage maybe is that these objects will also be packaged in Finset and List forms in other places, so Set disambiguates these.

[Eric Wieser]

Peter Nelson said:

Single capital letters look strange with the capitalization convention in lemma names, I find

But we do use them extensively in Polynomial

[Andrew Yang]

My two cents as a passerby:
I think it is very strange if the name of the definition doesn't match the name in lemmas. Maybe one could consider naming the field vertexSet but introduce a scoped notation V(G) for that?

[Peter Nelson]

That hadn’t occurred to me, but that is exactly how it is written, and would be perfect. If there are no technical problems with that, it would be a great compromise-free solution.

[Peter Nelson]

I've now played around with V(G)/E(G) notation, and it has caused no problems, even when the same notation is used for multiple related objects, eg V(P) for the vertex set of a path in a graph G, with statements like V(P) = V(G). See this proof in my repo for an example of the notation in action.

[Peter Nelson]

I think this is really the ideal solution - it will mean that no actual definitions or lemma names in SimpleGraph need to be deprecated or refactored; we just define new notation E(G) for SimpleGraph.edgeSet G and change lemma statements to use it.
The E(_) and V(_) notation could also become standard for paths, walks, cycles, subgraphs, etc in both simple and non-simple graphs.

We could also introduce a similar notation like E₀(G) for G.edgeFinset.

[Peter Nelson]

I've added a new poll option, and changed my vote in that direction.

[Eric Wieser]

Are you suggesting vxSet as the name, or did the poll force you to truncate?

[Peter Nelson]

Yes, I am. vertexSet is a bit long. SimpleGraph.subgraph uses verts, but I think it is less obvious from the name what type that should have.

[Peter Nelson]

vx is the normal 'teaching on the board' abbreviation for 'vertex'.

[Sébastien Gouëzel]

If you have a notation available, isn't it reasonable for the full name to be as understandable as possible, i.e., vertexSet? (I have never encountered vx)

[Peter Nelson]

It was a late addition to the poll, but reactions seems to suggest we are on board with the V(G)/E(G) notation, with vertexSet/edgeSet in definitions. Is this correct?

[Eric Wieser]

Should we pick a notation for the finset ones at the same time?

[Peter Nelson]

E₀(G) and V₀(G) are what come to mind - are there any other suggestions? (Note that this really only applies to SimpleGraph.edgeFinset at the moment - there is nothing planned immediately for finsets and Graph)

[Eric Wieser]

I don't know if there's any precedent in mathlib for using _0 in that way

[Andrew Yang]

I'm guessing the idea comes from →₀, but that notation is probably because Finsupp is a function that is mostly zero, not that ₀ has anything inherent to do with finiteness.

[Peter Nelson]

Maybe a subscript f, similar to finsum?

[Eric Wieser]

I thought finsum was superscript?

[Peter Nelson]

It is. Either would work