refactor(Combinatorics): move Dart from SimpleGraph to HasAdj

Mathlib.lean

@@ -3285,6 +3285,7 @@ public import Mathlib.Combinatorics.Derangements.Basic
 public import Mathlib.Combinatorics.Derangements.Exponential
 public import Mathlib.Combinatorics.Derangements.Finite
 public import Mathlib.Combinatorics.Digraph.Basic
+public import Mathlib.Combinatorics.Digraph.HasAdj
 public import Mathlib.Combinatorics.Digraph.Orientation
 public import Mathlib.Combinatorics.Enumerative.Bell
 public import Mathlib.Combinatorics.Enumerative.Catalan
@@ -3304,6 +3305,8 @@ public import Mathlib.Combinatorics.Graph.Basic
 public import Mathlib.Combinatorics.HalesJewett
 public import Mathlib.Combinatorics.Hall.Basic
 public import Mathlib.Combinatorics.Hall.Finite
+public import Mathlib.Combinatorics.HasAdj.Basic
+public import Mathlib.Combinatorics.HasAdj.Dart
 public import Mathlib.Combinatorics.Hindman
 public import Mathlib.Combinatorics.KatonaCircle
 public import Mathlib.Combinatorics.Matroid.Basic
@@ -3386,6 +3389,7 @@ public import Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
 public import Mathlib.Combinatorics.SimpleGraph.Girth
 public import Mathlib.Combinatorics.SimpleGraph.Hall
 public import Mathlib.Combinatorics.SimpleGraph.Hamiltonian
+public import Mathlib.Combinatorics.SimpleGraph.HasAdj
 public import Mathlib.Combinatorics.SimpleGraph.Hasse
 public import Mathlib.Combinatorics.SimpleGraph.IncMatrix
 public import Mathlib.Combinatorics.SimpleGraph.Init

Mathlib/Combinatorics/Digraph/HasAdj.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Iván Renison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Iván Renison
+-/
+module
+
+public import Mathlib.Combinatorics.HasAdj.Basic
+public import Mathlib.Combinatorics.Digraph.Basic
+
+/-!
+In this file we make `Digraph` an instance of `HasAdj`.
+-/
+
+@[expose] public section
+
+variable {α : Type*}
+
+instance : HasAdj α (Digraph α) where
+  verts _ := Set.univ
+  Adj G := G.Adj
+  left_mem_verts_of_adj _ := Set.mem_univ _
+  right_mem_verts_of_adj _ := Set.mem_univ _

Mathlib/Combinatorics/HasAdj/Basic.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Iván Renison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Iván Renison
+-/
+module
+
+public import Batteries.Data.List.Basic
+public import Mathlib.Data.Rel
+
+/-!
+# Typeclass for different kinds of (simple) graphs
+
+This module defines the typeclass `HasAdj` for capturing the common structure of different kinds of
+(simple) graphs.
+
+## Main definitions
+
+* `HasAdj`: is the main typeclass in question. The field `verts` gives the set of vertices of a
+  graph, and the field `Adj` gives the adjacency relation between vertices.
+
+## TODO
+* Migrate from `SimpleGraph` all the results that only depend on the adjacency relation.
+
+-/
+
+@[expose] public section
+
+/-- Typeclass for (simple) graphs. -/
+class HasAdj (α : outParam Type*) (Gr : Type*) where
+  /-- The set of vertices of the graph. -/
+  verts (G : Gr) : Set α
+  /-- The adjacency relation of the graph. -/
+  Adj (G : Gr) : α → α → Prop
+  /-- 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. -/
+  right_mem_verts_of_adj {G : Gr} {v w : α} (h : Adj G v w) : w ∈ verts G
+
+namespace HasAdj
+
+variable {Gr : Type*} {α : Type*} [HasAdj α Gr]
+
+/-- Dot notation for `left_mem_verts_of_adj`. -/
+lemma Adj.left_mem_verts {G : Gr} {v w : α} (h : Adj G v w) : v ∈ verts G :=
+  left_mem_verts_of_adj h
+
+/-- Dot notation for `right_mem_verts_of_adj`. -/
+lemma Adj.right_mem_verts {G : Gr} {v w : α} (h : Adj G v w) : w ∈ verts G :=
+  right_mem_verts_of_adj h
+
+end HasAdj

Mathlib/Combinatorics/HasAdj/Dart.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 Iván Renison, Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Iván Renison, Kyle Miller
+-/
+module
+
+public import Mathlib.Combinatorics.HasAdj.Basic
+public import Mathlib.Data.Fintype.Sets
+public import Mathlib.Data.Fintype.Sigma
+
+/-!
+# Darts in graphs
+
+A `Dart` or half-edge or bond in a graph is an ordered pair of adjacent vertices, regarded as an
+oriented edge. This file defines darts and proves some of their basic properties.
+-/
+
+@[expose] public section
+
+namespace HasAdj
+
+variable {α : Type*} {Gr : Type*} [HasAdj α Gr]
+
+/-- A `Dart` is an oriented edge, implemented as an ordered pair of adjacent vertices.
+This terminology comes from combinatorial maps, and they are also known as "half-edges"
+or "bonds." -/
+structure Dart (G : Gr) extends α × α where
+  adj : Adj G fst snd
+
+initialize_simps_projections Dart (+toProd, -fst, -snd)
+
+attribute [simp] Dart.adj
+
+variable {G : Gr}
+
+theorem Dart.ext_iff (d₁ d₂ : Dart G) : d₁ = d₂ ↔ d₁.toProd = d₂.toProd := by
+  cases d₁; cases d₂; simp
+
+@[ext]
+theorem Dart.ext (d₁ d₂ : Dart G) (h : d₁.toProd = d₂.toProd) : d₁ = d₂ :=
+  (Dart.ext_iff d₁ d₂).mpr h
+
+theorem Dart.toProd_injective : Function.Injective (Dart.toProd : Dart G → α × α) :=
+  Dart.ext
+
+instance [DecidableEq α] (G : Gr) : DecidableEq (Dart G) :=
+  Dart.toProd_injective.decidableEq
+
+instance Dart.fintype [Fintype α] [DecidableRel (Adj G)] : Fintype (Dart G) :=
+  Fintype.ofEquiv (Σ v, { w | Adj G v w })
+    { toFun := fun s => ⟨(s.fst, s.snd), s.snd.property⟩
+      invFun := fun d => ⟨d.fst, d.snd, d.adj⟩ }
+
+variable (G)
+
+/-- Two darts are said to be adjacent if they could be consecutive
+darts in a walk -- that is, the first dart's second vertex is equal to
+the second dart's first vertex. -/
+def DartAdj (d d' : Dart G) : Prop :=
+  d.snd = d'.fst
+
+end HasAdj

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -47,6 +47,7 @@ acyclic graphs, trees
 namespace SimpleGraph
 
 open Walk
+open HasAdj
 
 variable {V V' : Type*} (G : SimpleGraph V) (G' : SimpleGraph V')
 

Mathlib/Combinatorics/SimpleGraph/Dart.lean

@@ -5,135 +5,92 @@ Authors: Kyle Miller
 -/
 module
 
-public import Mathlib.Combinatorics.SimpleGraph.Basic
-public import Mathlib.Data.Fintype.Sigma
+public import Mathlib.Combinatorics.HasAdj.Dart
+public import Mathlib.Combinatorics.SimpleGraph.HasAdj
 
 /-!
-# Darts in graphs
+# Darts in simple graphs
 
-A `Dart` or half-edge or bond in a graph is an ordered pair of adjacent vertices, regarded as an
-oriented edge. This file defines darts and proves some of their basic properties.
+This files gives simple-graph-specific properties of darts.
 -/
 
 @[expose] public section
 
-namespace SimpleGraph
+namespace HasAdj
 
-variable {V : Type*} (G : SimpleGraph V)
-
-/-- A `Dart` is an oriented edge, implemented as an ordered pair of adjacent vertices.
-This terminology comes from combinatorial maps, and they are also known as "half-edges"
-or "bonds." -/
-structure Dart extends V × V where
-  adj : G.Adj fst snd
-  deriving DecidableEq
-
-initialize_simps_projections Dart (+toProd, -fst, -snd)
-
-attribute [simp] Dart.adj
-
-variable {G}
-
-theorem Dart.ext_iff (d₁ d₂ : G.Dart) : d₁ = d₂ ↔ d₁.toProd = d₂.toProd := by
-  cases d₁; cases d₂; simp
-
-@[ext]
-theorem Dart.ext (d₁ d₂ : G.Dart) (h : d₁.toProd = d₂.toProd) : d₁ = d₂ :=
-  (Dart.ext_iff d₁ d₂).mpr h
-
-@[simp]
-theorem Dart.fst_ne_snd (d : G.Dart) : d.fst ≠ d.snd :=
-  fun h ↦ G.irrefl (h ▸ d.adj)
-
-@[simp]
-theorem Dart.snd_ne_fst (d : G.Dart) : d.snd ≠ d.fst :=
-  fun h ↦ G.irrefl (h ▸ d.adj)
-
-theorem Dart.toProd_injective : Function.Injective (Dart.toProd : G.Dart → V × V) :=
-  Dart.ext
-
-instance Dart.fintype [Fintype V] [DecidableRel G.Adj] : Fintype G.Dart :=
-  Fintype.ofEquiv (Σ v, G.neighborSet v)
-    { toFun := fun s => ⟨(s.fst, s.snd), s.snd.property⟩
-      invFun := fun d => ⟨d.fst, d.snd, d.adj⟩ }
+variable {V : Type*} {G : SimpleGraph V}
 
 /-- The edge associated to the dart. -/
-def Dart.edge (d : G.Dart) : Sym2 V := s(d.fst, d.snd)
+def Dart.edge (d : Dart G) : Sym2 V := s(d.fst, d.snd)
 
 @[simp]
 theorem Dart.edge_mk {p : V × V} (h : G.Adj p.1 p.2) : (Dart.mk p h).edge = s(p.1, p.2) :=
   rfl
 
 @[simp]
-theorem Dart.edge_mem (d : G.Dart) : d.edge ∈ G.edgeSet :=
+theorem Dart.edge_mem (d : Dart G) : d.edge ∈ G.edgeSet :=
   d.adj
 
 /-- The dart with reversed orientation from a given dart. -/
 @[simps]
-def Dart.symm (d : G.Dart) : G.Dart :=
+def Dart.symm (d : Dart G) : Dart G :=
   ⟨d.toProd.swap, G.symm d.adj⟩
 
 @[simp]
 theorem Dart.symm_mk {p : V × V} (h : G.Adj p.1 p.2) : (Dart.mk p h).symm = Dart.mk p.swap h.symm :=
   rfl
 
 @[simp]
-theorem Dart.edge_symm (d : G.Dart) : d.symm.edge = d.edge :=
+theorem Dart.edge_symm (d : Dart G) : d.symm.edge = d.edge :=
   Sym2.eq_swap
 
 @[simp]
-theorem Dart.edge_comp_symm : Dart.edge ∘ Dart.symm = (Dart.edge : G.Dart → Sym2 V) :=
+theorem Dart.edge_comp_symm : Dart.edge ∘ Dart.symm = (Dart.edge : Dart G → Sym2 V) :=
   funext Dart.edge_symm
 
 @[simp]
-theorem Dart.symm_symm (d : G.Dart) : d.symm.symm = d :=
+theorem Dart.symm_symm (d : Dart G) : d.symm.symm = d :=
   Dart.ext _ _ <| Prod.swap_swap _
 
 @[simp]
-theorem Dart.symm_involutive : Function.Involutive (Dart.symm : G.Dart → G.Dart) :=
+theorem Dart.symm_involutive : Function.Involutive (Dart.symm : Dart G → Dart G) :=
   Dart.symm_symm
 
-theorem Dart.symm_ne (d : G.Dart) : d.symm ≠ d :=
+theorem Dart.symm_ne (d : Dart G) : d.symm ≠ d :=
   ne_of_apply_ne (Prod.snd ∘ Dart.toProd) d.adj.ne
 
-theorem dart_edge_eq_iff : ∀ d₁ d₂ : G.Dart, d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm := by
+theorem dart_edge_eq_iff : ∀ d₁ d₂ : Dart G, d₁.edge = d₂.edge ↔ d₁ = d₂ ∨ d₁ = d₂.symm := by
   rintro ⟨p, hp⟩ ⟨q, hq⟩
   simp
 
 theorem dart_edge_eq_mk'_iff :
-    ∀ {d : G.Dart} {u v : V}, d.edge = s(u, v) ↔ d.toProd = (u, v) ∨ d.toProd = (v, u) := by
+    ∀ {d : Dart G} {u v : V}, d.edge = s(u, v) ↔ d.toProd = (u, v) ∨ d.toProd = (v, u) := by
   rintro ⟨p, h⟩ _ _
   simp
 
 theorem dart_edge_eq_mk'_iff' :
-    ∀ {d : G.Dart} {u v : V},
+    ∀ {d : Dart G} {u v : V},
       d.edge = s(u, v) ↔ d.fst = u ∧ d.snd = v ∨ d.fst = v ∧ d.snd = u := by
   rintro ⟨⟨a, b⟩, h⟩ u v
   rw [dart_edge_eq_mk'_iff]
   simp
 
 variable (G)
 
-/-- Two darts are said to be adjacent if they could be consecutive
-darts in a walk -- that is, the first dart's second vertex is equal to
-the second dart's first vertex. -/
-def DartAdj (d d' : G.Dart) : Prop :=
-  d.snd = d'.fst
-
 /-- For a given vertex `v`, this is the bijective map from the neighbor set at `v`
 to the darts `d` with `d.fst = v`. -/
 @[simps]
-def dartOfNeighborSet (v : V) (w : G.neighborSet v) : G.Dart :=
+def dartOfNeighborSet (v : V) (w : G.neighborSet v) : Dart G :=
   ⟨(v, w), w.property⟩
 
-theorem dartOfNeighborSet_injective (v : V) : Function.Injective (G.dartOfNeighborSet v) :=
+theorem dartOfNeighborSet_injective (v : V) : Function.Injective (dartOfNeighborSet G v) :=
   fun e₁ e₂ h =>
   Subtype.ext <| by
     injection h with h'
     convert congr_arg Prod.snd h'
 
-instance nonempty_dart_top [Nontrivial V] : Nonempty (⊤ : SimpleGraph V).Dart := by
+instance nonempty_dart_top [Nontrivial V] : Nonempty (Dart (⊤ : SimpleGraph V)) := by
   obtain ⟨v, w, h⟩ := exists_pair_ne V
   exact ⟨⟨(v, w), h⟩⟩
 
-end SimpleGraph
+end HasAdj