From 8ae7095cc41e70557822df5e44158ef385593d60 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 15:21:34 +0200
Subject: [PATCH 01/36] basic graph PR

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 86 ++++++++++++++++++++++++++
 1 file changed, 86 insertions(+)
 create mode 100644 Cslib/Algorithms/Lean/Graph/Basic.lean

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
new file mode 100644
index 000000000..7b7cf3cf5
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2026 Basil Rohner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner, Sorrachai Yingchareonthawornchai
+-/
+import Mathlib.Data.Sym.Sym2
+import Cslib.Foundations.Semantics.LTS.Basic
+
+@[expose] public section
+
+/-!
+# Graph structures
+
+This file introduces a small hierarchy of graph-like combinatorial structures on a vertex
+type `α`. `SimpleGraph` and `SimpleDiGraph` carry their adjacency relation directly and
+disallow loops and multi-edges. `DiGraph` reuses `Cslib.LTS` to additionally support
+edge labels, and hence parallel edges. Both `SimpleGraph` and `SimpleDiGraph` follow
+the `Graph` definitions in Mathlib.
+
+## Main definitions
+
+* `SimpleGraph α`: an undirected graph with adjacency `Adj : α → α → Prop`, no loops or
+  multi-edges.
+* `SimpleDiGraph α`: a directed graph with adjacency `Adj : α → α → Prop`, no loops or
+  multi-edges.
+* `DiGraph α β`: a directed graph built from `Cslib.LTS α β`, with edge labels in `β`.
+  Parallel edges and loops are permitted.
+
+## Main API
+
+* `SimpleGraph.edgeSet`, `SimpleDiGraph.edgeSet`, `DiGraph.edgeSet`: the edge set of a
+  graph, derived from its adjacency/transition relation.
+-/
+
+namespace Cslib.Algorithms.Lean.Graph
+
+variable {α β : Type*}
+
+/-- An undirected graph on `α` with adjacency relation `Adj`, containing no loops or
+multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
+structure SimpleGraph (α : Type*) where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- The adjacency relation. `Adj x y` means `x` and `y` are joined by an edge. -/
+  Adj : α → α → Prop
+  /-- Adjacency is symmetric: if `x` is adjacent to `y`, then `y` is adjacent to `x`. -/
+  symm : Std.Symm Adj := by grind
+  /-- No vertex is adjacent to itself. -/
+  loopless : Std.Irrefl Adj := by grind
+  /-- The left endpoint of every adjacent pair is a vertex. -/
+  incidence_left : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
+
+/-- The edge set of a `SimpleGraph`, as unordered pairs of adjacent vertices. -/
+def SimpleGraph.edgeSet (G : SimpleGraph α) : Set (Sym2 α) :=
+  Sym2.fromRel (G.symm)
+
+/-- A directed graph on `α` with adjacency relation `Adj`, containing no loops or
+multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
+structure SimpleDiGraph (α : Type*) where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- The adjacency relation. `Adj x y` means there is an arc from `x` to `y`. -/
+  Adj : α → α → Prop
+  /-- No vertex is adjacent to itself. -/
+  loopless : Std.Irrefl Adj := by grind
+  /-- Both endpoints of every adjacent pair are vertices. -/
+  incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
+
+/-- The edge set of a `SimpleDiGraph`, as ordered pairs of adjacent vertices. -/
+def SimpleDiGraph.edgeSet (G : SimpleDiGraph α) : Set (α × α) :=
+  { (x,y) | G.Adj x y}
+
+/-- A directed graph on vertex type `α` with edge labels in `β`, built from `Cslib.LTS`.
+Parallel edges (distinguished by label) and loops are permitted, and both the vertex and
+edge sets may be infinite. -/
+structure DiGraph (α β : Type*) extends Cslib.LTS α β where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- Both endpoints of every transition are vertices. -/
+  incidence : ∀ ⦃x l y⦄, Tr x l y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
+
+/-- The edge set of a `DiGraph`, as labelled ordered triples `(source, label, target)`. -/
+def DiGraph.edgeSet (G : DiGraph α β) : Set (α × β × α) :=
+  {(x, l, y) | G.Tr x l y}
+
+end Cslib.Algorithms.Lean.Graph

From 05ded5657de361cdb9577aa77cede3cf0685013e Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 15:30:22 +0200
Subject: [PATCH 02/36] update

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 7b7cf3cf5..9170c0033 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -34,8 +34,6 @@ the `Graph` definitions in Mathlib.
 
 namespace Cslib.Algorithms.Lean.Graph
 
-variable {α β : Type*}
-
 /-- An undirected graph on `α` with adjacency relation `Adj`, containing no loops or
 multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
 structure SimpleGraph (α : Type*) where
@@ -51,7 +49,7 @@ structure SimpleGraph (α : Type*) where
   incidence_left : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
 
 /-- The edge set of a `SimpleGraph`, as unordered pairs of adjacent vertices. -/
-def SimpleGraph.edgeSet (G : SimpleGraph α) : Set (Sym2 α) :=
+def SimpleGraph.edgeSet {α} (G : SimpleGraph α) : Set (Sym2 α) :=
   Sym2.fromRel (G.symm)
 
 /-- A directed graph on `α` with adjacency relation `Adj`, containing no loops or
@@ -67,7 +65,7 @@ structure SimpleDiGraph (α : Type*) where
   incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
 
 /-- The edge set of a `SimpleDiGraph`, as ordered pairs of adjacent vertices. -/
-def SimpleDiGraph.edgeSet (G : SimpleDiGraph α) : Set (α × α) :=
+def SimpleDiGraph.edgeSet {α} (G : SimpleDiGraph α) : Set (α × α) :=
   { (x,y) | G.Adj x y}
 
 /-- A directed graph on vertex type `α` with edge labels in `β`, built from `Cslib.LTS`.
@@ -80,7 +78,7 @@ structure DiGraph (α β : Type*) extends Cslib.LTS α β where
   incidence : ∀ ⦃x l y⦄, Tr x l y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
 
 /-- The edge set of a `DiGraph`, as labelled ordered triples `(source, label, target)`. -/
-def DiGraph.edgeSet (G : DiGraph α β) : Set (α × β × α) :=
+def DiGraph.edgeSet {α β} (G : DiGraph α β) : Set (α × β × α) :=
   {(x, l, y) | G.Tr x l y}
 
 end Cslib.Algorithms.Lean.Graph

From edd657d054bb7c78d7c9b6975040cbe0969dc98a Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 15:37:37 +0200
Subject: [PATCH 03/36] update

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 9170c0033..550e62af0 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -11,8 +11,11 @@ import Cslib.Foundations.Semantics.LTS.Basic
 /-!
 # Graph structures
 
-This file introduces a small hierarchy of graph-like combinatorial structures on a vertex
-type `α`. `SimpleGraph` and `SimpleDiGraph` carry their adjacency relation directly and
+This file introduces graph-like combinatorial structures on a vertex
+type `α`. We follow `Graph` definition in Mathlib: The main principle is to define a vertex set
+as a `Set α`. Since Mathlib already defined a simple multi graph, ww define other
+three combinations here:  `SimpleGraph`, `SimpleDiGraph` and `DiGraph`.
+`SimpleGraph` and `SimpleDiGraph` carry their adjacency relation directly and
 disallow loops and multi-edges. `DiGraph` reuses `Cslib.LTS` to additionally support
 edge labels, and hence parallel edges. Both `SimpleGraph` and `SimpleDiGraph` follow
 the `Graph` definitions in Mathlib.

From 8f690ddb82dffcbffd82f507b61f52684809652f Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 15:41:16 +0200
Subject: [PATCH 04/36] update

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 550e62af0..992a2d891 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -13,12 +13,12 @@ import Cslib.Foundations.Semantics.LTS.Basic
 
 This file introduces graph-like combinatorial structures on a vertex
 type `α`. We follow `Graph` definition in Mathlib: The main principle is to define a vertex set
-as a `Set α`. Since Mathlib already defined a simple multi graph, ww define other
-three combinations here:  `SimpleGraph`, `SimpleDiGraph` and `DiGraph`.
-`SimpleGraph` and `SimpleDiGraph` carry their adjacency relation directly and
-disallow loops and multi-edges. `DiGraph` reuses `Cslib.LTS` to additionally support
-edge labels, and hence parallel edges. Both `SimpleGraph` and `SimpleDiGraph` follow
-the `Graph` definitions in Mathlib.
+as a `Set α` (see https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Graph/Basic.html#Graph for the rationale behind the design).
+Since Mathlib already defined a simple multi graph, ww define other three combinations here:
+`SimpleGraph`, `SimpleDiGraph` and `DiGraph`. `SimpleGraph` and `SimpleDiGraph` carry
+their adjacency relation directly and disallow loops and multi-edges. `DiGraph` reuses `Cslib.LTS`
+to additionally support edge labels, and hence parallel edges.
+Both `SimpleGraph` and `SimpleDiGraph` follow `Graph` definitions in Mathlib.
 
 ## Main definitions
 

From c2a452c0eccec788cb0e9c2cceb9ced774d7f5d2 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 15:52:23 +0200
Subject: [PATCH 05/36] up

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 992a2d891..e6d7a394e 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -14,7 +14,7 @@ import Cslib.Foundations.Semantics.LTS.Basic
 This file introduces graph-like combinatorial structures on a vertex
 type `α`. We follow `Graph` definition in Mathlib: The main principle is to define a vertex set
 as a `Set α` (see https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Graph/Basic.html#Graph for the rationale behind the design).
-Since Mathlib already defined a simple multi graph, ww define other three combinations here:
+Since Mathlib already defined a simple multi graph, ww define the other three combinations here:
 `SimpleGraph`, `SimpleDiGraph` and `DiGraph`. `SimpleGraph` and `SimpleDiGraph` carry
 their adjacency relation directly and disallow loops and multi-edges. `DiGraph` reuses `Cslib.LTS`
 to additionally support edge labels, and hence parallel edges.
@@ -55,6 +55,13 @@ structure SimpleGraph (α : Type*) where
 def SimpleGraph.edgeSet {α} (G : SimpleGraph α) : Set (Sym2 α) :=
   Sym2.fromRel (G.symm)
 
+lemma SimpleGraph.Adj.symm {G : SimpleGraph α} {x y : α} (h : G.Adj x y) : G.Adj y x :=
+  G.symm.symm x y h
+
+lemma SimpleGraph.incidence {G : SimpleGraph α} ⦃x y : α⦄ (h : G.Adj x y) :
+    x ∈ G.vertexSet ∧ y ∈ G.vertexSet :=
+  ⟨G.incidence_left h, G.incidence_left h.symm⟩
+
 /-- A directed graph on `α` with adjacency relation `Adj`, containing no loops or
 multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
 structure SimpleDiGraph (α : Type*) where

From e5d1be2c9071a73e11e9b7b2265e84fe4c8ed64a Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 15:53:46 +0200
Subject: [PATCH 06/36] typo

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index e6d7a394e..cd9be2834 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -14,7 +14,7 @@ import Cslib.Foundations.Semantics.LTS.Basic
 This file introduces graph-like combinatorial structures on a vertex
 type `α`. We follow `Graph` definition in Mathlib: The main principle is to define a vertex set
 as a `Set α` (see https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Graph/Basic.html#Graph for the rationale behind the design).
-Since Mathlib already defined a simple multi graph, ww define the other three combinations here:
+Since Mathlib already defined a simple multi graph, we define the other three combinations here:
 `SimpleGraph`, `SimpleDiGraph` and `DiGraph`. `SimpleGraph` and `SimpleDiGraph` carry
 their adjacency relation directly and disallow loops and multi-edges. `DiGraph` reuses `Cslib.LTS`
 to additionally support edge labels, and hence parallel edges.

From 794208f40d4ead289cbcbfbf016f9fc3a00d99dd Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 16:01:02 +0200
Subject: [PATCH 07/36] update

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index cd9be2834..e067a2e78 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -5,6 +5,7 @@ Authors: Basil Rohner, Sorrachai Yingchareonthawornchai
 -/
 import Mathlib.Data.Sym.Sym2
 import Cslib.Foundations.Semantics.LTS.Basic
+import Mathlib.Combinatorics.SimpleGraph.Basic
 
 @[expose] public section
 
@@ -39,15 +40,9 @@ namespace Cslib.Algorithms.Lean.Graph
 
 /-- An undirected graph on `α` with adjacency relation `Adj`, containing no loops or
 multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
-structure SimpleGraph (α : Type*) where
+structure SimpleGraph (α : Type*) extends _root_.SimpleGraph α where
   /-- The set of vertices. -/
   vertexSet : Set α
-  /-- The adjacency relation. `Adj x y` means `x` and `y` are joined by an edge. -/
-  Adj : α → α → Prop
-  /-- Adjacency is symmetric: if `x` is adjacent to `y`, then `y` is adjacent to `x`. -/
-  symm : Std.Symm Adj := by grind
-  /-- No vertex is adjacent to itself. -/
-  loopless : Std.Irrefl Adj := by grind
   /-- The left endpoint of every adjacent pair is a vertex. -/
   incidence_left : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
 

From a807a8ada079cc5ad11751506aca6131abea36cc Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 17:01:26 +0200
Subject: [PATCH 08/36] clean

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 58 ++++++++++++++------------
 1 file changed, 31 insertions(+), 27 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index e067a2e78..46eb34e66 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -1,34 +1,35 @@
 /-
 Copyright (c) 2026 Basil Rohner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Basil Rohner, Sorrachai Yingchareonthawornchai
+Authors: Basil Rohner, Fabrizio Montesi, Sorrachai Yingchareonthawornchai
 -/
-import Mathlib.Data.Sym.Sym2
+
 import Cslib.Foundations.Semantics.LTS.Basic
 import Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Combinatorics.Graph.Basic
 
 @[expose] public section
 
 /-!
 # Graph structures
 
-This file introduces graph-like combinatorial structures on a vertex
-type `α`. We follow `Graph` definition in Mathlib: The main principle is to define a vertex set
-as a `Set α` (see https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Graph/Basic.html#Graph for the rationale behind the design).
-Since Mathlib already defined a simple multi graph, we define the other three combinations here:
-`SimpleGraph`, `SimpleDiGraph` and `DiGraph`. `SimpleGraph` and `SimpleDiGraph` carry
-their adjacency relation directly and disallow loops and multi-edges. `DiGraph` reuses `Cslib.LTS`
-to additionally support edge labels, and hence parallel edges.
-Both `SimpleGraph` and `SimpleDiGraph` follow `Graph` definitions in Mathlib.
+This file follows the `Set`-based vertex/edge design of `Mathlib.Combinatorics.Graph`: a
+vertex set of type `Set α`, with any relation on `α` or `β` constrained by an incidence
+relation. `Graph` is Mathlib's `Graph` directly. `SimpleGraph` extends Mathlib's
+`SimpleGraph`, adding a vertex subset in the same style. `SimpleDiGraph` has no Mathlib
+counterpart to extend and is built by hand. `DiGraph` reuses `Cslib.LTS` for its
+transition relation and adds the same vertex-subset layer.
 
 ## Main definitions
 
+* `Graph α β`: an undirected multi-graph as a Mathlib's graph.
 * `SimpleGraph α`: an undirected graph with adjacency `Adj : α → α → Prop`, no loops or
   multi-edges.
-* `SimpleDiGraph α`: a directed graph with adjacency `Adj : α → α → Prop`, no loops or
-  multi-edges.
 * `DiGraph α β`: a directed graph built from `Cslib.LTS α β`, with edge labels in `β`.
   Parallel edges and loops are permitted.
+* `SimpleDiGraph α`: a directed graph with adjacency `Adj : α → α → Prop`, no loops or
+  multi-edges.
+
 
 ## Main API
 
@@ -36,7 +37,11 @@ Both `SimpleGraph` and `SimpleDiGraph` follow `Graph` definitions in Mathlib.
   graph, derived from its adjacency/transition relation.
 -/
 
-namespace Cslib.Algorithms.Lean.Graph
+namespace Cslib.Algorithms.Lean
+
+
+/-- An undirected multigraph on vertex type `α` with edge labels in `β` -/
+abbrev Graph (α β : Type*) :=  _root_.Graph α β
 
 /-- An undirected graph on `α` with adjacency relation `Adj`, containing no loops or
 multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
@@ -57,6 +62,18 @@ lemma SimpleGraph.incidence {G : SimpleGraph α} ⦃x y : α⦄ (h : G.Adj x y)
     x ∈ G.vertexSet ∧ y ∈ G.vertexSet :=
   ⟨G.incidence_left h, G.incidence_left h.symm⟩
 
+/-- A directed graph on vertex type `α` with edge labels in `β`, built from `Cslib.LTS`.
+Parallel edges (distinguished by label) and loops are permitted. -/
+structure DiGraph (α β : Type*) extends Cslib.LTS α β where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- Both endpoints of every transition are vertices. -/
+  incidence : ∀ ⦃x l y⦄, Tr x l y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
+
+/-- The edge set of a `DiGraph`, as labelled ordered triples `(source, label, target)`. -/
+def DiGraph.edgeSet {α β} (G : DiGraph α β) : Set (α × β × α) :=
+  {(x, l, y) | G.Tr x l y}
+
 /-- A directed graph on `α` with adjacency relation `Adj`, containing no loops or
 multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
 structure SimpleDiGraph (α : Type*) where
@@ -73,17 +90,4 @@ structure SimpleDiGraph (α : Type*) where
 def SimpleDiGraph.edgeSet {α} (G : SimpleDiGraph α) : Set (α × α) :=
   { (x,y) | G.Adj x y}
 
-/-- A directed graph on vertex type `α` with edge labels in `β`, built from `Cslib.LTS`.
-Parallel edges (distinguished by label) and loops are permitted, and both the vertex and
-edge sets may be infinite. -/
-structure DiGraph (α β : Type*) extends Cslib.LTS α β where
-  /-- The set of vertices. -/
-  vertexSet : Set α
-  /-- Both endpoints of every transition are vertices. -/
-  incidence : ∀ ⦃x l y⦄, Tr x l y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
-
-/-- The edge set of a `DiGraph`, as labelled ordered triples `(source, label, target)`. -/
-def DiGraph.edgeSet {α β} (G : DiGraph α β) : Set (α × β × α) :=
-  {(x, l, y) | G.Tr x l y}
-
-end Cslib.Algorithms.Lean.Graph
+end Cslib.Algorithms.Lean

From 64e7750d3b58b64bc5edbd70ebc584306bac3b71 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 17:11:32 +0200
Subject: [PATCH 09/36] update

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 46eb34e66..6eea408de 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -69,6 +69,8 @@ structure DiGraph (α β : Type*) extends Cslib.LTS α β where
   vertexSet : Set α
   /-- Both endpoints of every transition are vertices. -/
   incidence : ∀ ⦃x l y⦄, Tr x l y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
+  /-- Each edge label is used at most once. -/
+  tr_inj : ∀ ⦃x y x' y' : α⦄ ⦃l : β⦄, Tr x l y → Tr x' l y' → x = x' ∧ y = y'
 
 /-- The edge set of a `DiGraph`, as labelled ordered triples `(source, label, target)`. -/
 def DiGraph.edgeSet {α β} (G : DiGraph α β) : Set (α × β × α) :=

From 4e39303c995da54a2b2c160c486e642a8d627eaf Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 17:13:11 +0200
Subject: [PATCH 10/36] minor

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 6eea408de..46468b883 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -69,7 +69,7 @@ structure DiGraph (α β : Type*) extends Cslib.LTS α β where
   vertexSet : Set α
   /-- Both endpoints of every transition are vertices. -/
   incidence : ∀ ⦃x l y⦄, Tr x l y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
-  /-- Each edge label is used at most once. -/
+  /-- Each label is used at most once. -/
   tr_inj : ∀ ⦃x y x' y' : α⦄ ⦃l : β⦄, Tr x l y → Tr x' l y' → x = x' ∧ y = y'
 
 /-- The edge set of a `DiGraph`, as labelled ordered triples `(source, label, target)`. -/

From a7a5c33ffed2766b101f4a0085f9df605dd5f696 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 17:22:35 +0200
Subject: [PATCH 11/36] minor

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 46468b883..78cafc0a5 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -39,7 +39,6 @@ transition relation and adds the same vertex-subset layer.
 
 namespace Cslib.Algorithms.Lean
 
-
 /-- An undirected multigraph on vertex type `α` with edge labels in `β` -/
 abbrev Graph (α β : Type*) :=  _root_.Graph α β
 

From fc57b05fb7e070baddc8a80116981aca1b7c1c92 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 17:24:16 +0200
Subject: [PATCH 12/36] minor

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 78cafc0a5..5dcf6f1bb 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -17,7 +17,7 @@ This file follows the `Set`-based vertex/edge design of `Mathlib.Combinatorics.G
 vertex set of type `Set α`, with any relation on `α` or `β` constrained by an incidence
 relation. `Graph` is Mathlib's `Graph` directly. `SimpleGraph` extends Mathlib's
 `SimpleGraph`, adding a vertex subset in the same style. `SimpleDiGraph` has no Mathlib
-counterpart to extend and is built by hand. `DiGraph` reuses `Cslib.LTS` for its
+counterpart to extend and is built from scratch. `DiGraph` reuses `Cslib.LTS` for its
 transition relation and adds the same vertex-subset layer.
 
 ## Main definitions

From bb36d7252caf0dfadf6531b47fd7e8440fe69bb7 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 17:47:25 +0200
Subject: [PATCH 13/36] minor

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 5dcf6f1bb..c90c59b83 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -61,8 +61,8 @@ lemma SimpleGraph.incidence {G : SimpleGraph α} ⦃x y : α⦄ (h : G.Adj x y)
     x ∈ G.vertexSet ∧ y ∈ G.vertexSet :=
   ⟨G.incidence_left h, G.incidence_left h.symm⟩
 
-/-- A directed graph on vertex type `α` with edge labels in `β`, built from `Cslib.LTS`.
-Parallel edges (distinguished by label) and loops are permitted. -/
+/-- A directed graph on vertex type `α`  whose edges are identified by labels `β`
+  built from `Cslib.LTS`. Parallel edges (distinguished by label) and loops are permitted. -/
 structure DiGraph (α β : Type*) extends Cslib.LTS α β where
   /-- The set of vertices. -/
   vertexSet : Set α

From 61fc0760b2df53f7f00fd68bbe0c08d0b1608d3c Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Fri, 14 Aug 2026 23:24:21 +0200
Subject: [PATCH 14/36] minor

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index c90c59b83..6d9fb49c0 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2026 Basil Rohner. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Basil Rohner, Fabrizio Montesi, Sorrachai Yingchareonthawornchai
+Authors: Basil Rohner, Sorrachai Yingchareonthawornchai
 -/
 
 import Cslib.Foundations.Semantics.LTS.Basic

From 6da55e5d303c68994767d7f34420aff57f3f9ce0 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Sat, 15 Aug 2026 10:13:36 +0200
Subject: [PATCH 15/36] revise

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 54 +++++++++++++++++++-------
 1 file changed, 39 insertions(+), 15 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 6d9fb49c0..d0522a63b 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -39,8 +39,44 @@ transition relation and adds the same vertex-subset layer.
 
 namespace Cslib.Algorithms.Lean
 
-/-- An undirected multigraph on vertex type `α` with edge labels in `β` -/
-abbrev Graph (α β : Type*) :=  _root_.Graph α β
+/-- An undirected edge with a label of type `β` and an unordered pair of endpoints. -/
+structure Edge (α β : Type*) where
+  /-- The edge label, used to distinguish parallel edges. -/
+  endpointsLabel : β
+  /-- The unordered pair of endpoints. -/
+  endpoints : Sym2 α
+deriving DecidableEq
+
+/-- A directed edge with a label of type `β` and an ordered pair of endpoints. -/
+structure Arc (α β : Type*) where
+  /-- The edge label, used to distinguish parallel edges. -/
+  endpointsLabel : β
+  /-- The ordered pair `(source, target)` of endpoints. -/
+  endpoints : α × α
+deriving DecidableEq
+
+/-- A general graph on vertex type `α` with edge labels in `β`. Each edge bundles a label
+and an unordered pair of endpoints. Parallel edges and loops are permitted, and both the
+vertex and edge sets may be infinite. -/
+structure Graph (α β : Type*) where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- The set of edges. -/
+  edgeSet : Set (Edge α β)
+  /-- Every endpoint of an edge is a vertex. Prefer `Graph.incidence`. -/
+  incidence' : ∀ e ∈ edgeSet, ∀ v ∈ e.endpoints, v ∈ vertexSet
+
+/-- A directed graph on vertex type `α` with edge labels in `β`. Each edge bundles a label
+and an ordered pair of endpoints. Parallel edges and loops are permitted, and both the
+vertex and edge sets may be infinite. -/
+structure DiGraph (α β : Type*) where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- The set of edges. -/
+  edgeSet : Set (Arc α β)
+  /-- Both endpoints of every edge are vertices. Prefer `DiGraph.incidence`. -/
+  incidence' : ∀ e ∈ edgeSet, e.endpoints.1 ∈ vertexSet ∧ e.endpoints.2 ∈ vertexSet
+
 
 /-- An undirected graph on `α` with adjacency relation `Adj`, containing no loops or
 multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
@@ -61,19 +97,6 @@ lemma SimpleGraph.incidence {G : SimpleGraph α} ⦃x y : α⦄ (h : G.Adj x y)
     x ∈ G.vertexSet ∧ y ∈ G.vertexSet :=
   ⟨G.incidence_left h, G.incidence_left h.symm⟩
 
-/-- A directed graph on vertex type `α`  whose edges are identified by labels `β`
-  built from `Cslib.LTS`. Parallel edges (distinguished by label) and loops are permitted. -/
-structure DiGraph (α β : Type*) extends Cslib.LTS α β where
-  /-- The set of vertices. -/
-  vertexSet : Set α
-  /-- Both endpoints of every transition are vertices. -/
-  incidence : ∀ ⦃x l y⦄, Tr x l y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
-  /-- Each label is used at most once. -/
-  tr_inj : ∀ ⦃x y x' y' : α⦄ ⦃l : β⦄, Tr x l y → Tr x' l y' → x = x' ∧ y = y'
-
-/-- The edge set of a `DiGraph`, as labelled ordered triples `(source, label, target)`. -/
-def DiGraph.edgeSet {α β} (G : DiGraph α β) : Set (α × β × α) :=
-  {(x, l, y) | G.Tr x l y}
 
 /-- A directed graph on `α` with adjacency relation `Adj`, containing no loops or
 multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
@@ -91,4 +114,5 @@ structure SimpleDiGraph (α : Type*) where
 def SimpleDiGraph.edgeSet {α} (G : SimpleDiGraph α) : Set (α × α) :=
   { (x,y) | G.Adj x y}
 
+
 end Cslib.Algorithms.Lean

From 1ea0bbb1efc8bfee7560d50d66966062cbc66d32 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Sat, 15 Aug 2026 10:19:49 +0200
Subject: [PATCH 16/36] update

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index d0522a63b..631b901de 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -14,27 +14,23 @@ import Mathlib.Combinatorics.Graph.Basic
 # Graph structures
 
 This file follows the `Set`-based vertex/edge design of `Mathlib.Combinatorics.Graph`: a
-vertex set of type `Set α`, with any relation on `α` or `β` constrained by an incidence
-relation. `Graph` is Mathlib's `Graph` directly. `SimpleGraph` extends Mathlib's
+vertex set of type `Set α`. `SimpleGraph` extends Mathlib's
 `SimpleGraph`, adding a vertex subset in the same style. `SimpleDiGraph` has no Mathlib
-counterpart to extend and is built from scratch. `DiGraph` reuses `Cslib.LTS` for its
-transition relation and adds the same vertex-subset layer.
+counterpart to extend and is built from scratch. We proritize computability., and thus
+`DiGraph, Graph` require storing `Arc, Edge` structure.
 
 ## Main definitions
 
-* `Graph α β`: an undirected multi-graph as a Mathlib's graph.
-* `SimpleGraph α`: an undirected graph with adjacency `Adj : α → α → Prop`, no loops or
-  multi-edges.
-* `DiGraph α β`: a directed graph built from `Cslib.LTS α β`, with edge labels in `β`.
-  Parallel edges and loops are permitted.
+* `Graph α β`: an undirected multi-graph.
+* `DiGraph α β`: a directed graph.
+* `SimpleGraph α`: an undirected graph build on top of Mathlib's SimpleGraph.
 * `SimpleDiGraph α`: a directed graph with adjacency `Adj : α → α → Prop`, no loops or
   multi-edges.
 
-
 ## Main API
 
-* `SimpleGraph.edgeSet`, `SimpleDiGraph.edgeSet`, `DiGraph.edgeSet`: the edge set of a
-  graph, derived from its adjacency/transition relation.
+* `SimpleGraph.edgeSet`, `SimpleDiGraph.edgeSet`: the edge set of a
+  graph, derived from its adjacency relation.
 -/
 
 namespace Cslib.Algorithms.Lean

From 55984dfd5da0a96feef453b08617a52793c3700a Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Mon, 17 Aug 2026 12:02:59 +0200
Subject: [PATCH 17/36] update

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 172 ++++++++++++++-----------
 1 file changed, 94 insertions(+), 78 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 631b901de..b8a06a6fe 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -4,111 +4,127 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Basil Rohner, Sorrachai Yingchareonthawornchai
 -/
 
-import Cslib.Foundations.Semantics.LTS.Basic
-import Mathlib.Combinatorics.SimpleGraph.Basic
-import Mathlib.Combinatorics.Graph.Basic
+module
+
+public import Cslib.Foundations.Semantics.LTS.Basic
+public import Mathlib.Combinatorics.Digraph.Basic
+public import Mathlib.Combinatorics.Graph.Basic
+public import Mathlib.Combinatorics.SimpleGraph.Basic
+
 
 @[expose] public section
 
 /-!
 # Graph structures
 
-This file follows the `Set`-based vertex/edge design of `Mathlib.Combinatorics.Graph`: a
-vertex set of type `Set α`. `SimpleGraph` extends Mathlib's
-`SimpleGraph`, adding a vertex subset in the same style. `SimpleDiGraph` has no Mathlib
-counterpart to extend and is built from scratch. We proritize computability., and thus
-`DiGraph, Graph` require storing `Arc, Edge` structure.
+Vertex and edge sets are `Set`-valued, following the design of
+`Mathlib.Combinatorics.Graph`: a subgraph of `G : Graph α β` is another term of
+`Graph α β` rather than a separate type, so no coercion maps are needed.
+
+Four structures are provided, in two pairs. `Graph` and `Digraph` are multigraphs whose
+edges carry labels in `β`, so parallel edges and loops are permitted. `SimpleGraph` and
+`SimpleDigraph` have `Prop`-valued adjacency and therefore admit neither loops nor
+parallel edges.
 
 ## Main definitions
 
-* `Graph α β`: an undirected multi-graph.
-* `DiGraph α β`: a directed graph.
-* `SimpleGraph α`: an undirected graph build on top of Mathlib's SimpleGraph.
-* `SimpleDiGraph α`: a directed graph with adjacency `Adj : α → α → Prop`, no loops or
-  multi-edges.
+* `Graph α β`: an undirected multigraph, extending Mathlib's `Graph α β`.
+* `Digraph α β`: a directed multigraph; the directed counterpart of Mathlib's `Graph α β`.
+* `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 α`.
 
 ## Main API
 
-* `SimpleGraph.edgeSet`, `SimpleDiGraph.edgeSet`: the edge set of a
-  graph, derived from its adjacency relation.
--/
+* `Graph.endpoints`, `Digraph.endpoints`: the ends of an edge or arc.
+* `SimpleDigraph.arcSet`: the arc set of a `SimpleDigraph`, derived from its adjacency
+  relation. The corresponding `SimpleGraph.edgeSet` is inherited from Mathlib rather than
+  redefined here.
 
-namespace Cslib.Algorithms.Lean
+## Implementation notes
 
-/-- An undirected edge with a label of type `β` and an unordered pair of endpoints. -/
-structure Edge (α β : Type*) where
-  /-- The edge label, used to distinguish parallel edges. -/
-  endpointsLabel : β
-  /-- The unordered pair of endpoints. -/
-  endpoints : Sym2 α
-deriving DecidableEq
-
-/-- A directed edge with a label of type `β` and an ordered pair of endpoints. -/
-structure Arc (α β : Type*) where
-  /-- The edge label, used to distinguish parallel edges. -/
-  endpointsLabel : β
-  /-- The ordered pair `(source, target)` of endpoints. -/
-  endpoints : α × α
-deriving DecidableEq
-
-/-- A general graph on vertex type `α` with edge labels in `β`. Each edge bundles a label
-and an unordered pair of endpoints. Parallel edges and loops are permitted, and both the
-vertex and edge sets may be infinite. -/
-structure Graph (α β : Type*) where
-  /-- The set of vertices. -/
-  vertexSet : Set α
-  /-- The set of edges. -/
-  edgeSet : Set (Edge α β)
-  /-- Every endpoint of an edge is a vertex. Prefer `Graph.incidence`. -/
-  incidence' : ∀ e ∈ edgeSet, ∀ v ∈ e.endpoints, v ∈ vertexSet
-
-/-- A directed graph on vertex type `α` with edge labels in `β`. Each edge bundles a label
-and an ordered pair of endpoints. Parallel edges and loops are permitted, and both the
-vertex and edge sets may be infinite. -/
-structure DiGraph (α β : Type*) where
-  /-- The set of vertices. -/
-  vertexSet : Set α
-  /-- The set of edges. -/
-  edgeSet : Set (Arc α β)
-  /-- Both endpoints of every edge are vertices. Prefer `DiGraph.incidence`. -/
-  incidence' : ∀ e ∈ edgeSet, e.endpoints.1 ∈ vertexSet ∧ e.endpoints.2 ∈ vertexSet
+`IsLink` and `IsArc` are `Prop`-valued, so nothing about them is executable. To recover
+computation, `Graph` and `Digraph` each carry an `endpoints : β → Option _` field together
+with `endpoints_spec`. That specification pins the value of `endpoints` at *every* label —
+`some` on the edge set, and `none` off it, since every `s : Sym2 α` is of the form
+`s(x, y)`.
 
+-/
 
-/-- An undirected graph on `α` with adjacency relation `Adj`, containing no loops or
-multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
-structure SimpleGraph (α : Type*) extends _root_.SimpleGraph α where
-  /-- The set of vertices. -/
-  vertexSet : Set α
-  /-- The left endpoint of every adjacent pair is a vertex. -/
-  incidence_left : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
+namespace Cslib.Algorithms.Lean
 
-/-- The edge set of a `SimpleGraph`, as unordered pairs of adjacent vertices. -/
-def SimpleGraph.edgeSet {α} (G : SimpleGraph α) : Set (Sym2 α) :=
-  Sym2.fromRel (G.symm)
 
-lemma SimpleGraph.Adj.symm {G : SimpleGraph α} {x y : α} (h : G.Adj x y) : G.Adj y x :=
-  G.symm.symm x y h
+/-- An undirected multigraph on vertex type `α` with edge labels in `β`, bundled with a
+computable map from an edge label to its ends.
 
-lemma SimpleGraph.incidence {G : SimpleGraph α} ⦃x y : α⦄ (h : G.Adj x y) :
-    x ∈ G.vertexSet ∧ y ∈ G.vertexSet :=
-  ⟨G.incidence_left h, G.incidence_left h.symm⟩
+This is Mathlib's `Graph α β` — so parallel edges and loops are permitted, and both the
+vertex and edge sets may be infinite — together with the `endpoints` field. That field is
+uniquely determined by `toGraph`, so it carries no mathematical content; it exists so that
+incidence can be evaluated rather than only reasoned about. -/
+structure Graph (α β : Type*) extends _root_.Graph α β where
+  /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of the graph. -/
+  endpoints : β → Option (Sym2 α)
+  /-- `endpoints` computes `Graph.IsLink`. This forces `endpoints e = none` for every
+  `e ∉ edgeSet`, since every `s : Sym2 α` is of the form `s(x, y)`. -/
+  endpoints_spec : ∀ e x y, toGraph.IsLink e x y ↔ endpoints e = some s(x, y)
 
+/-- A directed multigraph on vertex type `α` with arc labels in `β`, bundled with a
+computable map from an arc label to its endpoints.
 
-/-- A directed graph on `α` with adjacency relation `Adj`, containing no loops or
-multi-edges. Both endpoints of every adjacent pair lie in `vertexSet`. -/
-structure SimpleDiGraph (α : Type*) where
+The directed counterpart of Mathlib's `Graph α β`, which has no Mathlib counterpart to
+extend; the field layout mirrors it, with symmetry dropped. -/
+structure Digraph (α β : Type*) where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- The incidence predicate: `IsArc e x y` states that the arc labelled `e` runs from
+  `x` to `y`. -/
+  IsArc : β → α → α → Prop
+  /-- Both ends of every arc are vertices. `IsArc` is not symmetric, so neither direction
+  follows from the other. -/
+  incidence  : ∀ ⦃e x y⦄, IsArc e x y → (x ∈ vertexSet ∧ y ∈ vertexSet)
+  /-- The ends of the arc labelled `e`, or `none` if `e` is not an arc of the graph. -/
+  endpoints : β → Option (α × α)
+  /-- `endpoints` computes `IsArc`. This forces `endpoints e = none` for every
+  `e ∉ arcSet`. -/
+  endpoints_spec : ∀ e x y, IsArc e x y ↔ endpoints e = some (x, y)
+  /-- The set of arc labels. -/
+  arcSet : Set β := { e | ∃ x y, IsArc e x y}
+  /-- A label lies in `arcSet` exactly when it is used by some arc. -/
+  arc_mem_iff_exists_isArc (e) : e ∈ arcSet ↔ ∃ x y, IsArc e x y := by exact fun _ ↦ Iff.rfl
+
+/-- A simple graph on `α` — irreflexive and symmetric adjacency, hence no loops and no
+parallel edges — together with a vertex set containing every end of an adjacent pair.
+
+Extends Mathlib's `SimpleGraph α`, so its API is available through `toSimpleGraph`; in
+particular `edgeSet`, the unordered pairs of adjacent vertices, is inherited rather than
+redefined. Note that `Adj` is a relation on all of `α`, so `vertexSet` may be any superset
+of the vertices actually incident to an edge. -/
+structure SimpleGraph (α : Type*) extends _root_.SimpleGraph α where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- The left end of every adjacent pair is a vertex. The right end then follows by
+  symmetry of `Adj`. -/
+  left_incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
+
+/-- A simple directed graph on `α` — adjacency `Adj : α → α → Prop`, hence no parallel
+arcs — with loops explicitly excluded, together with a vertex set containing every end of
+an adjacent pair.
+
+Extends Mathlib's `Digraph α`, which is a bare adjacency relation and does permit loops;
+`loopless` is what rules them out here. Antiparallel arcs are permitted: `Adj x y` and
+`Adj y x` may both hold. -/
+structure SimpleDigraph (α : Type*) extends _root_.Digraph α where
   /-- The set of vertices. -/
   vertexSet : Set α
-  /-- The adjacency relation. `Adj x y` means there is an arc from `x` to `y`. -/
-  Adj : α → α → Prop
   /-- No vertex is adjacent to itself. -/
   loopless : Std.Irrefl Adj := by grind
-  /-- Both endpoints of every adjacent pair are vertices. -/
+  /-- Both ends of every adjacent pair are vertices. Unlike `SimpleGraph`, `Adj` is not
+  symmetric, so neither direction follows from the other. -/
   incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
 
-/-- The edge set of a `SimpleDiGraph`, as ordered pairs of adjacent vertices. -/
-def SimpleDiGraph.edgeSet {α} (G : SimpleDiGraph α) : Set (α × α) :=
-  { (x,y) | G.Adj x y}
+/-- The arc set of a `SimpleDigraph`, as ordered pairs of adjacent vertices. -/
+def SimpleDigraph.arcSet (G : SimpleDigraph α) : Set (α × α) :=
+  {p | G.Adj p.1 p.2}
 
 
 end Cslib.Algorithms.Lean

From aeaa1865f3dd8b7b0b8073b9dea59a4d5cd176bb Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Mon, 17 Aug 2026 13:21:33 +0200
Subject: [PATCH 18/36] update

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index b8a06a6fe..152138421 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -81,7 +81,7 @@ structure Digraph (α β : Type*) where
   IsArc : β → α → α → Prop
   /-- Both ends of every arc are vertices. `IsArc` is not symmetric, so neither direction
   follows from the other. -/
-  incidence  : ∀ ⦃e x y⦄, IsArc e x y → (x ∈ vertexSet ∧ y ∈ vertexSet)
+  incidence  : ∀ ⦃e x y⦄, IsArc e x y → (x ∈ vertexSet ∧ y ∈ vertexSet) := by grind
   /-- The ends of the arc labelled `e`, or `none` if `e` is not an arc of the graph. -/
   endpoints : β → Option (α × α)
   /-- `endpoints` computes `IsArc`. This forces `endpoints e = none` for every
@@ -117,7 +117,7 @@ structure SimpleDigraph (α : Type*) extends _root_.Digraph α where
   /-- The set of vertices. -/
   vertexSet : Set α
   /-- No vertex is adjacent to itself. -/
-  loopless : Std.Irrefl Adj := by grind
+  loopless : Std.Irrefl Adj
   /-- Both ends of every adjacent pair are vertices. Unlike `SimpleGraph`, `Adj` is not
   symmetric, so neither direction follows from the other. -/
   incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind

From 7dde507891087e52817380d6a0de436f77788717 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Mon, 17 Aug 2026 14:30:40 +0200
Subject: [PATCH 19/36] update

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 152138421..02479741c 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -23,17 +23,22 @@ Vertex and edge sets are `Set`-valued, following the design of
 
 Four structures are provided, in two pairs. `Graph` and `Digraph` are multigraphs whose
 edges carry labels in `β`, so parallel edges and loops are permitted. `SimpleGraph` and
-`SimpleDigraph` have `Prop`-valued adjacency and therefore admit neither loops nor
-parallel edges.
+`SimpleDigraph` have `Prop`-valued adjacency and therefore disallowing parallel edges.
 
 ## Main definitions
 
+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.
+In particular, f is a computable function. We reuse the definitions from Mathlib as much as we can.
+
 * `Graph α β`: an undirected multigraph, extending Mathlib's `Graph α β`.
 * `Digraph α β`: a directed multigraph; the directed counterpart of Mathlib's `Graph α β`.
 * `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 α`.
 
+
 ## Main API
 
 * `Graph.endpoints`, `Digraph.endpoints`: the ends of an edge or arc.

From de3f7ba37771ab75a3dd73f212960f38c2673fea Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Mon, 17 Aug 2026 14:47:07 +0200
Subject: [PATCH 20/36] fix_ci

---
 Cslib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib.lean b/Cslib.lean
index d74457919..ecc19a433 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,5 +1,6 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import Cslib.Algorithms.Lean.Graph.Basic
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor

From 8fcdb1d32f438032b0e59e37cc9243fd09935c46 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Mon, 17 Aug 2026 14:56:31 +0200
Subject: [PATCH 21/36] docstring

---
 Cslib.lean                             | 2 +-
 Cslib/Algorithms/Lean/Graph/Basic.lean | 5 ++---
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/Cslib.lean b/Cslib.lean
index cf01d4d40..85cc74f91 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,7 +1,7 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
-public import Cslib.Algorithms.Lean.Graph.Basic
 public import Cslib.Algorithms.CCS.VendingMachine
+public import Cslib.Algorithms.Lean.Graph.Basic
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor
diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 02479741c..3f6a60229 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -11,9 +11,6 @@ public import Mathlib.Combinatorics.Digraph.Basic
 public import Mathlib.Combinatorics.Graph.Basic
 public import Mathlib.Combinatorics.SimpleGraph.Basic
 
-
-@[expose] public section
-
 /-!
 # Graph structures
 
@@ -56,6 +53,8 @@ with `endpoints_spec`. That specification pins the value of `endpoints` at *ever
 
 -/
 
+@[expose] public section
+
 namespace Cslib.Algorithms.Lean
 
 

From fe8b5da17650280c08c5ad715397f7a0049454f5 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Mon, 17 Aug 2026 16:05:58 +0200
Subject: [PATCH 22/36] typeclass HasEndpoints

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 55 +++++++++++++++++++-------
 1 file changed, 41 insertions(+), 14 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 3f6a60229..35787107c 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -29,7 +29,7 @@ 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.
 In particular, f is a computable function. We reuse the definitions from Mathlib as much as we can.
 
-* `Graph α β`: an undirected multigraph, extending Mathlib's `Graph α β`.
+* `Graph α β`: an undirected multigraph (abbrev for Mathlib's `Graph α β`).
 * `Digraph α β`: a directed multigraph; the directed counterpart of Mathlib's `Graph α β`.
 * `SimpleGraph α`: a simple graph with a vertex set, extending Mathlib's `SimpleGraph α`.
 * `SimpleDigraph α`: a loopless directed graph with adjacency `Adj : α → α → Prop` and a
@@ -62,15 +62,23 @@ namespace Cslib.Algorithms.Lean
 computable map from an edge label to its ends.
 
 This is Mathlib's `Graph α β` — so parallel edges and loops are permitted, and both the
-vertex and edge sets may be infinite — together with the `endpoints` field. That field is
-uniquely determined by `toGraph`, so it carries no mathematical content; it exists so that
-incidence can be evaluated rather than only reasoned about. -/
-structure Graph (α β : Type*) extends _root_.Graph α β where
-  /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of the graph. -/
+vertex and edge sets may be infinite. -/
+abbrev Graph (α β : Type*) :=  _root_.Graph α β
+
+/-- A computable map from an edge label of `G` to its ends. -/
+class Graph.HasEndpoints {α β : Type*} (G : Graph α β) where
+  /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
   endpoints : β → Option (Sym2 α)
-  /-- `endpoints` computes `Graph.IsLink`. This forces `endpoints e = none` for every
-  `e ∉ edgeSet`, since every `s : Sym2 α` is of the form `s(x, y)`. -/
-  endpoints_spec : ∀ e x y, toGraph.IsLink e x y ↔ endpoints e = some s(x, y)
+  /-- `endpoints` computes `Graph.IsLink`. -/
+  endpoints_spec : ∀ e x y, G.IsLink e x y ↔ endpoints e = some s(x, y)
+
+/-- The ends of `e` in `G`, or `none` if `e ∉ E(G)`. -/
+def Graph.endpoints? (G : Graph α β) [inst : G.HasEndpoints] (e : β) : Option (Sym2 α) :=
+  inst.endpoints e
+
+theorem isLink_iff_endpoints (G : Graph α β) [G.HasEndpoints] :
+  G.IsLink e x y ↔ G.endpoints? e = some s(x, y) :=
+  Graph.HasEndpoints.endpoints_spec e x y
 
 /-- A directed multigraph on vertex type `α` with arc labels in `β`, bundled with a
 computable map from an arc label to its endpoints.
@@ -83,19 +91,38 @@ structure Digraph (α β : Type*) where
   /-- The incidence predicate: `IsArc e x y` states that the arc labelled `e` runs from
   `x` to `y`. -/
   IsArc : β → α → α → Prop
+  /-- An arc is mapped at most once. -/
+  eq_or_eq_of_isArc_of_isArc ⦃e : β⦄ ⦃x y v w : α⦄ : IsArc e x y → IsArc e v w → x = v ∧ y = w
   /-- Both ends of every arc are vertices. `IsArc` is not symmetric, so neither direction
   follows from the other. -/
   incidence  : ∀ ⦃e x y⦄, IsArc e x y → (x ∈ vertexSet ∧ y ∈ vertexSet) := by grind
-  /-- The ends of the arc labelled `e`, or `none` if `e` is not an arc of the graph. -/
-  endpoints : β → Option (α × α)
-  /-- `endpoints` computes `IsArc`. This forces `endpoints e = none` for every
-  `e ∉ arcSet`. -/
-  endpoints_spec : ∀ e x y, IsArc e x y ↔ endpoints e = some (x, y)
   /-- The set of arc labels. -/
   arcSet : Set β := { e | ∃ x y, IsArc e x y}
   /-- A label lies in `arcSet` exactly when it is used by some arc. -/
   arc_mem_iff_exists_isArc (e) : e ∈ arcSet ↔ ∃ x y, IsArc e x y := by exact fun _ ↦ Iff.rfl
 
+/-- A computable map from an edge label of `G` to its ends. -/
+class Digraph.HasEndpoints {α β : Type*} (G : Digraph α β) where
+  /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
+  endpoints : β → Option (α × α)
+  /-- `endpoints` computes `Graph.IsLink`. -/
+  endpoints_spec : ∀ e x y, G.IsArc e x y ↔ endpoints e = some (x, y)
+
+/-- The ends of the arc `e` in `G`, or `none` if `e ∉ G.arcSet`. -/
+def Digraph.endpoints? (G : Digraph α β) [inst : G.HasEndpoints] (e : β) : Option (α × α) :=
+  inst.endpoints e
+
+/-- The tail (source) of `e`. -/
+def tail? (G : Digraph α β) [G.HasEndpoints] (e : β) : Option α :=
+  (G.endpoints? e).map Prod.fst
+
+/-- The head (target) of `e`. -/
+def head? (G : Digraph α β) [G.HasEndpoints] (e : β) : Option α :=
+  (G.endpoints? e).map Prod.snd
+
+theorem isArc_iff_endpoints? (G : Digraph α β) [G.HasEndpoints] :
+  G.IsArc e x y ↔ G.endpoints? e = some (x, y) := Digraph.HasEndpoints.endpoints_spec e x y
+
 /-- A simple graph on `α` — irreflexive and symmetric adjacency, hence no loops and no
 parallel edges — together with a vertex set containing every end of an adjacent pair.
 

From cf9c2631020873ca99dbcec5ae32a876dcf5835e Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 00:19:18 +0200
Subject: [PATCH 23/36] Update to reflect comments

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 104 ++++++++++---------------
 1 file changed, 40 insertions(+), 64 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 35787107c..1a222a1b7 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -15,11 +15,11 @@ public import Mathlib.Combinatorics.SimpleGraph.Basic
 # Graph structures
 
 Vertex and edge sets are `Set`-valued, following the design of
-`Mathlib.Combinatorics.Graph`: a subgraph of `G : Graph α β` is another term of
-`Graph α β` rather than a separate type, so no coercion maps are needed.
+`Mathlib.Combinatorics.Graph`: a subgraph of `G : Graph V E` is another term of
+`Graph V E` rather than a separate type, so no coercion maps are needed.
 
 Four structures are provided, in two pairs. `Graph` and `Digraph` are multigraphs whose
-edges carry labels in `β`, so parallel edges and loops are permitted. `SimpleGraph` and
+edges carry labels in `E`, so parallel edges and loops are permitted. `SimpleGraph` and
 `SimpleDigraph` have `Prop`-valued adjacency and therefore disallowing parallel edges.
 
 ## Main definitions
@@ -29,12 +29,11 @@ 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.
 In particular, f is a computable function. We reuse the definitions from Mathlib as much as we can.
 
-* `Graph α β`: an undirected multigraph (abbrev for Mathlib's `Graph α β`).
-* `Digraph α β`: a directed multigraph; the directed counterpart of Mathlib's `Graph α β`.
-* `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 α`.
-
+* `MultiGraph V E`: an undirected multigraph (abbrev for Mathlib's `Graph V E`).
+* `MultiDigraph V E`: a directed multigraph; the directed counterpart of Mathlib's `Graph V E`.
+* `SimpleGraph V`: a simple graph with a vertex set, extending Mathlib's `SimpleGraph V`.
+* `SimpleDigraph V`: a loopless directed graph with adjacency `Adj : V → V → Prop` and a
+  vertex set, extending Mathlib's `Digraph V`.
 
 ## Main API
 
@@ -46,107 +45,84 @@ In particular, f is a computable function. We reuse the definitions from Mathlib
 ## Implementation notes
 
 `IsLink` and `IsArc` are `Prop`-valued, so nothing about them is executable. To recover
-computation, `Graph` and `Digraph` each carry an `endpoints : β → Option _` field together
+computation, `Graph` and `Digraph` each carry an `endpoints : E → Option _` field together
 with `endpoints_spec`. That specification pins the value of `endpoints` at *every* label —
-`some` on the edge set, and `none` off it, since every `s : Sym2 α` is of the form
+`some` on the edge set, and `none` off it, since every `s : Sym2 V` is of the form
 `s(x, y)`.
-
 -/
 
 @[expose] public section
 
 namespace Cslib.Algorithms.Lean
 
+/-- An undirected multigraph on vertex type `V` with edge labels in `E`.
 
-/-- An undirected multigraph on vertex type `α` with edge labels in `β`, bundled with a
-computable map from an edge label to its ends.
-
-This is Mathlib's `Graph α β` — so parallel edges and loops are permitted, and both the
+This is Mathlib's `Graph V E` — so parallel edges and loops are permitted, and both the
 vertex and edge sets may be infinite. -/
-abbrev Graph (α β : Type*) :=  _root_.Graph α β
+abbrev MultiGraph (V E : Type*) :=  _root_.Graph V E
 
 /-- A computable map from an edge label of `G` to its ends. -/
-class Graph.HasEndpoints {α β : Type*} (G : Graph α β) where
+class MultiGraph.HasEndpoints {V E : Type*} (G : MultiGraph V E) where
   /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
-  endpoints : β → Option (Sym2 α)
+  endpoints : E → Option (Sym2 V)
   /-- `endpoints` computes `Graph.IsLink`. -/
-  endpoints_spec : ∀ e x y, G.IsLink e x y ↔ endpoints e = some s(x, y)
+  endpoints_spec : ∀ e x y, G.IsLink e x y ↔ s(x, y) ∈ endpoints e
 
 /-- The ends of `e` in `G`, or `none` if `e ∉ E(G)`. -/
-def Graph.endpoints? (G : Graph α β) [inst : G.HasEndpoints] (e : β) : Option (Sym2 α) :=
+def MultiGraph.endpoints? (G : MultiGraph V E) [inst : G.HasEndpoints] (e : E) : Option (Sym2 V) :=
   inst.endpoints e
 
-theorem isLink_iff_endpoints (G : Graph α β) [G.HasEndpoints] :
-  G.IsLink e x y ↔ G.endpoints? e = some s(x, y) :=
-  Graph.HasEndpoints.endpoints_spec e x y
+theorem isLink_iff_endpoints (G : MultiGraph V E) [G.HasEndpoints] :
+  G.IsLink e x y ↔ s(x, y) ∈ G.endpoints? e :=
+  MultiGraph.HasEndpoints.endpoints_spec e x y
 
-/-- A directed multigraph on vertex type `α` with arc labels in `β`, bundled with a
+/-- A directed multigraph on vertex type `V` with arc labels in `E`, bundled with a
 computable map from an arc label to its endpoints.
 
-The directed counterpart of Mathlib's `Graph α β`, which has no Mathlib counterpart to
+The directed counterpart of Mathlib's `Graph V E`, which has no Mathlib counterpart to
 extend; the field layout mirrors it, with symmetry dropped. -/
-structure Digraph (α β : Type*) where
+structure MultiDigraph (V E : Type*) where
   /-- The set of vertices. -/
-  vertexSet : Set α
+  vertexSet : Set V
   /-- The incidence predicate: `IsArc e x y` states that the arc labelled `e` runs from
   `x` to `y`. -/
-  IsArc : β → α → α → Prop
-  /-- An arc is mapped at most once. -/
-  eq_or_eq_of_isArc_of_isArc ⦃e : β⦄ ⦃x y v w : α⦄ : IsArc e x y → IsArc e v w → x = v ∧ y = w
+  IsArc : E → V → V → Prop
+  /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
+  endpoints : E → Option (V × V)
+  /-- `endpoints` computes `Graph.IsLink`. -/
+  endpoints_spec : ∀ e x y, IsArc e x y ↔ (x, y) ∈ endpoints e
   /-- Both ends of every arc are vertices. `IsArc` is not symmetric, so neither direction
   follows from the other. -/
   incidence  : ∀ ⦃e x y⦄, IsArc e x y → (x ∈ vertexSet ∧ y ∈ vertexSet) := by grind
   /-- The set of arc labels. -/
-  arcSet : Set β := { e | ∃ x y, IsArc e x y}
+  arcSet : Set E := { e | ∃ x y, IsArc e x y}
   /-- A label lies in `arcSet` exactly when it is used by some arc. -/
   arc_mem_iff_exists_isArc (e) : e ∈ arcSet ↔ ∃ x y, IsArc e x y := by exact fun _ ↦ Iff.rfl
 
-/-- A computable map from an edge label of `G` to its ends. -/
-class Digraph.HasEndpoints {α β : Type*} (G : Digraph α β) where
-  /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
-  endpoints : β → Option (α × α)
-  /-- `endpoints` computes `Graph.IsLink`. -/
-  endpoints_spec : ∀ e x y, G.IsArc e x y ↔ endpoints e = some (x, y)
-
-/-- The ends of the arc `e` in `G`, or `none` if `e ∉ G.arcSet`. -/
-def Digraph.endpoints? (G : Digraph α β) [inst : G.HasEndpoints] (e : β) : Option (α × α) :=
-  inst.endpoints e
-
-/-- The tail (source) of `e`. -/
-def tail? (G : Digraph α β) [G.HasEndpoints] (e : β) : Option α :=
-  (G.endpoints? e).map Prod.fst
-
-/-- The head (target) of `e`. -/
-def head? (G : Digraph α β) [G.HasEndpoints] (e : β) : Option α :=
-  (G.endpoints? e).map Prod.snd
-
-theorem isArc_iff_endpoints? (G : Digraph α β) [G.HasEndpoints] :
-  G.IsArc e x y ↔ G.endpoints? e = some (x, y) := Digraph.HasEndpoints.endpoints_spec e x y
-
-/-- A simple graph on `α` — irreflexive and symmetric adjacency, hence no loops and no
+/-- A simple graph on `V` — irreflexive and symmetric adjacency, hence no loops and no
 parallel edges — together with a vertex set containing every end of an adjacent pair.
 
-Extends Mathlib's `SimpleGraph α`, so its API is available through `toSimpleGraph`; in
+Extends Mathlib's `SimpleGraph V`, so its API is available through `toSimpleGraph`; in
 particular `edgeSet`, the unordered pairs of adjacent vertices, is inherited rather than
-redefined. Note that `Adj` is a relation on all of `α`, so `vertexSet` may be any superset
+redefined. Note that `Adj` is a relation on all of `V`, so `vertexSet` may be any superset
 of the vertices actually incident to an edge. -/
-structure SimpleGraph (α : Type*) extends _root_.SimpleGraph α where
+structure SimpleGraph (V : Type*) extends _root_.SimpleGraph V where
   /-- The set of vertices. -/
-  vertexSet : Set α
+  vertexSet : Set V
   /-- The left end of every adjacent pair is a vertex. The right end then follows by
   symmetry of `Adj`. -/
   left_incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
 
-/-- A simple directed graph on `α` — adjacency `Adj : α → α → Prop`, hence no parallel
+/-- A simple directed graph on `V` — adjacency `Adj : V → V → Prop`, hence no parallel
 arcs — with loops explicitly excluded, together with a vertex set containing every end of
 an adjacent pair.
 
-Extends Mathlib's `Digraph α`, which is a bare adjacency relation and does permit loops;
+Extends Mathlib's `Digraph V`, which is a bare adjacency relation and does permit loops;
 `loopless` is what rules them out here. Antiparallel arcs are permitted: `Adj x y` and
 `Adj y x` may both hold. -/
-structure SimpleDigraph (α : Type*) extends _root_.Digraph α where
+structure SimpleDigraph (V : Type*) extends _root_.Digraph V where
   /-- The set of vertices. -/
-  vertexSet : Set α
+  vertexSet : Set V
   /-- No vertex is adjacent to itself. -/
   loopless : Std.Irrefl Adj
   /-- Both ends of every adjacent pair are vertices. Unlike `SimpleGraph`, `Adj` is not
@@ -154,7 +130,7 @@ structure SimpleDigraph (α : Type*) extends _root_.Digraph α where
   incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
 
 /-- The arc set of a `SimpleDigraph`, as ordered pairs of adjacent vertices. -/
-def SimpleDigraph.arcSet (G : SimpleDigraph α) : Set (α × α) :=
+def SimpleDigraph.arcSet (G : SimpleDigraph V) : Set (V × V) :=
   {p | G.Adj p.1 p.2}
 
 

From 7ad844889dfd9b2b402b46505e4f14ad0b8d961a Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 09:00:12 +0200
Subject: [PATCH 24/36] Update Cslib/Algorithms/Lean/Graph/Basic.lean

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 1a222a1b7..3d5433c06 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -93,7 +93,7 @@ structure MultiDigraph (V E : Type*) where
   endpoints_spec : ∀ e x y, IsArc e x y ↔ (x, y) ∈ endpoints e
   /-- Both ends of every arc are vertices. `IsArc` is not symmetric, so neither direction
   follows from the other. -/
-  incidence  : ∀ ⦃e x y⦄, IsArc e x y → (x ∈ vertexSet ∧ y ∈ vertexSet) := by grind
+  incidence : ∀ ⦃e x y⦄, IsArc e x y → (x ∈ vertexSet ∧ y ∈ vertexSet) := by grind
   /-- The set of arc labels. -/
   arcSet : Set E := { e | ∃ x y, IsArc e x y}
   /-- A label lies in `arcSet` exactly when it is used by some arc. -/

From 11d9fd57042b796e38250699f1e56105dd3efe3b Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 09:00:27 +0200
Subject: [PATCH 25/36] Update Cslib/Algorithms/Lean/Graph/Basic.lean

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 3d5433c06..173c07fa0 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -129,8 +129,8 @@ structure SimpleDigraph (V : Type*) extends _root_.Digraph V where
   symmetric, so neither direction follows from the other. -/
   incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
 
-/-- The arc set of a `SimpleDigraph`, as ordered pairs of adjacent vertices. -/
-def SimpleDigraph.arcSet (G : SimpleDigraph V) : Set (V × V) :=
+/-- The edge set of a `SimpleDigraph`, as ordered pairs of adjacent vertices. -/
+def SimpleDigraph.edgeSet (G : SimpleDigraph V) : Set (V × V) :=
   {p | G.Adj p.1 p.2}
 
 

From 75b99fce104f850df8e4eaa2fb0bb5d4feeebc0c Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 09:00:35 +0200
Subject: [PATCH 26/36] Update Cslib/Algorithms/Lean/Graph/Basic.lean

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 173c07fa0..71893870b 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -124,7 +124,7 @@ structure SimpleDigraph (V : Type*) extends _root_.Digraph V where
   /-- The set of vertices. -/
   vertexSet : Set V
   /-- No vertex is adjacent to itself. -/
-  loopless : Std.Irrefl Adj
+  irrefl_adj : Std.Irrefl Adj
   /-- Both ends of every adjacent pair are vertices. Unlike `SimpleGraph`, `Adj` is not
   symmetric, so neither direction follows from the other. -/
   incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind

From 2a6097f0f4362ad75a1e955a7d42c660a683b910 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 09:00:43 +0200
Subject: [PATCH 27/36] Update Cslib/Algorithms/Lean/Graph/Basic.lean

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 71893870b..73e9d4056 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -111,7 +111,7 @@ structure SimpleGraph (V : Type*) extends _root_.SimpleGraph V where
   vertexSet : Set V
   /-- The left end of every adjacent pair is a vertex. The right end then follows by
   symmetry of `Adj`. -/
-  left_incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
+  adj_imp_left_mem_vertexSet : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
 
 /-- A simple directed graph on `V` — adjacency `Adj : V → V → Prop`, hence no parallel
 arcs — with loops explicitly excluded, together with a vertex set containing every end of

From 68df648fdeefae0eafa39789c32087c7b8d00993 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 09:00:51 +0200
Subject: [PATCH 28/36] Update Cslib/Algorithms/Lean/Graph/Basic.lean

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 73e9d4056..cd1a48ef5 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -94,8 +94,8 @@ structure MultiDigraph (V E : Type*) where
   /-- Both ends of every arc are vertices. `IsArc` is not symmetric, so neither direction
   follows from the other. -/
   incidence : ∀ ⦃e x y⦄, IsArc e x y → (x ∈ vertexSet ∧ y ∈ vertexSet) := by grind
-  /-- The set of arc labels. -/
-  arcSet : Set E := { e | ∃ x y, IsArc e x y}
+  /-- The set of edge labels. -/
+  edgeSet : Set E := { e | ∃ x y, IsArc e x y}
   /-- A label lies in `arcSet` exactly when it is used by some arc. -/
   arc_mem_iff_exists_isArc (e) : e ∈ arcSet ↔ ∃ x y, IsArc e x y := by exact fun _ ↦ Iff.rfl
 

From 357b02174e63ea8e6216839cda2f69fe080b7faf Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 09:01:03 +0200
Subject: [PATCH 29/36] Update Cslib/Algorithms/Lean/Graph/Basic.lean

Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index cd1a48ef5..4c4d80ff8 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -127,7 +127,8 @@ structure SimpleDigraph (V : Type*) extends _root_.Digraph V where
   irrefl_adj : Std.Irrefl Adj
   /-- Both ends of every adjacent pair are vertices. Unlike `SimpleGraph`, `Adj` is not
   symmetric, so neither direction follows from the other. -/
-  incidence : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet ∧ y ∈ vertexSet := by grind
+  adj_imp_left_mem_vertexSet : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
+  adj_imp_right_mem_vertexSet : ∀ ⦃x y⦄, Adj x y → y ∈ vertexSet := by grind
 
 /-- The edge set of a `SimpleDigraph`, as ordered pairs of adjacent vertices. -/
 def SimpleDigraph.edgeSet (G : SimpleDigraph V) : Set (V × V) :=

From 59f944613419b78f8bbe02bbe5288bec9774a29c Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 09:10:30 +0200
Subject: [PATCH 30/36] update to reflect comments

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 4c4d80ff8..e75554bbc 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -10,6 +10,8 @@ public import Cslib.Foundations.Semantics.LTS.Basic
 public import Mathlib.Combinatorics.Digraph.Basic
 public import Mathlib.Combinatorics.Graph.Basic
 public import Mathlib.Combinatorics.SimpleGraph.Basic
+public import Mathlib.Data.PFun
+
 
 /-!
 # Graph structures
@@ -61,19 +63,19 @@ This is Mathlib's `Graph V E` — so parallel edges and loops are permitted, and
 vertex and edge sets may be infinite. -/
 abbrev MultiGraph (V E : Type*) :=  _root_.Graph V E
 
-/-- A computable map from an edge label of `G` to its ends. -/
+/-- A map from an edge label of `G` to its ends. -/
 class MultiGraph.HasEndpoints {V E : Type*} (G : MultiGraph V E) where
   /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
-  endpoints : E → Option (Sym2 V)
+  endpoints : E →. (Sym2 V)
   /-- `endpoints` computes `Graph.IsLink`. -/
   endpoints_spec : ∀ e x y, G.IsLink e x y ↔ s(x, y) ∈ endpoints e
 
-/-- The ends of `e` in `G`, or `none` if `e ∉ E(G)`. -/
-def MultiGraph.endpoints? (G : MultiGraph V E) [inst : G.HasEndpoints] (e : E) : Option (Sym2 V) :=
-  inst.endpoints e
+/-- The ends of `e` in `G`; undefined when `e ∉ E(G)`. -/
+def MultiGraph.endpoints (G : MultiGraph α β) [inst : G.HasEndpoints] : β →. Sym2 α :=
+  inst.endpoints
 
 theorem isLink_iff_endpoints (G : MultiGraph V E) [G.HasEndpoints] :
-  G.IsLink e x y ↔ s(x, y) ∈ G.endpoints? e :=
+  G.IsLink e x y ↔ s(x, y) ∈ G.endpoints e :=
   MultiGraph.HasEndpoints.endpoints_spec e x y
 
 /-- A directed multigraph on vertex type `V` with arc labels in `E`, bundled with a
@@ -86,18 +88,18 @@ structure MultiDigraph (V E : Type*) where
   vertexSet : Set V
   /-- The incidence predicate: `IsArc e x y` states that the arc labelled `e` runs from
   `x` to `y`. -/
-  IsArc : E → V → V → Prop
+  IsLink : E → V → V → Prop
   /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
   endpoints : E → Option (V × V)
   /-- `endpoints` computes `Graph.IsLink`. -/
-  endpoints_spec : ∀ e x y, IsArc e x y ↔ (x, y) ∈ endpoints e
+  endpoints_spec : ∀ e x y, IsLink e x y ↔ (x, y) ∈ endpoints e
   /-- Both ends of every arc are vertices. `IsArc` is not symmetric, so neither direction
   follows from the other. -/
-  incidence : ∀ ⦃e x y⦄, IsArc e x y → (x ∈ vertexSet ∧ y ∈ vertexSet) := by grind
+  incidence : ∀ ⦃e x y⦄, IsLink e x y → (x ∈ vertexSet ∧ y ∈ vertexSet) := by grind
   /-- The set of edge labels. -/
-  edgeSet : Set E := { e | ∃ x y, IsArc e x y}
-  /-- A label lies in `arcSet` exactly when it is used by some arc. -/
-  arc_mem_iff_exists_isArc (e) : e ∈ arcSet ↔ ∃ x y, IsArc e x y := by exact fun _ ↦ Iff.rfl
+  edgeSet : Set E := { e | ∃ x y, IsLink e x y}
+  /-- A label lies in `edgeSet` exactly when it is used by some arc. -/
+  arc_mem_iff_exists_isArc (e) : e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl
 
 /-- A simple graph on `V` — irreflexive and symmetric adjacency, hence no loops and no
 parallel edges — together with a vertex set containing every end of an adjacent pair.

From fc3ad94016d146cdb51e16ed23f73a30d30f765f Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 09:14:15 +0200
Subject: [PATCH 31/36] add partial function

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index e75554bbc..454df8130 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -46,7 +46,7 @@ In particular, f is a computable function. We reuse the definitions from Mathlib
 
 ## Implementation notes
 
-`IsLink` and `IsArc` are `Prop`-valued, so nothing about them is executable. To recover
+`IsLink` and `IsLink` are `Prop`-valued, so nothing about them is executable. To recover
 computation, `Graph` and `Digraph` each carry an `endpoints : E → Option _` field together
 with `endpoints_spec`. That specification pins the value of `endpoints` at *every* label —
 `some` on the edge set, and `none` off it, since every `s : Sym2 V` is of the form
@@ -86,20 +86,21 @@ extend; the field layout mirrors it, with symmetry dropped. -/
 structure MultiDigraph (V E : Type*) where
   /-- The set of vertices. -/
   vertexSet : Set V
-  /-- The incidence predicate: `IsArc e x y` states that the arc labelled `e` runs from
+  /-- The incidence predicate: `IsLink e x y` states that the arc labelled `e` runs from
   `x` to `y`. -/
   IsLink : E → V → V → Prop
   /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
-  endpoints : E → Option (V × V)
+  endpoints : E →. (V × V)
   /-- `endpoints` computes `Graph.IsLink`. -/
   endpoints_spec : ∀ e x y, IsLink e x y ↔ (x, y) ∈ endpoints e
-  /-- Both ends of every arc are vertices. `IsArc` is not symmetric, so neither direction
+  /-- Both ends of every arc are vertices. `IsLink` is not symmetric, so neither direction
   follows from the other. -/
-  incidence : ∀ ⦃e x y⦄, IsLink e x y → (x ∈ vertexSet ∧ y ∈ vertexSet) := by grind
+  isLink_imp_left_mem_vertexSet : ∀ ⦃e x y⦄, IsLink e x y → x ∈ vertexSet := by grind
+  isLink_imp_right_mem_vertexSet : ∀ ⦃e x y⦄, IsLink e x y → y ∈ vertexSet := by grind
   /-- The set of edge labels. -/
   edgeSet : Set E := { e | ∃ x y, IsLink e x y}
   /-- A label lies in `edgeSet` exactly when it is used by some arc. -/
-  arc_mem_iff_exists_isArc (e) : e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl
+  arc_mem_iff_exists_IsLink (e) : e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl
 
 /-- A simple graph on `V` — irreflexive and symmetric adjacency, hence no loops and no
 parallel edges — together with a vertex set containing every end of an adjacent pair.

From e5fb4569ee554b14e3a137dab2f951a69b30c7d3 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 17:59:34 +0200
Subject: [PATCH 32/36] replace arc with edge

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 454df8130..66b9bc1a3 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -39,8 +39,8 @@ In particular, f is a computable function. We reuse the definitions from Mathlib
 
 ## Main API
 
-* `Graph.endpoints`, `Digraph.endpoints`: the ends of an edge or arc.
-* `SimpleDigraph.arcSet`: the arc set of a `SimpleDigraph`, derived from its adjacency
+* `Graph.endpoints`, `Digraph.endpoints`: the ends of an edge.
+* `SimpleDigraph.edgeSet`: the edge set of a `SimpleDigraph`, derived from its adjacency
   relation. The corresponding `SimpleGraph.edgeSet` is inherited from Mathlib rather than
   redefined here.
 
@@ -78,29 +78,29 @@ theorem isLink_iff_endpoints (G : MultiGraph V E) [G.HasEndpoints] :
   G.IsLink e x y ↔ s(x, y) ∈ G.endpoints e :=
   MultiGraph.HasEndpoints.endpoints_spec e x y
 
-/-- A directed multigraph on vertex type `V` with arc labels in `E`, bundled with a
-computable map from an arc label to its endpoints.
+/-- A directed multigraph on vertex type `V` with edge labels in `E`, bundled with a
+computable map from an edge label to its endpoints.
 
 The directed counterpart of Mathlib's `Graph V E`, which has no Mathlib counterpart to
 extend; the field layout mirrors it, with symmetry dropped. -/
 structure MultiDigraph (V E : Type*) where
   /-- The set of vertices. -/
   vertexSet : Set V
-  /-- The incidence predicate: `IsLink e x y` states that the arc labelled `e` runs from
+  /-- The incidence predicate: `IsLink e x y` states that the edge labelled `e` runs from
   `x` to `y`. -/
   IsLink : E → V → V → Prop
   /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
   endpoints : E →. (V × V)
   /-- `endpoints` computes `Graph.IsLink`. -/
   endpoints_spec : ∀ e x y, IsLink e x y ↔ (x, y) ∈ endpoints e
-  /-- Both ends of every arc are vertices. `IsLink` is not symmetric, so neither direction
+  /-- Both ends of every edge are vertices. `IsLink` is not symmetric, so neither direction
   follows from the other. -/
   isLink_imp_left_mem_vertexSet : ∀ ⦃e x y⦄, IsLink e x y → x ∈ vertexSet := by grind
   isLink_imp_right_mem_vertexSet : ∀ ⦃e x y⦄, IsLink e x y → y ∈ vertexSet := by grind
   /-- The set of edge labels. -/
   edgeSet : Set E := { e | ∃ x y, IsLink e x y}
-  /-- A label lies in `edgeSet` exactly when it is used by some arc. -/
-  arc_mem_iff_exists_IsLink (e) : e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl
+  /-- A label lies in `edgeSet` exactly when it is used by some edge. -/
+  edge_mem_iff_exists_IsLink (e) : e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl
 
 /-- A simple graph on `V` — irreflexive and symmetric adjacency, hence no loops and no
 parallel edges — together with a vertex set containing every end of an adjacent pair.
@@ -117,11 +117,11 @@ structure SimpleGraph (V : Type*) extends _root_.SimpleGraph V where
   adj_imp_left_mem_vertexSet : ∀ ⦃x y⦄, Adj x y → x ∈ vertexSet := by grind
 
 /-- A simple directed graph on `V` — adjacency `Adj : V → V → Prop`, hence no parallel
-arcs — with loops explicitly excluded, together with a vertex set containing every end of
+edges — with loops explicitly excluded, together with a vertex set containing every end of
 an adjacent pair.
 
 Extends Mathlib's `Digraph V`, which is a bare adjacency relation and does permit loops;
-`loopless` is what rules them out here. Antiparallel arcs are permitted: `Adj x y` and
+`loopless` is what rules them out here. Antiparallel edges are permitted: `Adj x y` and
 `Adj y x` may both hold. -/
 structure SimpleDigraph (V : Type*) extends _root_.Digraph V where
   /-- The set of vertices. -/

From 0500dd4bff0228327f844f62ee80ea4c399138af Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 18:11:17 +0200
Subject: [PATCH 33/36] Change Graph to MultiGraph

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 66b9bc1a3..818a7077f 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -20,7 +20,7 @@ Vertex and edge sets are `Set`-valued, following the design of
 `Mathlib.Combinatorics.Graph`: a subgraph of `G : Graph V E` is another term of
 `Graph V E` rather than a separate type, so no coercion maps are needed.
 
-Four structures are provided, in two pairs. `Graph` and `Digraph` are multigraphs whose
+Four structures are provided, in two pairs. `MultiGraph` and `MultiDigraph` are multigraphs whose
 edges carry labels in `E`, so parallel edges and loops are permitted. `SimpleGraph` and
 `SimpleDigraph` have `Prop`-valued adjacency and therefore disallowing parallel edges.
 
@@ -39,18 +39,18 @@ In particular, f is a computable function. We reuse the definitions from Mathlib
 
 ## Main API
 
-* `Graph.endpoints`, `Digraph.endpoints`: the ends of an edge.
+* `MultiGraph.endpoints`, `MultiDigraph.endpoints`: the ends of an edge.
 * `SimpleDigraph.edgeSet`: the edge set of a `SimpleDigraph`, derived from its adjacency
   relation. The corresponding `SimpleGraph.edgeSet` is inherited from Mathlib rather than
   redefined here.
 
 ## Implementation notes
 
-`IsLink` and `IsLink` are `Prop`-valued, so nothing about them is executable. To recover
-computation, `Graph` and `Digraph` each carry an `endpoints : E → Option _` field together
+`IsLink` are `Prop`-valued, so nothing about them is executable. To recover
+computation, `MultiGraph` and `Digraph` each carry an `endpoints : E →. _` field together
 with `endpoints_spec`. That specification pins the value of `endpoints` at *every* label —
-`some` on the edge set, and `none` off it, since every `s : Sym2 V` is of the form
-`s(x, y)`.
+`some` on the edge set, and `none` otherwise.
+
 -/
 
 @[expose] public section
@@ -91,7 +91,7 @@ structure MultiDigraph (V E : Type*) where
   IsLink : E → V → V → Prop
   /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
   endpoints : E →. (V × V)
-  /-- `endpoints` computes `Graph.IsLink`. -/
+  /-- `endpoints` computes `IsLink`. -/
   endpoints_spec : ∀ e x y, IsLink e x y ↔ (x, y) ∈ endpoints e
   /-- Both ends of every edge are vertices. `IsLink` is not symmetric, so neither direction
   follows from the other. -/

From ee137b4e5c3eba9e9e794810ef1145def2a16a3f Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 21:52:55 +0200
Subject: [PATCH 34/36] Remove redundant fields of MultiDiGraph

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 62 ++++++++++++++++----------
 1 file changed, 38 insertions(+), 24 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 818a7077f..230c25248 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -71,44 +71,59 @@ class MultiGraph.HasEndpoints {V E : Type*} (G : MultiGraph V E) where
   endpoints_spec : ∀ e x y, G.IsLink e x y ↔ s(x, y) ∈ endpoints e
 
 /-- The ends of `e` in `G`; undefined when `e ∉ E(G)`. -/
-def MultiGraph.endpoints (G : MultiGraph α β) [inst : G.HasEndpoints] : β →. Sym2 α :=
+def MultiGraph.endpoints (G : MultiGraph V E) [inst : G.HasEndpoints] : E →. Sym2 V :=
   inst.endpoints
 
 theorem isLink_iff_endpoints (G : MultiGraph V E) [G.HasEndpoints] :
   G.IsLink e x y ↔ s(x, y) ∈ G.endpoints e :=
   MultiGraph.HasEndpoints.endpoints_spec e x y
 
-/-- A directed multigraph on vertex type `V` with edge labels in `E`, bundled with a
-computable map from an edge label to its endpoints.
-
-The directed counterpart of Mathlib's `Graph V E`, which has no Mathlib counterpart to
-extend; the field layout mirrors it, with symmetry dropped. -/
+/-- A directed multigraph on vertex type `V` with edge labels in `E`, given by a partial
+function from an edge label to its ends. -/
 structure MultiDigraph (V E : Type*) where
   /-- The set of vertices. -/
   vertexSet : Set V
-  /-- The incidence predicate: `IsLink e x y` states that the edge labelled `e` runs from
-  `x` to `y`. -/
-  IsLink : E → V → V → Prop
-  /-- The ends of the edge labelled `e`, or `none` if `e` is not an edge of `G`. -/
+  /-- The ends of the edge labelled `e`; undefined when `e` is not an edge of `G`. -/
   endpoints : E →. (V × V)
-  /-- `endpoints` computes `IsLink`. -/
-  endpoints_spec : ∀ e x y, IsLink e x y ↔ (x, y) ∈ endpoints e
-  /-- Both ends of every edge are vertices. `IsLink` is not symmetric, so neither direction
-  follows from the other. -/
-  isLink_imp_left_mem_vertexSet : ∀ ⦃e x y⦄, IsLink e x y → x ∈ vertexSet := by grind
-  isLink_imp_right_mem_vertexSet : ∀ ⦃e x y⦄, IsLink e x y → y ∈ vertexSet := by grind
-  /-- The set of edge labels. -/
-  edgeSet : Set E := { e | ∃ x y, IsLink e x y}
-  /-- A label lies in `edgeSet` exactly when it is used by some edge. -/
-  edge_mem_iff_exists_IsLink (e) : e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl
+  /-- The tail of every edge is a vertex. -/
+  left_mem_of_mem_endpoints ⦃e x y⦄ : (x, y) ∈ endpoints e → x ∈ vertexSet := by grind
+  /-- The head of every edge is a vertex. -/
+  right_mem_of_mem_endpoints ⦃e x y⦄ : (x, y) ∈ endpoints e → y ∈ vertexSet := by grind
+
+namespace MultiDigraph
+variable {V E : Type*} {G : MultiDigraph V E} {e : E} {x y x' y' : V}
+
+/-- The set of edge labels. -/
+def edgeSet (G : MultiDigraph V E) : Set E := G.endpoints.Dom
+
+/-- `IsLink e x y` states that the edge labelled `e` runs from `x` to `y`. -/
+def IsLink (G : MultiDigraph V E) (e : E) (x y : V) : Prop := (x, y) ∈ G.endpoints e
+
+@[simp] lemma isLink_iff : G.IsLink e x y ↔ (x, y) ∈ G.endpoints e := Iff.rfl
+@[simp] lemma mem_edgeSet_iff : e ∈ G.edgeSet ↔ (G.endpoints e).Dom := Iff.rfl
+
+lemma mem_edgeSet_iff_exists_isLink : e ∈ G.edgeSet ↔ ∃ x y, G.IsLink e x y := by
+  rw [mem_edgeSet_iff, Part.dom_iff_mem]
+  exact ⟨fun ⟨p, hp⟩ => ⟨p.1, p.2, hp⟩, fun ⟨_, _, h⟩ => ⟨_, h⟩⟩
+
+lemma IsLink.mem_edgeSet (h : G.IsLink e x y) : e ∈ G.edgeSet :=
+  mem_edgeSet_iff_exists_isLink.2 ⟨x, y, h⟩
+
+/-- An edge is incident with at most one ordered pair of vertices. -/
+lemma eq_and_eq_of_isLink_of_isLink (h : G.IsLink e x y) (h' : G.IsLink e x' y') :
+    x = x' ∧ y = y' :=
+  have hp : (x, y) = (x', y') := Part.mem_unique h h'
+  ⟨congrArg Prod.fst hp, congrArg Prod.snd hp⟩
+
+end MultiDigraph
+
 
 /-- A simple graph on `V` — irreflexive and symmetric adjacency, hence no loops and no
 parallel edges — together with a vertex set containing every end of an adjacent pair.
 
 Extends Mathlib's `SimpleGraph V`, so its API is available through `toSimpleGraph`; in
 particular `edgeSet`, the unordered pairs of adjacent vertices, is inherited rather than
-redefined. Note that `Adj` is a relation on all of `V`, so `vertexSet` may be any superset
-of the vertices actually incident to an edge. -/
+redefined. -/
 structure SimpleGraph (V : Type*) extends _root_.SimpleGraph V where
   /-- The set of vertices. -/
   vertexSet : Set V
@@ -121,8 +136,7 @@ edges — with loops explicitly excluded, together with a vertex set containing
 an adjacent pair.
 
 Extends Mathlib's `Digraph V`, which is a bare adjacency relation and does permit loops;
-`loopless` is what rules them out here. Antiparallel edges are permitted: `Adj x y` and
-`Adj y x` may both hold. -/
+`loopless` is what rules them out here. -/
 structure SimpleDigraph (V : Type*) extends _root_.Digraph V where
   /-- The set of vertices. -/
   vertexSet : Set V

From e00fd44156c9466f2f03ea209c46da5e2ef7879f Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 22:08:29 +0200
Subject: [PATCH 35/36] minor

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 230c25248..10cff8724 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -86,9 +86,9 @@ structure MultiDigraph (V E : Type*) where
   /-- The ends of the edge labelled `e`; undefined when `e` is not an edge of `G`. -/
   endpoints : E →. (V × V)
   /-- The tail of every edge is a vertex. -/
-  left_mem_of_mem_endpoints ⦃e x y⦄ : (x, y) ∈ endpoints e → x ∈ vertexSet := by grind
+  endpoints_left_mem_vertexSet ⦃e x y⦄ : (x, y) ∈ endpoints e → x ∈ vertexSet := by grind
   /-- The head of every edge is a vertex. -/
-  right_mem_of_mem_endpoints ⦃e x y⦄ : (x, y) ∈ endpoints e → y ∈ vertexSet := by grind
+  endpoints_right_mem_vertexSet ⦃e x y⦄ : (x, y) ∈ endpoints e → y ∈ vertexSet := by grind
 
 namespace MultiDigraph
 variable {V E : Type*} {G : MultiDigraph V E} {e : E} {x y x' y' : V}

From f9383816081da344f4b0e277d40b1d9cb3b40281 Mon Sep 17 00:00:00 2001
From: Sorrachai Yingchareonthawornchai <sorrachai.cp@gmail.com>
Date: Tue, 18 Aug 2026 22:47:38 +0200
Subject: [PATCH 36/36] isLink_imp_left_mem_vertexSet

---
 Cslib/Algorithms/Lean/Graph/Basic.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Basic.lean b/Cslib/Algorithms/Lean/Graph/Basic.lean
index 10cff8724..4d9ce0cf1 100644
--- a/Cslib/Algorithms/Lean/Graph/Basic.lean
+++ b/Cslib/Algorithms/Lean/Graph/Basic.lean
@@ -86,9 +86,9 @@ structure MultiDigraph (V E : Type*) where
   /-- The ends of the edge labelled `e`; undefined when `e` is not an edge of `G`. -/
   endpoints : E →. (V × V)
   /-- The tail of every edge is a vertex. -/
-  endpoints_left_mem_vertexSet ⦃e x y⦄ : (x, y) ∈ endpoints e → x ∈ vertexSet := by grind
+  left_endpoint_mem_vertexSet ⦃e x y⦄ : (x, y) ∈ endpoints e → x ∈ vertexSet := by grind
   /-- The head of every edge is a vertex. -/
-  endpoints_right_mem_vertexSet ⦃e x y⦄ : (x, y) ∈ endpoints e → y ∈ vertexSet := by grind
+  right_endpoint_mem_vertexSet ⦃e x y⦄ : (x, y) ∈ endpoints e → y ∈ vertexSet := by grind
 
 namespace MultiDigraph
 variable {V E : Type*} {G : MultiDigraph V E} {e : E} {x y x' y' : V}
@@ -115,6 +115,11 @@ lemma eq_and_eq_of_isLink_of_isLink (h : G.IsLink e x y) (h' : G.IsLink e x' y')
   have hp : (x, y) = (x', y') := Part.mem_unique h h'
   ⟨congrArg Prod.fst hp, congrArg Prod.snd hp⟩
 
+lemma isLink_imp_left_mem_vertexSet : ∀ ⦃e x y⦄, G.IsLink e x y → x ∈ G.vertexSet :=
+  fun _ _ _ a => G.left_endpoint_mem_vertexSet a
+lemma isLink_imp_right_mem_vertexSet : ∀ ⦃e x y⦄, G.IsLink e x y → y ∈ G.vertexSet :=
+  fun _ _ _ a => G.right_endpoint_mem_vertexSet a
+
 end MultiDigraph