diff --git a/Cslib.lean b/Cslib.lean index ef09e6f16..f79085022 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -1,5 +1,6 @@ module -- shake: keep-all +public import Cslib.Algorithms.Lean.Graph.Graph 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/Graph.lean b/Cslib/Algorithms/Lean/Graph/Graph.lean new file mode 100644 index 000000000..77af9c4f9 --- /dev/null +++ b/Cslib/Algorithms/Lean/Graph/Graph.lean @@ -0,0 +1,212 @@ +/- +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, Weixuan Yuan +-/ + +module +public import Cslib.Init +public import Mathlib.Data.Sym.Sym2 + +@[expose] public section + +/-! +# Graph structures + +This file introduces a small hierarchy of graph-like combinatorial structures on a vertex +type `α`. Each structure carries its vertex and edge sets explicitly. + +## Design rationale + +We intentionally diverge from Mathlib's graph definitions (`Mathlib.Combinatorics.Graph.Basic`, +`Mathlib.Combinatorics.SimpleGraph.Basic`), +prioritizing representations that support algorithmic reasoning. In graph algorithm design, +it is common to manipulate graphs dynamically (adding or removing nodes/edges, contracting +edges, etc.). We therefore use set-based definitions for both vertex and edge sets with +minimal additional axioms, reducing early proof obligations and keeping proofs closer to +their textbook counterparts. + +## Main definitions + +* `Edge α β`: an undirected edge with a label of type `β` and endpoints as a `Sym2 α`. +* `DiEdge α β`: a directed edge with a label of type `β` and endpoints as `α × α`. +* `Graph α β`: a general graph whose edges are `Edge α β` values. Parallel edges and + loops are permitted. +* `SimpleGraph α`: a simple graph with edges as `Sym2 α`, no loops. +* `DiGraph α β`: a directed graph whose edges are `DiEdge α β` values. Parallel edges + and loops are permitted. +* `SimpleDiGraph α`: a simple directed graph with edges as `α × α`, no loops. + +## Notation + +* `V(G)`: the vertex set of `G`, via `HasVertexSet`. +* `E(G)`: the edge set of `G`, via `HasEdgeSet`. + +## Main API + +The structure fields are named with a `'` suffix (e.g. `incidence'`, `loopless'`). The +preferred API restates these in terms of `V(G)` and `E(G)`: + +* `Graph.incidence`, `SimpleGraph.incidence`, `DiGraph.incidence`, `SimpleDiGraph.incidence` +* `SimpleGraph.loopless`, `SimpleDiGraph.loopless` + +## Main forgetful maps + +* `SimpleGraph.toGraph`: forget the looplessness axiom of a simple graph. +* `SimpleDiGraph.toDiGraph`: forget the looplessness axiom of a simple directed graph. + +The corresponding `Coe` instances are registered. +-/ + +namespace Cslib.Algorithms.Lean +variable {α β : Type*} + +/-- 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. -/ + edgeLabel : β + /-- The unordered pair of endpoints. -/ + endpoints : Sym2 α +deriving DecidableEq + +/-- A directed edge with a label of type `β` and an ordered pair of endpoints. -/ +structure DiEdge (α β : Type*) where + /-- The edge label, used to distinguish parallel edges. -/ + edgeLabel : β + /-- 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 simple graph on `α` with edges as unordered pairs of distinct vertices. -/ +@[grind] +structure SimpleGraph (α : Type*) where + /-- The set of vertices. -/ + vertexSet : Set α + /-- The set of edges, each an unordered pair of vertices. -/ + edgeSet : Set (Sym2 α) + /-- Both endpoints of every edge are vertices. Prefer `SimpleGraph.incidence`. -/ + incidence' : ∀ e ∈ edgeSet, ∀ v ∈ e, v ∈ vertexSet + /-- No edge is a loop. Prefer `SimpleGraph.loopless`. -/ + loopless' : ∀ e ∈ edgeSet, ¬ e.IsDiag + +/-- 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 (DiEdge α β) + /-- Both endpoints of every edge are vertices. Prefer `DiGraph.incidence`. -/ + incidence' : ∀ e ∈ edgeSet, e.endpoints.1 ∈ vertexSet ∧ e.endpoints.2 ∈ vertexSet + +/-- A simple directed graph on `α` with edges as ordered pairs of distinct vertices. -/ +structure SimpleDiGraph (α : Type*) where + /-- The set of vertices. -/ + vertexSet : Set α + /-- The set of directed edges. -/ + edgeSet : Set (α × α) + /-- Both endpoints of every directed edge are vertices. Prefer `SimpleDiGraph.incidence`. -/ + incidence' : ∀ e ∈ edgeSet, e.1 ∈ vertexSet ∧ e.2 ∈ vertexSet + /-- No directed edge is a loop. Prefer `SimpleDiGraph.loopless`. -/ + loopless' : ∀ e ∈ edgeSet, e.1 ≠ e.2 + +/-- Forget the looplessness axiom of a `SimpleGraph`, viewing it as a `Graph` whose edges +are `Edge α (Sym2 α)` with the pair as both label and endpoints. -/ +def SimpleGraph.toGraph (G : SimpleGraph α) : Graph α (Sym2 α) where + vertexSet := G.vertexSet + edgeSet := (fun e => ⟨e, e⟩) '' G.edgeSet + incidence' := by + rintro _ ⟨e, he, rfl⟩ v hv + exact G.incidence' e he v hv + +/-- Forget the looplessness axiom of a `SimpleDiGraph`, viewing it as a `DiGraph` whose +edges are `DiEdge α (α × α)` with the pair as both label and endpoints. -/ +def SimpleDiGraph.toDiGraph (G : SimpleDiGraph α) : DiGraph α (α × α) where + vertexSet := G.vertexSet + edgeSet := (fun e => ⟨e, e⟩) '' G.edgeSet + incidence' := by + rintro _ ⟨e, he, rfl⟩ + exact G.incidence' e he + +instance : Coe (SimpleGraph α) (Graph α (Sym2 α)) := ⟨SimpleGraph.toGraph⟩ + +instance : Coe (SimpleDiGraph α) (DiGraph α (α × α)) := ⟨SimpleDiGraph.toDiGraph⟩ + +/-- Typeclass for graph-like structures that have a vertex set. -/ +class HasVertexSet (G : Type*) (V : outParam Type*) where + /-- The vertex set of the graph. -/ + vertexSet : G → V + +/-- Typeclass for graph-like structures that have an edge set. -/ +class HasEdgeSet (G : Type*) (E : outParam Type*) where + /-- The edge set of the graph. -/ + edgeSet : G → E + +@[simp] instance {α β : Type*} : HasVertexSet (Graph α β) (Set α) := + ⟨Graph.vertexSet⟩ + +@[simp] instance {α : Type*} : HasVertexSet (SimpleGraph α) (Set α) := + ⟨SimpleGraph.vertexSet⟩ + +@[simp] instance {α β : Type*} : HasVertexSet (DiGraph α β) (Set α) := + ⟨DiGraph.vertexSet⟩ + +@[simp] instance {α : Type*} : HasVertexSet (SimpleDiGraph α) (Set α) := + ⟨SimpleDiGraph.vertexSet⟩ + +@[simp] instance {α β : Type*} : HasEdgeSet (Graph α β) (Set (Sym2 α)) := + ⟨fun G => Edge.endpoints '' G.edgeSet⟩ + +@[simp] instance {α : Type*} : HasEdgeSet (SimpleGraph α) (Set (Sym2 α)) := + ⟨SimpleGraph.edgeSet⟩ + +@[simp] instance {α β : Type*} : HasEdgeSet (DiGraph α β) (Set (α × α)) := + ⟨fun G => DiEdge.endpoints '' G.edgeSet⟩ + +@[simp] instance {α : Type*} : HasEdgeSet (SimpleDiGraph α) (Set (α × α)) := + ⟨SimpleDiGraph.edgeSet⟩ + +/-- Notation for the vertex set of a graph. -/ +scoped notation "V(" G ")" => HasVertexSet.vertexSet G +/-- Notation for the edge set of a graph. -/ +scoped notation "E(" G ")" => HasEdgeSet.edgeSet G + +theorem Graph.incidence (G : Graph α β) {e : Sym2 α} (he : e ∈ E(G)) + {v : α} (hv : v ∈ e) : v ∈ V(G) := by + obtain ⟨e', he', rfl⟩ := he + exact G.incidence' e' he' v hv + +theorem SimpleGraph.incidence (G : SimpleGraph α) {e : Sym2 α} (he : e ∈ E(G)) + {v : α} (hv : v ∈ e) : v ∈ V(G) := + G.incidence' e he v hv + +theorem SimpleGraph.loopless (G : SimpleGraph α) {e : Sym2 α} (he : e ∈ E(G)) : + ¬ e.IsDiag := + G.loopless' e he + +theorem DiGraph.incidence (G : DiGraph α β) {e : α × α} (he : e ∈ E(G)) : + e.1 ∈ V(G) ∧ e.2 ∈ V(G) := by + obtain ⟨e', he', rfl⟩ := he + exact G.incidence' e' he' + +theorem SimpleDiGraph.incidence (G : SimpleDiGraph α) {e : α × α} (he : e ∈ E(G)) : + e.1 ∈ V(G) ∧ e.2 ∈ V(G) := + G.incidence' e he + +theorem SimpleDiGraph.loopless (G : SimpleDiGraph α) {e : α × α} (he : e ∈ E(G)) : + e.1 ≠ e.2 := + G.loopless' e he + +end Cslib.Algorithms.Lean