refactor(Machines): binary successor as one linear-time streaming transducer (#608)

Complexity.lean

@@ -1587,7 +1587,6 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.S
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Words
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower
-public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatStream
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Padding
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair

Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean

@@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Foldl
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Basic
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat
+import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormalForm
 
 /-!
 # Tidy computability in polynomial time
@@ -281,10 +282,12 @@ public theorem ComputableTidilyInPolyTime.foldl {γ α β : Type u} {encIn : γ
       ((hlen.add (.const 1)).mul ((hmax.add hlMax').add (.const 1)))),
     (PolyBounded.const c).mul ((((hs₁.add hs₂).add hmax).add hlMax').add (.const 1)), h⟩
 
-/-- The successor is tidily computable in polynomial time, in the binary encoding `encNat`. -/
+/-- The successor is tidily computable in polynomial time, in the binary encoding `encNat`, from
+the transducer certificate `computableInTimeAndSpace_succ`. -/
 @[fun_prop]
 public theorem computableTidilyInPolyTime_succ : ComputableTidilyInPolyTime (· + 1) encNat encNat :=
-  let ⟨c, h⟩ := computableTidilyInTimeAndSpace_succ
-  ⟨_, _, .of_forall_le c 2 (fun _ => le_rfl), .of_forall_le c 1 (fun _ => by simp), h⟩
+  let ⟨c, h⟩ := computableInTimeAndSpace_succ.exists_computableTidilyInTimeAndSpace
+  ⟨_, _, .of_forall_le (c + 6) 1 (fun _ => by simp only [pow_one]; nlinarith),
+    .of_forall_le c 0 (fun _ => by simp), h⟩
 
 end Turing.MultiTapeTM

Complexity/Computability/Machines/Turing/MultiTape/Complexity/Quantitative.lean

@@ -34,6 +34,7 @@ Framed-list and option rules infer the payload encoding from the representation
 
 * `Turing.MultiTapeTM.ComputableInDegree.foldl'`,
   `Turing.MultiTapeTM.ComputableInDegree.foldlWith`: plain left folds with degree bounds.
+* `Turing.MultiTapeTM.ComputableInDegree.natSucc`: binary successor with degrees one.
 * `Turing.MultiTapeTM.computableInDegree_add`, `Turing.MultiTapeTM.computableInDegree_mul`:
   plain binary addition (quadratic) and multiplication (cubic).
 * `Turing.MultiTapeTM.ComputableInO.comp_enc`: reuse a bit-word computation on encoded
@@ -305,6 +306,11 @@ private lemma run_copy_fin3 (T : Transducer Bool (Fin 3)) (hT : ∀ b, T.step 2
   | nil => simp [hf]
   | cons b w ih => simp [hT, ih]
 
+/-- Binary successor has cost and output degree one, from the transducer certificate
+`computableInTimeAndSpace_succ`. -/
+theorem natSucc : ComputableInDegree (· + 1) encNat encNat 1 1 :=
+  of_linear .natSucc
+
 /-- Adding one on unary-magnitude signed integers. -/
 theorem int_succ : ComputableInDegree (· + 1) encInt encInt 1 1 := by
   refine of_linear (.of_transducer intSuccT fun z => ?_)

Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat.lean

@@ -8,31 +8,26 @@ module
 -- upstream: vendored crei:crei/tidy-universal @7f7c0696 (unsubmitted)
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits
-public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Foldl
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Option
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
-import Mathlib.Data.Nat.Bitwise
-import Mathlib.Tactic.Ring
+public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer
 
 /-!
 # The successor in binary
 
 `encNat`, reexported from `Encodings.Nat.Bits`, 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.
-* `Turing.MultiTapeTM.encNat3`: triples of natural numbers encoded in binary.
+The successor is computed by one streaming transducer whose state is the carry: on each digit `b`
+in carry `c` it emits `c ^^ b` and keeps the carry `c && b`, and at the end it emits a final `1`
+exactly when a carry remains. The machine reads its input once and uses no work tape.
 
 ## Main results
 
-* `Turing.MultiTapeTM.computableTidilyInTimeAndSpace_succ`: the successor is tidily computable in
-  quadratic time and linear space.
+* `Turing.MultiTapeTM.computableInTimeAndSpace_succ`: the successor is computable within
+  `2 * (encNat n).length + 3` steps and zero work space.
+* `Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natSucc`: its linear form.
 -/
 
 namespace Turing.MultiTapeTM
@@ -42,96 +37,39 @@ public abbrev encNat3 : ℕ × ℕ × ℕ ↪ List Bool := encPair encNat (encPa
 
 namespace NatSucc
 
-open ComputableInLinearTimeAndSpace
-
-/-- A round is tidily computable in linear time and space. -/
-public lemma linear_succStep :
-    ComputableTidilyInLinearTimeAndSpace (fun p => succStep p.1 p.2)
-      (encPair encAcc encBool) encAcc := by
-  apply Internal.NormalForm.linear
-  have hacc : ComputableInLinearTimeAndSpace Prod.fst (encPair encAcc encBool) encAcc :=
-    PairEncoding.fst encBool
-  have hcarry : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => p.1.1)
-      (encPair encAcc encBool) encBool :=
-    (PairEncoding.fst encBits).comp hacc
-  have hdigit : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => p.2)
-      (encPair encAcc encBool) encBool :=
-    PairEncoding.snd encAcc
-  have hdigits : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => p.1.2)
-      (encPair encAcc encBool) encBits :=
-    (PairEncoding.snd encBool).comp hacc
-  have hand : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool =>
-      p.1.1 && p.2) (encPair encAcc encBool) encBool := by
-    convert hdigit.ite (hcarry.restrict _) ((const false).restrict _) using 1
-    funext p
-    cases p.2 <;> simp
-  have hnot : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool => !p.1.1)
-      (encPair encAcc encBool) encBool := by
-    convert hcarry.ite ((const false).restrict _) ((const true).restrict _) using 1
-    funext p
-    cases p.1.1 <;> rfl
-  have hxor : ComputableInLinearTimeAndSpace (fun p : (Bool × List Bool) × Bool =>
-      p.1.1 ^^ p.2) (encPair encAcc encBool) encBool := by
-    convert hdigit.ite (hnot.restrict _) (hcarry.restrict _) using 1
-    funext p
-    cases p.2 <;> simp
-  exact hand.pair (hdigits.append hxor (encOut := encBits) fun _ => rfl)
-
-/-- The final carry digit is appended in linear time and space. -/
-public lemma linear_succFinish :
-    ComputableTidilyInLinearTimeAndSpace succFinish encAcc encBits := by
-  apply Internal.NormalForm.linear
-  have hdigits : ComputableInLinearTimeAndSpace Prod.snd encAcc encBits :=
-    PairEncoding.snd encBool
-  have happend : ComputableInLinearTimeAndSpace (fun p => p.2 ++ [true]) encAcc encBits :=
-    hdigits.append (const (encMid := encBool) true) (encOut := encBits) fun _ => rfl
-  have hcarry : ComputableInLinearTimeAndSpace Prod.fst encAcc encBool :=
-    PairEncoding.fst encBits
-  exact hcarry.ite (happend.restrict _) (hdigits.restrict _)
+/-- The successor as a transducer: the state is the carry, initially set. -/
+private def succTransducer : Transducer Bool Bool where
+  q₀ := true
+  step c b := (c && b, [c ^^ b])
+  final c := if c then [true] else []
+  length_step_le _ _ := by simp
+  length_final_le c := by cases c <;> simp
+
+private lemma run_succTransducer (c : Bool) (l : List Bool) :
+    succTransducer.run c l = incr c l := by
+  induction l generalizing c with
+  | nil => cases c <;> rfl
+  | cons b l ih =>
+    rw [Transducer.run_cons, ih]
+    cases c <;> cases b <;> simp [succTransducer, incr]
 
 end NatSucc
 
 open NatSucc in
-/-- The successor is tidily computable in quadratic time and linear space, in the binary encoding
-`encNat`. -/
-public theorem computableTidilyInTimeAndSpace_succ :
-    ∃ c, ComputableTidilyInTimeAndSpace (· + 1) encNat encNat
-      (fun n => c * ((encNat n).length + 1) ^ 2) (fun n => c * ((encNat n).length + 1)) := by
-  obtain ⟨cl, hlist⟩ := ComputableTidilyInLinearTimeAndSpace.of_eq (f := Nat.bits)
-    (encIn := encNat) (encMid := encBits) fun _ => rfl
-  obtain ⟨ci, hinit⟩ := ComputableTidilyInLinearTimeAndSpace.const (encIn := encNat)
-    (encMid := encAcc) (true, [])
-  obtain ⟨cs, hstep⟩ := linear_succStep
-  -- the bounds of a round and of the state of the fold
-  have hlen (n i : ℕ) : (((n.bits.take i).foldl succStep (true, [])).2).length ≤ n.bits.length := by
-    rw [length_foldl_succStep]
-    simp
-  obtain ⟨cf, hfold⟩ := ComputableTidilyInTimeAndSpace.foldl (encA := encBool) (encL := encBits)
-    (encBA := encPair encAcc encBool) (encS := encPair encBits encAcc)
-    (encO := encOption (encPair encBits encAcc))
-    (hlist.mono (t' := fun n => (cl + ci) * ((encNat n).length + 1))
-      (s' := fun n => (cl + ci) * ((encNat n).length + 1))
-      (fun n => by ring_nf; omega) (fun n => by ring_nf; omega))
-    (hinit.mono (fun n => by ring_nf; omega) (fun n => by ring_nf; omega)) hstep
-    (tMax := fun n => cs * (2 * (encNat n).length + 9))
-    (sMax := fun n => cs * (2 * (encNat n).length + 9))
-    (lMax := fun n => 2 * (encNat n).length + 4)
-    (fun n i _ => Nat.mul_le_mul_left cs (by simp; have := hlen n i; omega))
-    (fun n i _ => Nat.mul_le_mul_left cs (by simp; have := hlen n i; omega))
-    (fun n i hi => by simp [length_foldl_succStep]; omega)
-  obtain ⟨cg, hfinish⟩ := linear_succFinish
-  -- vendored: crei's `comp` is `comp_linear` here, as cslib #1111 restates `comp`
-  obtain ⟨cc, h⟩ := ComputableTidilyInTimeAndSpace.comp_linear hfinish hfold
-  obtain ⟨k, S, _, tm, htm⟩ := h
-  refine ⟨cf * (cl + ci + 9 * cs + 5) + 4 * (cg + cc), k, S, inferInstance, tm, fun n => ?_⟩
-  have hmid : (encAcc (n.bits.foldl succStep (true, []))).length = n.bits.length + 3 := by
-    rw [length_encAcc, length_foldl_succStep]
-    simp
-  change tm.ComputesTidilyInTimeAndSpace _ (n + 1).bits _ _
-  rw [bits_succ_eq_foldl]
-  refine (htm n).mono ?_ ?_ <;>
-  · simp only [hmid, encNat_apply]
-    ring_nf
-    omega
+/-- **Binary successor in linear time and zero work space.** One streaming transducer computes
+`n + 1` from `encNat n` within `2 * (encNat n).length + 3` steps without work tapes. -/
+public theorem computableInTimeAndSpace_succ :
+    ComputableInTimeAndSpace (· + 1) encNat encNat (fun n => 2 * (encNat n).length + 3)
+      (fun _ => 0) :=
+  ⟨0, _, inferInstance, succTransducer.toTM, fun n => by
+    rw [encNat_apply, encNat_apply, bits_succ, ← run_succTransducer]
+    exact succTransducer.computesInTimeAndSpace_toTM n.bits⟩
+
+/-- Binary successor in linear time and work space, from `computableInTimeAndSpace_succ`. -/
+public theorem ComputableInLinearTimeAndSpace.natSucc :
+    ComputableInLinearTimeAndSpace (· + 1) encNat encNat :=
+  let ⟨k, Q, hQ, tm, h⟩ := computableInTimeAndSpace_succ
+  ⟨3, k, Q, hQ, tm, fun n =>
+    ⟨(h n).1, (h n).2.1.mono (by dsimp; omega), (h n).2.2.mono (Nat.zero_le _)⟩⟩
 
 end Turing.MultiTapeTM

Complexity/Computability/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean

@@ -8,21 +8,24 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops
-public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Bits
+public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
 
 /-!
 # Direct binary counter resource certificates
 
-The original carry, borrow and leading-zero normalization folds compute successor and predecessor.
-Their time is quadratic and their charged workspace linear in the binary input length. The zero
-test uses the existing empty-word machine. All round certificates are plain; normalization occurs
-only when the internal machine combinators construct the fold.
+The original borrow and leading-zero normalization folds compute the predecessor. Its time is
+quadratic and its charged workspace linear in the binary input length. The successor's
+certificate here is a weakening of the streaming transducer `computableInTimeAndSpace_succ`; the
+carry rounds remain as the shared step of binary addition. The zero test uses the existing
+empty-word machine. All round certificates are plain; normalization occurs only when the internal
+machine combinators construct the fold.
 
 ## Main results
 
-* `ComputableInO.succStep`, `ComputableInO.succFinish`: shared linear carry-round certificates.
+* `ComputableInO.succStep`, `ComputableInO.succFinish`: shared linear carry-round certificates
+  for binary addition.
 * `ComputableInO.natSucc`, `ComputableInO.natPred`: quadratic-time, linear-space binary counters.
 * `ComputableInO.natIsZero`: linear zero testing.
 -/
@@ -143,19 +146,13 @@ theorem foldl_bits {β : Type} {encB : β ↪ List Bool} {init : β} {step : β
   · simp only [encBits_apply]
     nlinarith
 
-/-- Binary successor with the original quadratic clock and linear output-charged workspace. -/
+/-- Binary successor within the quadratic clock and linear charged workspace used by its
+clients, weakened from the linear-time, zero-work-space transducer certificate
+`computableInTimeAndSpace_succ`. -/
 theorem natSucc :
     ComputableInO (· + 1) encNat encNat (fun n => ((encNat n).length + 1) ^ 2)
-      (fun n => (encNat n).length + 1) := by
-  have hfold := foldl_bits (init := (true, [])) succStep 3 fun l i => by
-    rw [NatSucc.length_encAcc, NatSucc.length_foldl_succStep]
-    simp only [List.length_nil, Nat.zero_add]
-    have := List.length_take_le' i l
-    omega
-  have h := (succFinish.comp_linear hfold).of_encIn_eq (encD := encNat) Nat.bits (fun _ => rfl)
-  refine h.of_enc_eq fun n => ?_
-  simp only [encNat_apply, encBits_apply, Function.comp_apply, NatSucc.succFinish_foldl,
-    List.nil_append, NatSucc.bits_succ]
+      (fun n => (encNat n).length + 1) :=
+  (of_linear .natSucc).mono_le (fun n => by simp only [encNat_apply]; nlinarith) fun _ => by omega
 
 /-- Binary predecessor keeps zero at zero and preserves the original independent resource bounds. -/
 theorem natPred :