def Hex.SparseGraph.Builder.unique {α : Type u_1} [BEq α] : List α → List α

Remove consecutive duplicates in one pass.

Equations

• Hex.SparseGraph.Builder.unique [] = []
• Hex.SparseGraph.Builder.unique (b :: xs) = Hex.SparseGraph.Builder.unique.go b xs

def Hex.SparseGraph.Builder.unique.go {α : Type u_1} [BEq α] (a : α) : List α → List α

Equations

• Hex.SparseGraph.Builder.unique.go a [] = [a]
• Hex.SparseGraph.Builder.unique.go a (b :: xs) = if (a == b) = true then Hex.SparseGraph.Builder.unique.go a xs else a :: Hex.SparseGraph.Builder.unique.go b xs

@[csimp]

theorem Hex.SparseGraph.Builder.unique_eq_eraseReps : @unique = @List.eraseReps

Use the standard tail-recursive implementation in compiled code.

theorem Hex.SparseGraph.Builder.mem_go {α : Type u_1} [BEq α] [LawfulBEq α] (a b : α) (xs : List α) : b ∈ unique.go a xs ↔ b = a ∨ b ∈ xs

@[simp]

theorem Hex.SparseGraph.Builder.mem_unique {α : Type u_1} [BEq α] [LawfulBEq α] (a : α) (xs : List α) : a ∈ unique xs ↔ a ∈ xs

def Hex.SparseGraph.Builder.normalize {n : Nat} (xs : List (Fin n)) : List (Fin n)

Sort a row and collapse repeated neighbours in linear time after sorting.

Equations

• Hex.SparseGraph.Builder.normalize xs = Hex.SparseGraph.Builder.unique (Hex.List.sort xs fun (a b : Fin n) => decide (a ≤ b))

@[simp]

theorem Hex.SparseGraph.Builder.mem_normalize {n : Nat} (a : Fin n) (xs : List (Fin n)) : a ∈ normalize xs ↔ a ∈ xs

theorem Hex.SparseGraph.Builder.sorted_normalize {n : Nat} (xs : List (Fin n)) : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) (normalize xs)

def Hex.SparseGraph.Builder.add {n : Nat} (rows : Vector (List (Fin n)) n) (e : Fin n × Fin n) : Vector (List (Fin n)) n

Scatter an undirected edge into its two rows; diagonal pairs are dropped.

Equations

• Hex.SparseGraph.Builder.add rows e = if (e.fst == e.snd) = true then rows else have rows := rows.set (↑e.fst) (e.snd :: rows[e.fst]) ⋯; rows.set (↑e.snd) (e.fst :: rows[e.snd]) ⋯

theorem Hex.SparseGraph.Builder.mem_add {n : Nat} (rows : Vector (List (Fin n)) n) (e : Fin n × Fin n) (i j : Fin n) : j ∈ (add rows e)[↑i] ↔ j ∈ rows[↑i] ∨ i ≠ j ∧ (e = (i, j) ∨ e = (j, i))

def Hex.SparseGraph.Builder.scatter {n : Nat} (edges : List (Fin n × Fin n)) : Vector (List (Fin n)) n

Build unsorted adjacency lists with one array update per directed edge.

Equations

• Hex.SparseGraph.Builder.scatter edges = List.foldl Hex.SparseGraph.Builder.add (Vector.replicate n []) edges

@[simp]

theorem Hex.SparseGraph.Builder.mem_scatter {n : Nat} (edges : List (Fin n × Fin n)) (i j : Fin n) : j ∈ (scatter edges)[↑i] ↔ i ≠ j ∧ ((i, j) ∈ edges ∨ (j, i) ∈ edges)

def Hex.SparseGraph.Builder.checked (n : Nat) (edges : List (Nat × Nat)) (h : edges.all (Graph.validEdge n) = true) : List (Fin n × Fin n)

Range-checking supplies erased proofs for the finite endpoints.

Equations

• Hex.SparseGraph.Builder.checked n edges h = List.map (fun (e : { e : Nat × Nat // e ∈ edges }) => have hv := ⋯; (⟨e.val.fst, ⋯⟩, ⟨e.val.snd, ⋯⟩)) edges.attach

@[simp]

theorem Hex.SparseGraph.Builder.mem_checked (n : Nat) (edges : List (Nat × Nat)) (h : edges.all (Graph.validEdge n) = true) (i j : Fin n) : (i, j) ∈ checked n edges h ↔ (↑i, ↑j) ∈ edges

def Hex.SparseGraph.Builder.normalizeRows {n : Nat} (rows : Vector (List (Fin n)) n) : Vector (List (Fin n)) n

Expose row normalization to the kernel while retaining the existing array map in compiled graph construction.

Equations

• Hex.SparseGraph.Builder.normalizeRows rows = Vector.mk (Hex.Array.map' Hex.SparseGraph.Builder.normalize rows.toArray) ⋯

@[simp]

theorem Hex.SparseGraph.Builder.normalizeRows_eq {n : Nat} (rows : Vector (List (Fin n)) n) : normalizeRows rows = Vector.map normalize rows

@[inline]

def Hex.SparseGraph.Builder.normalizeRowsFast {n : Nat} (rows : Vector (List (Fin n)) n) : Vector (List (Fin n)) n

Equations

• Hex.SparseGraph.Builder.normalizeRowsFast rows = Vector.map Hex.SparseGraph.Builder.normalize rows

@[csimp]

theorem Hex.SparseGraph.Builder.normalizeRows_eq_map : @normalizeRows = @normalizeRowsFast

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

Build from unordered Fin pairs, collapsing duplicates and dropping loops. Scattering and packing are linear; each row is sorted separately.

Equations

• Hex.SparseGraph.ofEdges edges = Hex.SparseGraph.ofRows (Hex.SparseGraph.Builder.normalizeRows (Hex.SparseGraph.Builder.scatter edges)) ⋯ ⋯ ⋯

@[simp]

theorem Hex.SparseGraph.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)))

@[simp]

theorem Hex.SparseGraph.toDense_ofEdges {n : Nat} (edges : List (Fin n × Fin n)) : (ofEdges edges).toDense = Graph.ofEdges edges

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

Checked edge-list builder: reject loops and out-of-range endpoints, otherwise normalize duplicate undirected pairs into compressed rows.

Equations

• Hex.SparseGraph.ofEdges? n edges = if h : edges.all (Hex.Graph.validEdge n) = true then some (Hex.SparseGraph.ofEdges (Hex.SparseGraph.Builder.checked n edges h)) else none

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

@[simp]

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

theorem Hex.SparseGraph.toDense_ofEdges? (n : Nat) (edges : List (Nat × Nat)) : Option.map toDense (ofEdges? n edges) = Graph.ofEdges? n edges

The two checked constructors accept the same inputs and represent the same graph.

def Hex.SparseGraph.edges {n : Nat} (G : SparseGraph n) : List (Fin n × Fin n)

Enumerate each undirected edge once, in increasing endpoint order.

Equations

• G.edges = List.flatMap (fun (i : Fin n) => List.map (fun (j : Fin n) => (i, j)) (List.filter (fun (j : Fin n) => decide (i < j)) (G.nbrs i).toList)) (List.finRange n)

@[simp]

theorem Hex.SparseGraph.mem_edges {n : Nat} (G : SparseGraph n) (i j : Fin n) : (i, j) ∈ G.edges ↔ i < j ∧ G.adj i j = true

@[simp]

theorem Hex.SparseGraph.ofEdges_edges {n : Nat} (G : SparseGraph n) : ofEdges G.edges = G