refactor(Combinatorics): move Walk from SimpleGraph to HasAdj

Archive/Wiedijk100Theorems/Konigsberg.lean

@@ -74,7 +74,7 @@ lemma setOf_odd_degree_eq :
   simp [not_even_degree_iff, ← Nat.not_even_iff_odd]
 
 /-- The Königsberg graph is not Eulerian. -/
-theorem not_isEulerian {u v : Verts} (p : graph.Walk u v) (h : p.IsEulerian) : False := by
+theorem not_isEulerian {u v : Verts} (p : HasAdj.Walk graph u v) (h : p.IsEulerian) : False := by
   have h := h.card_odd_degree
   have h' := setOf_odd_degree_eq
   apply_fun Fintype.card at h'

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,9 @@ 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.HasAdj.Walks.Basic
 public import Mathlib.Combinatorics.Hindman
 public import Mathlib.Combinatorics.KatonaCircle
 public import Mathlib.Combinatorics.Matroid.Basic
@@ -3386,6 +3390,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