The successor in binary

encNat encodes a natural number by its binary digits, least significant first (Nat.bits). The successor is a left fold over the digits that keeps a carry and appends one digit per round, followed by a final carry digit. Its tidy computability is derived from that of the fold (Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.foldl) and of the parts of a round.

Main definitions

• Turing.MultiTapeTM.encNat: natural numbers encoded by their binary digits.

Main results

• Turing.MultiTapeTM.computableTidilyInTimeAndSpace_succ: the successor is tidily computable in quadratic time and linear space.

def Turing.MultiTapeTM.encNat : ℕ ↪ List Bool

Natural numbers encoded by their binary digits, least significant first.

@[simp]

theorem Turing.MultiTapeTM.encNat_apply (n : ℕ) : encNat n = n.bits

def Turing.MultiTapeTM.NatSucc.incr : Bool → List Bool → List Bool

Adds the carry c to the binary digits l, least significant first.

theorem Turing.MultiTapeTM.NatSucc.bits_succ (n : ℕ) : (n + 1).bits = incr true n.bits

def Turing.MultiTapeTM.NatSucc.succStep (p : Bool × List Bool) (b : Bool) : Bool × List Bool

One round: add the carry to the digit b, append the resulting digit and keep the carry.

def Turing.MultiTapeTM.NatSucc.succFinish (p : Bool × List Bool) : List Bool

Appends the final carry digit.

theorem Turing.MultiTapeTM.NatSucc.succFinish_foldl (l : List Bool) (c : Bool) (out : List Bool) : succFinish (List.foldl succStep (c, out) l) = out ++ incr c l

theorem Turing.MultiTapeTM.NatSucc.length_foldl_succStep (l : List Bool) (p : Bool × List Bool) : (List.foldl succStep p l).2.length = p.2.length + l.length

@[reducible, inline]

abbrev Turing.MultiTapeTM.NatSucc.encAcc : Bool × List Bool ↪ List Bool

The encoding of the accumulator: the carry and the digits so far.

theorem Turing.MultiTapeTM.NatSucc.length_encAcc (p : Bool × List Bool) : (encAcc p).length = p.2.length + 3

theorem Turing.MultiTapeTM.NatSucc.linear_succStep : ComputableTidilyInLinearTimeAndSpace (fun (p : (Bool × List Bool) × Bool) => succStep p.1 p.2) (encPair encAcc encBool) encAcc

A round is tidily computable in linear time and space.

theorem Turing.MultiTapeTM.NatSucc.linear_succFinish : ComputableTidilyInLinearTimeAndSpace succFinish encAcc encBits

The final carry digit is appended in linear time and space.

theorem Turing.MultiTapeTM.computableTidilyInTimeAndSpace_succ : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace (fun (x : ℕ) => x + 1) encNat encNat (fun (n : ℕ) => c * ((encNat n).length + 1) ^ 2) fun (n : ℕ) => c * ((encNat n).length + 1)

The successor is tidily computable in quadratic time and linear space, in the binary encoding encNat.