Binary natural encoding and digit algorithms

The encoding and the carry, borrow and normalization word folds are independent of resource certificates. Their original definitions and arithmetic correctness proofs are retained here.

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.bits_succ_eq_foldl (n : ℕ) : (n + 1).bits = succFinish (List.foldl succStep (true, []) n.bits)

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

def Turing.MultiTapeTM.NatPred.decr : List Bool → List Bool

Subtracts a borrow from the binary digits l, least significant first, keeping a leading zero.

def Turing.MultiTapeTM.NatPred.norm (l : List Bool) : List Bool

Drops a leading zero, the last digit.

theorem Turing.MultiTapeTM.NatPred.norm_cons {l : List Bool} (hl : l ≠ []) (b : Bool) : norm (b :: l) = b :: norm l

theorem Turing.MultiTapeTM.NatPred.bits_ne_nil {m : ℕ} (hm : m ≠ 0) : m.bits ≠ []

theorem Turing.MultiTapeTM.NatPred.decr_ne_nil {l : List Bool} (hl : l ≠ []) : decr l ≠ []

theorem Turing.MultiTapeTM.NatPred.norm_bits (n : ℕ) : norm n.bits = n.bits

theorem Turing.MultiTapeTM.NatPred.bits_pred (n : ℕ) : (n - 1).bits = norm (decr n.bits)

def Turing.MultiTapeTM.NatPred.decrStep (p : Bool × List Bool) (b : Bool) : Bool × List Bool

One round of the decrement: subtract the borrow from the digit b, append the result and keep the borrow.

theorem Turing.MultiTapeTM.NatPred.length_decr (l : List Bool) : (decr l).length = l.length

theorem Turing.MultiTapeTM.NatPred.foldl_decrStep (l : List Bool) (c : Bool) (out : List Bool) : (List.foldl decrStep (c, out) l).2 = out ++ if c = true then decr l else l

def Turing.MultiTapeTM.NatPred.normStep (p : Option Bool × List Bool) (b : Bool) : Option Bool × List Bool

One round of dropping a leading zero: append the pending digit and keep the new one.

def Turing.MultiTapeTM.NatPred.normFinish (p : Option Bool × List Bool) : List Bool

Appends the pending digit unless it is a zero.

theorem Turing.MultiTapeTM.NatPred.length_foldl_normStep (l : List Bool) (p : Option Bool) (acc : List Bool) : (List.foldl normStep (p, acc) l).2.length ≤ acc.length + p.toList.length + l.length

theorem Turing.MultiTapeTM.NatPred.normFinish_foldl (l : List Bool) (p : Option Bool) (acc : List Bool) : normFinish (List.foldl normStep (p, acc) l) = acc ++ norm (p.toList ++ l)