LeanPool.Polylean.ConjInvLength.WordTree

inductive LeanPool.Polylean.ProofTree : Word → Type

A proof tree witnessing an upper bound for a word length.

• emptyWord : ProofTree []
• normalized (l : Letter) : ProofTree [l]
• conjugate (l : Letter) (w : Word) : ProofTree w → ProofTree (w ^ l)
• triangleIneq (w₁ w₂ : Word) : ProofTree w₁ → ProofTree w₂ → ProofTree (w₁ ++ w₂)

@[implicit_reducible]

instance LeanPool.Polylean.instReprProofTree {a✝ : Word} : Repr (ProofTree a✝)

Equations

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

def LeanPool.Polylean.instReprProofTree.repr {a✝ : Word} : ProofTree a✝ → ℕ → Std.Format

Equations

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

def LeanPool.Polylean.ProofTree.bound (w : Word) : ProofTree w → ℕ

The numeric bound represented by a proof tree.

Equations

• LeanPool.Polylean.ProofTree.bound [] LeanPool.Polylean.ProofTree.emptyWord = 0
• LeanPool.Polylean.ProofTree.bound [a_1] (LeanPool.Polylean.ProofTree.normalized a_1) = 1
• LeanPool.Polylean.ProofTree.bound (a_2 ^ a_1) (LeanPool.Polylean.ProofTree.conjugate a_1 a_2 a_3) = LeanPool.Polylean.ProofTree.bound a_2 a_3
• LeanPool.Polylean.ProofTree.bound (a_1 ++ a_2) (LeanPool.Polylean.ProofTree.triangleIneq a_1 a_2 a_3 a_4) = LeanPool.Polylean.ProofTree.bound a_1 a_3 + LeanPool.Polylean.ProofTree.bound a_2 a_4

def LeanPool.Polylean.ProofTree.provedBound (w : Word) : ProofTree w → ProvedBound w

Convert a proof tree into a certified bound.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.ProofTree.provedBound [] LeanPool.Polylean.ProofTree.emptyWord = LeanPool.Polylean.ProvedBound.emptyWord
• LeanPool.Polylean.ProofTree.provedBound [a_1] (LeanPool.Polylean.ProofTree.normalized a_1) = { bound := 1, pf := ⋯ }
• LeanPool.Polylean.ProofTree.provedBound (a_2 ^ a_1) (LeanPool.Polylean.ProofTree.conjugate a_1 a_2 a_3) = { bound := (LeanPool.Polylean.ProofTree.provedBound a_2 a_3).bound, pf := ⋯ }

def LeanPool.Polylean.ProofTree.headMatches (x : Letter) (ys fst snd : Word) (eqn : ys = fst ++ [x⁻¹] ++ snd) : ProofTree fst → ProofTree snd → ProofTree (x :: ys)

Combine proof trees across a split around a conjugating letter.

Equations

• LeanPool.Polylean.ProofTree.headMatches x ys fst snd eqn pt1 pt2 = ⋯.mpr (LeanPool.Polylean.ProofTree.triangleIneq (fst ^ x) snd (LeanPool.Polylean.ProofTree.conjugate x fst pt1) pt2)

def LeanPool.Polylean.ProofTree.prepend {w : Word} (x : Letter) (pt : ProofTree w) : ProofTree (x :: w)

Prepend a normalized letter to a proof tree.

Equations

• LeanPool.Polylean.ProofTree.prepend x pt = id (LeanPool.Polylean.ProofTree.triangleIneq [x] w (LeanPool.Polylean.ProofTree.normalized x) pt)

def LeanPool.Polylean.ProofTree.min {w : Word} : ProofTree w → List (ProofTree w) → ProofTree w

Choose the proof tree with the smallest bound from a nonempty list.

Equations

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

def LeanPool.Polylean.simpleTree (w : Word) : ProofTree w

A simple proof tree obtained by splitting a word into letters.

Equations

• LeanPool.Polylean.simpleTree [] = LeanPool.Polylean.ProofTree.emptyWord
• LeanPool.Polylean.simpleTree (x :: ys) = id (LeanPool.Polylean.ProofTree.triangleIneq [x] ys (LeanPool.Polylean.ProofTree.normalized x) (LeanPool.Polylean.simpleTree ys))

@[implicit_reducible]

instance LeanPool.Polylean.instInhabitedProofTree {w : Word} : Inhabited (ProofTree w)

Equations

• LeanPool.Polylean.instInhabitedProofTree = { default := LeanPool.Polylean.simpleTree w }

@[irreducible]

def LeanPool.Polylean.proofTree (w : Word) : ProofTree w

Compute a proof tree for a word.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.proofTree [] = LeanPool.Polylean.ProofTree.emptyWord