def Hex.SparseGraph.offsetsFrom {α : Type u_1} : List (List α) → Nat → List Nat

Kernel-reducible offset accumulation, including the final endpoint.

Equations

• Hex.SparseGraph.offsetsFrom [] x✝ = [x✝]
• Hex.SparseGraph.offsetsFrom (row :: rows) x✝ = x✝ :: Hex.SparseGraph.offsetsFrom rows (x✝ + row.length)

@[simp]

theorem Hex.SparseGraph.offsetsFrom_eq {α : Type u_1} (rows : List (List α)) (start : Nat) : offsetsFrom rows start = List.scanl (fun (off : Nat) (row : List α) => off + row.length) start rows

def Hex.SparseGraph.offsetsOf {α : Type u_1} (rows : List (List α)) : List Nat

Offsets of consecutive adjacency rows, including the final endpoint.

Equations

• Hex.SparseGraph.offsetsOf rows = Hex.SparseGraph.offsetsFrom rows 0

@[simp]

theorem Hex.SparseGraph.length_offsetsOf {α : Type u_1} (rows : List (List α)) : (offsetsOf rows).length = rows.length + 1

theorem Hex.SparseGraph.get_offsetsOf {α : Type u_1} (rows : List (List α)) (i : Nat) (hi : i ≤ rows.length) : (offsetsOf rows)[i] = (List.take i rows).flatten.length

An offset is the size of the preceding rows.

def Hex.SparseGraph.row {α : Type u_1} (offsets : Array Nat) (neighbors : Array α) (i : Nat) : Array α

A row of compressed adjacency, with an exclusive end offset.

Equations

• Hex.SparseGraph.row offsets neighbors i = neighbors.extract offsets[i]! offsets[i + 1]!

theorem Hex.SparseGraph.row_pack {α : Type u_1} (rows : List (List α)) (i : Nat) (hi : i < rows.length) : (row (offsetsOf rows).toArray rows.flatten.toArray i).toList = rows[i]

Packing consecutive rows and extracting one recovers it exactly.

def Hex.SparseGraph.Layout {α : Type u_1} (n : Nat) (offsets : Array Nat) (neighbors : Array α) : Prop

The arrays consist of exactly n consecutive rows, without gaps or padding. The row witness is proof data and is erased from the executable graph.

Equations

• Hex.SparseGraph.Layout n offsets neighbors = ∃ (rows : List (List α)), rows.length = n ∧ offsets = (Hex.SparseGraph.offsetsOf rows).toArray ∧ neighbors = rows.flatten.toArray

structure Hex.SparseGraph (n : Nat) : Type

A finite simple undirected graph with compressed, sorted adjacency lists.

• offsets : Array Nat

  Start of each row and the final endpoint.

• neighbors : Array (Fin n)

  Consecutive neighbour lists.

• layout : Layout n self.offsets self.neighbors

  Every adjacency entry belongs to exactly one row.

• sorted (i : Fin n) : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) (row self.offsets self.neighbors ↑i).toList

  Rows are strictly increasing, hence duplicate-free.

• symm (i j : Fin n) : j ∈ row self.offsets self.neighbors ↑i ↔ i ∈ row self.offsets self.neighbors ↑j

  Every edge has its reverse.

• loopless (i : Fin n) : ¬i ∈ row self.offsets self.neighbors ↑i

  No vertex is adjacent to itself.

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

The sorted neighbours of a vertex. Extracting a row copies its entries.

Equations

• G.nbrs i = Hex.SparseGraph.row G.offsets G.neighbors ↑i

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

Adjacency is membership in a compressed row.

Equations

• G.adj i j = (G.nbrs i).contains j

@[simp]

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

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

@[simp]

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

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

Degree is the difference between consecutive offsets.

Equations

• G.degree i = G.offsets[↑i + 1]! - G.offsets[↑i]!

def Hex.SparseGraph.ofRows {n : Nat} (rows : Vector (List (Fin n)) n) (hs : ∀ (i : Fin n), List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) rows[i]) (hr : ∀ (i j : Fin n), j ∈ rows[i] ↔ i ∈ rows[j]) (hl : ∀ (i : Fin n), ¬i ∈ rows[i]) : SparseGraph n

Pack a vector of sorted, symmetric, loopless neighbour lists.

Equations

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

@[simp]

theorem Hex.SparseGraph.nbrs_ofRows {n : Nat} (rows : Vector (List (Fin n)) n) (hs : ∀ (i : Fin n), List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) rows[i]) (hr : ∀ (i j : Fin n), j ∈ rows[i] ↔ i ∈ rows[j]) (hl : ∀ (i : Fin n), ¬i ∈ rows[i]) (i : Fin n) : ((ofRows rows hs hr hl).nbrs i).toList = rows[i]

def Hex.SparseGraph.toDense {n : Nat} (G : SparseGraph n) : Graph n

Dense conversion is explicit and allocates the full Boolean matrix.

Equations

• G.toDense = Hex.Graph.ofAdj G.adj ⋯ ⋯

@[simp]

theorem Hex.SparseGraph.adj_toDense {n : Nat} (G : SparseGraph n) (i j : Fin n) : G.toDense.adj i j = G.adj i j

@[simp]

theorem Hex.SparseGraph.size_offsets {n : Nat} (G : SparseGraph n) : G.offsets.size = n + 1

The offset array includes both endpoints of every row.

@[simp]

theorem Hex.SparseGraph.offset_zero {n : Nat} (G : SparseGraph n) : G.offsets[0]! = 0

@[simp]

theorem Hex.SparseGraph.offset_last {n : Nat} (G : SparseGraph n) : G.offsets[n]! = G.neighbors.size

theorem Hex.SparseGraph.degree_eq_size {n : Nat} (G : SparseGraph n) (i : Fin n) : G.degree i = (G.nbrs i).size

The constant-time degree operation counts the entries of the row.

theorem Hex.SparseGraph.ext_arrays {n : Nat} {G H : SparseGraph n} (ho : G.offsets = H.offsets) (hn : G.neighbors = H.neighbors) : G = H

Equality of the two stored arrays determines the graph.

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

Sorted rows and a packed layout make graph equality extensional.

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

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

@[instance_reducible]

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

Equations

• G.instDecidableEq H = if ho : G.offsets = H.offsets then if hn : G.neighbors = H.neighbors then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

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

The edgeless graph stores n + 1 zero offsets and no neighbours.

Equations

• Hex.SparseGraph.empty n = Hex.SparseGraph.ofRows (Vector.replicate n []) ⋯ ⋯ ⋯

@[simp]

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

def Hex.Graph.toSparse {n : Nat} (G : Graph n) : SparseGraph n

Explicit conversion scans the dense matrix once to build sorted sparse rows.

Equations

• G.toSparse = Hex.SparseGraph.ofRows (Vector.ofFn fun (i : Fin n) => (G.nbrs i).toList) ⋯ ⋯ ⋯

@[simp]

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

@[simp]

theorem Hex.Graph.toDense_toSparse {n : Nat} (G : Graph n) : G.toSparse.toDense = G

@[simp]

theorem Hex.SparseGraph.toSparse_toDense {n : Nat} (G : SparseGraph n) : G.toDense.toSparse = G