LeanPool.Polylean.ConjInvLength.LengthBound

inductive LeanPool.Polylean.Letter : Type

The four generators used for words in the conjugation-invariant length example.

• α : Letter
• β : Letter
• α! : Letter
• β! : Letter

@[implicit_reducible]

instance LeanPool.Polylean.instDecidableEqLetter : DecidableEq Letter

Equations

• LeanPool.Polylean.instDecidableEqLetter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanPool.Polylean.instReprLetter.repr : Letter → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LeanPool.Polylean.instReprLetter : Repr Letter

Equations

• LeanPool.Polylean.instReprLetter = { reprPrec := LeanPool.Polylean.instReprLetter.repr }

@[implicit_reducible]

instance LeanPool.Polylean.instHashableLetter : Hashable Letter

Equations

• LeanPool.Polylean.instHashableLetter = { hash := LeanPool.Polylean.instHashableLetter.hash }

def LeanPool.Polylean.instHashableLetter.hash : Letter → UInt64

Equations

• LeanPool.Polylean.instHashableLetter.hash LeanPool.Polylean.Letter.α = 0
• LeanPool.Polylean.instHashableLetter.hash LeanPool.Polylean.Letter.β = 1
• LeanPool.Polylean.instHashableLetter.hash LeanPool.Polylean.Letter.α! = 2
• LeanPool.Polylean.instHashableLetter.hash LeanPool.Polylean.Letter.β! = 3

@[implicit_reducible]

instance LeanPool.Polylean.instInhabitedLetter : Inhabited Letter

Equations

• LeanPool.Polylean.instInhabitedLetter = { default := LeanPool.Polylean.instInhabitedLetter.default }

def LeanPool.Polylean.Letter.toString : Letter → String

Render a letter as a string.

Equations

• LeanPool.Polylean.Letter.α.toString = "α"
• LeanPool.Polylean.Letter.β.toString = "β"
• LeanPool.Polylean.Letter.α!.toString = "alpha!"
• LeanPool.Polylean.Letter.β!.toString = "beta!"

@[implicit_reducible]

instance LeanPool.Polylean.Letter.instToString : ToString Letter

Equations

• LeanPool.Polylean.Letter.instToString = { toString := LeanPool.Polylean.Letter.toString }

def LeanPool.Polylean.Letter.inv : Letter → Letter

The formal inverse of a letter.

Equations

• LeanPool.Polylean.Letter.α.inv = LeanPool.Polylean.Letter.α!
• LeanPool.Polylean.Letter.β.inv = LeanPool.Polylean.Letter.β!
• LeanPool.Polylean.Letter.α!.inv = LeanPool.Polylean.Letter.α
• LeanPool.Polylean.Letter.β!.inv = LeanPool.Polylean.Letter.β

@[implicit_reducible, inline]

instance LeanPool.Polylean.letInv : Inv Letter

Equations

• LeanPool.Polylean.letInv = { inv := LeanPool.Polylean.Letter.inv }

@[reducible, inline]

abbrev LeanPool.Polylean.Word : Type

A word is a list of letters.

Equations

• LeanPool.Polylean.Word = List LeanPool.Polylean.Letter

def LeanPool.Polylean.Word.toString (w : Word) : String

Render a word by concatenating its rendered letters.

Equations

• w.toString = List.foldl (fun (x : String) (y : LeanPool.Polylean.Letter) => toString x ++ toString y) "" w

@[implicit_reducible]

instance LeanPool.Polylean.Word.instToString : ToString Word

Equations

• LeanPool.Polylean.Word.instToString = { toString := LeanPool.Polylean.Word.toString }

def LeanPool.Polylean.Word.pow : Word → ℕ → Word

Repeated concatenation of a word.

Equations

• x✝.pow 0 = []
• x✝.pow m.succ = x✝ ++ x✝.pow m

@[implicit_reducible]

instance LeanPool.Polylean.Word.instPowNat : Pow Word ℕ

Equations

• LeanPool.Polylean.Word.instPowNat = { pow := fun (w : LeanPool.Polylean.Word) (n : ℕ) => w.pow n }

def LeanPool.Polylean.splits (l : Letter) (w : Word) : List { p : Word × Word // List.length p.fst + List.length p.snd < List.length w }

All splits of a word around occurrences of a letter, with length witnesses.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.splits l [] = []

@[irreducible]

def LeanPool.Polylean.length : Word → ℕ

A recursively computed conjugation-invariant length candidate.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.length [] = 0

def LeanPool.Polylean.Word.conj : Word → Letter → Word

Conjugate a word by a letter.

Equations

• w.conj l = [l] ++ w ++ [l⁻¹]

@[implicit_reducible]

instance LeanPool.Polylean.instPowWordLetter : Pow Word Letter

Equations

• LeanPool.Polylean.instPowWordLetter = { pow := fun (w : LeanPool.Polylean.Word) (l : LeanPool.Polylean.Letter) => w.conj l }