refactor(Machines): binary predecessor and zero test as streaming transducers (#608)

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

@@ -13,23 +13,30 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Optio
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pair
 public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer
+import Complexity.Foundations.Data.Nat.Bits
 
 /-!
-# The successor in binary
+# The successor, predecessor and zero test in binary
 
 `encNat`, reexported from `Encodings.Nat.Bits`, encodes a natural number by its binary digits,
 least significant first (`Nat.bits`).
-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.
+Each of the three counter operations is computed by one streaming transducer that reads its input
+once and uses no work tape:
+
+* the successor's 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 predecessor turns the borrowed `0`s into `1`s and the first `1` into a `0`, which it holds
+  back until a further digit shows that it is not the leading digit, and then copies the rest;
+* the zero test emits whether the input was empty.
 
 ## Main results
 
-* `Turing.MultiTapeTM.computableInTimeAndSpace_succ`: the successor is computable within
+* `Turing.MultiTapeTM.computableInTimeAndSpace_succ`, `computableInTimeAndSpace_pred`,
+  `computableInTimeAndSpace_isZero`: the operations are computable within
   `2 * (encNat n).length + 3` steps and zero work space.
-* `Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natSucc`: its linear form.
+* `Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.natSucc`, `.natPred`, `.natIsZero`: their
+  linear forms.
 -/
-
 namespace Turing.MultiTapeTM
 
 /-- The framed binary encoding of triples of natural numbers. -/
@@ -55,6 +62,80 @@ private lemma run_succTransducer (c : Bool) (l : List Bool) :
 
 end NatSucc
 
+namespace NatPred
+
+/-- The predecessor as a transducer. In the borrow state `none` each `0` becomes `1`; the first
+`1` becomes a pending `0` (state `some false`), emitted only once a further digit shows it is not
+the leading digit; from then on (state `some true`) the digits are copied. -/
+private def predTransducer : Transducer Bool (Option Bool) where
+  q₀ := none
+  step
+    | none, false => (none, [true])
+    | none, true => (some false, [])
+    | some false, b => (some true, [false, b])
+    | some true, b => (some true, [b])
+  final _ := []
+  length_step_le q b := by rcases q with _ | _ | _ <;> cases b <;> simp
+  length_final_le _ := by simp
+
+private lemma run_predTransducer_copy (l : List Bool) : predTransducer.run (some true) l = l := by
+  induction l with
+  | nil => rfl
+  | cons b l ih => exact congrArg (b :: ·) ih
+
+private lemma run_predTransducer_pending (l : List Bool) :
+    predTransducer.run (some false) l = if l = [] then [] else false :: l := by
+  cases l with
+  | nil => rfl
+  | cons b l =>
+    change [false, b] ++ predTransducer.run (some true) l = _
+    rw [run_predTransducer_copy]
+    rfl
+
+private lemma run_predTransducer (n : ℕ) : predTransducer.run none n.bits = (n - 1).bits := by
+  induction n using Nat.strong_induction_on with
+  | _ n ih =>
+    rcases Nat.even_or_odd' n with ⟨m, rfl | rfl⟩
+    · rcases Nat.eq_zero_or_pos m with rfl | hm
+      · rfl
+      · rw [Nat.bit0_bits m (by omega), show 2 * m - 1 = 2 * (m - 1) + 1 by omega,
+          Nat.bit1_bits, ← ih m (by omega)]
+        rfl
+    · rw [Nat.bit1_bits, Nat.add_sub_cancel]
+      change predTransducer.run (some false) m.bits = _
+      rw [run_predTransducer_pending]
+      rcases Nat.eq_zero_or_pos m with rfl | hm
+      · rfl
+      · rw [Nat.bit0_bits m hm.ne']
+        simp [Nat.bits_eq_nil_iff, hm.ne']
+
+/-- The zero test as a transducer: the state records that no digit has been read yet. -/
+private def isZeroTransducer : Transducer Bool Bool where
+  q₀ := true
+  step _ _ := (false, [])
+  final b := [b]
+  length_step_le _ _ := by simp
+  length_final_le _ := by simp
+
+private lemma run_isZeroTransducer (q : Bool) (l : List Bool) :
+    isZeroTransducer.run q l = [q && l.isEmpty] := by
+  induction l generalizing q with
+  | nil => simp [isZeroTransducer]
+  | cons b l ih =>
+    change [] ++ isZeroTransducer.run false l = _
+    simp [ih]
+
+end NatPred
+
+/-- A transducer certificate on `encNat` is linear in time and work space. -/
+private theorem ComputableInTimeAndSpace.linear {β : Type} {encOut : β ↪ List Bool} {f : ℕ → β}
+    (h : ComputableInTimeAndSpace f encNat encOut (fun n => 2 * (encNat n).length + 3)
+      (fun _ => 0)) :
+    ComputableInLinearTimeAndSpace f encNat encOut :=
+  let ⟨k, Q, hQ, tm, h⟩ := h
+  ⟨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 _)⟩⟩
+
 open NatSucc in
 /-- **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. -/
@@ -68,8 +149,40 @@ public theorem computableInTimeAndSpace_succ :
 /-- 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 _)⟩⟩
+  computableInTimeAndSpace_succ.linear
+
+open NatPred in
+/-- **Binary predecessor in linear time and zero work space.** One streaming transducer computes
+`n - 1` (so `0 ↦ 0`) from `encNat n` within `2 * (encNat n).length + 3` steps without work
+tapes. -/
+public theorem computableInTimeAndSpace_pred :
+    ComputableInTimeAndSpace (· - 1) encNat encNat (fun n => 2 * (encNat n).length + 3)
+      (fun _ => 0) :=
+  ⟨0, _, inferInstance, predTransducer.toTM, fun n => by
+    rw [encNat_apply, encNat_apply, ← run_predTransducer]
+    exact predTransducer.computesInTimeAndSpace_toTM n.bits⟩
+
+/-- Binary predecessor in linear time and work space, from `computableInTimeAndSpace_pred`. -/
+public theorem ComputableInLinearTimeAndSpace.natPred :
+    ComputableInLinearTimeAndSpace (· - 1) encNat encNat :=
+  computableInTimeAndSpace_pred.linear
+
+open NatPred in
+/-- **Binary zero test in linear time and zero work space.** One streaming transducer decides
+`n = 0` from `encNat n` within `2 * (encNat n).length + 3` steps without work tapes. -/
+public theorem computableInTimeAndSpace_isZero :
+    ComputableInTimeAndSpace (fun n => decide (n = 0)) encNat encBool
+      (fun n => 2 * (encNat n).length + 3) (fun _ => 0) :=
+  ⟨0, _, inferInstance, isZeroTransducer.toTM, fun n => by
+    beta_reduce
+    rw [encNat_apply, encBool_apply, show decide (n = 0) = (true && n.bits.isEmpty) by
+      rw [Bool.true_and, Bool.eq_iff_iff, List.isEmpty_iff, Nat.bits_eq_nil_iff,
+        decide_eq_true_iff], ← run_isZeroTransducer]
+    exact isZeroTransducer.computesInTimeAndSpace_toTM n.bits⟩
+
+/-- Binary zero test in linear time and work space, from `computableInTimeAndSpace_isZero`. -/
+public theorem ComputableInLinearTimeAndSpace.natIsZero :
+    ComputableInLinearTimeAndSpace (fun n => decide (n = 0)) encNat encBool :=
+  computableInTimeAndSpace_isZero.linear
 
 end Turing.MultiTapeTM

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

@@ -16,8 +16,8 @@ import Mathlib.Tactic.Ring
 /-!
 # 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.
+The encoding and the carry word folds are independent of resource certificates. Their
+definitions and arithmetic correctness proofs are retained here.
 -/
 
 public section
@@ -80,102 +80,4 @@ public lemma length_encAcc (p : Bool × List Bool) : (encAcc p).length = p.2.len
 
 end NatSucc
 
-namespace NatPred
-
-/-- Subtracts a borrow from the binary digits `l`, least significant first, keeping a leading
-zero. -/
-@[expose] public def decr : List Bool → List Bool
-  | [] => []
-  | true :: l => false :: l
-  | false :: l => true :: decr l
-
-/-- Drops a leading zero, the last digit. -/
-@[expose] public def norm (l : List Bool) : List Bool :=
-  if l.getLast? = some false then l.dropLast else l
-
-lemma norm_cons {l : List Bool} (hl : l ≠ []) (b : Bool) : norm (b :: l) = b :: norm l := by
-  obtain ⟨x, hx⟩ := Option.isSome_iff_exists.mp (List.getLast?_isSome.mpr hl)
-  simp only [norm, List.getLast?_cons, hx, Option.getD_some, List.dropLast_cons_of_ne_nil hl]
-  split_ifs <;> rfl
-
-lemma bits_ne_nil {m : ℕ} (hm : m ≠ 0) : m.bits ≠ [] := by
-  rcases Nat.even_or_odd' m with ⟨k, rfl | rfl⟩
-  · rw [Nat.bit0_bits k (by omega)]; simp
-  · rw [Nat.bit1_bits]; simp
-
-lemma decr_ne_nil {l : List Bool} (hl : l ≠ []) : decr l ≠ [] := by
-  rcases l with _ | ⟨_ | _, l⟩ <;> simp_all [decr]
-
-lemma norm_bits (n : ℕ) : norm n.bits = n.bits := by
-  induction n using Nat.strong_induction_on with
-  | _ n ih =>
-    rcases Nat.even_or_odd' n with ⟨m, rfl | rfl⟩
-    · rcases Nat.eq_zero_or_pos m with rfl | hm
-      · rfl
-      · rw [Nat.bit0_bits m (by omega), norm_cons (bits_ne_nil (by omega)), ih m (by omega)]
-    · rcases Nat.eq_zero_or_pos m with rfl | hm
-      · rfl
-      · rw [Nat.bit1_bits, norm_cons (bits_ne_nil (by omega)), ih m (by omega)]
-
-public lemma bits_pred (n : ℕ) : (n - 1).bits = norm (decr n.bits) := by
-  induction n using Nat.strong_induction_on with
-  | _ n ih =>
-    rcases Nat.even_or_odd' n with ⟨m, rfl | rfl⟩
-    · rcases Nat.eq_zero_or_pos m with rfl | hm
-      · rfl
-      · rw [Nat.bit0_bits m (by omega), decr, show 2 * m - 1 = 2 * (m - 1) + 1 by omega,
-          Nat.bit1_bits, ih m (by omega), norm_cons (decr_ne_nil (bits_ne_nil (by omega)))]
-    · rw [Nat.bit1_bits, decr, Nat.add_sub_cancel]
-      rcases Nat.eq_zero_or_pos m with rfl | hm
-      · rfl
-      · rw [Nat.bit0_bits m (by omega), norm_cons (bits_ne_nil (by omega)), norm_bits]
-
-/-- One round of the decrement: subtract the borrow from the digit `b`, append the result and keep
-the borrow. -/
-@[expose] public def decrStep (p : Bool × List Bool) (b : Bool) : Bool × List Bool :=
-  (p.1 && !b, p.2 ++ [p.1 ^^ b])
-
-lemma length_decr (l : List Bool) : (decr l).length = l.length := by
-  induction l with
-  | nil => rfl
-  | cons b l ih => cases b <;> simp [decr, ih]
-
-lemma foldl_decrStep (l : List Bool) (c : Bool) (out : List Bool) :
-    (l.foldl decrStep (c, out)).2 = out ++ if c then decr l else l := by
-  induction l generalizing c out with
-  | nil => cases c <;> simp [decr]
-  | cons b l ih => cases c <;> cases b <;> simp [decrStep, ih, decr]
-
-/-- One round of dropping a leading zero: append the pending digit and keep the new one. -/
-@[expose] public def normStep (p : Option Bool × List Bool) (b : Bool) :
-    Option Bool × List Bool :=
-  (some b, p.2 ++ p.1.toList)
-
-/-- Appends the pending digit unless it is a zero. -/
-@[expose] public def normFinish (p : Option Bool × List Bool) : List Bool :=
-  if p.1 = some true then p.2 ++ [true] else p.2
-
-lemma length_foldl_normStep (l : List Bool) (p : Option Bool) (acc : List Bool) :
-    (l.foldl normStep (p, acc)).2.length ≤ acc.length + p.toList.length + l.length := by
-  induction l generalizing p acc with
-  | nil => simp
-  | cons b l ih =>
-    rw [List.foldl_cons, normStep]
-    have := ih (some b) (acc ++ p.toList)
-    simp only [Option.toList_some, List.length_append, List.length_cons, List.length_nil]
-      at this ⊢
-    omega
-
-lemma normFinish_foldl (l : List Bool) (p : Option Bool) (acc : List Bool) :
-    normFinish (l.foldl normStep (p, acc)) = acc ++ norm (p.toList ++ l) := by
-  induction l generalizing p acc with
-  | nil => rcases p with _ | _ | _ <;> simp [normFinish, norm]
-  | cons b l ih =>
-    rw [List.foldl_cons, normStep, ih]
-    rcases p with _ | p
-    · simp
-    · simp [norm_cons]
-
-end NatPred
-
 end Turing.MultiTapeTM