Simproc deciding Matrix.IsIndecomposable

Matrix.reduceIsIndecomposable rewrites M.IsIndecomposable to True or False for a closed square matrix literal M indexed by Fin n. This requires a kernel-decidable equality for the matrix entry type.

This is equivalent to determining whether the directed graph corresponding to M is strongly connected.

Main definitions

• Matrix.reduceIsIndecomposable: the simproc deciding M.IsIndecomposable.
• SpansFrom: states that every vertex is visited following a list of edges starting from a root.
• isClosed: tests whether a set of vertices has no edges leaving it.
• packedAdj: a Boolean adjacency matrix stored as the bits of a natural number computed from a matrix literal by packRows.
• decideStronglyConnected: searches the graph from and to vertex 0, returning two spanning trees or a closed set of vertices.

Implementation notes

This simproc simply runs two bfs on the graph from vertex 0 forwards and backwards. If all vertices are reached in both passes, then the indecomposability is certified by the two search trees. Otherwise, M is decomposable, witnessed by a set of rows whose entries outside the set evaluate to 0.

There is an existing implementation of Tarjan's algorithm at Tactic.Order.Graph.findSCCs, but it doesn't return a witness for the strongly connected components, and the algorithm is also an overkill.

The Boolean adjacency matrix of a !![…] literal is packed into one natural number, with entry (i, j) at bit i * n + j, and both certificates are checked against that number, since reading the literal by position costs the kernel a walk per entry.

Reachability in a Boolean adjacency matrix

def Mathlib.Tactic.Matrix.IsIndecomposable.reached {n : ℕ} (adj : Fin n → Fin n → Bool) (s : ℕ) (es : List (Fin n × Fin n)) : ℕ

The vertices reached from the set bits of s by following the edges es in order. An edge counts only when it leaves a vertex already reached and is an edge of adj.

Equations

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

theorem Mathlib.Tactic.Matrix.IsIndecomposable.reflTransGen_of_testBit_reached {n : ℕ} {adj : Fin n → Fin n → Bool} {root : Fin n} {s : ℕ} {es : List (Fin n × Fin n)} (hs : ∀ (v : Fin n), s.testBit ↑v = true → Relation.ReflTransGen (fun (i j : Fin n) => adj i j = true) root v) {v : Fin n} (hv : (reached adj s es).testBit ↑v = true) : Relation.ReflTransGen (fun (i j : Fin n) => adj i j = true) root v

@[reducible, inline]

abbrev Mathlib.Tactic.Matrix.IsIndecomposable.SpansFrom {n : ℕ} (adj : Fin n → Fin n → Bool) (es : List (Fin n × Fin n)) (root : Fin n) : Prop

The edges es in order reach every vertex of adj starting from root.

Equations

• Mathlib.Tactic.Matrix.IsIndecomposable.SpansFrom adj es root = (Mathlib.Tactic.Matrix.IsIndecomposable.reached adj (1 <<< ↑root) es = 2 ^ n - 1)

theorem Mathlib.Tactic.Matrix.IsIndecomposable.SpansFrom.reflTransGen {n : ℕ} {adj : Fin n → Fin n → Bool} {es : List (Fin n × Fin n)} {root : Fin n} (h : SpansFrom adj es root) (v : Fin n) : Relation.ReflTransGen (fun (i j : Fin n) => adj i j = true) root v

If adj has a spanning list of edges from root, then root reaches every vertex.

Closed sets of vertices in a Boolean adjacency matrix, and the packed version

def Mathlib.Tactic.Matrix.IsIndecomposable.isClosed {n : ℕ} (adj : Fin n → Fin n → Bool) (s : ℕ) : Bool

Whether no edge of adj leaves the set of vertices given by the set bits of s.

Equations

• Mathlib.Tactic.Matrix.IsIndecomposable.isClosed adj s = (List.finRange n).all fun (i : Fin n) => !s.testBit ↑i || (List.finRange n).all fun (j : Fin n) => s.testBit ↑j || !adj i j

def Mathlib.Tactic.Matrix.IsIndecomposable.packedAdj (n bits : ℕ) (i j : Fin n) : Bool

Entry (i, j) of the n × n Boolean adjacency matrix represented by bits.

Equations

• Mathlib.Tactic.Matrix.IsIndecomposable.packedAdj n bits i j = bits.testBit (↑i * n + ↑j)

def Mathlib.Tactic.Matrix.IsIndecomposable.isClosedPacked (n bits s : ℕ) : Bool

Whether no edge of the n × n Boolean adjacency matrix represented by bits leaves the set of vertices given by the set bits of s. Each row of bits is read at once.

Equations

• Mathlib.Tactic.Matrix.IsIndecomposable.isClosedPacked n bits s = (List.range n).all fun (i : ℕ) => have row := bits >>> (i * n) &&& 2 ^ n - 1; !s.testBit i || row &&& s == row

theorem Mathlib.Tactic.Matrix.IsIndecomposable.isClosed_of_isClosedPacked {n bits s : ℕ} (h : isClosedPacked n bits s = true) : isClosed (packedAdj n bits) s = true

Certificates for a matrix from its Boolean adjacency matrix

theorem Mathlib.Tactic.Matrix.IsIndecomposable.isIndecomposable_of_spansFrom {R : Type u_1} [Zero R] {n : ℕ} {M : Matrix (Fin n) (Fin n) R} {adj : Fin n → Fin n → Bool} (hadj : ∀ (i j : Fin n), adj i j = true ↔ M i j ≠ 0) {root : Fin n} {fwd bwd : List (Fin n × Fin n)} (hf : SpansFrom adj fwd root) (hb : SpansFrom (Function.swap adj) bwd root) : M.IsIndecomposable

If both adj and its reverse have spanning edge lists from root, then M is indecomposable (strong connectivity of adj).

theorem Mathlib.Tactic.Matrix.IsIndecomposable.not_isIndecomposable_of_isClosed {R : Type u_1} [Zero R] {n : ℕ} {M : Matrix (Fin n) (Fin n) R} {adj : Fin n → Fin n → Bool} (hadj : ∀ (i j : Fin n), adj i j = true ↔ M i j ≠ 0) {s : ℕ} (h : isClosed adj s = true) {i j : Fin n} (hij : s.testBit ↑i ≠ s.testBit ↑j) : ¬M.IsIndecomposable

If adj has a nonempty proper subset of vertices that is closed, then M is decomposable.

The Boolean adjacency matrix of a matrix literal

def Mathlib.Tactic.Matrix.IsIndecomposable.packRow {R : Type u_1} [Zero R] [DecidableEq R] (row : List R) : ℕ

The nonzero entries of row, as the set bits of a natural number.

Equations

• Mathlib.Tactic.Matrix.IsIndecomposable.packRow row = List.foldr (fun (a : R) (acc : ℕ) => (if a = 0 then 0 else 1) ||| acc <<< 1) 0 row

def Mathlib.Tactic.Matrix.IsIndecomposable.packRows {R : Type u_1} [Zero R] [DecidableEq R] (n : ℕ) (rows : List (List R)) : ℕ

The Boolean adjacency matrix of rows interpreted as an n × n matrix, as the set bits of a natural number with entry (i, j) at bit i * n + j.

Equations

• Mathlib.Tactic.Matrix.IsIndecomposable.packRows n rows = List.foldr (fun (row : List R) (acc : ℕ) => Mathlib.Tactic.Matrix.IsIndecomposable.packRow row &&& 2 ^ n - 1 ||| acc <<< n) 0 rows

theorem Mathlib.Tactic.Matrix.IsIndecomposable.testBit_packRow {R : Type u_1} [Zero R] [DecidableEq R] (row : List R) (j : ℕ) : (packRow row).testBit j = decide (row.getD j 0 ≠ 0)

theorem Mathlib.Tactic.Matrix.IsIndecomposable.testBit_packRows {R : Type u_1} [Zero R] [DecidableEq R] {n : ℕ} (rows : List (List R)) (i : ℕ) {j : ℕ} (hj : j < n) : (packRows n rows).testBit (i * n + j) = decide ((rows.getD i []).getD j 0 ≠ 0)

theorem Mathlib.Tactic.Matrix.IsIndecomposable.packedAdj_packRows_iff {R : Type u_1} [Zero R] [DecidableEq R] {n : ℕ} (rows : List (List R)) (i j : Fin n) : packedAdj n (packRows n rows) i j = true ↔ ofLists n n rows i j ≠ 0

def Mathlib.Tactic.Matrix.IsIndecomposable.bfs (n : ℕ) (adj : ℕ → ℕ → Bool) (root : ℕ) : Array (ℕ × ℕ) × Array Bool

Breadth-first search from root along adj, returning the tree edges in discovery order and the reached vertices.

Equations

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

def Mathlib.Tactic.Matrix.IsIndecomposable.mkEdgeListLitQ (n : ℕ) (edges : Array (ℕ × ℕ)) : Lean.MetaM Q(List (Fin «$n» × Fin «$n»))

The list literal of the edges edges.

Equations

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

inductive Mathlib.Tactic.Matrix.IsIndecomposable.StrongConnectivityResult : Type

The outcome of searching a directed graph from and to vertex 0.

• connected (outTree inTree : Array (ℕ × ℕ)) : StrongConnectivityResult

  The graph is strongly connected, with the spanning out-tree outTree from 0 and in-tree inTree to 0.

• disconnected (closedSet : Array Bool) : StrongConnectivityResult

  The graph is not strongly connected. No edge leaves the nonempty proper set of vertices closedSet.

def Mathlib.Tactic.Matrix.IsIndecomposable.decideStronglyConnected (adjMatrix : Array (Array Bool)) : StrongConnectivityResult

Search the directed graph with Boolean adjacency matrix adjMatrix from and to vertex 0.

Equations

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

def Mathlib.Tactic.Matrix.IsIndecomposable.evalAdjMatrix? {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (dα : Q(DecidableEq «$α»)) (n : ℕ) (lit : Q(List (List «$α»))) : Lean.MetaM (Option (Array (Array Bool)))

The Boolean adjacency matrix of the matrix with rows lit evaluated by the kernel. Returns none if the kernel cannot decide which entries are zero.

The kernel evaluates the packed number packRows n lit and then unpacks the boolean adjacency matrix from the bits. This round trip evaluates every entry in one Kernel.whnf call instead of needing a call per cell (about 2.5x the cost).

Equations

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

def Mathlib.Tactic.Matrix.IsIndecomposable.certifyIsIndecomposable {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (dα : Q(DecidableEq «$α»)) (n : ℕ) (lit : Q(List (List «$α»))) (outTree inTree : Array (ℕ × ℕ)) : Lean.MetaM Q((ofLists «$n» «$n» «$lit»).IsIndecomposable)

Prove that lit interpreted as an n × n matrix is indecomposable using the spanning out-tree outTree from vertex 0 and the in-tree inTree to it in its graph.

Equations

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

def Mathlib.Tactic.Matrix.IsIndecomposable.certifyNotIsIndecomposable {u : Lean.Level} {α : Q(Type u)} (zα : Q(Zero «$α»)) (dα : Q(DecidableEq «$α»)) (n : ℕ) (lit : Q(List (List «$α»))) (closedSet : Array Bool) : Lean.MetaM Q(¬(ofLists «$n» «$n» «$lit»).IsIndecomposable)

Prove that lit interpreted as an n × n matrix is decomposable from a nonempty proper set closedSet of vertices that no edge of its graph leaves.

def Mathlib.Tactic.Matrix.IsIndecomposable.reduceIsIndecomposableCore : Lean.Meta.Simp.Simproc

Core of the Matrix.reduceIsIndecomposable simproc.

Equations

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

def Matrix.reduceIsIndecomposable : Lean.Meta.Simp.Simproc

Matrix.reduceIsIndecomposable decides M.IsIndecomposable for a closed matrix literal M indexed by Fin n with n a numeral, whose entry type has an equality the kernel can decide.

Equations

• Matrix.reduceIsIndecomposable = Mathlib.Tactic.Matrix.IsIndecomposable.reduceIsIndecomposableCore