refactor(machines): move raw machine lemmas out of the classes (part 1)

Complexity.lean

@@ -560,7 +560,6 @@ public import Complexity.Computability.Complexity.Classes.FewP.Machine
 public import Complexity.Computability.Complexity.Classes.Hierarchy
 public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc
 public import Complexity.Computability.Complexity.Classes.Hierarchy.Space
-public import Complexity.Computability.Complexity.Classes.Hierarchy.SpaceUniversal
 public import Complexity.Computability.Complexity.Classes.Hierarchy.Time
 public import Complexity.Computability.Complexity.Classes.IP
 public import Complexity.Computability.Complexity.Classes.IP.CoinFixing
@@ -852,6 +851,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Tid
 public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Transducer
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Arith
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Option
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Pi
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain
@@ -1080,6 +1080,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Machi
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.PolyTime
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.ResourceBound
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Space
+public import Complexity.Computability.Machines.Turing.MultiTape.Universal.SpaceBudget
 public import Complexity.Computability.Machines.Turing.SingleTape.Partrec
 public import Complexity.Computability.Machines.Turing.SingleTape.PostTuringMachine
 public import Complexity.Computability.Machines.Turing.TM2.ConfigBound

Complexity/Computability/Complexity/Classes/Alternation/GuessVerify.lean

@@ -15,6 +15,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Ba
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame
 
 /-!
 # Games of polynomially many moves are in `AP`
@@ -93,60 +94,6 @@ theorem tapeOfList_set {Symbol : Type*} (w : List Symbol) {i : ℕ} (hi : i < w.
       simp [hi]
     · simp [h, Ne.symm h]
 
-namespace MultiTapeTM
-
-/-! ### Frames followed by a word -/
-
-section Frames
-
-private theorem length_flatMap_pair (w : List Bool) :
-    (w.flatMap fun b => [true, b]).length = 2 * w.length := by
-  induction w with
-  | nil => rfl
-  | cons b w ih =>
-    simp only [List.flatMap_cons, List.length_append, ih, List.length_cons, List.length_nil]
-    ring
-
-/-- A frame split at a symbol. -/
-theorem frame_append_cons (w v : List Bool) (c : Bool) :
-    frame (w ++ c :: v) = (w.flatMap fun b => [true, b]) ++ true :: c :: frame v := by
-  simp [frame]
-
-/-- After the pairs of a frame comes its terminator `false`. -/
-theorem getElem?_frame_append_length (w x : List Bool) :
-    (frame w ++ x)[2 * w.length]? = some false := by
-  rw [frame, List.append_assoc, List.getElem?_append_right (by rw [length_flatMap_pair]),
-    length_flatMap_pair]
-  simp
-
-/-- Each pair of a frame starts with the tag `true`. -/
-theorem getElem?_frame_append_cons (w v x : List Bool) (c : Bool) :
-    (frame (w ++ c :: v) ++ x)[2 * w.length]? = some true := by
-  rw [frame_append_cons, List.append_assoc,
-    List.getElem?_append_right (by rw [length_flatMap_pair]), length_flatMap_pair]
-  simp
-
-theorem lt_length_frame_append_cons (w v x : List Bool) (c : Bool) :
-    2 * w.length + 1 < (frame (w ++ c :: v) ++ x).length := by
-  simp only [List.length_append, length_frame, List.length_cons]
-  omega
-
-/-- Setting the second cell of a pair of a frame replaces the framed symbol. -/
-theorem set_frame_append_cons (w v x : List Bool) (c b : Bool) :
-    (frame (w ++ c :: v) ++ x).set (2 * w.length + 1) b = frame (w ++ b :: v) ++ x := by
-  rw [frame_append_cons, frame_append_cons, List.append_assoc, List.append_assoc,
-    List.set_append_right _ _ (by rw [length_flatMap_pair]; omega), length_flatMap_pair]
-  simp
-
-theorem two_mul_length_le_length_frame_append (w x : List Bool) :
-    2 * w.length ≤ (frame w ++ x).length := by
-  simp only [List.length_append, length_frame]
-  omega
-
-end Frames
-
-end MultiTapeTM
-
 namespace MultiTapeATM
 
 open MultiTapeMachine

Complexity/Computability/Complexity/Classes/Constructible.lean

@@ -11,10 +11,10 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Spac
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative
 import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormalForm
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Arith
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower
 import Complexity.Computability.Machines.Turing.MultiTape.Universal.Compose
-import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
 import Cslib.Computability.Machines.Turing.MultiTape.Combinators.AlmostConstant
 
 /-!
@@ -26,8 +26,11 @@ The input tape is read-only and the output tape write-only. Neither definition i
 bound on the resource function; hierarchy theorems state the lower bounds they need separately.
 
 The shared length and arithmetic routines give concrete constructible bounds, without importing
-any hierarchy theorem. Unary word length is supplied by the quantitative API
-(`Turing.MultiTapeTM.ComputableTidilyInO.lengthUnary`).
+any hierarchy theorem. The length of a word in binary
+(`Turing.MultiTapeTM.ComputableTidilyInO.lengthNat`) and the bounds on binary digits
+(`Turing.MultiTapeTM.exists_pow_length_encNat_le`) are in
+`Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible`; unary word
+length is supplied by the quantitative API (`Turing.MultiTapeTM.ComputableTidilyInO.lengthUnary`).
 
 ## Main definitions
 
@@ -52,144 +55,6 @@ any hierarchy theorem. Unary word length is supplied by the quantitative API
 
 @[expose] public section
 
-namespace Turing.MultiTapeTM
-
-/-- The binary digits of `m` are logarithmic: `2 ^ (encNat m).length ≤ 2 * (m + 1)`. -/
-theorem two_pow_length_encNat_le (m : ℕ) : 2 ^ (encNat m).length ≤ 2 * (m + 1) := by
-  rw [encNat_apply, Nat.size_eq_bits_len]
-  rcases Nat.eq_zero_or_pos m with rfl | hm
-  · simp
-  · have h₁ : 2 ^ (m.size - 1) ≤ m := Nat.lt_size.mp (by
-      have := Nat.size_pos.mpr hm
-      omega)
-    have h₂ : 1 ≤ m.size := Nat.size_pos.mpr hm
-    rw [show m.size = (m.size - 1) + 1 by omega, pow_succ]
-    omega
-
-/-- Every power of the number of binary digits of `m` is `O(m + 1)`. -/
-theorem exists_pow_length_encNat_le (d : ℕ) :
-    ∃ C, ∀ m, ((encNat m).length + 1) ^ d ≤ C * (m + 1) := by
-  obtain ⟨C, hC⟩ := Cslib.PolynomiallyBounded.exists_le_mul_two_pow (p := fun L => (L + 1) ^ d)
-    (by fun_prop)
-  refine ⟨2 * C, fun m => (hC _).trans ?_⟩
-  calc C * 2 ^ (encNat m).length ≤ C * (2 * (m + 1)) :=
-        Nat.mul_le_mul_left _ (two_pow_length_encNat_le m)
-    _ = 2 * C * (m + 1) := by ring
-
-/-! ### Lengths and comparisons, computed -/
-
-namespace ComputableTidilyInO
-
-/-- The length of a bit word in binary, by a binary counter, within quadratic time and linear
-space. -/
-theorem lengthNat : ComputableTidilyInO (fun l : List Bool => l.length) encBits encNat
-    (fun l => (l.length + 1) ^ 2) fun l => l.length + 1 := by
-  obtain ⟨C, hC⟩ := exists_pow_length_encNat_le 2
-  have hstep := natSucc.comp (fst encNat encBool)
-  have hlen (x : List Bool) (i : ℕ) :
-      (List.take i x).foldl (fun n _ => n + 1) 0 = min i x.length := by
-    simp [List.foldl_const]
-  have h := foldl (encA := encBool) (encL := encBits) (encB := encNat) (list := id)
-    (init := fun _ => 0) (step := fun n _ => n + 1) (of_linear (.of_eq fun _ => rfl)) (const 0)
-    hstep (R := fun x => (C + 3) * (x.length + 1)) (Q := fun x => 3 * (x.length + 1))
-    (B := fun x => x.length)
-    (fun x i hi => by
-      simp only [id] at hi ⊢
-      rw [hlen]
-      have h₁ := hC (min i x.length)
-      have h₂ := Universal.length_encNat_le (min i x.length)
-      have h₃ : C * (min i x.length + 1) ≤ C * (x.length + 1) :=
-        Nat.mul_le_mul_left _ (by omega)
-      have e : (C + 3) * (x.length + 1) = C * (x.length + 1) + 3 * (x.length + 1) := by ring
-      simp only [length_encPair, encBool_apply, List.length_singleton]
-      omega)
-    (fun x i hi => by
-      simp only [id] at hi ⊢
-      rw [hlen]
-      have h₂ := Universal.length_encNat_le (min i x.length)
-      simp only [length_encPair, encBool_apply, List.length_singleton]
-      omega)
-    (fun x i hi => by
-      simp only [id] at hi ⊢
-      rw [hlen]
-      exact (Universal.length_encNat_le _).trans (Nat.min_le_right _ _))
-  refine (h.mono (C + 16) (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_
-  · simp only [id, encBits_apply]
-    nlinarith
-  · simp only [id, encBits_apply]
-    nlinarith
-  · simp [List.foldl_const]
-
-/-- The comparison of unary numbers, by counting down, within quadratic time and linear space. -/
-theorem unaryLe : ComputableTidilyInO (fun p : ℕ × ℕ => decide (p.1 ≤ p.2))
-    (encPair encUnary encUnary) encBool (fun p => ((encPair encUnary encUnary p).length + 1) ^ 2)
-    fun p => (encPair encUnary encUnary p).length + 1 := by
-  have hstep := (ComputableTidilyInDegree.unary_pred.inO_one).comp (fst encUnary encBool)
-  have hrep (a b : ℕ) : (List.replicate b true).foldl (fun n _ => n - 1) a = a - b := by
-    induction b generalizing a with
-    | zero => rfl
-    | succ b ih => rw [List.replicate_succ, List.foldl_cons, ih]; omega
-  have h := foldl (encA := encBool) (encL := encBits) (encB := encUnary)
-    (list := fun p : ℕ × ℕ => List.replicate p.2 true) (init := fun p => p.1)
-    (step := fun n _ => n - 1)
-    ((of_linear (.of_eq (f := fun n => List.replicate n true) (encIn := encUnary)
-      (encMid := encBits) fun _ => rfl)).comp (snd encUnary encUnary))
-    (fst encUnary encUnary) hstep
-    (R := fun p => 3 * ((encPair encUnary encUnary p).length + 1))
-    (Q := fun p => 3 * ((encPair encUnary encUnary p).length + 1))
-    (B := fun p => (encPair encUnary encUnary p).length)
-    (fun p i hi => by
-      rw [List.take_replicate, hrep]
-      simp only [length_encPair, encUnary_apply, List.length_replicate,
-        encBool_apply, List.length_singleton]
-      omega)
-    (fun p i hi => by
-      rw [List.take_replicate, hrep]
-      simp only [length_encPair, encUnary_apply, List.length_replicate,
-        encBool_apply, List.length_singleton]
-      omega)
-    (fun p i hi => by
-      rw [List.take_replicate, hrep]
-      simp only [length_encPair, encUnary_apply, List.length_replicate]
-      omega)
-  have hz := (ComputableTidilyInDegree.unary_isZero.inO_one).comp_linear h
-  refine (hz.mono 16 (fun p => ?_) fun p => ?_).of_enc_eq fun p => ?_
-  · simp only [length_encPair, encUnary_apply, List.length_replicate,
-      encBits_apply]
-    nlinarith
-  · simp only [length_encPair, encUnary_apply, List.length_replicate,
-      encBits_apply]
-    omega
-  · simp only [Function.comp_apply, hrep, Nat.sub_eq_zero_iff_le]
-
-end ComputableTidilyInO
-
-/-- **From binary to unary**, by counting down: within time `O((n + 1) ^ 3)` and space `O(n)`. -/
-theorem ComputableTidilyInO.natToUnary : ComputableTidilyInO (fun n : ℕ => n) encNat encUnary
-    (fun n => (n + 1) ^ 3) fun n => n := by
-  have hiter (n : ℕ) : (· + 1)^[n] 0 = n := by
-    induction n with
-    | zero => rfl
-    | succ n ih => rw [Function.iterate_succ_apply', ih]
-  have h := ComputableTidilyInO.iterate (n := fun n : ℕ => n) (init := fun _ => 0)
-    (step := (· + 1)) (encIn := encNat) (encB := encUnary)
-    (ComputableTidilyInO.of_linear (.of_eq fun _ => rfl)) (ComputableTidilyInO.const 0)
-    ComputableTidilyInDegree.unary_succ.inO_one (R := fun n => n) (Q := fun n => n)
-    (B := fun n => n)
-    (fun n k hk => by simp only [hiter, encUnary_apply, List.length_replicate]; exact hk)
-    (fun n k hk => by simp only [hiter, encUnary_apply, List.length_replicate]; exact hk)
-    (fun n k hk => by simp only [hiter, encUnary_apply, List.length_replicate]; exact hk)
-  refine (h.of_enc_eq fun n => by rw [hiter]).mono 8 (fun n => ?_) fun n => ?_
-  all_goals
-    have := Universal.length_encNat_le n
-    have h₁ : (n + 1) ^ 2 ≤ (n + 1) ^ 3 := Nat.pow_le_pow_right (by omega) (by omega)
-    have h₂ : n + 1 ≤ (n + 1) ^ 2 := Nat.le_self_pow (by norm_num) _
-    have h₃ := Nat.pow_le_pow_left (show (encNat n).length + 1 ≤ n + 1 by omega) 2
-  · nlinarith
-  · omega
-
-end Turing.MultiTapeTM
-
 namespace Cslib.Complexity
 
 open Turing Turing.MultiTapeTM Turing.MultiTapeTM.Universal

Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean

@@ -7,8 +7,12 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Computability.Complexity.Classes.Constructible
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative
+import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame
 import Complexity.Computability.Machines.Turing.MultiTape.Universal.Bound
+import Mathlib.Data.Nat.Size
 
 /-!
 # Short descriptions

Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean

@@ -10,10 +10,11 @@ module
 public import Complexity.Computability.Complexity.Classes.Constructible
 public import Complexity.Computability.Complexity.Classes.Hierarchy
 public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc
-public import Complexity.Computability.Complexity.Classes.Hierarchy.SpaceUniversal
 public import Complexity.Computability.Complexity.Classes.LogSpace
 public import Complexity.Computability.Complexity.Classes.Space.Time
 public import Complexity.Computability.Machines.Turing.MultiTape.Run
+public import Complexity.Computability.Machines.Turing.MultiTape.Universal.SpaceBudget
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
 

Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean

@@ -12,6 +12,7 @@ public import Complexity.Computability.Complexity.Classes.Hierarchy
 public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc
 public import Complexity.Computability.Complexity.Classes.Time
 public import Complexity.Computability.Machines.Turing.MultiTape.Run
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential