From 462d17c79cdb5fe18e3ad2ef189c28bdb851ba05 Mon Sep 17 00:00:00 2001 From: Sorrachai Yingchareonthawornchai Date: Sun, 15 Mar 2026 10:49:38 +0100 Subject: [PATCH 1/5] graph definitions --- .../Lean/Graph/Core/Simple/Undirected.lean | 96 +++++++++++++++++++ 1 file changed, 96 insertions(+) create mode 100644 Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean diff --git a/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean b/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean new file mode 100644 index 000000000..e27b6a6ed --- /dev/null +++ b/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean @@ -0,0 +1,96 @@ +/- +Copyright (c) 2026 Sorrachai Yingchareonthawornhcai. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sorrachai Yingchareonthawornhcai +-/ + +module + +public import Mathlib.Data.Sym.Sym2 + +@[expose] public section + +/-! +# Simple Undirected Graphs +This file defines simple undirected graphs and basic definitions. + +-- +## Main definitions +- `Edge`: A type alias for `Sym2 α`, representing an undirected edge as an + unordered pair. +- `SimpleGraph`: A structure encoding a simple graph with a finite vertex set, + a finite edge set, an incidence condition (every endpoint of every edge is a + vertex), and a looplessness condition (no edge is a diagonal of `Sym2`). +- `IncidentEdgeSet`: The set of all edges in a graph that are incident to a + given vertex. +- `Neighbors`: The set of all vertices adjacent to a given vertex, i.e. the + open neighbourhood of that vertex. +- `subgraphOf`: A relation asserting that one graph is a subgraph of another; + both the vertex set and the edge set of the first are subsets of those of the + second. + +## Implementation notes + +Edges are represented as elements of `Sym2 α` (i.e., `{x, y}` with `x ≠ y` +enforced via the `loopless` field rather than the type). This mirrors the +approach used in Mathlib's combinatorics library. + +The graph definitions in this file intentionally diverge from those in Mathlib; +we prioritise representations that support algorithmic reasoning over those designed for +classical combinatorial arguments. +-/ + +variable {α : Type*} [DecidableEq α] + +/-- An undirected edge, represented as an unordered pair via `Sym2`. -/ +abbrev Edge := Sym2 + +/-- A simple graph on vertex type `α` consists of a finite vertex set, a finite +edge set, and two well-formedness conditions: every edge endpoint is a vertex, +and no edge is a self-loop. -/ +structure SimpleGraph (α : Type*) where + /-- The finite set of vertices of the graph. -/ + vertexSet : Finset α + /-- The finite set of edges of the graph. -/ + edgeSet : Finset (Edge α) + /-- Every endpoint of every edge is a vertex. -/ + incidence : ∀ e ∈ edgeSet, ∀ v ∈ e, v ∈ vertexSet + /-- The graph has no self-loops. -/ + loopless : ∀ e ∈ edgeSet, ¬ e.IsDiag + +open Finset + +namespace SimpleGraphs + +/-- `V(G)` denotes the `vertexSet` of a graph `G`. -/ +scoped notation "V(" G ")" => SimpleGraph.vertexSet G + +/-- `E(G)` denotes the `edgeSet` of a graph `G`. -/ +scoped notation "E(" G ")" => SimpleGraph.edgeSet G + +/-- The set of all edges in a graph that are incident to a given vertex. -/ +abbrev IncidentEdgeSet (G : SimpleGraph α) (s : α) : + Finset (Edge α) := {e ∈ E(G) | s ∈ e} + +/-- `δ(G,v)` denotes the `edge-incident-set` of a vertex `v` in `G`. -/ +scoped notation "δ(" G "," v ")" => SimpleGraph.IncidentEdgeSet G v + +/-- The set of all vertices adjacent to a given vertex, i.e. the + open neighbourhood of that vertex. -/ +abbrev Neighbors (G : SimpleGraph α) (s : α) : + Finset α := {u ∈ V(G) | ∃ e ∈ E(G), s ∈ e ∧ u ∈ e ∧ u ≠ s} + +/-- `N(G,v)` denotes the `neighbors` of a vertex `v` in `G`. -/ +scoped notation "N(" G "," v ")" => SimpleGraph.Neighbors G v + +/-- `deg(G)` denotes the `degree` of a vertex `v` in `G`. -/ +scoped notation "deg(" G "," v ")" => #δ(G,v) + +/-- A graph `H` is a subgraph of `G` if both vertex and edge sets are subsets of those in G -/ +abbrev subgraphOf (H G : SimpleGraph α) : Prop := + V(H) ⊆ V(G) ∧ E(H) ⊆ E(G) + +/-- Notation for the subgraph relation -/ +scoped infix:50 " ⊆ᴳ " => SimpleGraph.subgraphOf + +end SimpleGraphs From d3f567a65fc043ee35a912200310bc3d02c2d2d6 Mon Sep 17 00:00:00 2001 From: Sorrachai Yingchareonthawornchai Date: Sun, 15 Mar 2026 11:04:03 +0100 Subject: [PATCH 2/5] lake exec mk_all --module --- Cslib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Cslib.lean b/Cslib.lean index 4e42a8959..a766c0e5f 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -1,5 +1,6 @@ module -- shake: keep-all +public import Cslib.Algorithms.Lean.Graph.Core.Simple.Undirected public import Cslib.Algorithms.Lean.MergeSort.MergeSort public import Cslib.Algorithms.Lean.TimeM public import Cslib.Computability.Automata.Acceptors.Acceptor From cf2595398717939830b0bc573462a262f15d87db Mon Sep 17 00:00:00 2001 From: Sorrachai Yingchareonthawornchai Date: Sun, 15 Mar 2026 11:11:26 +0100 Subject: [PATCH 3/5] namespace changed --- Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean b/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean index e27b6a6ed..cf0611a24 100644 --- a/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean +++ b/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean @@ -42,6 +42,7 @@ classical combinatorial arguments. variable {α : Type*} [DecidableEq α] + /-- An undirected edge, represented as an unordered pair via `Sym2`. -/ abbrev Edge := Sym2 @@ -60,7 +61,7 @@ structure SimpleGraph (α : Type*) where open Finset -namespace SimpleGraphs +namespace Cslib.Algorithms.Lean.Graph.Core.Simple /-- `V(G)` denotes the `vertexSet` of a graph `G`. -/ scoped notation "V(" G ")" => SimpleGraph.vertexSet G @@ -93,4 +94,4 @@ abbrev subgraphOf (H G : SimpleGraph α) : Prop := /-- Notation for the subgraph relation -/ scoped infix:50 " ⊆ᴳ " => SimpleGraph.subgraphOf -end SimpleGraphs +end Cslib.Algorithms.Lean.Graph.Core.Simple From 39efe0c9c75950866a1fd303356f948a744b9b7f Mon Sep 17 00:00:00 2001 From: Sorrachai Yingchareonthawornchai Date: Sun, 15 Mar 2026 11:12:19 +0100 Subject: [PATCH 4/5] namespace --- Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean b/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean index cf0611a24..fa8eb0892 100644 --- a/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean +++ b/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean @@ -40,6 +40,8 @@ we prioritise representations that support algorithmic reasoning over those desi classical combinatorial arguments. -/ +namespace Cslib.Algorithms.Lean.Graph.Core.Simple + variable {α : Type*} [DecidableEq α] @@ -61,7 +63,6 @@ structure SimpleGraph (α : Type*) where open Finset -namespace Cslib.Algorithms.Lean.Graph.Core.Simple /-- `V(G)` denotes the `vertexSet` of a graph `G`. -/ scoped notation "V(" G ")" => SimpleGraph.vertexSet G From 5a71eda95157391482f64279b72761ef7d3dddaf Mon Sep 17 00:00:00 2001 From: Sorrachai Yingchareonthawornchai Date: Sun, 15 Mar 2026 11:24:32 +0100 Subject: [PATCH 5/5] checkInitImports --- Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean b/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean index fa8eb0892..ceeb492bc 100644 --- a/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean +++ b/Cslib/Algorithms/Lean/Graph/Core/Simple/Undirected.lean @@ -5,7 +5,7 @@ Authors: Sorrachai Yingchareonthawornhcai -/ module - +public import Cslib.Init public import Mathlib.Data.Sym.Sym2 @[expose] public section