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₂)

@[instance_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✝ → Nat → Std.Format

Equations

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

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

The numeric bound represented by a proof tree.

Equations

• LeanPool.Polylean.ProofTree.bound [] LeanPool.Polylean.ProofTree.emptyWord = 0
• LeanPool.Polylean.ProofTree.bound [l] (LeanPool.Polylean.ProofTree.normalized l) = 1
• LeanPool.Polylean.ProofTree.bound (w_2 ^ l) (LeanPool.Polylean.ProofTree.conjugate l w_2 t_2) = LeanPool.Polylean.ProofTree.bound w_2 t_2
• LeanPool.Polylean.ProofTree.bound (w₁ ++ w₂) (LeanPool.Polylean.ProofTree.triangleIneq w₁ w₂ t₁ t₂) = LeanPool.Polylean.ProofTree.bound w₁ t₁ + LeanPool.Polylean.ProofTree.bound w₂ t₂

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 [l] (LeanPool.Polylean.ProofTree.normalized l) = { bound := 1, pf := ⋯ }
• LeanPool.Polylean.ProofTree.provedBound (w_2 ^ l) (LeanPool.Polylean.ProofTree.conjugate l w_2 t_2) = { bound := (LeanPool.Polylean.ProofTree.provedBound w_2 t_2).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))

@[instance_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