Documentation

LeanPool.Polylean.ConjInvLength.LengthNode

Cached proof nodes for conjugacy-invariant length bounds #

source
inductive LeanPool.Polylean.ProofNode :
Type

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

Instances For
    source
    def LeanPool.Polylean.instReprProofNode.repr :
    ProofNode → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance LeanPool.Polylean.instReprProofNode :
      Repr ProofNode
      Equations
      source
      @[implicit_reducible]
      instance LeanPool.Polylean.instBEqProofNode :
      BEq ProofNode
      Equations
      source
      def LeanPool.Polylean.instBEqProofNode.beq :
      ProofNode → ProofNode → Bool
      Equations
      Instances For
        source
        def LeanPool.Polylean.ProofNode.top :
        ProofNode → Wrd

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

        Equations
        Instances For
          source
          def LeanPool.Polylean.ProofNode.toString :
          ProofNode → String

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

          Equations
          Instances For
            source
            @[implicit_reducible]
            instance LeanPool.Polylean.ProofNode.instToString :
            ToString ProofNode
            Equations
            source
            def LeanPool.Polylean.ProofNode.base :
            ProofNode → List Wrd

            The previously derived words needed by this proof node.

            Equations
            Instances For
              source
              def LeanPool.Polylean.ProofNode.baseLength :
              ProofNode → Option ℕ

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

              Equations
              Instances For
                source
                opaque LeanPool.Polylean.floatNormCache :
                IO.Ref (Std.HashMap Wrd Float)

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

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

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

                source
                @[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.
                Instances For
                  source
                  def LeanPool.Polylean.powerLength :
                  Wrd → ℕ → 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.
                  Instances For
                    source
                    def LeanPool.Polylean.resolveProof (w : Wrd) :
                    IO (List ProofNode × List Wrd)

                    Recursively expand cached proof nodes needed to justify a word.

                    Equations
                    Instances For
                      source
                      def LeanPool.Polylean.derivedLength (w : Wrd) :
                      IO Float

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

                      Equations
                      Instances For
                        source
                        def LeanPool.Polylean.derivedProof (w : Wrd) :
                        IO (Float × List ProofNode)

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

                        Equations
                        Instances For