feat(Combinatorics/GraphLike): introduce GraphLike typeclass

[Jun2M]

Per discussion at (#graph theory > HasAdj), This PR introduces the GraphLike typeclass to capture the notions like dart and walk across various graph objects, such as SimpleGraph, Graph, and Digraph.

The goal is that by abstracting these core components into a typeclass, we can prove these results once for all graph-like structures rather than duplicating them across different graph types.

Main definitions

• GraphLike V D E Gr: A typeclass parameterized by a vertex type V, dart type D and a graph type Gr (with V, D & E as an outParam).
  • GraphLike.verts : Set V: The set of vertices of the graph.
  • GraphLike.darts : Set D: The set of darts of the graph.
  • GraphLike.edges : Set E: The set of edges of the graph.
  • GraphLike.Adj : V → V → Prop: The adjacency relation, defined by default as ∃ d ∈ darts, fst d = u ∧ snd d = v.

---

This PR generalises #35776 to also unify Graph.

PRs depending on this PR are
#39047 (graphLike with no multi edges) => #39050 (Digraph is graphLike)
||
V
#36829 (undirected graphLike) => #39053 (Graph is graphLike) & #39054 (Simplegraph is graphLike)
||
V
#36756 (def of walk on GraphLike) => #36971 (change Simplegraph to use GraphLike walk)

[github-actions]

PR summary 18c5d4a69c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.GraphLike.Basic (new file)	489

---

Declarations diff

+ Adj.left_mem
+ Adj.right_mem
+ DartAdj
+ GraphLike
+ adj_source_target
+ darts_ext
+ toProd

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[lauramonk]

Thank you! This seems great to me, maybe a few names to pick carefully. Notably I agree with the idea of calling the notion GraphLike. I am not certain about prodDart and in particular I do not fully understand the point of having the two different objects (but this is my own ignorance).

[lauramonk]

Looks great, have added a few comments.

[YaelDillies]

Is this a concept in the informal literature? Why do we need it?

[Jun2M]

Mathematically speaking, they are exactly darts, therefore not a separate concept in informal literature. The only difference with darts is that it has its endpoints (src & tgt) in its type.
I made this as a replacement for what Adj does in the def of walk in SimpleGraph. Walk in SimpleGraph is constructed from a vertex by iteratively adding Adj : V → V → Prop. Mathematically, they should be replaced with darts, d : D, but they do not have their endpoints in the type. To minimize the changes needed, I created Step : V → V → Type* as a endpoint-typed version of darts to replace the role of Adj in walks.
So Step is the way I achieved "endpoint-type version of darts". If you are not happy with the way it is done, it can easily be changed.
If you think we should not have "endpoint-type version of darts", that would mean I have to rewrite #36756, the definition of walk, and #36971, migrating Simplegraph to use GraphLike walk. Migration PR is already changing ~1000 lines and I have no idea how much worse it will get if I don't have something like Step. Nevertheless, I could try if you want.

[YaelDillies]

Why do we have one global type of darts, instead of one type of darts per pair of vertices?

[Jun2M]

I think SimpleGraph.Dart poses a problem with getting rid of "darts as global type" and sticking with "darts as vertex-indexed type".

As GraphLike has darts, or mathematically equivalent one as vertex-indexed version, in the definition, I would argue, SimpleGraph.Dart would obviously be generalised and handled in GraphLike level.

Also, in the combinatorial map that dart comes from, dart is the primitive type and vertices are derived from the orbit of a function on darts, φᵥ, whereas dart being a type indexed by vertices implies you already have vertices before having darts. Given the history, if a mathematician is looking for a Lean implementation of "darts", I don't think they would expect it to be vertex-indexed. Lastly, I think it is more ergonomic to talk about the single set of darts in a global type rather than indexed set of darts for each pair of vertices.

So, the decision to not have "darts as global type" would imply that either deprecating or migrating SimpleGraph.Dart and all theorems about it to be vertex indexed, along with some other issues.

[Jun2M]

@YaelDillies, Step is only needed to be used in Walk so if you are happy to define dart to be globally typed, I can move Step and its lemmas to the PR that introduces Walk on GraphLike. If we do that, it would give me time to try and find out what removing Step would mean to the migration PR of SimpleGraph to use GraphLike.Walk.

[YaelDillies]

Yes, delaying sounds like a great idea here!

[YaelDillies]

Can you explain why adding a class is a better solution than, say, rebuilding SimpleGraph, Digraph and Graph on top of Quiver?

[Jun2M]

It is kinda hard to contrast without a concrete suggestion but here are some of the worries.
To my understanding, one of the things we would like to do is to introduce ground sets (vertex set, edge set ..) as part of the definition of graphs. If the suggestion is to redefine the graphs as class ... extend Quiver ... then the fact that it is instance class is a problem: ground sets allow modelling most graph operations/relations within one type, but if we have multiple graphs that are instances with same type, I think Lean will have difficult time understanding what is going on. Also, Quiver has a relation on the entire type, so Lean would say two graphs are not equal if they disagree outside the ground set even if they are the same within the ground set and therefore mathematically represents the same graph.
Lastly, migrating just Walk to a new definition is currently requiring about 1000 lines of change. Changing the definition of SimpleGraph would probably require changing the entire SimpleGraph in one go. Hardly an enviable task, I would say. The current approach allows the migration to happen one part at a time at a much more managable size compared to rewriting everything.

[YaelDillies]

I understand but similarly this PR is a major shift in the way we formalise graphs in mathlib, and it will be painful if we decide to refactor away from it later on. We will not merge this PR until we have tried a reasonable range of implementations, and basing everything off a single type is a promising one that I haven't seen implemented yet.

How many lines it takes to refactor mathlib is mostly irrelevant. We are looking for a long term solution here. Also 1k lines is really not that big. I got a 5k lines refactor merged over the course of two weeks three years ago, and many more that were around 2-3k.

Good point about Quiver. Probably I mean DirectedGraph, which doesn't exist yet.

[Jun2M]

I understand the need for a lot of care with a PR like this. I would not want huge changes to Mathlib to feel rushed in without due considerations. If it is okay, I have some questions to clarify some things and make the most of this as a learning experience.

1. Until "a reasonable range of implemenatations" are tried
   Now that this PR is not being merged (if at all) until "a reasonable range of implemenatations" are tried, I am wondering what I should do with Walk on Graph. So far, I had, perhaps unreasonable, assumption that this PR should not take that long to merge and once it is merged, there would be a defintion of Walk on Graph along with wealth of lemmas/theorems generalized from SimpleGraph. If this is assumption is not true, can I pursue making PRs for Graph only definitions of Walk? I have a number of theorems I would love to make PRs for which depends on having a definition of Walk (or Connected from feat(Combinatorics/Graph): connected graphs #37861).

2. Refactor and number of lines
   Because I read "try to make many PRs containing small, self-contained pieces; in general, the smaller the better!" (with no concrete number), so far, I have made an arbitrary decision to make sure to keep my PRs to be about 100 lines change. Similar applied to here where I made 7 difference PRs, doing my best to keep them small-ish. I am wondering,

• Is 1k not that big for a PR in general?
• Is 1k not that big for a refactor PR? I would it have been fine to have just one PR for GraphLike instead of 7?

3. "basing everything off a single type"
   Just out of curiosity, I would be interested to know what you mean by "basing everything off a single type". Is this similar to hypermap with a single type of darts? Is this having a single type of vertices and type of edges to be derived from it? the other way? Is there a place/repo that someone is working on which I can have a look? I would be happy to discuss other potential implementations!

4. DirectedGraph
   In the design of GraphLike, I have done my best to also accommodate (directed/undirected) hypergraphs. Perhaps I am wrong but, rebuilding the defs on top of DirectedGraph sounds like it is not going to accommodate hypergraphs. Is this true?

Thank you for your time and consideration.