Documentation

MIPRE.Foundations.Cost.Unary

The closure library, part III: unary arithmetic and tree size #

Programs on unary numerals (Data.ofNat) built from the length loop of Cost.Loops: addition (addProg), the bit string of a power of two (expBitsProg), and the size of a tree in unary (sizeProg, a stack-driven traversal proved with Eval.loop_of_invariant). These are the ingredients of the threshold function r e = 2 ^ q(esize e) of the recursive compression argument (planning/compression-track.md, K3 step 4); multiplication and powers follow in Cost.Numeric.

source
def MIPRE.Cost.Data.sumSize :
List Data → ℕ

Sum of the sizes of the elements of a list.

Equations
Instances For
    source
    @[simp]
    theorem MIPRE.Cost.Data.sumSize_nil :
    sumSize [] = 0
    source
    @[simp]
    theorem MIPRE.Cost.Data.sumSize_cons (a : Data) (l : List Data) :
    sumSize (a :: l) = a.size + sumSize l
    source
    theorem MIPRE.Cost.Data.length_le_sumSize (l : List Data) :
    l.length ≤ sumSize l
    source
    theorem MIPRE.Cost.Data.size_list_eq (l : List Data) :
    (list l).size = sumSize l + l.length + 1
    source
    def MIPRE.Cost.Data.nodeSum :
    Data → ℕ

    The sum of the sizes of the elements of a cons-chain, as a function on data (the measure of the tree-size loop).

    Equations
    Instances For
      source
      theorem MIPRE.Cost.Data.nodeSum_list (l : List Data) :
      (list l).nodeSum = sumSize l
      source
      def MIPRE.Cost.Data.stackMeasure :
      Data → ℕ

      The measure of the tree-size loop: the node sum of the stack component.

      Equations
      Instances For

        Addition of unary numerals #

        source
        def MIPRE.Cost.Prog.addProg :
        Prog

        addProg on cons (ofNat a) (ofNat b) computes ofNat (a + b): it is the length loop with the second numeral as accumulator.

        Equations
        Instances For
          source
          theorem MIPRE.Cost.Prog.addProg_wellScoped :
          WellScoped 1 addProg
          source
          theorem MIPRE.Cost.Prog.addProg_runs (a b : ℕ) (env : Env) :
          ∃ t ≤ (a + 1) * (4 * a + 2 * b + 15), Eval ((Data.ofNat a).cons (Data.ofNat b) :: env) addProg (Data.ofNat (a + b)) t

          Powers of two, as bit strings #

          source
          theorem Nat.bits_two_pow (j : ℕ) :
          (2 ^ j).bits = List.replicate j false ++ [true]
          source
          def MIPRE.Cost.Prog.expBitsProg :
          Prog

          expBitsProg on the unary numeral ofNat j computes encode (2 ^ j), the bit string false^j ++ [true].

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem MIPRE.Cost.Prog.expBitsProg_wellScoped :
            WellScoped 1 expBitsProg
            source
            theorem MIPRE.Cost.Prog.encode_two_pow (j : ℕ) :
            encode (2 ^ j) = Data.list (List.replicate j Data.nil ++ [Data.nil.cons Data.nil])
            source
            theorem MIPRE.Cost.Prog.expBitsProg_runs (j : ℕ) :
            ∃ t ≤ (j + 1 + 1) * (4 * j + 20), expBitsProg.Runs (Data.ofNat j) (encode (2 ^ j)) t

            Size of a tree, in unary #

            source
            def MIPRE.Cost.Prog.sizeBody :
            Prog

            Body of sizeProg: the state is cons stack count with stack a list of pending subtrees and count a unary numeral. Pop a subtree: if it is nil, count it; if it is cons a b, count it and push a and b. Stop with count when the stack is empty.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem MIPRE.Cost.Prog.sizeBody_wellScoped :
              WellScoped 1 sizeBody
              source
              theorem MIPRE.Cost.Prog.sizeBody_stop (k : ℕ) :
              Eval [(Data.list []).cons (Data.ofNat k)] sizeBody (Data.nil.cons (Data.ofNat k)) (2 * k + 6)
              source
              theorem MIPRE.Cost.Prog.sizeBody_step_nil (rest : List Data) (k : ℕ) :
              Eval [(Data.list (Data.nil :: rest)).cons (Data.ofNat k)] sizeBody ((Data.nil.cons Data.nil).cons ((Data.list rest).cons (Data.ofNat (k + 1)))) ((Data.list rest).size + 2 * k + 13)
              source
              theorem MIPRE.Cost.Prog.sizeBody_step_cons (a b : Data) (rest : List Data) (k : ℕ) :
              Eval [(Data.list (a.cons b :: rest)).cons (Data.ofNat k)] sizeBody ((Data.nil.cons Data.nil).cons ((Data.list (a :: b :: rest)).cons (Data.ofNat (k + 1)))) (a.size + b.size + (Data.list rest).size + 2 * k + 17)
              source
              def MIPRE.Cost.Prog.sizeInv (N : ℕ) (s : Data) :
              Prop

              The invariant of the tree-size loop for a tree of size N: the state is cons stack count with count + Σ size (stack) = N.

              Equations
              Instances For
                source
                theorem MIPRE.Cost.Prog.sizeLoop_runs (N : ℕ) (env : Env) (s : Data) (hs : sizeInv N s) :
                ∃ t ≤ (s.stackMeasure + 1) * (5 * N + 20), Eval (s :: env) sizeBody.loop (Data.ofNat N) t
                source
                def MIPRE.Cost.Prog.sizeProg :
                Prog

                Size of a tree in unary: sizeProg on d computes ofNat d.size.

                Equations
                Instances For
                  source
                  theorem MIPRE.Cost.Prog.sizeProg_wellScoped :
                  WellScoped 1 sizeProg
                  source
                  theorem MIPRE.Cost.Prog.sizeProg_runs (d : Data) :
                  ∃ t ≤ (d.size + 1) * (5 * d.size + 20) + d.size + 6, sizeProg.Runs d (Data.ofNat d.size) t