Documentation

Complexitylib.RationalHitting.Internal.BinaryMultiply

Rational hitting lists: binary multiply #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/BinaryMultiply.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

source
theorem Complexity.RationalHitting.StackLanguage.wordValue_append (a b : List Bool) :
wordValue (a ++ b) = wordValue a + 2 ^ a.length * wordValue b
source
def Complexity.RationalHitting.StackLanguage.trimMSD :
List Bool → List Bool

Removes the high zero bits of a most-significant-first word.

Equations
Instances For
    source
    theorem Complexity.RationalHitting.StackLanguage.trimMSD_length (l : List Bool) :
    (trimMSD l).length ≤ l.length
    source
    theorem Complexity.RationalHitting.StackLanguage.trimMSD_reverse_value (l : List Bool) :
    wordValue (trimMSD l).reverse = wordValue l.reverse
    source
    def Complexity.RationalHitting.StackLanguage.Canonical (l : List Bool) :
    Prop

    A little-endian word with no redundant high zero bits.

    Equations
    Instances For
      source
      theorem Complexity.RationalHitting.StackLanguage.canonical_tail {b : Bool} {l : List Bool} (h : Canonical (b :: l)) :
      Canonical l
      source
      theorem Complexity.RationalHitting.StackLanguage.canonical_single {b : Bool} (h : Canonical [b]) :
      b = true
      source
      theorem Complexity.RationalHitting.StackLanguage.bits_wordValue (l : List Bool) (h : Canonical l) :
      (wordValue l).bits = l
      source
      theorem Complexity.RationalHitting.StackLanguage.canonical_trim_reverse (l : List Bool) :
      Canonical (trimMSD l).reverse
      source
      def Complexity.RationalHitting.StackLanguage.normalizeWord (l : List Bool) :
      List Bool

      Remove redundant high zero bits from a binary word.

      Equations
      Instances For
        source
        theorem Complexity.RationalHitting.StackLanguage.normalizeWord_value (l : List Bool) :
        wordValue (normalizeWord l) = wordValue l
        source
        @[simp]
        theorem Complexity.RationalHitting.StackLanguage.normalizeWord_eq_bits (l : List Bool) :
        normalizeWord l = (wordValue l).bits
        source
        theorem Complexity.RationalHitting.StackLanguage.normalizeWord_length (l : List Bool) :
        (normalizeWord l).length = (wordValue l).size
        source
        def Complexity.RationalHitting.StackLanguage.trimBody {K : Type} (a flag : K) :
        Program K

        One step removing high zero bits from a reversed word.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Complexity.RationalHitting.StackLanguage.trimLoop {K : Type} (a flag : K) :
          Program K

          Trim high zeros until the leading one or the empty word is reached.

          Equations
          Instances For
            source
            theorem Complexity.RationalHitting.StackLanguage.eval_trimLoop {K : Type} [DecidableEq K] {a flag : K} (haf : a ≠ flag) (s : Store K) (hf : s flag = [true]) :
            ∃ t ≤ 3 * (s a).length + 6, Eval (trimLoop a flag) s (Function.update (Function.update s a (trimMSD (s a))) flag []) t
            source
            def Complexity.RationalHitting.StackLanguage.normalize {K : Type} (a tmp flag : K) :
            Program K

            Normalize a binary stack word using a reversed temporary copy.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Complexity.RationalHitting.StackLanguage.eval_normalize {K : Type} [DecidableEq K] {a tmp flag : K} (hat : a ≠ tmp) (haf : a ≠ flag) (htf : tmp ≠ flag) (s : Store K) :
              ∃ t ≤ 7 * (s a).length + 2 * (s tmp).length + 2 * (s flag).length + 16, Eval (normalize a tmp flag) s (Function.update (Function.update (Function.update s a (normalizeWord (s a))) tmp []) flag []) t