refactor(Machines): binary multiplication as one cubic-time linear-space certificate (#608)

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

@@ -12,17 +12,13 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.A
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Primitives
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.NormalForm
-import Mathlib.Tactic.Linarith
-import Mathlib.Tactic.Ring
 
 /-!
 # Addition and multiplication with bounds of given degrees
 
-Natural numbers are encoded in binary (`Turing.MultiTapeTM.encNat`). Addition is a left fold over
-the digits of the first summand that keeps the carry, the rest of the digits of the second summand
-and the digits of the sum so far; at the end the carry is added to the rest of the second summand.
-Multiplication is a left fold over the digits of the first factor that keeps the product so far and
-the second factor shifted by the digits read, adding the shifted factor for every digit `1`.
+Natural numbers are encoded in binary (`Turing.MultiTapeTM.encNat`). Both results are tidy forms of
+the schoolbook certificates `Turing.MultiTapeTM.ComputableInO.natAdd` and
+`Turing.MultiTapeTM.ComputableInO.natMul`.
 
 ## Main results
 
@@ -32,50 +28,26 @@ the second factor shifted by the digits read, adding the shifted factor for ever
 
 namespace Turing.MultiTapeTM
 
-open ComputableTidilyInDegree
+/-- A `ComputableInO` certificate with bounds of degrees `d` and `e ≤ d` is tidy within them. -/
+private theorem ComputableInO.computableTidilyInDegree {f : ℕ × ℕ → ℕ} {T S : ℕ × ℕ → ℕ}
+    {d e : ℕ} (h : ComputableInO f (encPair encNat encNat) encNat T S)
+    (hT : DegreeBounded (fun p => (encPair encNat encNat p).length) T d)
+    (hS : DegreeBounded (fun p => (encPair encNat encNat p).length) S e) (hed : e ≤ d) :
+    ComputableTidilyInDegree f (encPair encNat encNat) encNat d e := by
+  obtain ⟨c, hc, hl⟩ := Internal.NormalForm.inO h
+  have hs := (hS.add_const 1).smul c
+  exact ⟨⟨_, _, (hT.add_const 1).smul c, hs.mono_deg hed, hc⟩, hs.mono hl⟩
 
 /-- **Addition is tidily computable in quadratic time and space**, in the binary encoding. -/
 public theorem computableTidilyInDegree_add :
-    ComputableTidilyInDegree (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat 2 1 := by
-  obtain ⟨c, hc, hl⟩ := Internal.NormalForm.inO ComputableInO.natAdd
-  have hT : DegreeBounded (fun p => (encPair encNat encNat p).length)
-      (fun p => ((encPair encNat encNat p).length + 1) ^ 2) 2 := ⟨1, fun _ => by simp⟩
-  have hS : DegreeBounded (fun p => (encPair encNat encNat p).length)
-      (fun p => (encPair encNat encNat p).length + 1) 1 := ⟨1, fun _ => by simp⟩
-  have ht := (hT.add_const 1).smul c
-  have hs := (hS.add_const 1).smul c
-  exact ⟨⟨_, _, ht, hs.mono_deg (by decide), hc⟩, hs.mono hl⟩
-
+    ComputableTidilyInDegree (fun p : ℕ × ℕ => p.1 + p.2) (encPair encNat encNat) encNat 2 1 :=
+  ComputableInO.natAdd.computableTidilyInDegree ⟨1, fun _ => by simp⟩ ⟨1, fun _ => by simp⟩
+    (by decide)
 
-open NatMul in
 /-- **Multiplication is tidily computable in cubic time and space**, in the binary encoding. -/
 public theorem computableTidilyInDegree_mul :
-    ComputableTidilyInDegree (fun p : ℕ × ℕ => p.1 * p.2) (encPair encNat encNat) encNat 3 1 := by
-  let encS := encPair encNat encNat
-  have hadd := computableTidilyInDegree_add
-  -- a round of the fold
-  have hstep : ComputableTidilyInDegree (fun p : (ℕ × ℕ) × Bool => mulStep p.1 p.2)
-      (encPair encS encBool) encS 2 1 := by
-    have hs := fst encS encBool
-    exact (((snd encS encBool).ite ((hadd.comp hs).restrict _) (hs.fst'.restrict _)).prod
-      (hadd.comp (hs.snd'.prod hs.snd'))).mono
-  have hfold := foldl' (encL := encBits) (encB := encS)
-    (list := fun p : ℕ × ℕ => p.1.bits) (init := fun p => (0, p.2))
-    (of_eq (encIn := encNat) (encMid := encBits) (f := Nat.bits) (fun _ => rfl) |>.comp
-      (fst encNat encNat))
-    ((const 0).prod (snd encNat encNat)) hstep
-    (B := fun p => 3 * (encPair encNat encNat p).length + 1)
-    ((DegreeBounded.self.smul 3).add_const 1) fun p i hi => ?_
-  · have h : ComputableTidilyInDegree (_ ∘ _) _ encNat 3 1 := ((fst encNat encNat).comp hfold).mono
-    convert h using 1
-    funext p
-    simp [foldl_mulStep]
-  · obtain ⟨h₁, h₂⟩ := foldl_mulStep_le (p.1.bits.take i) 0 p.2
-    have hi' : (p.1.bits.take i).length ≤ p.1.size := by simp [← Nat.size_eq_bits_len]
-    have hacc := size_le_of_le _ (by omega : (List.foldl mulStep (0, p.2) (p.1.bits.take i)).1 ≤
-      2 ^ (p.1.bits.take i).length * p.2)
-    have hsh := size_le_of_le _ h₂.le
-    simp only [encS, length_encPair, encNat_apply, Nat.size_eq_bits_len] at hacc hsh hi' ⊢
-    omega
+    ComputableTidilyInDegree (fun p : ℕ × ℕ => p.1 * p.2) (encPair encNat encNat) encNat 3 1 :=
+  ComputableInO.natMul.computableTidilyInDegree ⟨1, fun _ => by simp⟩ ⟨1, fun _ => by simp⟩
+    (by decide)
 
 end Turing.MultiTapeTM

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

@@ -285,44 +285,11 @@ theorem natMod :
       fun p => 16 * ((encPair encNat encNat p).length + 1) :=
   snd' natDivMod
 
-/-- Adding the first component to the second. -/
-def addStep (q : ℕ × ℕ) : ℕ × ℕ := (q.1, q.2 + q.1)
-
-theorem iterate_addStep (k x a : ℕ) : addStep^[k] (x, a) = (x, a + k * x) := by
-  induction k generalizing a with
-  | zero => simp
-  | succ k ih => rw [Function.iterate_succ_apply, addStep, ih]; congr 1; ring
-
 /-- **Multiplication in binary.** -/
 theorem natMul :
     ComputableInSpace (fun p : ℕ × ℕ => p.1 * p.2) (encPair encNat encNat) encNat
-      fun p => 32 * ((encPair encNat encNat p).length + 1) := by
-  have hstep : ComputableInSpace addStep (encPair encNat encNat) (encPair encNat encNat)
-      fun q => 4 * ((encPair encNat encNat q).length + 1) := by
-    have hl : (fun q => (encPair encNat encNat q).length) ≼
-        fun q => 4 * ((encPair encNat encNat q).length + 1) := .of_le fun _ => by omega
-    have h := budget_prod ((fst encNat encNat).weaken hl)
-      (budget_binop natAdd linear_succ ((snd encNat encNat).weaken hl)
-        ((fst encNat encNat).weaken hl))
-    exact h.of_enc_eq fun _ => rfl
-  have hinit : ComputableInSpace (fun p : ℕ × ℕ => (p.1, 0)) (encPair encNat encNat)
-      (encPair encNat encNat) fun p => 2 * ((encPair encNat encNat p).length + 1) :=
-    (budget_prod (fst _ _) (budget_const 0 (.refl _))).weaken (.of_le fun p => by omega)
-  have hlen (p : ℕ × ℕ) (k : ℕ) (hk : k ≤ p.2) :
-      (encPair encNat encNat (addStep^[k] (p.1, 0))).length ≤
-        3 * ((encPair encNat encNat p).length + 1) := by
-    rw [iterate_addStep, zero_add]
-    have := (Turing.MultiTapeTM.length_encNat_mono (Nat.mul_le_mul_right p.1 hk)).trans
-      (length_encNat_mul_le p.2 p.1)
-    simp only [length_encPair] at this ⊢
-    omega
-  have h := iterate (n := fun p : ℕ × ℕ => p.2) (snd _ _) hinit hstep
-    (Q := fun p => 4 * (3 * ((encPair encNat encNat p).length + 1) + 1))
-    (B := fun p => 3 * ((encPair encNat encNat p).length + 1))
-    (fun p k hk => by have := hlen p k hk; omega) hlen
-  refine (snd' h).mono_le (fun p => ?_) |>.of_enc_eq fun p => ?_
-  · simp only [length_encPair]; omega
-  · rw [iterate_addStep, zero_add, Nat.mul_comm]
+      fun p => 32 * ((encPair encNat encNat p).length + 1) :=
+  (of_inO ComputableInO.natMul).weaken (.of_le fun _ => by omega)
 
 /-! ### Lists of naturals -/
 
@@ -844,12 +811,6 @@ theorem natMod :
       fun p => 16 * ((encPair encNat encNat p).length + 1) :=
   snd' natDivMod
 
-/-- Adding the first component to the second, retained in the tidy namespace. -/
-abbrev addStep : ℕ × ℕ → ℕ × ℕ := ComputableInSpace.addStep
-
-theorem iterate_addStep (k x a : ℕ) : addStep^[k] (x, a) = (x, a + k * x) :=
-  ComputableInSpace.iterate_addStep k x a
-
 theorem natMul :
     ComputableTidilyInSpace (fun p : ℕ × ℕ => p.1 * p.2) (encPair encNat encNat) encNat
       fun p => 32 * ((encPair encNat encNat p).length + 1) :=

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

@@ -10,10 +10,8 @@ module
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Streaming
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives
 public import Mathlib.Tactic.FunProp
-import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Nat.Arithmetic
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryAddition
-import Mathlib.Data.Nat.Size
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
@@ -387,38 +385,11 @@ theorem computableInDegree_add :
   ComputableInO.natAdd.computableInDegree
     ⟨1, fun _ => by simp⟩ ⟨1, fun _ => by simp⟩ (by decide)
 
-
-open NatMul in
 /-- **Multiplication is computable in cubic time and space**, with linear output length, in the
 binary encoding. -/
 theorem computableInDegree_mul :
-    ComputableInDegree (fun p : ℕ × ℕ => p.1 * p.2) (encPair encNat encNat) encNat 3 1 := by
-  let encS := encPair encNat encNat
-  have hadd := computableInDegree_add
-  have hstep : ComputableInDegree (fun p : (ℕ × ℕ) × Bool => mulStep p.1 p.2)
-      (encPair encS encBool) encS 2 1 := by
-    have hs := ComputableInDegree.fst encS encBool
-    exact (((ComputableInDegree.snd encS encBool).ite ((hadd.comp hs).restrict _)
-      (hs.fst'.restrict _)).prod (hadd.comp (hs.snd'.prod hs.snd'))).mono
-  have hfold := ComputableInDegree.foldl' (encL := encBits) (encB := encS)
-    (list := fun p : ℕ × ℕ => p.1.bits) (init := fun p => (0, p.2))
-    (ComputableInDegree.of_eq (encIn := encNat) (encMid := encBits) (f := Nat.bits)
-      (fun _ => rfl) |>.comp (ComputableInDegree.fst encNat encNat))
-    ((ComputableInDegree.const 0).prod (ComputableInDegree.snd encNat encNat)) hstep
-    (B := fun p => 3 * (encPair encNat encNat p).length + 1)
-    ((DegreeBounded.self.smul 3).add_const 1) fun p i _ => ?_
-  · have h : ComputableInDegree (_ ∘ _) _ encNat 3 1 :=
-      ((ComputableInDegree.fst encNat encNat).comp hfold).mono
-    convert h using 1
-    funext p
-    simp [foldl_mulStep]
-  · obtain ⟨h₁, h₂⟩ := foldl_mulStep_le (p.1.bits.take i) 0 p.2
-    have hi' : (p.1.bits.take i).length ≤ p.1.size := by simp [← Nat.size_eq_bits_len]
-    have hacc := size_le_of_le _ (by omega : (List.foldl mulStep (0, p.2) (p.1.bits.take i)).1 ≤
-      2 ^ (p.1.bits.take i).length * p.2)
-    have hsh := size_le_of_le _ h₂.le
-    simp only [encS, length_encPair, encNat_apply, Nat.size_eq_bits_len] at hacc hsh hi' ⊢
-    omega
+    ComputableInDegree (fun p : ℕ × ℕ => p.1 * p.2) (encPair encNat encNat) encNat 3 1 :=
+  ComputableInO.natMul.computableInDegree ⟨1, fun _ => by simp⟩ ⟨1, fun _ => by simp⟩ (by decide)
 
 attribute [fun_prop] ComputableInDegree
 attribute [fun_prop] ComputableInDegree.const ComputableInDegree.fst

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

@@ -17,17 +17,23 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreePrimiti
 import Mathlib.Tactic.Linarith
 
 /-!
-# Quadratic schoolbook binary addition
+# Schoolbook binary addition and multiplication
 
 The existing `NatAdd.addStep` fold consumes the first input's bits and the remaining bits of the
 second input, emitting one sum digit per round. A second consuming fold adds the carry to the
 remaining second input. Both folds have linear-sized states and linear-cost rounds, so addition
 takes quadratic time and independent linear output-charged workspace in the encoded input length.
 No iteration by the numeric operands or normalization of the result is needed.
 
+Multiplication folds the shift-and-add round `NatMul.mulStep` over the digits of the first factor.
+Its states have linear length and each round is one addition, so it takes cubic time and linear
+charged workspace. This is the only machine certificate for binary multiplication; the degree,
+space and polynomial-time forms are weakenings of it.
+
 ## Main results
 
 * `ComputableInO.natAdd`: binary addition in quadratic time and linear charged workspace.
+* `ComputableInO.natMul`: binary multiplication in cubic time and linear charged workspace.
 -/
 
 public section
@@ -150,4 +156,65 @@ theorem natAdd :
     rw [NatSucc.succFinish_foldl, ← NatAdd.foldl_addStep, List.nil_append, NatAdd.addBits_bits]
     rfl
 
+private abbrev encMul := encPair encNat encNat
+
+private theorem mulStep_inO :
+    ComputableInO (fun p : (ℕ × ℕ) × Bool => NatMul.mulStep p.1 p.2) (encPair encMul encBool)
+      encMul (fun p => ((encPair encMul encBool p).length + 1) ^ 2)
+      (fun p => (encPair encMul encBool p).length + 1) := by
+  have hs := fst encMul encBool
+  have hr := (snd encNat encNat).comp_linear hs
+  have h := ((snd encMul encBool).ite (natAdd.comp hs) ((fst encNat encNat).comp_linear hs)).prod
+    (natAdd.comp (hr.prod hr))
+  refine (h.mono 8 (fun p => ?_) (fun p => ?_)).of_enc_eq fun p => ?_
+  · simp only [Function.comp_apply, length_encPair, encBool_apply, List.length_singleton]
+    split_ifs <;> nlinarith
+  · simp only [Function.comp_apply, length_encPair, encBool_apply, List.length_singleton]
+    split_ifs <;> omega
+  · rfl
+
+/-- **Binary multiplication** by the shift-and-add fold `NatMul.mulStep` over the digits of the
+first factor. Each of the linearly many rounds adds numbers of linear length, so time is cubic and
+charged workspace linear in the framed input length, independently of the numeric operands. -/
+theorem natMul :
+    ComputableInO (fun p : ℕ × ℕ => p.1 * p.2) (encPair encNat encNat) encNat
+      (fun p => ((encPair encNat encNat p).length + 1) ^ 3)
+      (fun p => (encPair encNat encNat p).length + 1) := by
+  have hbits : ComputableInO Nat.bits encNat encBits (fun n => (encNat n).length)
+      (fun n => (encNat n).length) := of_eq fun _ => rfl
+  have hstate (p : ℕ × ℕ) (i : ℕ) :
+      (encMul ((p.1.bits.take i).foldl NatMul.mulStep (0, p.2))).length ≤
+        3 * (encPair encNat encNat p).length + 1 := by
+    obtain ⟨h₁, h₂⟩ := NatMul.foldl_mulStep_le (p.1.bits.take i) 0 p.2
+    have hi : (p.1.bits.take i).length ≤ p.1.size := by simp [← Nat.size_eq_bits_len]
+    have hacc := NatMul.size_le_of_le _ (by omega :
+      (List.foldl NatMul.mulStep (0, p.2) (p.1.bits.take i)).1 ≤
+        2 ^ (p.1.bits.take i).length * p.2)
+    have hsh := NatMul.size_le_of_le _ h₂.le
+    simp only [encMul, length_encPair, encNat_apply, Nat.size_eq_bits_len] at hacc hsh hi ⊢
+    omega
+  have hround (p : ℕ × ℕ) (i : ℕ) (hi : i < p.1.bits.length) :
+      (encPair encMul encBool
+        ((p.1.bits.take i).foldl NatMul.mulStep (0, p.2), p.1.bits[i])).length + 1 ≤
+        6 * (encPair encNat encNat p).length + 6 := by
+    have := hstate p i
+    rw [length_encPair]
+    simp only [encBool_apply, List.length_singleton]
+    omega
+  have hfold := foldl (hbits.comp_linear (fst encNat encNat))
+    ((const (encMid := encNat) 0).prod (snd encNat encNat)) mulStep_inO
+    (R := fun p => (6 * (encPair encNat encNat p).length + 6) ^ 2)
+    (Q := fun p => 6 * (encPair encNat encNat p).length + 6)
+    (B := fun p => 3 * (encPair encNat encNat p).length + 1)
+    (fun p i hi => Nat.pow_le_pow_left (hround p i hi) 2)
+    (fun p i hi => hround p i hi)
+    (fun p i _ => hstate p i)
+  refine ((fst encNat encNat).comp_linear hfold |>.mono 100 (fun p => ?_) (fun p => ?_))
+    |>.of_enc_eq fun p => ?_
+  · simp only [Function.comp_apply, encBits_apply, length_encPair, encNat_apply]
+    nlinarith
+  · simp only [Function.comp_apply, encBits_apply, length_encPair, encNat_apply]
+    omega
+  · simp only [Function.comp_apply, NatMul.foldl_mulStep, zero_add]
+
 end Turing.MultiTapeTM.ComputableInO

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

@@ -19,8 +19,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinaryCompari
 The existing carry folds are certified using plain machine closure.
 Reachable word states are bounded by the encoded input length, not the numeric operands.
 Strict comparison is the linear zip-transducer certificate of `BinaryComparison`.
-Captured multiplication uses the original shift-and-add fold over the first operand's bits,
-with the unchanged full-prefix state bound; its pair certificate remains private.
+Multiplication weakens the cubic-time schoolbook certificate `ComputableInO.natMul`.
 -/
 
 @[expose] public section
@@ -48,47 +47,13 @@ theorem binary_lt : ComputableInPolyTime (fun p : ℕ × ℕ => decide (p.1 < p.
     (PolyBounded.of_forall_le 1 1 (fun _ => by simp))
     (PolyBounded.of_forall_le 1 1 (fun _ => by simp))
 
-private theorem binaryMulPair :
-    ComputableInPolyTime (fun p : ℕ × ℕ => p.1 * p.2) (encPair encNat encNat) encNat := by
-  let encS := encPair encNat encNat
-  have hs := fst encS encBool
-  have hleft := (fst encNat encNat).comp hs
-  have hright := (snd encNat encNat).comp hs
-  have hstep : ComputableInPolyTime (fun p : (ℕ × ℕ) × Bool => NatMul.mulStep p.1 p.2)
-      (encPair encS encBool) encS := by
-    simpa only [NatMul.mulStep, Function.comp_apply] using
-      ((snd encS encBool).ite (binary_add.comp hs) hleft).prod
-        (binary_add.comp (hright.prod hright))
-  have hbits : ComputableInPolyTime Nat.bits encNat encBits := of_eq fun _ => rfl
-  have hfold := foldl' (encA := encBool) (encL := encBits) (encB := encS)
-    (list := fun p : ℕ × ℕ => p.1.bits) (init := fun p => (0, p.2))
-    (hbits.comp (fst encNat encNat)) ((const 0).prod (snd encNat encNat)) hstep
-    (B := fun p => 3 * (encPair encNat encNat p).length + 1)
-    (PolyBounded.of_forall_le 4 1 fun _ => by simp only [pow_one]; omega) (by
-      intro p i _
-      obtain ⟨h₁, h₂⟩ := NatMul.foldl_mulStep_le (p.1.bits.take i) 0 p.2
-      have hi' : (p.1.bits.take i).length ≤ p.1.size := by simp [← Nat.size_eq_bits_len]
-      have hacc := NatMul.size_le_of_le _ (by omega :
-        (List.foldl NatMul.mulStep (0, p.2) (p.1.bits.take i)).1 ≤
-          2 ^ (p.1.bits.take i).length * p.2)
-      have hsh := NatMul.size_le_of_le _ h₂.le
-      simp only [encS, length_encPair, encNat_apply, Nat.size_eq_bits_len] at hacc hsh hi' ⊢
-      omega)
-  have h := (fst encNat encNat).comp hfold
-  convert h using 1
-  funext p
-  simp only [Function.comp_apply, NatMul.foldl_mulStep, zero_add]
-
 /-- Multiply computed binary values, fixing their intermediate encodings for proof search. -/
-theorem binary_mul' {α : Type}
-    {input : α ↪ List Bool}
-    {left : α → ℕ}
-    {right : α → ℕ}
+theorem binary_mul' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ}
     (hleft : ComputableInPolyTime left input encNat)
     (hright : ComputableInPolyTime right input encNat) :
-    ComputableInPolyTime (fun (a : α) => left a * right a) input
-  encNat :=
-  binaryMulPair.comp (hleft.prod hright)
+    ComputableInPolyTime (fun a => left a * right a) input encNat :=
+  (ComputableInO.natMul.computableInPolyTime (PolyBounded.of_forall_le 1 3 fun _ => by simp)
+    (PolyBounded.of_forall_le 1 1 fun _ => by simp)).comp (hleft.prod hright)
 
 /-- Non-strict binary comparison, composed from the existing strict comparison certificate.
 Automatic composition uses the computed-operand rule `binary_le'`. -/