feat(Combinatorics/GraphLike): introduce `GraphLike` typeclass by Jun2M · Pull Request #36743 · leanprover-community/mathlib4

Jun2M · 2026-03-16T18:12:58Z

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.

This PR generalises #35776 to also unify Graph.

Main definitions

GraphLike α β Gr: A typeclass parameterized by a vertex type α, dart type β and a graph type Gr (with α as an outParam).
- GraphLike.verts : Set α: The set of vertices of the graph.
- GraphLike.darts : Set β: The set of darts of the graph.
- GraphLike.Adj : α → α → Prop: The adjacency relation, defined by default as Nonempty (darts G u v).

github-actions · 2026-03-16T18:14:18Z

PR summary e960b84129

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)	525
`Mathlib.Combinatorics.Digraph.GraphLike` (new file)	527
`Mathlib.Combinatorics.SimpleGraph.GraphLike` (new file)	545

Declarations diff

+ Adj.left_mem
+ Adj.right_mem
+ Adj.toStep
+ DartAdj
+ DartLike
+ DartLike.toProd
+ GraphLike
+ adj_of_mem_darts
+ dartStep
+ dartStep_val
+ darts_ext
+ fst_eq
+ instance : DartLike α (α × α)
+ instance : GraphLike α (α × α) (Digraph α)
+ instance : GraphLike α (α × α) (SimpleGraph α)
+ instance : Subsingleton (step G u v)
+ instance [DecidableEq β] : DecidableEq (step G u v) := Subtype.instDecidableEq
+ instance [DecidableRel (Adj G)] : DecidablePred (· ∈ darts G)
+ mem_darts_iff_adj
+ snd_eq
+ step
+ step.adj
+ step.ext
+ step.ext_HEq
+ step.fst
+ step.left_eq_of_val_eq
+ step.left_mem
+ step.right_eq_of_val_eq
+ step.right_mem
+ step.snd
+ step.todart
+ step.todart_fst
+ step.todart_snd
+ step.todart_val
+ toProd_eq
+ val_step_eq
++ darts_def

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

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).

Mathlib/Combinatorics/HasDart/Basic.lean

Mathlib/Combinatorics/GraphLike/Basic.lean

Jun2M · 2026-03-20T03:00:58Z

@IvanRenison, I have moved the instance of α × α being a SymmDartLike to #36829, PR for SymmDartLike and SymmGraphLike. For SimpleGraph, for example, I didn't want to introduce instance of GraphLike in this PR knowing that it will be immediately changed to SymmGraphLike in the following PR.

IvanRenison · 2026-03-20T12:21:34Z

Okay
And what about the instance for Graph? In that PR I see the instance for Digraph but not the instance for Graph

IvanRenison · 2026-03-20T12:33:06Z

Digraph is anyway not symmetric, so I think it should be here

lauramonk · 2026-03-20T13:43:06Z

Okay And what about the instance for Graph? In that PR I see the instance for Digraph but not the instance for Graph

Hi Ivan, the problem with Graph is that Darts have not yet been added for them. I have a repo with a notion of Dart of Graph, with the inversion and basic results, here. I need to adapt it to Jun2M's set-up to prove the instance for Graph; it should be fairly straightforward but I have not yet managed to (as I am a beginner).

Jun2M · 2026-03-20T13:43:57Z

@IvanRenison, For Graph, I asked @lauramonk to make a PR for it after some coordination in the zulip thread. Do you think it is a mistake to split it like that? I could do it myself pretty quickly to be honest. (and given that I changed the definition of GraphLike quite a bit, maybe that is the right thing to do)

For Digraph, proving GraphLike α (α × α) (Digraph α) requires DartLike α (α × α). However, the full generality is SymmDartLike α (α × α). If you want me to introduce temporary instances, I could do that. Otherwise, Digraph should be in that PR.

lauramonk · 2026-03-20T13:47:45Z

@Jun2M Please feel free to work on Dart for Graph, as you are a lot faster. I clearly cannot do it until next week. If our work on https://github.com/lauramonk/mathlib4/tree/GraphDart is of any use please also feel free to take it from there. I feel it would make sense to define Dart for Graph before GraphLike.

lauramonk · 2026-03-20T13:48:41Z

I can also PR Dart for Graph without the instance and let you write the instance.

IvanRenison · 2026-03-20T13:49:12Z

Ah, I didn't thought that there are still no Darts in Graph.

I think adding temporary instances here is a good idea. And later they could be moved, but also they can simply be extended

Jun2M · 2026-03-20T13:54:16Z

@IvanRenison, by adding temporary instances, do you mean Digraph or all 3 graphlikes?

IvanRenison · 2026-03-20T14:02:15Z

I would add Digraph and SimpleGraph, as you mention that we still not have darts for Graph

Jun2M · 2026-03-20T14:06:19Z

@lauramonk, I am realising I should have coordinated things much better. Perhaps there should be a separate Zulip thread to discuss the GraphLike implementation for Graph.

I did say I like your Dart definition and would be good to modify it to use for the GraphLike instance. Then, I experimented more and the definition of GraphLike has diverged quite a bit from when we discussed. (You may notice @IvanRenison's DarkLike class is revived among other things) For this new definition, we need a Graph-unaware dart type, where each graph can pick some set of darts as their darts. The Graph-aware dart type like yours is not quite the right thing.

I thought I would finish making PR for moving SimpleGraph stuff to be based on GraphLike and come back to Zulip. But perhaps that was a mistake. I will write something for Zulip that describes the changes made & pros and cons. I have an idea for what dart-type for Graph should be but I would be very happy to discuss it as I, admittedly, haven't explored that side so much yet.

mathlib-merge-conflicts · 2026-03-21T08:38:06Z

This pull request has conflicts, please merge master and resolve them.

IvanRenison

Some suggestions

Mathlib/Combinatorics/GraphLike/Basic.lean

IvanRenison · 2026-03-26T21:05:55Z

Mathlib/Combinatorics/GraphLike/Basic.lean

+  rfl
+
+/-- Convert a step to a dart. -/
+def step.todart (h : step G u v) : darts G := ⟨h.val, h.prop.1⟩


Maybe we want this to return β? I don't know, but it is is worth asking I think

This was initially defined as that but so many of the theorems in SimpleGraph expected the darts to be a type so it was changed. I think there is an argument to have whether there should be a function that returns β along with this function but, unless we want ⟨step.todart h, step.todart_mem h⟩ everywhere in SimpleGraph, I think we should have a function that returns darts G.

Mathlib/Combinatorics/GraphLike/Basic.lean

IvanRenison · 2026-03-28T15:01:28Z

Mathlib/Combinatorics/GraphLike/Basic.lean

+lemma adj_of_mem_darts (hd : d ∈ darts G) : Adj G (fst d) (snd d) :=
+  exists_darts_iff_adj.mp ⟨d, hd, rfl, rfl⟩


Could you make this an iff?

The other direction is not true as there can be d that does not belong in darts G yet shares fst and snd with a dart that is in darts G.

IvanRenison · 2026-04-04T13:48:03Z

Mathlib/Combinatorics/GraphLike/Basic.lean

+@[inherit_doc verts]
+scoped notation "V(" G ")" => verts G
+
+variable {α β Gr : Type*} {G : Gr} {u u' v v' w : α} {d : β}


Suggested change

variable {α β Gr : Type*} {G : Gr} {u u' v v' w : α} {d : β}

variable {V β Gr : Type*} {G : Gr} {u u' v v' w : V} {d : β}

From to the style guidelines:

Types with a mathematical content are expressed with the usual mathematical notation, often with an upper case letter (G for a group, R for a ring, K or 𝕜 for a field, E for a vector space, ...). This convention is not followed in older files, where greek letters are used for all types. Pull requests renaming type variables in these files are welcome.

In SimpleGraph the use is mixed, sometimes with α, β, etc. and some times with U, V, etc. but maybe for new things we should use U, V, etc.

init

eeeba14

github-actions bot added the t-combinatorics Combinatorics label Mar 16, 2026

Jun2M added 8 commits March 16, 2026 14:20

mkall

72a23c6

docs

ab6b965

inherit_doc

0e06a4a

prodDart

e759a8f

doc

391eca7

HasDart instances

4d2c7a7

minor cleanup

7a76b33

mk_all

0396da0

Jun2M mentioned this pull request Mar 16, 2026

feat(Combinatorics/GraphLike/Walks): add general walks for GraphLike structures #36756

Open

2 tasks

Jun2M added 2 commits March 16, 2026 19:55

Reflect doc

f6b609d

dart_iff_adj

757ed33

lauramonk reviewed Mar 17, 2026

View reviewed changes

Mathlib/Combinatorics/HasDart/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Combinatorics/HasDart/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Combinatorics/HasDart/Basic.lean Outdated Show resolved Hide resolved

Jun2M added 4 commits March 17, 2026 08:50

apply Laura's suggsetions

e2efa7c

Reverse of darts

5a1787d

update instances

45003bf

back to Dart

79cfe9b

lauramonk reviewed Mar 17, 2026

View reviewed changes

Mathlib/Combinatorics/HasDart/Basic.lean Outdated Show resolved Hide resolved

No fix points

b9957af

SnirBroshi reviewed Mar 17, 2026

View reviewed changes

Mathlib/Combinatorics/HasDart/Basic.lean Outdated Show resolved Hide resolved

Jun2M added 4 commits March 17, 2026 21:01

DartLike & step

8c9442b

doc change

8996b14

mk_all

5051f88

doc

f2115cb

SnirBroshi reviewed Mar 18, 2026

View reviewed changes

Mathlib/Combinatorics/GraphLike/Basic.lean Outdated Show resolved Hide resolved

IvanRenison mentioned this pull request Mar 18, 2026

feat(Combinatorics): define HasAdj for capturing the common structure of different kinds of (simple) graphs #35776

Closed

dartSym2 & dartSymm

cbfaa20

IvanRenison reviewed Mar 18, 2026

View reviewed changes

Mathlib/Combinatorics/GraphLike/Basic.lean Outdated Show resolved Hide resolved

Jun2M added 3 commits March 20, 2026 12:12

Instances

3064d67

lint

313de21

lowercase

98ba7c4

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 21, 2026

Merge branch 'master' into HasDartDef

a73392c

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 21, 2026

Jun2M added 2 commits March 21, 2026 18:30

rm Graph GraphLike for now

99f39d6

mk_all

c35faee

Jun2M mentioned this pull request Mar 22, 2026

feat(Combinatorics/GraphLike): Change SimpleGraph files to use GraphLike #36971

Open

3 tasks

Jun2M requested a review from IvanRenison March 26, 2026 16:33

IvanRenison suggested changes Mar 26, 2026

View reviewed changes

Jun2M added 2 commits March 27, 2026 12:41

accept review feedback

1586764

Merge branch 'master' into HasDartDef

6b57d36

IvanRenison reviewed Mar 27, 2026

View reviewed changes

Mathlib/Combinatorics/GraphLike/Basic.lean Show resolved Hide resolved

IvanRenison reviewed Mar 28, 2026

View reviewed changes

IvanRenison approved these changes Mar 28, 2026

View reviewed changes

Jun2M requested a review from SnirBroshi April 1, 2026 20:34

IvanRenison reviewed Apr 4, 2026

View reviewed changes

		lemma adj_of_mem_darts (hd : d ∈ darts G) : Adj G (fst d) (snd d) :=
		exists_darts_iff_adj.mp ⟨d, hd, rfl, rfl⟩

	variable {α β Gr : Type*} {G : Gr} {u u' v v' w : α} {d : β}
	variable {V β Gr : Type*} {G : Gr} {u u' v v' w : V} {d : β}

Conversation

Jun2M commented Mar 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Main definitions

Uh oh!

github-actions bot commented Mar 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary e960b84129

Import changes for modified files

Declarations diff

Uh oh!

lauramonk left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Jun2M commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

IvanRenison commented Mar 20, 2026

Uh oh!

IvanRenison commented Mar 20, 2026

Uh oh!

lauramonk commented Mar 20, 2026

Uh oh!

Jun2M commented Mar 20, 2026

Uh oh!

lauramonk commented Mar 20, 2026

Uh oh!

lauramonk commented Mar 20, 2026

Uh oh!

IvanRenison commented Mar 20, 2026

Uh oh!

Jun2M commented Mar 20, 2026

Uh oh!

IvanRenison commented Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Jun2M commented Mar 20, 2026

Uh oh!

mathlib-merge-conflicts bot commented Mar 21, 2026

Uh oh!

IvanRenison left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

IvanRenison Mar 26, 2026

Choose a reason for hiding this comment

Uh oh!

Jun2M Mar 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

IvanRenison Mar 28, 2026

Choose a reason for hiding this comment

Uh oh!

Jun2M Mar 28, 2026

Choose a reason for hiding this comment

Uh oh!

IvanRenison Apr 4, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Jun2M commented Mar 16, 2026 •

edited

Loading

github-actions bot commented Mar 16, 2026 •

edited

Loading

Jun2M commented Mar 20, 2026 •

edited

Loading

IvanRenison commented Mar 20, 2026 •

edited

Loading

IvanRenison left a comment •

edited

Loading

Jun2M Mar 27, 2026 •

edited

Loading