feat: graph definitions (#Attempts 3)

[sorrachai]

This PR introduces basic graph definitions: Graph, Digraph, SimpleGraph, and SimpleDiGraph.

We use the following definition of a multigraph.
A multigraph is a triple (V,E,f) where V is a vertex set, E is an edge set,
and f is a function from an edge to an (ordered/unordered) pair of vertices.
Preferably, f is a computable function. We reuse the definitions from Mathlib whenever possible.

• MultiGraph α β: abbrev for Mathlib Graph α β, adding a typeclass to keep track of endpoints explicitly.
• MultiDigraph α β: a directed multigraph; the directed counterpart of Mathlib's Graph α β with explicit endpoints.
• SimpleGraph α: a simple graph with a vertex set, extending Mathlib's SimpleGraph α.
• SimpleDigraph α: a loopless directed graph with adjacency Adj : α → α → Prop and a
  vertex set, extending Mathlib's Digraph α.

Comparison to PR #503 (#503): This version reuses Mathlib as much as possible. All vertex sets are Set-valued, following the design of Mathlib.Combinatorics.Graph.

Zulip discussion: Follow at
https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/A.20Set-based.20Multigraph.20Definition/with/616948793.

[ctchou]

I would suggest replacing α and β by V and E. When reading the code below, I have to constantly remind myself that α and β are the carrier types for vertices and edges. Using V and E will make this transparent.

[chenson2018]

I don't understand having this abbrev if they are both called Graph, and are defined exactly the same way.

[sorrachai]

Just to rename things for consistency. Now, it is renamed as MultiGraph.

[ctchou]

There is already a notion of partial functons in mathlib:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/PFun.html
which has a lot of API's.

[sorrachai]

I tried a bit, but I found that it allows even non-computable Prop. It would be overkill to use it, especially since we want to keep everything computable.

[ctchou]

That a non-computable Prop is allowed doesn't mean you have to use a non-computable Prop. It just means that Lean will not insists that the Prop is computable. Note that you can build a Set from a non-computable Prop as well. Do you want to replace Set by Finset everywhere in your code?

The main reason for my suggesting PFun is that it already has a lot of API support, including ones that work via Option.

[sorrachai]

Sure, let's do it.

[ctchou]

Same comment about partial functions as above.

[ctchou]

You don't need := by grind. There is nothing to prove here.

[chenson2018]

I think there's some confusion here: when declaring a structure/typeclass this is how you specify a default tactic to run.

[ctchou]

OK. I didn't know that. The syntax is not helpful here.

[sorrachai]

(Just to add the default tactic to prove the goal)

[ctchou]

You don't need := by grind. There is nothing to prove here.

[sorrachai]

(Just to add the default tactic to prove the goal)

[ctchou]

Since you are making this definition from scratch, why not state it using endpoints, rather than adapting mathlib's Graph? You should also consider if mathlib's Quiver is applicable here.

Also, since mathlib already has a Digraph and this definition is not an extension of it, I would suggest calling it something else. Perhaps DirectedMultigraph?

[sorrachai]

Good point. Rename it to MultiDigraph and from Graph to MultiGraph.

[sorrachai]

(Quiver is not quite what we want; they generalize V -> V -> Prop to V -> V -> Type, which means no global edge labeling.)

[SnirBroshi]

Can you replace all mentions of "arc" with "edge"?

[ctchou]

α, β -> V, E

[ctchou]

I don't think you need both IsLink and endpoints to be in the structure MultiDigraph, because endpoints_spec can serve as the definition of IsLink in terms of endpoints. The contents of isLink_imp_{left,right}_mem_vertexSet can be expressed in terms of endpoints directly: namely, the PFun.image of endpoints projected to a Set V is a subset of vertexSet. Then isLink_imp_{left,right}_mem_vertexSet can be derived as theorems. Going the other way (namely, defining endpoints in terms of IsLink) is also possible, but then you'll need an analogue of mathlib's Graph. eq_or_eq_of_isLink_of_isLink to prevent the same edge label to be applied to multiple edges. In either case, that analogue should probably be stated and proved/assumed.

Also, stylistically, I would prefer edgeSet and edge_mem_iff_exists_IsLink to become a separate definition and theorem outside the structure.

[sorrachai]

Thanks for the comment. Indeed, these two fields are redundant. The question is which one should be in the field (and which should be derived). I would prefer endpoints because they explicitly provide a vertex pair. The reason for the IsLink relation was to avoid quotient types (Sym2)#CSLib > New graph definitions @ 💬 in the case of an undirected multigraph. This is no longer the case for directed graphs.

[ctchou]

I think the following two Props should suffice to imply isLink_imp_{left,right}_mem_vertexSet:

left_endpoint_mem_vertexSet : endpoints.ran.MapsTo Prod.fst vertexSet
right_endpoint_mem_vertexSet : endpoints.ran.MapsTo Prod.snd vertexSet

[sorrachai]

Indeed. Added isLink_imp_left_mem_vertexSet and isLink_imp_right_mem_vertexSet.

[ctchou]

I wonder if it is possible to define MultiGraph.endpoints directly. Unfortunately, all definitions I can think of uses Classical.choose somewhere and hence must be marked as noncomputable. But if we accept that, then we can get rid of the assumption [G.HasEndpoints], which currently needs to be assumed whenever MultiGraph.endpoints is used. Perhaps that can be considered an improvement and a small price to pay for using mathlib's Graph.

[sorrachai]

Alternatively, one could extend Mathlib's Graph with field endpoints and endpoints_spec, but this seems redundant, since it subsumes IsLink. I am happy with the current price to pay if we cannot define MultiGraph ourselves.

[sorrachai]

I did everything I could. Let me know if you need anything else.

[ctchou]

I agree with @sorrachai's assessment.

[Shreyas4991]

I am sorry but I maintain as pointed out by others on Zulip that this PR still fractures and duplicates the Graph API. For instance, the correct step for "SimpleDigraph" is to adopt leanprover-community/mathlib4#33466 and get it merged.

Especially (but not limited to) the situation where one accepts the review in the immediately preceding set of review comments that using noncommputable is fine. I personally do not find the existing mathlib API lacking for basic graph algorithms, apart from vertex sets in SimpleGraph, which is being addressed in Mathlib through the ongoing refactors.

I propose first making PRs to add graph algorithms (such as my #804 and/or #805 ) and then, through those PRs, surfacing any deficiencies in mathlib's graph API. When they are found, they can be backfilled through mathlib PRs. Such an incremental process will also help mathlib graph developers and avoid fracturing and duplicating API for graph theory.

[sorrachai]

@chenson2018 Any thoughts?