Multigraphs

A multigraph is a set of vertices and a set of edges, together with incidence data that associates each edge e with an unordered pair s(x,y) of vertices called the ends of e. The pair of e and s(x,y) is called a link. The vertices x and y may be equal, in which case e is a loop. There may be more than one edge with the same ends.

If a multigraph has no loops and has at most one edge for every given ends, it is called simple, and these objects are also formalized as SimpleGraph.

This module defines Graph α β for a vertex type α and an edge type β, and gives basic API for incidence, adjacency and extensionality. The design broadly follows [Cho94].

Main definitions

For G : Graph α β, ...

• V(G) denotes the vertex set of G as a term in Set α.
• E(G) denotes the edge set of G as a term in Set β.
• G.IsLink e x y means that the edge e : β has vertices x : α and y : α as its ends.
• G.Inc e x means that the edge e : β has x as one of its ends.
• G.Adj x y means that there is an edge e having x and y as its ends.
• G.IsLoopAt e x means that e is a loop edge with both ends equal to x.
• G.IsNonloopAt e x means that e is a non-loop edge with one end equal to x.

Implementation notes

Unlike the design of SimpleGraph, the vertex and edge sets of G are modelled as sets V(G) : Set α and E(G) : Set β, within ambient types, rather than being types themselves. This mimics the 'embedded set' design used in Matroid, which seems to be more convenient for formalizing real-world proofs in combinatorics.

A specific advantage is that this allows subgraphs of G : Graph α β to also exist on an equal footing with G as terms in Graph α β, and so there is no need for a Graph.subgraph type and all the associated definitions and canonical coercion maps. The same will go for minors and the various other partial orders on multigraphs.

The main tradeoff is that parts of the API will need to care about whether a term x : α or e : β is a 'real' vertex or edge of the graph, rather than something outside the vertex or edge set. This is an issue, but is likely amenable to automation.

Notation

Reflecting written mathematics, we use the compact notations V(G) and E(G) to refer to the vertexSet and edgeSet of G : Graph α β. If G.IsLink e x y then we refer to e as edge and x and y as left and right in names.

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

A multigraph with vertices of type α and edges of type β, as described by vertex and edge sets vertexSet : Set α and edgeSet : Set β, and a predicate IsLink describing whether an edge e : β has vertices x y : α as its ends.

The edgeSet structure field can be inferred from IsLink via edge_mem_iff_exists_isLink (and this structure provides default values for edgeSet and edge_mem_iff_exists_isLink that use IsLink). While the field is not strictly necessary, when defining a graph we often immediately know what the edge set should be, and furthermore having edgeSet separate can be convenient for definitional equality reasons.

• vertexSet : Set α

  The vertex set.

• IsLink : β → α → α → Prop

  The binary incidence predicate, stating that x and y are the ends of an edge e. If G.IsLink e x y then we refer to e as edge and x and y as left and right.

• edgeSet : Set β

  The edge set.

• isLink_symm ⦃e : β⦄ : e ∈ self.edgeSet → Symmetric (self.IsLink e)

  If e goes from x to y, it goes from y to x.

• eq_or_eq_of_isLink_of_isLink ⦃e : β⦄ ⦃x y v w : α⦄ : self.IsLink e x y → self.IsLink e v w → x = v ∨ x = w

  An edge is incident with at most one pair of vertices.

• edge_mem_iff_exists_isLink (e : β) : e ∈ self.edgeSet ↔ ∃ (x : α) (y : α), self.IsLink e x y

  An edge e is incident to something if and only if e is in the edge set.

• left_mem_of_isLink ⦃e : β⦄ ⦃x y : α⦄ : self.IsLink e x y → x ∈ self.vertexSet

  If some edge e is incident to x, then x ∈ V.

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

V(G) denotes the vertexSet of a graph G.

Equations

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

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

E(G) denotes the edgeSet of a graph G.

Equations

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

Edge-vertex-vertex incidence

theorem Graph.IsLink.edge_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : e ∈ G.edgeSet

theorem Graph.IsLink.symm {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.IsLink e y x

theorem Graph.IsLink.left_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : x ∈ G.vertexSet

theorem Graph.IsLink.right_mem {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : y ∈ G.vertexSet

theorem Graph.isLink_comm {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} : G.IsLink e x y ↔ G.IsLink e y x

theorem Graph.exists_isLink_of_mem_edgeSet {α : Type u_1} {β : Type u_2} {e : β} {G : Graph α β} (h : e ∈ G.edgeSet) : ∃ (x : α) (y : α), G.IsLink e x y

theorem Graph.edgeSet_eq_setOf_exists_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.edgeSet = {e : β | ∃ (x : α) (y : α), G.IsLink e x y}

theorem Graph.IsLink.left_eq_or_eq {α : Type u_1} {β : Type u_2} {x y z w : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (h' : G.IsLink e z w) : x = z ∨ x = w

theorem Graph.IsLink.right_eq_or_eq {α : Type u_1} {β : Type u_2} {x y z w : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (h' : G.IsLink e z w) : y = z ∨ y = w

theorem Graph.IsLink.left_eq_of_right_ne {α : Type u_1} {β : Type u_2} {x y z w : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (h' : G.IsLink e z w) (hzx : x ≠ z) : x = w

theorem Graph.IsLink.right_unique {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) (h' : G.IsLink e x z) : y = z

theorem Graph.IsLink.left_unique {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.IsLink e x z) (h' : G.IsLink e y z) : x = y

theorem Graph.IsLink.eq_and_eq_or_eq_and_eq {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} {x' y' : α} (h : G.IsLink e x y) (h' : G.IsLink e x' y') : x = x' ∧ y = y' ∨ x = y' ∧ y = x'

theorem Graph.IsLink.isLink_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) {x' y' : α} : G.IsLink e x' y' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'

theorem Graph.IsLink.isLink_iff_sym2_eq {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) {x' y' : α} : G.IsLink e x' y' ↔ s(x, y) = s(x', y')

Edge-vertex incidence

def Graph.Inc {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : Prop

The unary incidence predicate of G. G.Inc e x means that the vertex x is one or both of the ends of the edge e. In the Inc namespace, we use edge and vertex to refer to e and x.

Equations

• G.Inc e x = ∃ (y : α), G.IsLink e x y

@[simp]

theorem Graph.Inc.edge_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : e ∈ G.edgeSet

@[simp]

theorem Graph.Inc.vertex_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : x ∈ G.vertexSet

@[simp]

theorem Graph.IsLink.inc_left {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.Inc e x

@[simp]

theorem Graph.IsLink.inc_right {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.Inc e y

theorem Graph.Inc.eq_or_eq_of_isLink {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.Inc e x) (h' : G.IsLink e y z) : x = y ∨ x = z

theorem Graph.Inc.eq_of_isLink_of_ne_left {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.Inc e x) (h' : G.IsLink e y z) (hxy : x ≠ y) : x = z

theorem Graph.IsLink.isLink_iff_eq {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.IsLink e x z ↔ z = y

theorem Graph.isLink_iff_inc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} : G.IsLink e x y ↔ G.Inc e x ∧ G.Inc e y ∧ ∀ (z : α), G.Inc e z → z = x ∨ z = y

The binary incidence predicate can be expressed in terms of the unary one.

noncomputable def Graph.Inc.other {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : α

Given a proof that the edge e is incident with the vertex x in G, noncomputably find the other end of e. (If e is a loop, this is equal to x itself).

Equations

• h.other = Exists.choose h

@[simp]

theorem Graph.Inc.isLink_other {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : G.IsLink e x h.other

@[simp]

theorem Graph.Inc.inc_other {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : G.Inc e h.other

theorem Graph.Inc.eq_or_eq_or_eq {α : Type u_1} {β : Type u_2} {x y z : α} {e : β} {G : Graph α β} (hx : G.Inc e x) (hy : G.Inc e y) (hz : G.Inc e z) : x = y ∨ x = z ∨ y = z

def Graph.IsLoopAt {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : Prop

G.IsLoopAt e x means that both ends of the edge e are equal to the vertex x.

Equations

• G.IsLoopAt e x = G.IsLink e x x

@[simp]

theorem Graph.isLink_self_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : G.IsLink e x x ↔ G.IsLoopAt e x

theorem Graph.IsLoopAt.inc {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : G.Inc e x

theorem Graph.IsLoopAt.eq_of_inc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) (h' : G.Inc e y) : x = y

@[simp]

theorem Graph.IsLoopAt.edge_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : e ∈ G.edgeSet

@[simp]

theorem Graph.IsLoopAt.vertex_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) : x ∈ G.vertexSet

def Graph.IsNonloopAt {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (x : α) : Prop

G.IsNonloopAt e x means that the vertex x is one but not both of the ends of the edge =e, or equivalently that e is incident with x but not a loop at x - see Graph.isNonloopAt_iff_inc_not_isLoopAt.

Equations

• G.IsNonloopAt e x = ∃ (y : α), y ≠ x ∧ G.IsLink e x y

theorem Graph.IsNonloopAt.inc {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : G.Inc e x

@[simp]

theorem Graph.IsNonloopAt.edge_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : e ∈ G.edgeSet

@[simp]

theorem Graph.IsNonloopAt.vertex_mem {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) : x ∈ G.vertexSet

theorem Graph.IsLoopAt.not_isNonloopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsLoopAt e x) (y : α) : ¬G.IsNonloopAt e y

theorem Graph.IsNonloopAt.not_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.IsNonloopAt e x) (y : α) : ¬G.IsLoopAt e y

theorem Graph.isNonloopAt_iff_inc_not_isLoopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : G.IsNonloopAt e x ↔ G.Inc e x ∧ ¬G.IsLoopAt e x

theorem Graph.isLoopAt_iff_inc_not_isNonloopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} : G.IsLoopAt e x ↔ G.Inc e x ∧ ¬G.IsNonloopAt e x

theorem Graph.Inc.isLoopAt_or_isNonloopAt {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x) : G.IsLoopAt e x ∨ G.IsNonloopAt e x

Adjacency

def Graph.Adj {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : α) : Prop

G.Adj x y means that G has an edge whose ends are the vertices x and y.

Equations

• G.Adj x y = ∃ (e : β), G.IsLink e x y

theorem Graph.Adj.symm {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (h : G.Adj x y) : G.Adj y x

theorem Graph.adj_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} (x y : α) : G.Adj x y ↔ G.Adj y x

@[simp]

theorem Graph.Adj.left_mem {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (h : G.Adj x y) : x ∈ G.vertexSet

@[simp]

theorem Graph.Adj.right_mem {α : Type u_1} {β : Type u_2} {x y : α} {G : Graph α β} (h : G.Adj x y) : y ∈ G.vertexSet

theorem Graph.IsLink.adj {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β} (h : G.IsLink e x y) : G.Adj x y

Extensionality

@[simp]

theorem Graph.mk_eq_self {α : Type u_1} {β : Type u_2} (G : Graph α β) {E : Set β} (hE : ∀ (e : β), e ∈ E ↔ ∃ (x : α) (y : α), G.IsLink e x y) : { vertexSet := G.vertexSet, IsLink := G.IsLink, edgeSet := E, isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ } = G

edgeSet can be determined using IsLink, so the graph constructed from G.vertexSet and G.IsLink using any value for edgeSet is equal to G itself.

theorem Graph.ext {α : Type u_1} {β : Type u_2} {G₁ G₂ : Graph α β} (hV : G₁.vertexSet = G₂.vertexSet) (h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y) : G₁ = G₂

Two graphs with the same vertex set and binary incidences are equal. (We use this as the default extensionality lemma rather than adding @[ext] to the definition of Graph, so it doesn't require equality of the edge sets.)

theorem Graph.ext_iff {α : Type u_1} {β : Type u_2} {G₁ G₂ : Graph α β} : G₁ = G₂ ↔ G₁.vertexSet = G₂.vertexSet ∧ ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y

theorem Graph.ext_inc {α : Type u_1} {β : Type u_2} {G₁ G₂ : Graph α β} (hV : G₁.vertexSet = G₂.vertexSet) (h : ∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x) : G₁ = G₂

Two graphs with the same vertex set and unary incidences are equal.