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.

structure GraphLib.Edge (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

An undirected edge with a label of type β and an unordered pair of endpoints.

• edgeLabel : β

  The edge label, used to distinguish parallel edges.

• endpoints : Sym2 α

  The unordered pair of endpoints.

@[implicit_reducible]

instance GraphLib.instDecidableEqEdge {α✝ : Type u_3} {β✝ : Type u_4} [DecidableEq α✝] [DecidableEq β✝] : DecidableEq (Edge α✝ β✝)

Equations

• GraphLib.instDecidableEqEdge = GraphLib.instDecidableEqEdge.decEq

def GraphLib.instDecidableEqEdge.decEq {α✝ : Type u_3} {β✝ : Type u_4} [DecidableEq α✝] [DecidableEq β✝] (x✝ x✝¹ : Edge α✝ β✝) : Decidable (x✝ = x✝¹)

Equations

• GraphLib.instDecidableEqEdge.decEq { edgeLabel := a, endpoints := a_1 } { edgeLabel := b, endpoints := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

structure GraphLib.DiEdge (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

A directed edge with a label of type β and an ordered pair of endpoints.

• edgeLabel : β

  The edge label, used to distinguish parallel edges.

• endpoints : α × α

  The ordered pair (source, target) of endpoints.

def GraphLib.instDecidableEqDiEdge.decEq {α✝ : Type u_3} {β✝ : Type u_4} [DecidableEq α✝] [DecidableEq β✝] (x✝ x✝¹ : DiEdge α✝ β✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GraphLib.instDecidableEqDiEdge {α✝ : Type u_3} {β✝ : Type u_4} [DecidableEq α✝] [DecidableEq β✝] : DecidableEq (DiEdge α✝ β✝)

Equations

• GraphLib.instDecidableEqDiEdge = GraphLib.instDecidableEqDiEdge.decEq

structure GraphLib.Graph (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

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.

• vertexSet : Set α

  The set of vertices.

• edgeSet : Set (Edge α β)

  The set of edges.

• incidence' (e : Edge α β) : e ∈ self.edgeSet → ∀ v ∈ e.endpoints, v ∈ self.vertexSet

  Every endpoint of an edge is a vertex. Prefer Graph.incidence.

structure GraphLib.SimpleGraph (α : Type u_3) : Type u_3

A simple graph on α with edges as unordered pairs of distinct vertices.

• vertexSet : Set α

  The set of vertices.

• edgeSet : Set (Sym2 α)

  The set of edges, each an unordered pair of vertices.

• incidence' (e : Sym2 α) : e ∈ self.edgeSet → ∀ v ∈ e, v ∈ self.vertexSet

  Both endpoints of every edge are vertices. Prefer SimpleGraph.incidence.

• loopless' (e : Sym2 α) : e ∈ self.edgeSet → ¬e.IsDiag

  No edge is a loop. Prefer SimpleGraph.loopless.

structure GraphLib.DiGraph (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

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.

• vertexSet : Set α

  The set of vertices.

• edgeSet : Set (DiEdge α β)

  The set of edges.

• incidence' (e : DiEdge α β) : e ∈ self.edgeSet → e.endpoints.1 ∈ self.vertexSet ∧ e.endpoints.2 ∈ self.vertexSet

  Both endpoints of every edge are vertices. Prefer DiGraph.incidence.

structure GraphLib.SimpleDiGraph (α : Type u_3) : Type u_3

A simple directed graph on α with edges as ordered pairs of distinct vertices.

• vertexSet : Set α

  The set of vertices.

• edgeSet : Set (α × α)

  The set of directed edges.

• incidence' (e : α × α) : e ∈ self.edgeSet → e.1 ∈ self.vertexSet ∧ e.2 ∈ self.vertexSet

  Both endpoints of every directed edge are vertices. Prefer SimpleDiGraph.incidence.

• loopless' (e : α × α) : e ∈ self.edgeSet → e.1 ≠ e.2

  No directed edge is a loop. Prefer SimpleDiGraph.loopless.

def GraphLib.SimpleGraph.toGraph {α : Type u_1} (G : SimpleGraph α) : Graph α (Sym2 α)

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.

Equations

• G.toGraph = { vertexSet := G.vertexSet, edgeSet := (fun (e : Sym2 α) => { edgeLabel := e, endpoints := e }) '' G.edgeSet, incidence' := ⋯ }

def GraphLib.SimpleDiGraph.toDiGraph {α : Type u_1} (G : SimpleDiGraph α) : DiGraph α (α × α)

Forget the looplessness axiom of a SimpleDiGraph, viewing it as a DiGraph whose edges are DiEdge α (α × α) with the pair as both label and endpoints.

Equations

• G.toDiGraph = { vertexSet := G.vertexSet, edgeSet := (fun (e : α × α) => { edgeLabel := e, endpoints := e }) '' G.edgeSet, incidence' := ⋯ }

@[implicit_reducible]

instance GraphLib.instCoeSimpleGraphGraphSym2 {α : Type u_1} : Coe (SimpleGraph α) (Graph α (Sym2 α))

Equations

• GraphLib.instCoeSimpleGraphGraphSym2 = { coe := GraphLib.SimpleGraph.toGraph }

@[implicit_reducible]

instance GraphLib.instCoeSimpleDiGraphDiGraphProd {α : Type u_1} : Coe (SimpleDiGraph α) (DiGraph α (α × α))

Equations

• GraphLib.instCoeSimpleDiGraphDiGraphProd = { coe := GraphLib.SimpleDiGraph.toDiGraph }

class GraphLib.HasVertexSet (G : Type u_3) (V : outParam (Type u_4)) : Type (max u_3 u_4)

Typeclass for graph-like structures that have a vertex set.

• vertexSet : G → V

  The vertex set of the graph.

class GraphLib.HasEdgeSet (G : Type u_3) (E : outParam (Type u_4)) : Type (max u_3 u_4)

Typeclass for graph-like structures that have an edge set.

• edgeSet : G → E

  The edge set of the graph.

@[implicit_reducible]

instance GraphLib.instHasVertexSetGraphSet {α : Type u_3} {β : Type u_4} : HasVertexSet (Graph α β) (Set α)

Equations

• GraphLib.instHasVertexSetGraphSet = { vertexSet := GraphLib.Graph.vertexSet }

@[implicit_reducible]

instance GraphLib.instHasVertexSetSimpleGraphSet {α : Type u_3} : HasVertexSet (SimpleGraph α) (Set α)

Equations

• GraphLib.instHasVertexSetSimpleGraphSet = { vertexSet := GraphLib.SimpleGraph.vertexSet }

@[implicit_reducible]

instance GraphLib.instHasVertexSetDiGraphSet {α : Type u_3} {β : Type u_4} : HasVertexSet (DiGraph α β) (Set α)

Equations

• GraphLib.instHasVertexSetDiGraphSet = { vertexSet := GraphLib.DiGraph.vertexSet }

@[implicit_reducible]

instance GraphLib.instHasVertexSetSimpleDiGraphSet {α : Type u_3} : HasVertexSet (SimpleDiGraph α) (Set α)

Equations

• GraphLib.instHasVertexSetSimpleDiGraphSet = { vertexSet := GraphLib.SimpleDiGraph.vertexSet }

@[implicit_reducible]

instance GraphLib.instHasEdgeSetGraphSetSym2 {α : Type u_3} {β : Type u_4} : HasEdgeSet (Graph α β) (Set (Sym2 α))

Equations

• GraphLib.instHasEdgeSetGraphSetSym2 = { edgeSet := fun (G : GraphLib.Graph α β) => GraphLib.Edge.endpoints '' G.edgeSet }

@[implicit_reducible]

instance GraphLib.instHasEdgeSetSimpleGraphSetSym2 {α : Type u_3} : HasEdgeSet (SimpleGraph α) (Set (Sym2 α))

Equations

• GraphLib.instHasEdgeSetSimpleGraphSetSym2 = { edgeSet := GraphLib.SimpleGraph.edgeSet }

@[implicit_reducible]

instance GraphLib.instHasEdgeSetDiGraphSetProd {α : Type u_3} {β : Type u_4} : HasEdgeSet (DiGraph α β) (Set (α × α))

Equations

• GraphLib.instHasEdgeSetDiGraphSetProd = { edgeSet := fun (G : GraphLib.DiGraph α β) => GraphLib.DiEdge.endpoints '' G.edgeSet }

@[implicit_reducible]

instance GraphLib.instHasEdgeSetSimpleDiGraphSetProd {α : Type u_3} : HasEdgeSet (SimpleDiGraph α) (Set (α × α))

Equations

• GraphLib.instHasEdgeSetSimpleDiGraphSetProd = { edgeSet := GraphLib.SimpleDiGraph.edgeSet }

def GraphLib.«termV(_)» : Lean.ParserDescr

Notation for the vertex set of a graph.

Equations

• One or more equations did not get rendered due to their size.

def GraphLib.«termE(_)» : Lean.ParserDescr

Notation for the edge set of a graph.

Equations

• One or more equations did not get rendered due to their size.

theorem GraphLib.Graph.incidence {α : Type u_1} {β : Type u_2} (G : Graph α β) {e : Sym2 α} (he : e ∈ HasEdgeSet.edgeSet G) {v : α} (hv : v ∈ e) : v ∈ HasVertexSet.vertexSet G

theorem GraphLib.SimpleGraph.incidence {α : Type u_1} (G : SimpleGraph α) {e : Sym2 α} (he : e ∈ HasEdgeSet.edgeSet G) {v : α} (hv : v ∈ e) : v ∈ HasVertexSet.vertexSet G

theorem GraphLib.SimpleGraph.loopless {α : Type u_1} (G : SimpleGraph α) {e : Sym2 α} (he : e ∈ HasEdgeSet.edgeSet G) : ¬e.IsDiag

theorem GraphLib.DiGraph.incidence {α : Type u_1} {β : Type u_2} (G : DiGraph α β) {e : α × α} (he : e ∈ HasEdgeSet.edgeSet G) : e.1 ∈ HasVertexSet.vertexSet G ∧ e.2 ∈ HasVertexSet.vertexSet G

theorem GraphLib.SimpleDiGraph.incidence {α : Type u_1} (G : SimpleDiGraph α) {e : α × α} (he : e ∈ HasEdgeSet.edgeSet G) : e.1 ∈ HasVertexSet.vertexSet G ∧ e.2 ∈ HasVertexSet.vertexSet G

theorem GraphLib.SimpleDiGraph.loopless {α : Type u_1} (G : SimpleDiGraph α) {e : α × α} (he : e ∈ HasEdgeSet.edgeSet G) : e.1 ≠ e.2