Skip to content

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

Closed
IvanRenison wants to merge 4 commits intoleanprover-community:masterfrom
IvanRenison:HasAdj
Closed

feat(Combinatorics): define HasAdj for capturing the common structure of different kinds of (simple) graphs#35776
IvanRenison wants to merge 4 commits intoleanprover-community:masterfrom
IvanRenison:HasAdj

Conversation

@IvanRenison
Copy link
Copy Markdown
Collaborator

@IvanRenison IvanRenison commented Feb 25, 2026 •
edited
Loading

We add a vertex set considering that we want to refactor SimpleGraph to also use one

This pr replaces #4127
Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/HasAdj/with/575843445

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 25, 2026 •
edited
Loading

PR summary 9b809f3970

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Combinatorics.HasAdj.Basic (new file) 214
Mathlib.Combinatorics.Digraph.HasAdj (new file) 502
Mathlib.Combinatorics.SimpleGraph.HasAdj (new file) 524

Declarations diff

+ Adj.left_mem_verts
+ Adj.right_mem_verts
+ HasAdj
+ instance : HasAdj α (Digraph α)
+ instance : HasAdj α (SimpleGraph α)

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

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

@github-actions github-actions bot added the t-combinatorics Combinatorics label Feb 25, 2026
@IvanRenison IvanRenison mentioned this pull request Feb 25, 2026
Closed
3 tasks
@IvanRenison IvanRenison added the WIP Work in progress label Feb 25, 2026
This was referenced Feb 25, 2026
Closed
Closed
@IvanRenison IvanRenison marked this pull request as ready for review February 27, 2026 22:09
@IvanRenison IvanRenison removed the WIP Work in progress label Feb 27, 2026
YaelDillies
YaelDillies reviewed Mar 16, 2026
View reviewed changes
Comment thread Mathlib/Combinatorics/HasAdj/Basic.lean
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Mar 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe Combinatorics.Graph.Adj, even though it's not restricted to Graph? Combinatorics as a folder is definitely too generic for this!

Comment thread Mathlib/Combinatorics/Digraph/HasAdj.lean
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Mar 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you merge this with Digraph.Basic? Same for SimpleGraph

Comment thread Mathlib/Combinatorics/HasAdj/Basic.lean
@[expose] public section

/-- Typeclass for (simple) graphs. -/
class HasAdj (α : outParam Type*) (Gr : Type*) where
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Mar 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
class HasAdj (α : outParam Type*) (Gr : Type*) where
class HasAdj (V : outParam Type*) (E : Type*) where

no?

Comment thread Mathlib/Combinatorics/HasAdj/Basic.lean
Comment on lines +35 to +37
/-- There is no edge of the graph outside of it vertices. -/
left_mem_verts_of_adj {G : Gr} {v w : α} (h : Adj G v w) : v ∈ verts G
/-- There is no edge of the graph outside of it vertices. -/
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies Mar 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
/-- There is no edge of the graph outside of it vertices. -/
left_mem_verts_of_adj {G : Gr} {v w : α} (h : Adj G v w) : v ∈ verts G
/-- There is no edge of the graph outside of it vertices. -/
/-- There is no edge of the graph outside of its vertices. -/
left_mem_verts_of_adj {G : Gr} {v w : α} (h : Adj G v w) : v ∈ verts G
/-- There is no edge of the graph outside of its vertices. -/

@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Mar 16, 2026

Do you have more code depending on this somewhere, so that we can tell whether this is a viable approach? eg have you tried refactoring the SimpleGraph API to use this?

@Jun2M Jun2M mentioned this pull request Mar 16, 2026
Open
@IvanRenison
Copy link
Copy Markdown
Collaborator Author

IvanRenison commented Mar 18, 2026

I made #35783 and #35831, however, after discussion in Zulip, I think we are replacing this pr by #36743

@IvanRenison
Copy link
Copy Markdown
Collaborator Author

IvanRenison commented Mar 18, 2026

#36743 is replacing this pr

@YaelDillies YaelDillies removed their assignment Mar 19, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

Assignees

No one assigned

Labels

t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@IvanRenison @YaelDillies