Finite folding of labelled inverse multigraphs

This module implements the quotient step at the heart of Stallings folding. The implementation is deliberately finite and exhaustive: it intersects all equivalence relations that make the labelled multigraph deterministic. This is a simple reference algorithm; a union-find implementation can later replace it without changing the correctness interface.

structure Stallings.InverseMultigraph (V : Type u_1) : Type u_1

An inverse-labelled multigraph with finite sets of outgoing targets. Multiple edges with the same source and label are allowed before folding.

• edges : V → Letter → Finset V

  The finite collection of targets with a given source and label.

• inverse_edges (v : V) (x : Letter) (w : V) : w ∈ self.edges v x ↔ v ∈ self.edges w (letterInv x)

def Stallings.IsFoldCongruence {V : Type u_1} (G : InverseMultigraph V) (r : V → V → Bool) : Prop

A Boolean relation is a fold congruence if it is an equivalence relation and equivalent vertices have equivalent targets along equally-labelled edges.

Equations

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

@[instance_reducible]

instance Stallings.foldCongruenceDecidable {V : Type u_1} [Fintype V] [DecidableEq V] (G : InverseMultigraph V) (r : V → V → Bool) : Decidable (IsFoldCongruence G r)

Equations

• Stallings.foldCongruenceDecidable G r = id inferInstance

def Stallings.foldRel {V : Type u_1} (G : InverseMultigraph V) (v w : V) : Prop

Vertices are equivalent after all possible folds have been performed.

For a finite vertex type, the quantification is over a finite type of Boolean relations, so this relation is decidable and executable.

Equations

• Stallings.foldRel G v w = ∀ (r : V → V → Bool), Stallings.IsFoldCongruence G r → r v w = true

@[instance_reducible]

instance Stallings.foldRelDecidable {V : Type u_1} [Fintype V] [DecidableEq V] (G : InverseMultigraph V) (v w : V) : Decidable (foldRel G v w)

Equations

• Stallings.foldRelDecidable G v w = id inferInstance

theorem Stallings.foldRel.refl {V : Type u_1} (G : InverseMultigraph V) (v : V) : foldRel G v v

theorem Stallings.foldRel.symm {V : Type u_1} (G : InverseMultigraph V) {v w : V} (h : foldRel G v w) : foldRel G w v

theorem Stallings.foldRel.trans {V : Type u_1} (G : InverseMultigraph V) {u v w : V} (huv : foldRel G u v) (hvw : foldRel G v w) : foldRel G u w

theorem Stallings.foldRel.edge_congr {V : Type u_1} (G : InverseMultigraph V) {v w u t : V} {x : Letter} (hvw : foldRel G v w) (hu : u ∈ G.edges v x) (ht : t ∈ G.edges w x) : foldRel G u t

def Stallings.foldRep {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (v : V) : V

The least representative of a fold-equivalence class.

Equations

• Stallings.foldRep G v = {w : V | Stallings.foldRel G w v}.min' ⋯

theorem Stallings.foldRep_rel {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (v : V) : foldRel G (foldRep G v) v

theorem Stallings.foldRep_eq_of_rel {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) {v w : V} (h : foldRel G v w) : foldRep G v = foldRep G w

theorem Stallings.foldRep_idem {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (v : V) : foldRep G (foldRep G v) = foldRep G v

def Stallings.foldTargets {V : Type u_1} [Fintype V] [DecidableEq V] (G : InverseMultigraph V) (v : V) (x : Letter) : Finset V

All original targets reachable from any vertex in the current fold class.

Equations

• Stallings.foldTargets G v x = {t : V | ∃ (u : V), Stallings.foldRel G u v ∧ t ∈ G.edges u x}

theorem Stallings.foldTargets_pair {V : Type u_1} [Fintype V] [DecidableEq V] (G : InverseMultigraph V) (v : V) (x : Letter) {u t : V} (hu : u ∈ foldTargets G v x) (ht : t ∈ foldTargets G v x) : foldRel G u t

Two targets of the same labelled edge out of a fold class are themselves fold-equivalent.

def Stallings.foldedNextCore {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (v : V) (x : Letter) : Option V

A deterministic representative transition before restricting to canonical representatives.

Equations

• Stallings.foldedNextCore G v x = if h : (Stallings.foldTargets G v x).Nonempty then some (Stallings.foldRep G ((Stallings.foldTargets G v x).min' h)) else none

def Stallings.foldedNext {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (v : V) (x : Letter) : Option V

The deterministic transition produced by folding.

Equations

• Stallings.foldedNext G v x = if v = Stallings.foldRep G v then Stallings.foldedNextCore G v x else none

def Stallings.foldAutomaton {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (base : V) : InverseAutomaton V

The deterministic inverse automaton obtained by quotienting the multigraph.

Equations

• Stallings.foldAutomaton G base = { base := Stallings.foldRep G base, next := Stallings.foldedNext G, inverse_next := ⋯ }

inductive Stallings.InverseMultigraph.Walk {V : Type u_1} (G : InverseMultigraph V) : V → Word → V → Prop

A path in a multigraph records one chosen edge for each letter.

• nil {V : Type u_1} {G : InverseMultigraph V} (v : V) : G.Walk v [] v
• cons {V : Type u_1} {G : InverseMultigraph V} {v u z : V} {x : Letter} {w : Word} (edge : u ∈ G.edges v x) (tail : G.Walk u w z) : G.Walk v (x :: w) z

def Stallings.InverseMultigraph.loopSubgroup {V : Type u_1} (G : InverseMultigraph V) (base : V) : Subgroup Free

The subgroup generated by labels of based loops in the multigraph.

Equations

• G.loopSubgroup base = Subgroup.closure {g : Stallings.Free | ∃ (w : Stallings.Word), Stallings.wordEval w = g ∧ G.Walk base w base}

theorem Stallings.foldedNext_of_edge {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) {v t : V} {x : Letter} (hedge : t ∈ G.edges v x) : foldedNext G (foldRep G v) x = some (foldRep G t)

Every original edge induces the corresponding transition between fold representatives.

theorem Stallings.foldWalk {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (base v z : V) {w : Word} (h : G.Walk v w z) : (foldAutomaton G base).run (foldRep G v) w = some (foldRep G z)

Folding preserves every path in the original multigraph, after mapping its endpoints to their canonical representatives.

def Stallings.CosetEquivalent (H : Subgroup Free) (g h : Free) : Prop

Equality of right cosets of a subgroup, in element form.

Equations

• Stallings.CosetEquivalent H g h = (g * h⁻¹ ∈ H)

theorem Stallings.CosetEquivalent.refl (H : Subgroup Free) (g : Free) : CosetEquivalent H g g

theorem Stallings.CosetEquivalent.symm {H : Subgroup Free} {g h : Free} (gh : CosetEquivalent H g h) : CosetEquivalent H h g

theorem Stallings.CosetEquivalent.trans {H : Subgroup Free} {g h k : Free} (gh : CosetEquivalent H g h) (hk : CosetEquivalent H h k) : CosetEquivalent H g k

theorem Stallings.CosetEquivalent.mem_of_mem_and_rel {H : Subgroup Free} {g h : Free} (hgh : CosetEquivalent H g h) (hg : g ∈ H) : h ∈ H

theorem Stallings.CosetEquivalent.right_mul {H : Subgroup Free} {g h : Free} (gh : CosetEquivalent H g h) (x : Free) : CosetEquivalent H (g * x) (h * x)

def Stallings.HasCosetPotential {V : Type u_1} (G : InverseMultigraph V) (H : Subgroup Free) (potential : V → Free) : Prop

A potential assigns a free-group value to each vertex, consistently up to left multiplication by H along every labelled edge.

Equations

• Stallings.HasCosetPotential G H potential = ∀ {v : V} {x : Stallings.Letter} {w : V}, w ∈ G.edges v x → Stallings.CosetEquivalent H (potential w) (potential v * Stallings.letterEval x)

theorem Stallings.InverseMultigraph.walk_cosetPotential {V : Type u_1} (G : InverseMultigraph V) (H : Subgroup Free) (potential : V → Free) (hpotential : HasCosetPotential G H potential) {v z : V} {w : Word} : G.Walk v w z → CosetEquivalent H (potential z) (potential v * wordEval w)

Along any path, a coset potential changes by the value of the path label.

theorem Stallings.foldRel_cosetPotential {V : Type u_1} (G : InverseMultigraph V) (H : Subgroup Free) (potential : V → Free) (hpotential : HasCosetPotential G H potential) {v w : V} (hvw : foldRel G v w) : CosetEquivalent H (potential v) (potential w)

A fold never identifies vertices with different subgroup cosets, whenever the input graph has a compatible coset potential.

theorem Stallings.foldedNext_cosetPotential {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (base : V) (H : Subgroup Free) (potential : V → Free) (hpotential : HasCosetPotential G H potential) {v t : V} {x : Letter} (hnext : (foldAutomaton G base).next v x = some t) : CosetEquivalent H (potential t) (potential v * letterEval x)

Each transition made by the folded automaton respects the subgroup potential.

theorem Stallings.run_cosetPotential {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (base : V) (H : Subgroup Free) (potential : V → Free) (hpotential : HasCosetPotential G H potential) {v t : V} {w : Word} : (foldAutomaton G base).run v w = some t → CosetEquivalent H (potential t) (potential v * wordEval w)

A successful folded traversal transports the potential by the value of its label word.

theorem Stallings.foldAutomaton_loopSubgroup_eq {V : Type u_1} [Fintype V] [DecidableEq V] [LinearOrder V] (G : InverseMultigraph V) (base : V) (potential : V → Free) (hpotential : HasCosetPotential G (G.loopSubgroup base) potential) (hbase : potential base = 1) : (foldAutomaton G base).loopSubgroup = G.loopSubgroup base

Folding preserves the subgroup generated by based loop labels, provided the original graph carries the canonical coset potential.