@[reducible, inline]

abbrev Hex.PermGroup.Word {n : Nat} (S : Array (Perm n)) : Type

A word in signed original-generator indices. true denotes an inverse.

Equations

• Hex.PermGroup.Word S = List (Fin S.size × Bool)

def Hex.PermGroup.Word.letter {n : Nat} (S : Array (Perm n)) (a : Fin S.size × Bool) : Perm n

Equations

• Hex.PermGroup.Word.letter S a = if a.snd = true then S[↑a.fst].inv else S[↑a.fst]

def Hex.PermGroup.Word.eval {n : Nat} (S : Array (Perm n)) : Word S → Perm n

Words use left-action composition: the rightmost letter acts first.

Equations

• Hex.PermGroup.Word.eval S [] = Hex.Perm.id n
• Hex.PermGroup.Word.eval S (a :: w) = (Hex.PermGroup.Word.letter S a).comp (Hex.PermGroup.Word.eval S w)

@[simp]

theorem Hex.PermGroup.Word.eval_nil {n : Nat} (S : Array (Perm n)) : eval S [] = Perm.id n

@[simp]

theorem Hex.PermGroup.Word.eval_cons {n : Nat} (S : Array (Perm n)) (a : Fin S.size × Bool) (w : Word S) : eval S (a :: w) = (letter S a).comp (eval S w)

theorem Hex.PermGroup.Word.eval_append {n : Nat} (S : Array (Perm n)) (u v : Word S) : eval S (u ++ v) = (eval S u).comp (eval S v)

def Hex.PermGroup.Word.inv {n : Nat} {S : Array (Perm n)} (w : Word S) : Word S

Invert a word by reversing its letters and changing their signs.

Equations

• w.inv = List.map (fun (a : Fin S.size × Bool) => (a.fst, !a.snd)) (List.reverse w)

@[simp]

theorem Hex.PermGroup.Word.letter_inv {n : Nat} (S : Array (Perm n)) (a : Fin S.size × Bool) : letter S (a.fst, !a.snd) = (letter S a).inv

theorem Hex.PermGroup.Word.eval_inv {n : Nat} (S : Array (Perm n)) (w : Word S) : eval S w.inv = (eval S w).inv

theorem Hex.PermGroup.Word.eval_generated {n : Nat} (S : Array (Perm n)) (w : Word S) : Generated S (eval S w)

def Hex.PermGroup.Word.push {n : Nat} {S : Array (Perm n)} (a : Fin S.size × Bool) : Word S → Word S

Prepend one letter, cancelling it against the first letter of w when that letter is its inverse.

Equations

• Hex.PermGroup.Word.push a [] = [a]
• Hex.PermGroup.Word.push a (a_1 :: w) = if a_1.fst = a.fst ∧ a_1.snd = !a.snd then w else a :: a_1 :: w

theorem Hex.PermGroup.Word.eval_push {n : Nat} (S : Array (Perm n)) (a : Fin S.size × Bool) (w : Word S) : eval S (push a w) = (letter S a).comp (eval S w)

def Hex.PermGroup.Word.reduce {n : Nat} {S : Array (Perm n)} : Word S → Word S

Free reduction: cancel adjacent letters (i, b) and (i, !b) until none remain. The result has no such adjacent pair.

Equations

• Hex.PermGroup.Word.reduce [] = []
• Hex.PermGroup.Word.reduce (a :: w) = Hex.PermGroup.Word.push a (Hex.PermGroup.Word.reduce w)

def Hex.PermGroup.Word.reduceTR {n : Nat} {S : Array (Perm n)} (w : Word S) : Word S

reduce in constant stack space: push the letters from the right end.

Equations

• w.reduceTR = List.foldl (fun (acc : Hex.PermGroup.Word S) (a : Fin S.size × Bool) => Hex.PermGroup.Word.push a acc) [] (List.reverse w)

@[csimp]

theorem Hex.PermGroup.Word.reduce_eq_reduceTR : @reduce = @reduceTR

@[simp]

theorem Hex.PermGroup.Word.eval_reduce {n : Nat} (S : Array (Perm n)) (w : Word S) : eval S w.reduce = eval S w

def Hex.PermGroup.Word.toString {n : Nat} {S : Array (Perm n)} (w : Word S) : String

Display a word as a product of generator names, such as g0 * g1⁻¹, with g i naming S[i]. The empty word is displayed as 1.

Equations

• w.toString = if List.isEmpty w = true then "1" else " * ".intercalate (List.map (fun (a : Fin S.size × Bool) => "g" ++ (↑a.fst).repr ++ if a.snd = true then "⁻¹" else "") w)

theorem Hex.PermGroup.generated_iff_word {n : Nat} {S : Array (Perm n)} {p : Perm n} : Generated S p ↔ ∃ (w : Word S), Word.eval S w = p

The closure predicate is exactly evaluation of finite signed words.

inductive Hex.PermGroup.Node : Type

One node in a straight-line program. References address earlier nodes only.

• id : Node
• generator (index : Nat) : Node
• inv (index : Nat) : Node
• comp (left right : Nat) : Node

@[instance_reducible]

instance Hex.PermGroup.instDecidableEqNode : DecidableEq Node

Equations

• Hex.PermGroup.instDecidableEqNode = Hex.PermGroup.instDecidableEqNode.decEq

def Hex.PermGroup.instDecidableEqNode.decEq (x✝ x✝¹ : Node) : Decidable (x✝ = x✝¹)

Equations

• Hex.PermGroup.instDecidableEqNode.decEq Hex.PermGroup.Node.id Hex.PermGroup.Node.id = isTrue ⋯
• Hex.PermGroup.instDecidableEqNode.decEq Hex.PermGroup.Node.id (Hex.PermGroup.Node.generator index) = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq Hex.PermGroup.Node.id (Hex.PermGroup.Node.inv index) = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq Hex.PermGroup.Node.id (Hex.PermGroup.Node.comp left right) = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.generator index) Hex.PermGroup.Node.id = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.generator a) (Hex.PermGroup.Node.generator b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.generator index) (Hex.PermGroup.Node.inv index_1) = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.generator index) (Hex.PermGroup.Node.comp left right) = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.inv index) Hex.PermGroup.Node.id = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.inv index) (Hex.PermGroup.Node.generator index_1) = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.inv a) (Hex.PermGroup.Node.inv b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.inv index) (Hex.PermGroup.Node.comp left right) = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.comp left right) Hex.PermGroup.Node.id = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.comp left right) (Hex.PermGroup.Node.generator index) = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.comp left right) (Hex.PermGroup.Node.inv index) = isFalse ⋯
• Hex.PermGroup.instDecidableEqNode.decEq (Hex.PermGroup.Node.comp a a_1) (Hex.PermGroup.Node.comp b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Hex.PermGroup.instReprNode.repr : Node → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.instReprNode.repr Hex.PermGroup.Node.id prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.PermGroup.Node.id")).group prec✝

@[instance_reducible]

instance Hex.PermGroup.instReprNode : Repr Node

Equations

• Hex.PermGroup.instReprNode = { reprPrec := Hex.PermGroup.instReprNode.repr }

structure Hex.PermGroup.Program : Type

Raw program data. Evaluation rejects an invalid node, even if unreachable from the root, and rejects an out-of-range root.

• nodes : Array Node
• root : Nat

def Hex.PermGroup.instDecidableEqProgram.decEq (x✝ x✝¹ : Program) : Decidable (x✝ = x✝¹)

Equations

• Hex.PermGroup.instDecidableEqProgram.decEq { nodes := a, root := a_1 } { nodes := b, root := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.PermGroup.instDecidableEqProgram : DecidableEq Program

Equations

• Hex.PermGroup.instDecidableEqProgram = Hex.PermGroup.instDecidableEqProgram.decEq

def Hex.PermGroup.instReprProgram.repr : Program → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.PermGroup.instReprProgram : Repr Program

Equations

• Hex.PermGroup.instReprProgram = { reprPrec := Hex.PermGroup.instReprProgram.repr }

def Hex.PermGroup.Program.evalNode {n : Nat} (S : Array (Perm n)) (values : Array { p : Perm n // Generated S p }) : Node → Option { p : Perm n // Generated S p }

Evaluate one node against the already evaluated values. Its result carries provenance, which is erased by compilation.

Equations

• Hex.PermGroup.Program.evalNode S values Hex.PermGroup.Node.id = some ⟨Hex.Perm.id n, ⋯⟩
• Hex.PermGroup.Program.evalNode S values (Hex.PermGroup.Node.generator i) = if h : i < S.size then some ⟨S[i], ⋯⟩ else none
• Hex.PermGroup.Program.evalNode S values (Hex.PermGroup.Node.inv i) = do let p ← values[i]? pure ⟨p.val.inv, ⋯⟩
• Hex.PermGroup.Program.evalNode S values (Hex.PermGroup.Node.comp i j) = do let p ← values[i]? let q ← values[j]? pure ⟨p.val.comp q.val, ⋯⟩

def Hex.PermGroup.Program.evalNodes {n : Nat} (S : Array (Perm n)) : List Node → Array { p : Perm n // Generated S p } → Option (Array { p : Perm n // Generated S p })

Check every node in order, using only the values for references.

Equations

• Hex.PermGroup.Program.evalNodes S [] x✝ = some x✝
• Hex.PermGroup.Program.evalNodes S (node :: rest) x✝ = do let p ← Hex.PermGroup.Program.evalNode S x✝ node Hex.PermGroup.Program.evalNodes S rest (x✝.push p)

def Hex.PermGroup.Program.evalCertified {n : Nat} (S : Array (Perm n)) (program : Program) : Option { p : Perm n // Generated S p }

Evaluate the root of a fully checked program.

Equations

• Hex.PermGroup.Program.evalCertified S program = do let values ← Hex.PermGroup.Program.evalNodes S program.nodes.toList #[] values[program.root]?

def Hex.PermGroup.Program.eval {n : Nat} (S : Array (Perm n)) (program : Program) : Option (Perm n)

The executable permutation denoted by a program, or failure for malformed references or generator indices.

Equations

• Hex.PermGroup.Program.eval S program = Option.map Subtype.val (Hex.PermGroup.Program.evalCertified S program)

theorem Hex.PermGroup.Program.eval_sound {n : Nat} {S : Array (Perm n)} {program : Program} {p : Perm n} (h : eval S program = some p) : Generated S p

def Hex.PermGroup.Program.wordNode {n : Nat} (S : Array (Perm n)) (words : Array (Thunk (Word S))) : Node → Option (Thunk (Word S))

The word of one node, computed from the words of earlier nodes. Words are deferred, so that only nodes reachable from the root are ever expanded, while the checks on indices and references match evalNode.

Equations

• Hex.PermGroup.Program.wordNode S words Hex.PermGroup.Node.id = some (Thunk.pure [])
• Hex.PermGroup.Program.wordNode S words (Hex.PermGroup.Node.generator i) = if h : i < S.size then some (Thunk.pure [(⟨i, h⟩, false)]) else none
• Hex.PermGroup.Program.wordNode S words (Hex.PermGroup.Node.inv i) = do let u ← words[i]? pure { fn := fun (x : Unit) => u.get.inv }
• Hex.PermGroup.Program.wordNode S words (Hex.PermGroup.Node.comp i j) = do let u ← words[i]? let v ← words[j]? pure { fn := fun (x : Unit) => (u.get ++ v.get).reduce }

def Hex.PermGroup.Program.wordNodes {n : Nat} (S : Array (Perm n)) : List Node → Array (Thunk (Word S)) → Option (Array (Thunk (Word S)))

Check every node in order, as evalNodes does, recording deferred words.

Equations

• Hex.PermGroup.Program.wordNodes S [] x✝ = some x✝
• Hex.PermGroup.Program.wordNodes S (node :: rest) x✝ = do let w ← Hex.PermGroup.Program.wordNode S x✝ node Hex.PermGroup.Program.wordNodes S rest (x✝.push w)

def Hex.PermGroup.Program.toWord? {n : Nat} (S : Array (Perm n)) (program : Program) : Option (Word S)

The freely reduced word in the original generators obtained by expanding the nodes reachable from the root. It is none exactly when eval S program is none. Expansion does not share subexpressions, so the word can be exponentially longer than the program. Use it to display short programs, not as a certificate.

Equations

• Hex.PermGroup.Program.toWord? S program = do let words ← Hex.PermGroup.Program.wordNodes S program.nodes.toList #[] let w ← words[program.root]? pure w.get

def Hex.PermGroup.Program.reachable (program : Program) : Array Bool

The nodes the root depends on. References point to earlier nodes, so one pass from the root downwards marks them all.

Equations

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

def Hex.PermGroup.Program.toWordImpl {n : Nat} (S : Array (Perm n)) (program : Program) : Option (Word S)

toWord? for compiled code: before reading the root, force the deferred words of the reachable nodes in increasing order, so that each finds its operands already computed and expansion never recurses through the program's depth. Unreachable nodes are still never expanded.

Equations

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

@[csimp]

theorem Hex.PermGroup.Program.toWord?_eq_toWordImpl : @toWord? = @toWordImpl

theorem Hex.PermGroup.Program.eval_of_toWord? {n : Nat} {S : Array (Perm n)} {program : Program} {w : Word S} (h : toWord? S program = some w) : eval S program = some (Word.eval S w)

A word obtained from a program evaluates to the program's value.

theorem Hex.PermGroup.Program.isSome_toWord? {n : Nat} (S : Array (Perm n)) (program : Program) : (toWord? S program).isSome = (eval S program).isSome

Flattening fails exactly when evaluation fails.

def Hex.PermGroup.Program.lengths (program : Program) : Array Nat

For each node, the length of the word toWord? expands it to before free reduction, computed with Nat arithmetic and without expanding. A reference to a missing node counts as length zero.

Equations

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

def Hex.PermGroup.Program.expandedLength (program : Program) : Nat

The length of the root's word before free reduction, an upper bound on the length of the word toWord? returns.

Equations

• program.expandedLength = program.lengths[program.root]?.getD 0

inductive Hex.PermGroup.Program.WordError : Type

Why toWordCapped returned no word.

• invalid : WordError

  The program does not evaluate.

• tooLong (length : Nat) : WordError

  The word before free reduction would have this many letters, more than the cap.

@[instance_reducible]

instance Hex.PermGroup.Program.instDecidableEqWordError : DecidableEq WordError

Equations

• Hex.PermGroup.Program.instDecidableEqWordError = Hex.PermGroup.Program.instDecidableEqWordError.decEq

def Hex.PermGroup.Program.instDecidableEqWordError.decEq (x✝ x✝¹ : WordError) : Decidable (x✝ = x✝¹)

Equations

• Hex.PermGroup.Program.instDecidableEqWordError.decEq Hex.PermGroup.Program.WordError.invalid Hex.PermGroup.Program.WordError.invalid = isTrue ⋯
• Hex.PermGroup.Program.instDecidableEqWordError.decEq Hex.PermGroup.Program.WordError.invalid (Hex.PermGroup.Program.WordError.tooLong length) = isFalse ⋯
• Hex.PermGroup.Program.instDecidableEqWordError.decEq (Hex.PermGroup.Program.WordError.tooLong length) Hex.PermGroup.Program.WordError.invalid = isFalse ⋯
• Hex.PermGroup.Program.instDecidableEqWordError.decEq (Hex.PermGroup.Program.WordError.tooLong a) (Hex.PermGroup.Program.WordError.tooLong b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Hex.PermGroup.Program.instReprWordError.repr : WordError → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.PermGroup.Program.instReprWordError : Repr WordError

Equations

• Hex.PermGroup.Program.instReprWordError = { reprPrec := Hex.PermGroup.Program.instReprWordError.repr }

def Hex.PermGroup.Program.toWordCapped {n : Nat} (cap : Nat) (S : Array (Perm n)) (program : Program) : Except WordError (Word S)

toWord? with a cap on the word's length before free reduction. The length is computed from the program first, so a word over the cap is never expanded; this check precedes the validity check.

Equations

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

theorem Hex.PermGroup.Program.toWordCapped_ok {n cap : Nat} {S : Array (Perm n)} {program : Program} {w : Word S} (h : toWordCapped cap S program = Except.ok w) : eval S program = some (Word.eval S w)

theorem Hex.PermGroup.Program.toWordCapped_tooLong {n cap : Nat} {S : Array (Perm n)} {program : Program} {length : Nat} (h : toWordCapped cap S program = Except.error (WordError.tooLong length)) : length = program.expandedLength ∧ cap < length

theorem Hex.PermGroup.Program.toWordCapped_invalid {n cap : Nat} {S : Array (Perm n)} {program : Program} (h : toWordCapped cap S program = Except.error WordError.invalid) : eval S program = none

def Hex.PermGroup.checkWord {n : Nat} (S : Array (Perm n)) (p : Perm n) (program : Program) : Bool

Check that a program in the original generators denotes the claimed element.

Equations

• Hex.PermGroup.checkWord S p program = decide (Hex.PermGroup.Program.eval S program = some p)

theorem Hex.PermGroup.checkWord_sound {n : Nat} {S : Array (Perm n)} {p : Perm n} {program : Program} (h : checkWord S p program = true) : Generated S p