Cached proof nodes for conjugacy-invariant length bounds

inductive LeanPool.Polylean.ProofNode : Type

A node recording which inequality or equality was used to derive a word-length bound.

• empty : ProofNode
• gen (l : Letter) : ProofNode
• triang (w₁ w₂ : Wrd) : ProofNode
• conj (l : Letter) (w : Wrd) : ProofNode
• power (n : Nat) (w : Wrd) : ProofNode

def LeanPool.Polylean.instReprProofNode.repr : ProofNode → Nat → Std.Format

Equations

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

@[instance_reducible]

instance LeanPool.Polylean.instReprProofNode : Repr ProofNode

Equations

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

def LeanPool.Polylean.instBEqProofNode.beq : ProofNode → ProofNode → Bool

Equations

• LeanPool.Polylean.instBEqProofNode.beq LeanPool.Polylean.ProofNode.empty LeanPool.Polylean.ProofNode.empty = true
• LeanPool.Polylean.instBEqProofNode.beq (LeanPool.Polylean.ProofNode.gen a) (LeanPool.Polylean.ProofNode.gen b) = (a == b)
• LeanPool.Polylean.instBEqProofNode.beq (LeanPool.Polylean.ProofNode.triang a a_1) (LeanPool.Polylean.ProofNode.triang b b_1) = (a == b && a_1 == b_1)
• LeanPool.Polylean.instBEqProofNode.beq (LeanPool.Polylean.ProofNode.conj a a_1) (LeanPool.Polylean.ProofNode.conj b b_1) = (a == b && a_1 == b_1)
• LeanPool.Polylean.instBEqProofNode.beq (LeanPool.Polylean.ProofNode.power a a_1) (LeanPool.Polylean.ProofNode.power b b_1) = (a == b && a_1 == b_1)
• LeanPool.Polylean.instBEqProofNode.beq x✝¹ x✝ = false

@[instance_reducible]

instance LeanPool.Polylean.instBEqProofNode : BEq ProofNode

Equations

• LeanPool.Polylean.instBEqProofNode = { beq := LeanPool.Polylean.instBEqProofNode.beq }

def LeanPool.Polylean.ProofNode.top : ProofNode → Wrd

The word whose length bound is justified by a proof node.

Equations

• LeanPool.Polylean.ProofNode.empty.top = #[]
• (LeanPool.Polylean.ProofNode.gen l).top = #[l]
• (LeanPool.Polylean.ProofNode.triang w₁ w₂).top = w₁ ++ w₂
• (LeanPool.Polylean.ProofNode.conj l w).top = w ^ l
• (LeanPool.Polylean.ProofNode.power n w).top = w

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

Render a proof node as a human-readable proof step.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.ProofNode.empty.toString = "l(e) = 0 (trivial word)"
• (LeanPool.Polylean.ProofNode.gen l).toString = toString "l(" ++ toString l ++ toString ") = 1 (normalization)"
• (LeanPool.Polylean.ProofNode.conj l w).toString = toString "l(" ++ toString w ++ toString "^" ++ toString l ++ toString ") = l(" ++ toString w ++ toString ") (conjugacy invariance)"
• (LeanPool.Polylean.ProofNode.power n w).toString = toString "l(w) ≤ l(" ++ toString (w ^ n) ++ toString ")/" ++ toString n ++ toString " (homogeneity)"

@[instance_reducible]

instance LeanPool.Polylean.ProofNode.instToString : ToString ProofNode

Equations

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

def LeanPool.Polylean.ProofNode.base : ProofNode → List Wrd

The previously derived words needed by this proof node.

Equations

• LeanPool.Polylean.ProofNode.empty.base = []
• (LeanPool.Polylean.ProofNode.gen l).base = []
• (LeanPool.Polylean.ProofNode.triang w₁ w₂).base = [w₁, w₂]
• (LeanPool.Polylean.ProofNode.conj l w).base = [w]
• (LeanPool.Polylean.ProofNode.power n w).base = [w ^ n]

def LeanPool.Polylean.ProofNode.baseLength : ProofNode → Option Nat

Length immediately justified by a base proof node, if any.

Equations

• LeanPool.Polylean.ProofNode.empty.baseLength = some 0
• (LeanPool.Polylean.ProofNode.gen l).baseLength = some 1
• x✝.baseLength = none

opaque LeanPool.Polylean.floatNormCache : IO.Ref (Std.HashMap Wrd Float)

Cache of floating-point length bounds for array-backed words.

opaque LeanPool.Polylean.proofCache : IO.Ref (Std.HashMap Wrd ProofNode)

Cache of proof nodes witnessing the best known bound for each word.

def LeanPool.Polylean.cachedLength (w : Wrd) : IO (Option Float)

Look up a cached floating-point length bound.

Equations

• LeanPool.Polylean.cachedLength w = do let cache ← ST.Ref.get LeanPool.Polylean.floatNormCache match cache.get? w with | some n => pure (some n) | none => pure none

@[irreducible]

def LeanPool.Polylean.lengthNodes (w : Wrd) : IO Float

Compute a floating-point length bound while caching the proof nodes used.

Equations

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

def LeanPool.Polylean.powerLength : Wrd → Nat → IO Float

Improve a word-length bound using a power of the word.

Equations

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

def LeanPool.Polylean.resolveProofWithFuel : Nat → Wrd → IO (List ProofNode × List Wrd)

Recursively expand cached proof nodes with a bounded traversal fuel.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.resolveProofWithFuel 0 x✝ = pure ([], [x✝])

def LeanPool.Polylean.resolveProof (w : Wrd) : IO (List ProofNode × List Wrd)

Recursively expand cached proof nodes needed to justify a word.

Equations

• LeanPool.Polylean.resolveProof w = do let cache ← ST.Ref.get LeanPool.Polylean.proofCache LeanPool.Polylean.resolveProofWithFuel (cache.size + 1) w

def LeanPool.Polylean.derivedLengthWithFuel : Nat → Wrd → IO Float

Recompute a derived length with a bounded traversal fuel.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.derivedLengthWithFuel 0 x✝ = throw (IO.userError (toString "proof cache recursion exhausted at " ++ toString x✝))

def LeanPool.Polylean.derivedLength (w : Wrd) : IO Float

Recompute the derived length from cached proof nodes, panicking if a node is absent.

Equations

• LeanPool.Polylean.derivedLength w = do let cache ← ST.Ref.get LeanPool.Polylean.proofCache LeanPool.Polylean.derivedLengthWithFuel (cache.size + 1) w

def LeanPool.Polylean.derivedProofWithFuel : Nat → Wrd → IO (Float × List ProofNode)

Recompute a derived length proof with a bounded traversal fuel.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.derivedProofWithFuel 0 x✝ = throw (IO.userError (toString "proof cache recursion exhausted at " ++ toString x✝))

def LeanPool.Polylean.derivedProof (w : Wrd) : IO (Float × List ProofNode)

Recompute the derived length together with the list of proof nodes used.

Equations

• LeanPool.Polylean.derivedProof w = do let cache ← ST.Ref.get LeanPool.Polylean.proofCache LeanPool.Polylean.derivedProofWithFuel (cache.size + 1) w