The existing binary subtraction word algorithm

The public borrow, digit-pair and subtraction definitions and laws are moved unchanged from the higher arithmetic facade. No machine or computability predicate is needed for these identities. The consuming-cursor realization has the same borrow rounds without repeated indexed lookup.

Main definitions

• BinarySub.borrow, BinarySub.subStep: the existing schoolbook borrow round.
• BinarySub.digitPairs: the original indexed pairs of input digits.
• BinarySub.cursorStep: consume the remaining words and execute that same round.

Main results

• BinarySub.sub_eq: the existing truncated-subtraction correctness law.
• BinarySub.foldl_cursorStep: equality of the consuming and indexed realizations.
• BinarySub.cursorStep_lengths: remaining words never grow; one output digit is added per round.

def Turing.MultiTapeTM.BinarySub.borrow (c x y : Bool) : Bool

The borrow out of a digit position: the minuend digit x minus the subtrahend digit y and the incoming borrow c is negative.

def Turing.MultiTapeTM.BinarySub.subStep (s : Bool × List Bool) (d : Bool × Bool) : Bool × List Bool

One round of schoolbook subtraction, least significant digit first: append the difference digit and pass on the borrow.

def Turing.MultiTapeTM.BinarySub.digitPairs (p : ℕ × ℕ) : List (Bool × Bool)

The digit pairs of two binary naturals at their first size a + size b positions.

theorem Turing.MultiTapeTM.BinarySub.bits_getD (n i : ℕ) : n.bits.getD i false = n.testBit i

theorem Turing.MultiTapeTM.BinarySub.foldl_subStep (ps : List (Bool × Bool)) (c : Bool) (out : List Bool) : ∃ (ds : List Bool), (List.foldl subStep (c, out) ps).2 = out ++ ds ∧ ds.length = ps.length ∧ List.foldr Nat.bit 0 ds + List.foldr Nat.bit 0 (List.map Prod.snd ps) + c.toNat = List.foldr Nat.bit 0 (List.map Prod.fst ps) + (List.foldl subStep (c, out) ps).1.toNat * 2 ^ ps.length

theorem Turing.MultiTapeTM.BinarySub.sub_eq (p : ℕ × ℕ) : p.1 - p.2 = if (List.foldl subStep (false, []) (digitPairs p)).1 = true then 0 else List.foldr Nat.bit 0 (List.foldl subStep (false, []) (digitPairs p)).2

Truncated subtraction through the borrow of schoolbook subtraction: when the final borrow is set the difference is negative, and otherwise the digits read off the difference.

def Turing.MultiTapeTM.BinarySub.cursorStep (s : (List Bool × List Bool) × Bool × List Bool) : Bool → (List Bool × List Bool) × Bool × List Bool

Realize one existing borrow round by consuming the two remaining input words. The clock symbol is ignored; its word supplies the number of digit positions to visit.

theorem Turing.MultiTapeTM.BinarySub.foldl_cursorStep (clock left right : List Bool) (acc : Bool × List Bool) : List.foldl cursorStep ((left, right), acc) clock = ((List.drop clock.length left, List.drop clock.length right), List.foldl subStep acc (List.map (fun (i : ℕ) => (left.getD i false, right.getD i false)) (List.range clock.length)))

The consuming-word realization executes exactly the original indexed borrow fold.

theorem Turing.MultiTapeTM.BinarySub.cursorStep_lengths (clock left right : List Bool) (acc : Bool × List Bool) : (List.foldl cursorStep ((left, right), acc) clock).1.1.length ≤ left.length ∧ (List.foldl cursorStep ((left, right), acc) clock).1.2.length ≤ right.length ∧ (List.foldl cursorStep ((left, right), acc) clock).2.2.length = acc.2.length + clock.length

No cursor grows, and the existing subtraction accumulator appends one digit per round.