structure Hex.Graph (n : Nat) : Type

A finite simple undirected graph on the vertex set Fin n, as a dense Boolean adjacency matrix constrained to be symmetric and loopless.

• adjMatrix : Matrix Bool n n

  The dense Boolean adjacency matrix.

• symm (i j : Fin n) : self.adjMatrix[i][j] = self.adjMatrix[j][i]

  The edge relation is symmetric.

• loopless (i : Fin n) : self.adjMatrix[i][i] = false

  The edge relation is irreflexive: no loops.

@[inline]

def Hex.Graph.adj {n : Nat} (G : Graph n) (i j : Fin n) : Bool

Executable adjacency test: G.adj i j is true exactly when {i, j} is an edge of G. O(1).

Equations

• G.adj i j = G.adjMatrix[(i, j)]

theorem Hex.Graph.adj_eq_getElem {n : Nat} (G : Graph n) (i j : Fin n) : G.adj i j = G.adjMatrix[i][j]

adj reads the adjacency matrix entry.

theorem Hex.Graph.adj_symm {n : Nat} (G : Graph n) (i j : Fin n) : G.adj i j = G.adj j i

Adjacency is symmetric.

@[simp]

theorem Hex.Graph.adj_self {n : Nat} (G : Graph n) (i : Fin n) : G.adj i i = false

Adjacency is irreflexive.

theorem Hex.Graph.ne_of_adj {n : Nat} {G : Graph n} {i j : Fin n} (h : G.adj i j = true) : i ≠ j

Adjacent vertices are distinct.

theorem Hex.Graph.ext_adjMatrix {n : Nat} {G H : Graph n} (h : G.adjMatrix = H.adjMatrix) : G = H

Two graphs with equal adjacency matrices are equal.

theorem Hex.Graph.ext {n : Nat} {G H : Graph n} (h : ∀ (i j : Fin n), G.adj i j = H.adj i j) : G = H

Two graphs are equal when they have the same edges.

theorem Hex.Graph.ext_iff {n : Nat} {G H : Graph n} : G = H ↔ ∀ (i j : Fin n), G.adj i j = H.adj i j

theorem Hex.Graph.eq_iff_adj {n : Nat} {G H : Graph n} : G = H ↔ ∀ (i j : Fin n), G.adj i j = H.adj i j

Equality of graphs is exactly equality of the represented edge relation.

@[instance_reducible]

instance Hex.Graph.instDecidableEq {n : Nat} : DecidableEq (Graph n)

Equations

• G.instDecidableEq H = if h : G.adjMatrix.data = H.adjMatrix.data then isTrue ⋯ else isFalse ⋯

def Hex.Graph.ofAdj {n : Nat} (f : Fin n → Fin n → Bool) (hs : ∀ (i j : Fin n), f i j = f j i) (hi : ∀ (i : Fin n), f i i = false) : Graph n

Build a graph from a symmetric irreflexive Boolean adjacency function.

Equations

• Hex.Graph.ofAdj f hs hi = { adjMatrix := Hex.Matrix.ofFn f, symm := ⋯, loopless := ⋯ }

@[simp]

theorem Hex.Graph.adj_ofAdj {n : Nat} (f : Fin n → Fin n → Bool) (hs : ∀ (i j : Fin n), f i j = f j i) (hi : ∀ (i : Fin n), f i i = false) (i j : Fin n) : (ofAdj f hs hi).adj i j = f i j

def Hex.Graph.ofRel {n : Nat} (f : Fin n → Fin n → Bool) : Graph n

Build a graph from an arbitrary Boolean relation by symmetrizing it and removing loops: i and j are adjacent when i ≠ j and the relation holds in either direction.

Equations

• Hex.Graph.ofRel f = Hex.Graph.ofAdj (fun (i j : Fin n) => i != j && (f i j || f j i)) ⋯ ⋯

@[simp]

theorem Hex.Graph.adj_ofRel {n : Nat} (f : Fin n → Fin n → Bool) (i j : Fin n) : (ofRel f).adj i j = (i != j && (f i j || f j i))

def Hex.Graph.empty (n : Nat) : Graph n

The graph on n vertices with no edges.

Equations

• Hex.Graph.empty n = Hex.Graph.ofAdj (fun (x x_1 : Fin n) => false) ⋯ ⋯

@[simp]

theorem Hex.Graph.adj_empty {n : Nat} (i j : Fin n) : (empty n).adj i j = false

def Hex.Graph.complete (n : Nat) : Graph n

The complete graph on n vertices.

Equations

• Hex.Graph.complete n = Hex.Graph.ofAdj (fun (i j : Fin n) => i != j) ⋯ ⋯

@[simp]

theorem Hex.Graph.adj_complete {n : Nat} (i j : Fin n) : (complete n).adj i j = (i != j)

def Hex.Graph.edgeListAdj {n : Nat} (edges : List (Nat × Nat)) (i j : Fin n) : Bool

The membership test behind ofEdges?: an unordered edge {i, j} is present when the input list contains it in either orientation.

Equations

• Hex.Graph.edgeListAdj edges i j = edges.any fun (e : Nat × Nat) => e.fst == ↑i && e.snd == ↑j || e.fst == ↑j && e.snd == ↑i

theorem Hex.Graph.edgeListAdj_symm {n : Nat} (edges : List (Nat × Nat)) (i j : Fin n) : edgeListAdj edges i j = edgeListAdj edges j i

def Hex.Graph.validEdge (n : Nat) (e : Nat × Nat) : Bool

A well-formed input for ofEdges? n: both endpoints in range, no loops.

Equations

• Hex.Graph.validEdge n e = (decide (e.fst < n) && decide (e.snd < n) && e.fst != e.snd)

def Hex.Graph.ofEdges? (n : Nat) (edges : List (Nat × Nat)) : Option (Graph n)

Checked edge-list builder. Returns none when some listed edge has an endpoint out of range or is a loop; otherwise builds the graph whose edges are the listed unordered pairs, collapsing duplicates in either orientation.

Equations

• Hex.Graph.ofEdges? n edges = if h : edges.all (Hex.Graph.validEdge n) = true then some (Hex.Graph.ofAdj (Hex.Graph.edgeListAdj edges) ⋯ ⋯) else none

def Hex.Graph.ofEdges {n : Nat} (edges : List (Fin n × Fin n)) : Graph n

Total edge-list builder over Fin pairs: the graph whose edges are the listed unordered pairs, collapsing duplicates in either orientation and dropping diagonal pairs. Beware that numeric literals in a Fin n pair wrap modulo n; use ofEdges? to range-check plain Nat input instead.

Equations

• Hex.Graph.ofEdges edges = Hex.Graph.ofRel fun (i j : Fin n) => edges.any fun (e : Fin n × Fin n) => e.fst == i && e.snd == j

@[simp]

theorem Hex.Graph.adj_ofEdges {n : Nat} (edges : List (Fin n × Fin n)) (i j : Fin n) : (ofEdges edges).adj i j = (i != j && (decide ((i, j) ∈ edges) || decide ((j, i) ∈ edges)))

The graph built by ofEdges has exactly the listed undirected edges, less the diagonal.

theorem Hex.Graph.isSome_ofEdges? (n : Nat) (edges : List (Nat × Nat)) : (ofEdges? n edges).isSome = edges.all (validEdge n)

ofEdges? succeeds exactly on well-formed inputs.

theorem Hex.Graph.adj_ofEdges? {n : Nat} {edges : List (Nat × Nat)} {G : Graph n} (h : ofEdges? n edges = some G) (i j : Fin n) : G.adj i j = (decide ((↑i, ↑j) ∈ edges) || decide ((↑j, ↑i) ∈ edges))

The graph built by ofEdges? has exactly the listed undirected edges.

def Hex.Graph.nbrs {n : Nat} (G : Graph n) (i : Fin n) : Array (Fin n)

The sorted duplicate-free array of neighbours of i. O(n) adjacency reads; the order is increasing vertex order.

Equations

• G.nbrs i = (List.filter (fun (j : Fin n) => G.adj i j) (List.finRange n)).toArray

theorem Hex.Graph.mem_nbrs {n : Nat} {G : Graph n} {i j : Fin n} : j ∈ G.nbrs i ↔ G.adj i j = true

def Hex.Graph.degree {n : Nat} (G : Graph n) (i : Fin n) : Nat

The degree of a vertex.

Equations

• G.degree i = (G.nbrs i).size

def Hex.Graph.relabel {n : Nat} (G : Graph n) (f : Fin n → Fin n) : Graph n

Relabel a graph along a vertex map: (G.relabel f).adj i j = G.adj (f i) (f j). For a bijective f this is relabelling by the inverse bijection; stated for an arbitrary map because neither invariant needs injectivity.

Equations

• G.relabel f = Hex.Graph.ofAdj (fun (i j : Fin n) => G.adj (f i) (f j)) ⋯ ⋯

@[simp]

theorem Hex.Graph.adj_relabel {n : Nat} (G : Graph n) (f : Fin n → Fin n) (i j : Fin n) : (G.relabel f).adj i j = G.adj (f i) (f j)

The adjacency correspondence for relabelling.

@[simp]

theorem Hex.Graph.relabel_id {n : Nat} (G : Graph n) : G.relabel id = G

theorem Hex.Graph.relabel_relabel {n : Nat} (G : Graph n) (f g : Fin n → Fin n) : (G.relabel f).relabel g = G.relabel (f ∘ g)