refactor(Encodings): close encoded length bounds with enc_len

Complexity.lean

@@ -4489,6 +4489,7 @@ public import Complexity.Probability.StatisticalDistance.UniformMod
 public import Complexity.Probability.Uniform
 public import Complexity.Probability.UniformNat
 public import Complexity.Probability.UniversalHash
+public import Complexity.Tactic.EncLen
 public import Complexity.Tactic.FOOperator
 public import Complexity.Tactic.FOOperator.Init
 public import Complexity.Tactic.FirstOrder

Complexity/Computability/Circuit/Boolean/BalancedCode.lean

@@ -16,6 +16,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
+import Complexity.Tactic.EncLen
 import Mathlib.Data.List.GetD
 import Mathlib.Data.List.TakeDrop
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
@@ -103,11 +104,9 @@ private theorem codeMass_le_encoding (c : Code) : codeMass c ≤ (encCode c).len
     apply List.sum_le_sum
     intro gate _
     have := length_le_length_encList encNat gate.2
-    simp only [encGate, Circuit.encGate, length_encPair]
-    omega
+    enc_len [encGate, Circuit.encGate]
   have ho := length_le_length_encList encNat c.2
-  simp only [codeMass, encCode, Circuit.encCode, encGate, length_encPair] at hg ⊢
-  omega
+  enc_len [codeMass, encCode, Circuit.encCode, encGate] at hg ⊢
 
 private theorem wireBitsLe_encoding (c : Code) : WireBitsLe c (encCode c).length := by
   constructor
@@ -121,8 +120,7 @@ private theorem wireBitsLe_encoding (c : Code) : WireBitsLe c (encCode c).length
     omega
   · intro wire hw
     have := length_le_encList_of_mem encNat hw
-    simp only [encCode, length_encPair]
-    omega
+    enc_len [encCode]
 
 private theorem codeMass_append (n : ℕ) (c d : Code) :
     codeMass (appendCode n c d) = codeMass c + codeMass d := by

Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionMachine
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionStep
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists
+import Complexity.Tactic.EncLen
 import Mathlib.Data.List.GetD
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
 
@@ -100,17 +101,14 @@ theorem scale_add_prec_add_length_fl_le (x : Call T) :
     x.scale + x.prec + x.fl.length ≤ (encCall encT x).length := by
   have h := length_le_length_encList encNat x.fl
   obtain ⟨⟨s, d, b, p, fl, r⟩, D⟩ := x
-  simp only [Call.scale, Call.prec, Call.fl, encCall, encParams, length_encPair, encUnary_apply,
-    List.length_replicate] at h ⊢
-  omega
+  enc_len [Call.scale, Call.prec, Call.fl, encCall, encParams] at h ⊢
 
 /-- The network of a call is at most its encoded length. -/
 theorem length_net_le (x : Call T) :
     (DescribedNetwork.encDescribed (VertexDesc.enc encT) x.net).length ≤
       (encCall encT x).length := by
   obtain ⟨p, D⟩ := x
-  simp only [Call.net, encCall, length_encPair]
-  omega
+  enc_len [Call.net, encCall]
 
 /-- A vertex of a call is at most its encoded length. -/
 theorem length_vertex_le {x : Call T} {v : List ℕ × VertexDesc T}
@@ -121,9 +119,7 @@ theorem length_vertex_le {x : Call T} {v : List ℕ × VertexDesc T}
       (DescribedNetwork.encDescribed (VertexDesc.enc encT) x.net).length := by
     change _ ≤ (encPair encUnary (encList (encPair (encList encNat) (VertexDesc.enc encT)))
       (x.net.numEdges, x.net.vertices)).length
-    rw [length_encPair]
-    dsimp only
-    omega
+    enc_len
   have h3 := length_net_le encT x
   omega
 

Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedResources.lean

@@ -13,6 +13,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds.Polynom
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListPrimitives
 import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends
+import Complexity.Tactic.EncLen
 
 /-!
 # Resources of the truncation-order reduction
@@ -146,8 +147,7 @@ theorem length_encCore_coreInput_le (y : List ℕ × ℕ × ℕ × ℕ × Descri
     (P, ℓ, fl, FastContraction.digits fl.length k)
   set L := (encEngine encT (fl, P, ℓ, r, G)).length
   have hd : (encSpecData (P, ℓ, fl, FastContraction.digits fl.length k)).length ≤ 3 * L := by
-    simp only [length_encPair, encUnary_apply, List.length_replicate] at hlen ⊢
-    omega
+    enc_len at hlen ⊢
   have hkL : G.vertices.length ≤ L := by omega
   have hmul : G.vertices.length *
       (2 * (encSpecData (P, ℓ, fl, FastContraction.digits fl.length k)).length) ≤ L * (6 * L) :=
@@ -175,8 +175,7 @@ theorem length_run_engineStep_le (y : List ℕ × ℕ × ℕ × ℕ × Described
       obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hv
       exact hY k (List.mem_range.mp hk)
   simp only [List.length_map, List.length_range] at h
-  simp only [length_encPair]
-  omega
+  enc_len
 
 /-! ### The loop -/
 
@@ -284,8 +283,7 @@ theorem engineCertificate_le (cc : NativeCertificate core (encCore encT) (encLis
     have hs := hstate j hj
     have hY := (hcore j hj).2.2
     rw [run_engineStep] at hs ⊢
-    simp only [length_encPair] at hs ⊢
-    omega
+    enc_len at hs ⊢
   have hround_time (j : ℕ) (hj : j ≤ N) :
       (IndexFold.roundCertificate (engineStepCertificate core cc)).time
           (IndexFold.run (engineStep core) j (y, [])) ≤
@@ -424,11 +422,8 @@ theorem specEntryCertificate_le :
   have hnZ : n ≤ Z := by omega
   have hH : (encPair encSpecData (encList encNat) ((P, ℓ, fl, ζ), entry t bs)).length ≤
       2 * Z + 1 := by
-    have : (encSpecData (P, ℓ, fl, ζ)).length ≤ n := by
-      simp only [hn, length_encPair]
-      omega
-    simp only [length_encPair] at this ⊢
-    omega
+    have : (encSpecData (P, ℓ, fl, ζ)).length ≤ n := by enc_len [hn]
+    enc_len at this ⊢
   simp only [U] at hUZ
   have h1 := (bD ((t, P, ℓ, fl, ζ), bs)).1.trans (mD hnZ)
   have h2 := (bE ((t, P, ℓ, fl, ζ), bs)).1.trans (mE hnZ)
@@ -506,8 +501,7 @@ theorem directCoreCertificate_le (entry : T → List Bool → List ℕ)
   set X := 2 ^ G.numEdges with hX
   have hX1 : 1 ≤ X := Nat.one_le_two_pow
   have hG'n : (DescribedNetwork.encDescribed (encSpecDesc encT) G').length ≤ n := by
-    simp only [hn, encCore, length_encPair]
-    omega
+    enc_len [hn, encCore]
   -- The specialized entries.
   have hv : ∀ v' ∈ G'.vertices, ∀ bs : List Bool, bs.length = v'.1.length →
       (specEntryCertificate entry ce).time (v'.2, bs) ≤ E + Uf Z ∧
@@ -543,19 +537,15 @@ theorem directCoreCertificate_le (entry : T → List Bool → List ℕ)
   have hr : ∀ z, SumOps.galois.Reduced (P, fl) z → (encList encNat z).length ≤ Z * (2 * Z + 3) :=
     fun z hz => (SumOps.length_encList_le_of_galois_reduced hz).trans (by
       have hfl := length_le_length_encList encNat fl
-      have hlen : (encList encNat fl).length + P ≤ n := by
-        simp only [hn, encCore, length_encPair, encUnary_apply, List.length_replicate]
-        omega
+      have hlen : (encList encNat fl).length + P ≤ n := by enc_len [hn, encCore]
       dsimp only
       exact Nat.mul_le_mul (by omega) (by omega))
   obtain ⟨hT, hS⟩ := hK₂ ((P, fl), G') (E + Uf Z) (ES + Uf Z) (cS * (Z + Uf Z + 1))
     (Z * (2 * Z + 3)) hv hr
   have hin : (DescribedNetwork.encInput (encPair encUnary (encList encNat)) (encSpecDesc encT)
       ((P, fl), G')).length ≤ 2 * Z + 1 := by
     have : (DescribedNetwork.encInput (encPair encUnary (encList encNat)) (encSpecDesc encT)
-        ((P, fl), G')).length ≤ 2 * n + 1 := by
-      simp only [hn, DescribedNetwork.encInput, encCore, length_encPair]
-      omega
+        ((P, fl), G')).length ≤ 2 * n + 1 := by enc_len [hn, DescribedNetwork.encInput, encCore]
     omega
   have hB : K₂ * ((DescribedNetwork.encInput (encPair encUnary (encList encNat))
       (encSpecDesc encT) ((P, fl), G')).length + cS * (Z + Uf Z + 1) + Z * (2 * Z + 3) + 1) ^ K₂ ≤

Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean

@@ -11,6 +11,7 @@ public import Complexity.Computability.GenericRAM.Native.IndexFold
 public import Complexity.Foundations.Data.Nat.ResidueSum
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv
+import Complexity.Tactic.EncLen
 
 /-!
 # Streamed sums modulo a computed modulus
@@ -175,8 +176,7 @@ theorem exists_computableInO_modSum {encC : C ↪ List Bool}
     rw [run_modSumStep hj]
     have hacc := length_encNat_mono (foldl_add_mod_lt (f := fun i => r (c, i)) (hpos c) j).le
     have hj' := length_encNat_mono hj
-    simp only [length_encPair, S, L, lm, lk] at hacc hj' ⊢
-    omega
+    enc_len [S, L, lm, lk] at hacc hj' ⊢
   have hround_time (c : C) (j : ℕ) (hj : j ≤ count c) :
       cstep.time (IndexFold.run (modSumStep r modulus count) j (c, 0)) ≤ U c + R c := by
     have hs := hstate c j hj
@@ -193,8 +193,7 @@ theorem exists_computableInO_modSum {encC : C ↪ List Bool}
           (acc, r (c, j), modulus c)).length ≤ S' c := by
         have := length_encNat_mono hacc_lt.le
         have := length_encNat_mono hrj.le
-        simp only [length_encPair, S', lm] at *
-        omega
+        enc_len [S', lm] at *
       have h2 := (bC (j, (c, acc))).1.trans (mC hs)
       have h3 := (bA (j, (c, acc))).1.trans (mA hs)
       have h4 := (bW (j, (c, acc))).1.trans (mW hs)
@@ -222,8 +221,7 @@ theorem exists_computableInO_modSum {encC : C ↪ List Bool}
           (acc, r (c, j), modulus c)).length ≤ S' c := by
         have := length_encNat_mono hacc_lt.le
         have := length_encNat_mono hrj.le
-        simp only [length_encPair, S', lm] at *
-        omega
+        enc_len [S', lm] at *
       have h2 := (bC (j, (c, acc))).2.trans (mC hs)
       have h3 := (bA (j, (c, acc))).2.trans (mA hs)
       have h4 := (bW (j, (c, acc))).2.trans (mW hs)
@@ -240,8 +238,7 @@ theorem exists_computableInO_modSum {encC : C ↪ List Bool}
         B c := by
     rw [run_modSumStep hj]
     have := length_encNat_mono (foldl_add_mod_lt (f := fun i => r (c, i)) (hpos c) j).le
-    simp only [length_encPair, B, L, lm] at this ⊢
-    omega
+    enc_len [B, L, lm] at this ⊢
   have hrun := IndexFold.computableInO (NativeCertificate.ofPolyTime hcount)
     (NativeCertificate.ofPolyTime hinit) cstep (fun c => U c + R c) (fun c => U c + Q c) B
     hround_time hround_space hacc_len

Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean

@@ -15,6 +15,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith
+import Complexity.Tactic.EncLen
 
 /-!
 # The deterministic counting simulation, assembled from its interfaces
@@ -197,8 +198,7 @@ theorem exists_computableInO_simulate (F : NetworkFamily encN value Admissible c
       cr.time (c, i) ≤ U c * E c ∧ cr.space (c, i) ≤ U c := by
     have hZ : (encPair (encPair encBits encUnary) encNat (c, i)).length ≤ Z c := by
       have := (length_encNat_mono hi.le)
-      simp only [length_encPair, Z, sz] at this ⊢
-      omega
+      enc_len [Z, sz] at this ⊢
     have hG : (encN (F.net (c.1, c.2, i))).length ≤
         an * ((encPair (encPair encBits encUnary) encNat (c, i)).length + 1) ^ dn := hnl (c, i)
     have hY : (encPair encNat encN (paddedTime c.2 + 1, F.net (c.1, c.2, i))).length ≤ Y c := by
@@ -298,9 +298,7 @@ theorem exists_computableInO_simulate (F : NetworkFamily encN value Admissible c
   -- Absorb the constants.
   set k := k₀ * 2 ^ d₀ + d₀ + K with hk
   have hVk (c : List Bool × ℕ) : V c ≤ k * (c.1.length + c.2 + 1) ^ k := by
-    have hszc : sz c + 1 ≤ 2 * (c.1.length + c.2 + 1) := by
-      simp only [sz, length_encPair, encBits_apply, encUnary_apply, List.length_replicate]
-      omega
+    have hszc : sz c + 1 ≤ 2 * (c.1.length + c.2 + 1) := by enc_len [sz]
     calc V c ≤ k₀ * (sz c + 1) ^ d₀ := hV c
       _ ≤ k₀ * (2 * (c.1.length + c.2 + 1)) ^ d₀ :=
           Nat.mul_le_mul_left _ (Nat.pow_le_pow_left hszc _)
@@ -372,9 +370,7 @@ theorem exists_computableInO_countPair (F : NetworkFamily encN value Admissible
     have hτ := paddedTime_add_one_le h2t
     have hcnt1 : 1 ≤ scheduleCount F.heads t := Nat.one_le_pow _ _ (by norm_num)
     have hE : 1 ≤ 2 ^ (k * t / Nat.sqrt (Nat.log 2 t)) := Nat.one_le_two_pow
-    have hctx : (encPair encBits encUnary (x, t)).length ≤ 3 * t + 1 := by
-      simp only [length_encPair, encBits_apply, encUnary_apply, List.length_replicate]
-      omega
+    have hctx : (encPair encBits encUnary (x, t)).length ≤ 3 * t + 1 := by enc_len
     have hsimx : simulate F (x, t) = count x (paddedTime t) :=
       simulate_eq F hnt h2t (hcount x _)
     have hout : (encPair encUnary encNat (paddedTime t, simulate F (x, t))).length ≤ 6 * t + 3 := by
@@ -384,8 +380,7 @@ theorem exists_computableInO_countPair (F : NetworkFamily encN value Admissible
         rw [hsimx]
         calc _ ≤ (encNat (2 ^ paddedTime t)).length := length_encNat_mono (hcount x _)
           _ = paddedTime t + 1 := by rw [length_encNat_eq_size, Nat.size_pow]
-      simp only [length_encPair]
-      omega
+      enc_len
     have hTu : (encUnary (T n)).length ≤ t := by
       simp only [encUnary_apply, List.length_replicate]
       exact hTt

Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean

@@ -11,6 +11,7 @@ public import Complexity.Computability.Complexity.Classes.CountingSimulation.Fas
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionSchedule
 public import Complexity.Computability.Circuit.Frontier.TensorNetwork.FastContractionSize
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
+import Complexity.Tactic.EncLen
 
 /-!
 # The resource analysis of the native recursion: the recursion tree and the sizes
@@ -299,9 +300,7 @@ theorem le_one_of_mem_modulus {m z : ℕ} (hz : z ∈ modulus m) : z ≤ 1 := by
 /-- The encoded network is at most the encoded input long. -/
 theorem length_encExplicitNetwork_le (P : ℕ) (G : ℕ × ExplicitTensorNetwork ℕ) :
     (ExplicitTensorNetwork.encExplicitNetwork G.2).length ≤
-      (FastContraction.encInput (P, G)).length := by
-  simp only [FastContraction.encInput, length_encPair]
-  omega
+      (FastContraction.encInput (P, G)).length := by enc_len [FastContraction.encInput]
 
 /-- The vertices of an explicit network, encoded, are at most the encoded network long. -/
 theorem length_vertices_le (G : ExplicitTensorNetwork ℕ) :
@@ -342,8 +341,7 @@ theorem fastSizes : FastSizes := by
   have hp₀ : x₀.prec ≤ n := (min_le_left _ _).trans hnet
   have hrows : (encNat x₀.rows).length ≤ n := by
     change (encNat G.1).length ≤ n
-    simp only [hn, FastContraction.encInput, length_encPair]
-    omega
+    enc_len [hn, FastContraction.encInput]
   have hV₀ : x₀.net.vertices.length ≤ n := by
     change (List.map _ G.2.vertices).length ≤ n
     rw [List.length_map]; omega

Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean

@@ -20,6 +20,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.TwoPow
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
+import Complexity.Tactic.EncLen
 
 /-!
 # A nondeterministic exponential time hierarchy by lazy diagonalization
@@ -506,8 +507,7 @@ private theorem exists_computableInO_verifier (k : ℕ) :
       CE * 2 ^ (2 * (unframe p.1).length + 1) +
         4 ^ ((k + 2) * (2 * (unframe p.1).length + 1 + 1)) ≤ (2 * CE + 1) * cheap k p := by
     have hu := length_unframe_le p.1
-    have hn : p.1.length ≤ (encPair encBits encBits p).length := by
-      simp only [length_encPair, encBits_apply]; omega
+    have hn : p.1.length ≤ (encPair encBits encBits p).length := by enc_len
     obtain ⟨hZ, hE'⟩ := horizon_le k CE p.1
     set Y := 4 ^ ((k + 2) * (p.1.length + 1))
     have hY : 1 ≤ Y := Nat.one_le_pow _ _ (by norm_num)
@@ -653,8 +653,7 @@ theorem expLazyDiagonal_mem_NTIME (k : ℕ) :
     omega
   -- the tests
   have hcheap : cheap k (x, v) ≤ A₁ * M := by
-    have hN : (encPair encBits encBits (x, v)).length + 1 ≤ 2 * V := by
-      simp only [length_encPair, encBits_apply, hv', ← hn]; omega
+    have hN : (encPair encBits encBits (x, v)).length + 1 ≤ 2 * V := by enc_len [hv', ← hn]
     calc cheap k (x, v) = ((encPair encBits encBits (x, v)).length + 1) ^ 2 *
           (4 ^ ((k + 2) * (n + 1))) ^ 2 := rfl
       _ ≤ (2 * V) ^ 2 * (4 ^ ((k + 2) * (n + 1))) ^ 2 :=
@@ -704,8 +703,7 @@ theorem expLazyDiagonal_mem_NTIME (k : ℕ) :
       Nat.lt_two_pow_self.le.trans
         (Nat.pow_le_pow_right Nat.one_lt_two.le (Nat.le_mul_of_pos_left _ (Nat.succ_pos _)))
     have hlen : (encPair encBits encBits (unframe (unframe x), frame (unframe x))).length +
-        certLen k P ≤ 3 * certLen k P := by
-      simp only [length_encPair, encBits_apply, length_frame]; omega
+        certLen k P ≤ 3 * certLen k P := by enc_len
     rcases le_or_gt (3 * K) (2 ^ (P + 1)) with hK | hK
     · have hle : K * ((encPair encBits encBits (unframe (unframe x), frame (unframe x))).length +
           certLen k P) ≤ horizon k P :=

Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean

@@ -17,6 +17,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
+import Complexity.Tactic.EncLen
 
 /-!
 # A nondeterministic time hierarchy by lazy diagonalization
@@ -338,9 +339,7 @@ private theorem exists_computableInO_brute (d : ℕ) : ∃ K, ComputableInO
   have hf := hacc.comp hre
   have hsize (q : (List Bool × List Bool) × List Bool) :
       q.1.1.length ≤ (enc q).length ∧ q.1.2.length ≤ (enc q).length ∧
-        q.2.length ≤ (enc q).length := by
-    simp only [enc, length_encPair, encBits_apply]
-    omega
+        q.2.length ≤ (enc q).length := by enc_len [enc]
   have hpoly : PolyBounded (fun q => (enc q).length) fun q =>
       (enc q).length + ((enc q).length + (enc q).length) +
         accBound d D (q.1.1, q.1.2, q.2) :=
@@ -408,8 +407,7 @@ private theorem exists_computableInO_verifier (d : ℕ) :
       (2 * (encPair encBits encBits p).length + 4 +
         (2 * (unframe p.1).length + 1 + 1) ^ (d + 3)) ^ 2 ≤ (G + 4) ^ 2 * cheap d p := by
     have hu := length_unframe_le p.1
-    have hn : p.1.length ≤ (encPair encBits encBits p).length := by
-      simp only [length_encPair, encBits_apply]; omega
+    have hn : p.1.length ≤ (encPair encBits encBits p).length := by enc_len
     have hZ : (2 * (unframe p.1).length + 1 + 1) ^ (d + 3) ≤
         2 ^ (d + 3) * (p.1.length + 1) ^ (d + 3) := by
       rw [← mul_pow]; exact Nat.pow_le_pow_left (by omega) _