From 8f3595fc5c6c0398b04221447247ee7c57aaf50c Mon Sep 17 00:00:00 2001 From: chris-ai1 Date: Sun, 1 Nov 2026 22:49:25 +0000 Subject: [PATCH 1/2] refactor(Encodings): close encoded length bounds with enc_len Add the public enc_len tactic and apply it where simp only plus omega spelled the same expansion. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../Circuit/Boolean/BalancedCode.lean | 10 +- .../TensorNetwork/FastContractionLeaf.lean | 12 +- .../TensorNetwork/TruncatedResources.lean | 28 ++--- .../CountingSimulation/Accumulate.lean | 13 +- .../Classes/CountingSimulation/Assembly.lean | 15 +-- .../CountingSimulation/FastAnalysis.lean | 8 +- .../NondeterministicExponentialTime.lean | 13 +- .../Hierarchy/NondeterministicTime.lean | 9 +- .../Classes/Hierarchy/TimePolylog.lean | 8 +- .../Complexity/Classes/NP/SelfReduction.lean | 12 +- .../GeneralizedGeography/Membership.lean | 15 +-- .../Complexity/Classes/Sparse/Kadin.lean | 8 +- .../FineGrained/CountingNativeEndpoint.lean | 15 +-- .../Complexity/Problems/Graph.lean | 8 +- .../Native/ExhaustiveCountFallback.lean | 8 +- .../GenericRAM/Native/HeavyBranchFold.lean | 14 +-- .../GenericRAM/Simulation/Degree.lean | 10 +- .../GenericRAM/Simulation/Run.lean | 16 +-- .../GenericRAM/SparseMemory/Turing.lean | 17 +-- .../Computability/Kolmogorov/MINcKT.lean | 9 +- .../MCSP/HardnessConsequences.lean | 8 +- Complexity/Computability/MCSP/NP.lean | 8 +- Complexity/Computability/MCSP/SuccinctNP.lean | 9 +- .../ConcreteSupplierSpace.lean | 8 +- .../BlockComputation/GateVectorBounds.lean | 10 +- .../BlockComputation/ImplicitPathSpace.lean | 8 +- .../BlockComputation/NormalizePoint.lean | 11 +- .../Turing/MultiTape/Combinators/DivConq.lean | 9 +- .../BoundedIncidenceCounter.lean | 23 ++-- .../PolyTime/CNF/GreedyParitySearch.lean | 15 +-- .../PolyTime/CNF/SparseCNFLeafCounter.lean | 14 +-- .../TreeEval/Reader/Cert/Offset.lean | 19 ++- .../Crypto/Computational/OneWay/BPP.lean | 8 +- Complexity/Tactic/EncLen.lean | 79 ++++++++++++ ComplexityTests/EncLenTactic.lean | 114 ++++++++++++++++++ 36 files changed, 339 insertions(+), 253 deletions(-) create mode 100644 Complexity/Tactic/EncLen.lean create mode 100644 ComplexityTests/EncLenTactic.lean diff --git a/Complexity.lean b/Complexity.lean index bcc308a876..268d1fbcb3 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -3823,6 +3823,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 diff --git a/Complexity/Computability/Circuit/Boolean/BalancedCode.lean b/Complexity/Computability/Circuit/Boolean/BalancedCode.lean index bd7177596e..60d8641385 100644 --- a/Complexity/Computability/Circuit/Boolean/BalancedCode.lean +++ b/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 diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean index fa8f9ecdbe..caeef06eac 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/FastContractionLeaf.lean +++ b/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 diff --git a/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedResources.lean b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedResources.lean index dc13398b89..7d7729e05a 100644 --- a/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedResources.lean +++ b/Complexity/Computability/Circuit/Frontier/TensorNetwork/TruncatedResources.lean @@ -12,6 +12,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length 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 @@ -145,8 +146,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) := @@ -174,8 +174,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 -/ @@ -283,8 +282,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, [])) ≤ @@ -423,11 +421,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) @@ -518,8 +513,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 ∧ @@ -555,9 +549,7 @@ 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)) @@ -565,9 +557,7 @@ theorem directCoreCertificate_le (entry : T → List Bool → List ℕ) 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₂ ≤ diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean index a464744eb1..cdbc602943 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Accumulate.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean index 1182c62cfd..7bbfd8ce47 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/Assembly.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean b/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean index 977c111927..79ca401884 100644 --- a/Complexity/Computability/Complexity/Classes/CountingSimulation/FastAnalysis.lean +++ b/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 diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean index 5444a5c486..da57719e60 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicExponentialTime.lean @@ -19,6 +19,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 @@ -612,9 +613,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) @@ -763,9 +762,7 @@ theorem expLazyDiagonal_mem_NTIME (k : ℕ) : _ ≤ M := Nat.pow_le_pow_right (by norm_num) (Nat.le_mul_of_pos_left _ (by 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 := @@ -815,9 +812,7 @@ theorem expLazyDiagonal_mem_NTIME (k : ℕ) : calc P + 1 ≤ 2 ^ (P + 1) := Nat.lt_two_pow_self.le _ ≤ certLen k P := Nat.pow_le_pow_right (by norm_num) (Nat.le_mul_of_pos_left _ (by omega)) 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 := diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean index 4f2eb8644d..f9764ac5de 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/NondeterministicTime.lean @@ -16,6 +16,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 @@ -442,9 +443,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) := @@ -530,9 +529,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] diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/TimePolylog.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/TimePolylog.lean index 1d66eb7406..a7f210b12a 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/TimePolylog.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/TimePolylog.lean @@ -13,6 +13,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Universal.WindowedComp import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential +import Complexity.Tactic.EncLen /-! # The time hierarchy with a polylogarithmic gap @@ -91,9 +92,7 @@ private theorem computableInO_verdict_linear : all_goals have h₁ := length_le_encPair_left (encList encUnary) encBool r have h₂ : (encList encUnary [eBit true]).length = 3 := rfl - simp only [Function.comp_apply, length_encPair, encBool_apply, List.length_singleton, - h₂] at h₁ ⊢ - omega + enc_len [Function.comp_apply, h₂] at h₁ ⊢ /-- The numeric core of the resources of the clocked diagonal with the `O(t log t)` universal machine, for the exponent `E` of its overhead: for an input of length `n` with a short framed @@ -184,8 +183,7 @@ theorem exists_computableInO_timeDiagonal_polylog : ∃ k, ∀ {J : ℕ → ℕ} (listMax_le fun a ha => ?_) ?_ · obtain ⟨b, -, rfl⟩ := List.mem_map.mp ha cases b <;> decide - · simp only [length_encPair, descLen] - omega + · enc_len [descLen] refine (h.mono ((K + 1) * (cO + 1) + 2) (fun x => ?_) fun x => ?_).computableInO all_goals have hO := hcO x diff --git a/Complexity/Computability/Complexity/Classes/NP/SelfReduction.lean b/Complexity/Computability/Complexity/Classes/NP/SelfReduction.lean index 5ae0be87ca..1feda667dd 100644 --- a/Complexity/Computability/Complexity/Classes/NP/SelfReduction.lean +++ b/Complexity/Computability/Complexity/Classes/NP/SelfReduction.lean @@ -14,6 +14,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Fold import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Tactic.EncLen import Mathlib.Data.List.GetD /-! @@ -152,8 +153,7 @@ theorem length_encList_le_of_mem_vars {φ : CNF ℕ} {answers : List (Literal have h := length_encList_le (encPair encNat encBool) answers (b := 2 * (encCNF φ).length + 2) fun l hl => by have := length_encNat_le_of_mem_vars (hanswers l hl) - rw [length_encPair, encBool_apply, List.length_singleton] - omega + enc_len calc _ ≤ answers.length * (2 * (2 * (encCNF φ).length + 2) + 1) := h _ = answers.length * (4 * (encCNF φ).length + 5) := by ring @@ -161,9 +161,7 @@ theorem length_encList_le_of_mem_vars {φ : CNF ℕ} {answers : List (Literal binary digits of `v`. -/ private theorem length_encCNF_unit (l : Literal ℕ) : (encCNF [[l]]).length = 8 * (encNat l.1).length + 11 := by - simp only [encCNF, encList_cons, encList_nil, List.append_nil, length_frame, length_encPair, - encBool_apply, List.length_singleton] - omega + enc_len [encCNF, encList_cons, encList_nil, List.append_nil] /-- The unit clause of a literal on a variable of `φ` takes at most `8 L + 11` bits, where `L` is the length of `φ`. -/ @@ -299,9 +297,7 @@ theorem computableInPolyTime_search {γ : Type} {encIn : γ ↪ List Bool} ⟨((PolyBounded.const 4).mul hφ.polyBounded_length).add (.const 5), fun x answers v hv => ?_⟩ have := length_encNat_le_of_mem_vars hv - simp only [selfReduceStep, encList_append, encList_cons, encList_nil, List.append_nil, - List.length_append, length_frame, length_encPair, encBool_apply, List.length_singleton] - omega + enc_len [selfReduceStep, encList_append, encList_cons, encList_nil, List.append_nil] unfold search exact listToBits.comp (map (snd encNat encBool) |>.comp hfold) diff --git a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean index f50112419c..14942f6ef6 100644 --- a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean +++ b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean @@ -15,6 +15,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Li import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option import Complexity.Foundations.Data.List.Counting +import Complexity.Tactic.EncLen /-! # Generalized Geography is in `PSPACE` @@ -395,8 +396,7 @@ private theorem length_le_length_encode (x : Graph × ℕ) : x.1.1.length ≤ (encPair encGraph encNat x).length := by have h₁ := length_le_length_encList (encPair encNat encNat) x.1.2 have h₂ := length_le_length_encList encNat x.1.1 - simp only [length_encPair, encGraph] - omega + enc_len [encGraph] /-- **The replay is a game verifier of Generalized Geography**, with `2 * (n + 1) ^ 2` single-bit moves on instances of encoded length `n`. -/ @@ -498,8 +498,7 @@ private theorem length_encNat_le_of_mem {G : Graph} {e : ℕ × ℕ} (he : e ∈ have h₂ := List.le_sum_of_mem (List.mem_map_of_mem (f := fun a => (encPair encNat encNat a).length) he) have h₃ := length_le_encPair_right encNat encNat e - simp only [encGraph, length_encPair] at h₁ h₂ h₃ ⊢ - omega + enc_len [encGraph] at h₁ h₂ h₃ ⊢ /-- **A block adds at most one vertex to a play.** -/ theorem length_encPlay_step_le (G : Graph) (B : ℕ) (st : Play) (block : List Bool) : @@ -516,12 +515,8 @@ theorem length_encPlay_step_le (G : Graph) (B : ℕ) (st : Play) (block : List B have hw := length_encNat_le_of_mem (G := G) (List.getElem_mem (l := G.2) (n := choice (moverBits B first block)) hi) rw [← arc_eq hi] at hw - simp only [length_encPair, encOption_none, encList_cons, List.length_append, length_frame, - encBool_apply, List.length_cons, List.length_nil, List.length_nil] at hw ⊢ - omega - · simp only [length_encPair, encOption_none, encOption_some, List.length_cons, - encBool_apply, List.length_nil] - omega + enc_len [encList_cons] at hw ⊢ + · enc_len /-- The inputs of the verifier: a graph with a start vertex, and the moves. -/ private abbrev encInput : (Graph × ℕ) × List Bool ↪ List Bool := diff --git a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean index 9102ebc8f4..bbd2b68cb3 100644 --- a/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean +++ b/Complexity/Computability/Complexity/Classes/Sparse/Kadin.lean @@ -29,6 +29,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Replay.S import Complexity.Computability.Probabilistic.Oracle.Composition import Complexity.Foundations.Data.List.Counting import Complexity.Foundations.Data.Nat.PolynomialBound.Log +import Complexity.Tactic.EncLen import Cslib.Foundations.Data.Polynomial.Monotone /-! @@ -279,8 +280,7 @@ theorem language_mem_NP (hS : S ∈ NP encBits) (hsparse : S ∈ SPARSE encBits) 4 * m.eval n + 2 * pS.eval (m.eval n) + 3 := by obtain ⟨hlenS, hc, -⟩ := hpairs sc hsc have hpS : pS.eval sc.1.length ≤ pS.eval (m.eval n) := pS.eval_mono hlenS - rw [length_encPair, encBits_apply, encBits_apply, hc] - omega + enc_len [hc] have hlist : (encList (encPair encBits encBits) pairs).length ≤ c * (m.eval n + 1) ^ d * (4 * m.eval n + 2 * pS.eval (m.eval n) + 3) := by rw [length_encList] @@ -469,9 +469,7 @@ theorem isOraclePPTOn_program {enc : α ↪ List Bool} {req fin : α × ℕ → · simp only [h, ↓reduceIte, OracleComp.interpret_pure] at hnext rw [OracleComp.eq_of_mem_supportWith_pure hnext] exact hinv) - hsize (fun a i st _ hinv => by - simp only [length_encPair, encUnary_apply, List.length_replicate] - omega) + hsize (fun a i st _ hinv => by enc_len) have hfinal : IsOraclePPTOn (encPair enc (encPair encUnary encUnary)) encBool (fun pair : α × ℕ × ℕ => OracleComp.interpret ProbOracleComp.query (queryBit (fin (pair.1, pair.2.1)))) := diff --git a/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean index d94ad11a16..499fb3176e 100644 --- a/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean +++ b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean @@ -25,6 +25,7 @@ import Complexity.Computability.Complexity.FineGrained.CountingSparsification import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic import Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceCounter import Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceExactness +import Complexity.Tactic.EncLen public import Complexity.Logics.Propositional.CNF.ModelCount.Declared /-! @@ -129,8 +130,7 @@ private theorem treeBound (k : ℕ) (p : Context) : countingTreeBound_countingThresholdBase _ (one_le_divisor p) private theorem declaredSize_le_inputSize (x : Input) : x.1 ≤ inputSize x := by - simp only [inputSize, encInput, length_encPair, encUnary_apply, List.length_replicate] - omega + enc_len [inputSize, encInput] private theorem polyBounded_depthCoeff (k : ℕ) : PolyBounded inputSize (fun x => depthCoeff k ((), x.1)) := @@ -153,9 +153,7 @@ private theorem length_prepare (x : Input) : private theorem length_leaf_input (N : ℕ) (ψ : CNF ℕ) : (encPair encContext encCNF (((), N), ψ)).length = 2 * N + 3 + (encCNF ψ).length := by - simp only [encContext, length_encPair, encUnit_apply, List.length_nil, encUnary_apply, - List.length_replicate] - omega + enc_len [encContext, encUnit_apply] private theorem divisor_eq_numGroups {p : Context} (h : 1 ≤ numGroups p.2) : divisor p = numGroups p.2 := max_eq_right h @@ -309,8 +307,7 @@ private theorem computableInPolyTime_declareInput : private theorem length_declareInput (φ : CNF ℕ) : (encInput (declareInput φ)).length + 1 ≤ 3 * ((encCNF φ).length + 1) := by have hn := φ.numVars_le_length_vars.trans (SAT.length_vars_le φ) - simp only [declareInput, encInput, length_encPair, encUnary_apply, List.length_replicate] - omega + enc_len [declareInput, encInput] private theorem dense_spec {k : ℕ} {count : Input → ℕ} (hspec : ∀ x, count x = if validDeclaredInput k x.1 x.2 then @@ -438,9 +435,7 @@ private def leafSize (k : ℕ) (x : FullInput) : ℕ := private theorem polyBounded_leafSize (k : ℕ) : PolyBounded (fun x : FullInput => (encFullInput x).length) (leafSize k) := by have hN : PolyBounded (fun x : FullInput => (encFullInput x).length) (fun x => x.2.1) := - PolyBounded.self.mono fun x => by - simp only [encFullInput, encInput, length_encPair, encUnary_apply, List.length_replicate] - omega + PolyBounded.self.mono fun x => by enc_len [encFullInput, encInput] have hL : PolyBounded (fun x : FullInput => (encFullInput x).length) (fun x => (encCNF x.2.2).length) := PolyBounded.self.mono fun x => diff --git a/Complexity/Computability/Complexity/Problems/Graph.lean b/Complexity/Computability/Complexity/Problems/Graph.lean index 00666a7ffc..05417e728d 100644 --- a/Complexity/Computability/Complexity/Problems/Graph.lean +++ b/Complexity/Computability/Complexity/Problems/Graph.lean @@ -18,6 +18,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Me import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives +import Complexity.Tactic.EncLen import Mathlib.Data.List.GetD import Mathlib.SetTheory.Cardinal.Finite @@ -125,9 +126,7 @@ namespace Graph /-- A graph has no more declared vertices than the length of its encoding. -/ theorem length_vertices_le_encGraph (G : Graph) : G.1.length ≤ (encGraph G).length := by calc G.1.length ≤ (encList encNat G.1).length := length_le_length_encList encNat G.1 - _ ≤ (encGraph G).length := by - simp only [encGraph, length_encPair] - omega + _ ≤ (encGraph G).length := by enc_len [encGraph] /-- The declared vertices of `G` without repetitions, in the order of their first occurrences. -/ def distinctVertices (G : Graph) : List ℕ := selectDistinct G.1 (List.replicate G.1.length true) @@ -259,8 +258,7 @@ theorem isVerifier_verifySubset {rel : Graph → ℕ → ℕ → Bool} {P : Grap refine isVerifier_subsetVerifier (fun x => by have := x.1.length_vertices_le_encGraph - simp only [Polynomial.eval_X, length_encPair] - omega) + enc_len [Polynomial.eval_X]) fun x l hl _ => ?_ simp only [Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true, Bool.or_eq_true, List.toFinset_card_of_nodup hl, List.coe_toFinset] diff --git a/Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean b/Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean index f94306a75c..8103812af4 100644 --- a/Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean +++ b/Complexity/Computability/GenericRAM/Native/ExhaustiveCountFallback.lean @@ -18,6 +18,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Li import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain import Complexity.Foundations.Data.BitString.ZModTwo +import Complexity.Tactic.EncLen import Mathlib.Data.List.GetD import Mathlib.Data.Nat.Size import Mathlib.Tactic.Linarith @@ -212,9 +213,7 @@ private theorem length_prefix_accumulator_le (pred : P → List Bool → Bool) ( (encPair (encPair encUnary encP) encNat (BooleanFold.runPrefix (countStep pred) x.1 j (x, 0)).2.2).length ≤ 3 * (encPair encUnary encP x).length + 2 := by - have hx_le : x.1 ≤ (encPair encUnary encP x).length := by - simp only [length_encPair, encUnary_apply, List.length_replicate] - omega + have hx_le : x.1 ≤ (encPair encUnary encP x).length := by enc_len have hz_le : (BooleanFold.runPrefix (countStep pred) x.1 j (x, 0)).2.2.2 ≤ 2 ^ x.1 := (prefix_count_le_index pred x j).trans hj have hlen_z : @@ -224,8 +223,7 @@ private theorem length_prefix_accumulator_le (pred : P → List Bool → Bool) ( simpa [Nat.size_eq_bits_len] using Nat.size_le_size hz_le rw [BooleanFold.length_clock] at hm exact hm - rw [length_encPair, prefix_payload_eq] - omega + enc_len [prefix_payload_eq] private theorem countPredicateCertificate_bounds {pred : P → List Bool → Bool} (hpred : ComputableInPolyTime (fun q : P × List Bool => pred q.1 q.2) (encPair encP encBits) diff --git a/Complexity/Computability/GenericRAM/Native/HeavyBranchFold.lean b/Complexity/Computability/GenericRAM/Native/HeavyBranchFold.lean index 842d554689..926e32f843 100644 --- a/Complexity/Computability/GenericRAM/Native/HeavyBranchFold.lean +++ b/Complexity/Computability/GenericRAM/Native/HeavyBranchFold.lean @@ -21,6 +21,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Me import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Tactic.EncLen import Mathlib.Data.Finset.Card import Mathlib.Data.Fintype.BigOperators import Mathlib.Data.List.GetD @@ -870,7 +871,7 @@ theorem length_enc_reduced_le_parent {n n' : ℕ} {S : List ℕ} {vals : List Bo (length_encList_map_le _ _ fun eq₁ _ => hrel eq₁).trans ((length_encList_sublist _ List.filter_sublist).trans (length_encList_map_le _ _ fun eq₀ _ => length_enc_substituteEquation_le S vals eq₀)) - simp only [length_encPair, encUnary_apply, List.length_replicate]; omega + enc_len /-- Encoded-size non-expansion: every `.reduced n' sys'` branch produced by `prepareBranch` has encoded solver input `(n', sys')` no longer than the parent `encBranchInput (n, S, sys)`. -/ @@ -879,7 +880,7 @@ theorem length_enc_reduced_le {n n' : ℕ} {S : List ℕ} {vals : List Bool} (encPair encUnary (encList (encList (encList encNat))) (n', sys')).length ≤ (encBranchInput (n, S, sys)).length := by refine (length_enc_reduced_le_parent hred).trans ?_ - simp only [encBranchInput, length_encPair]; omega + enc_len [encBranchInput] /-- Callback input tuple `((|S|, vals), (inp, accSum))` for `branchBody`. -/ abbrev PrepareStepInput : Type := (ℕ × List Bool) × (BranchInput × ℕ) @@ -1058,17 +1059,14 @@ private theorem branchCountCertificate_bounds {solver : ℕ → List (List (List NativeCertificate.linear, NativeCertificate.comp, NativeCertificate.payload, NativeCertificate.pull, NativeCertificate.post, BooleanFold.clock, BranchOutcome.toOption, Option.elim, reducedCost] - simp only [encBranchOutcome_eq, BranchOutcome.toOption, encOption_some, encOption_none, - length_encPair, List.length_cons, List.length_nil, encUnary_apply, List.length_replicate] - omega + enc_len [encBranchOutcome_eq, BranchOutcome.toOption] | reduced n' sys' => rw [encBranchOutcome_eq] dsimp only [branchCountCertificate, NativeCertificate.congr, NativeCertificate.option, NativeCertificate.linear, NativeCertificate.comp, NativeCertificate.payload, NativeCertificate.prod, NativeCertificate.fst, NativeCertificate.post, BranchOutcome.toOption, Option.elim, reducedCost] - simp only [encBranchOutcome_eq, BranchOutcome.toOption, encOption_some, length_encPair, - List.length_cons, encUnary_apply, List.length_replicate]; omega + enc_len [encBranchOutcome_eq, BranchOutcome.toOption] theorem computableInPolyTime_prepareStep : ComputableInPolyTime (fun p : PrepareStepInput => @@ -1119,7 +1117,7 @@ private theorem length_le_encBranchInput (inp : BranchInput) : 2 * inp.1 + 2 * inp.2.1.length + 2 ≤ (encBranchInput inp).length := by have hS : inp.2.1.length ≤ (encList encNat inp.2.1).length := SizedListEncoding.length_le (encA := encNat) inp.2.1 - simp only [encBranchInput, length_encPair, encUnary_apply, List.length_replicate]; omega + enc_len [encBranchInput] /-- Prefix sum bound: when `solver n' sys' ≤ 2 ^ n'` on reduced branches of `inp`, every streaming prefix `j ≤ 2 ^ |S|` keeps the running sum at most `j * 2 ^ (n - |S|)`. -/ diff --git a/Complexity/Computability/GenericRAM/Simulation/Degree.lean b/Complexity/Computability/GenericRAM/Simulation/Degree.lean index de54e3758d..ec12900935 100644 --- a/Complexity/Computability/GenericRAM/Simulation/Degree.lean +++ b/Complexity/Computability/GenericRAM/Simulation/Degree.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.GenericRAM.Simulation.Run public import Complexity.Computability.GenericRAM.Native.Degree +import Complexity.Tactic.EncLen /-! # Explicit-degree overhead of the finite-state RAM simulation @@ -95,7 +96,7 @@ theorem readRaw_hasDegree (enc : M.Encoding) (hD : 3 ≤ D) : ⟨32, fun q => ?_⟩ (by omega) · have hq : (SparseMemory.queryEncoding enc.address enc.value q.1).length ≤ (SparseMemory.readEncoding enc.address enc.value q).length := by - simp only [SparseMemory.readEncoding, length_encPair]; omega + enc_len [SparseMemory.readEncoding] have hp := Nat.pow_le_pow_left (Nat.add_le_add_right hq 1) 3 have ht := SparseMemory.scanTime_le_cube enc.address enc.value q.1 have he : (SparseMemory.readEncoding enc.address enc.value q).length ≤ @@ -104,9 +105,7 @@ theorem readRaw_hasDegree (enc : M.Encoding) (hD : 3 ≤ D) : unfold SparseMemory.readTime nlinarith · have hs := SparseMemory.scanSpace_le_linear enc.address enc.value q.1 - simp only [SparseMemory.readSpace, SparseMemory.readEncoding, - length_encPair, pow_one] at hs ⊢ - omega + enc_len [SparseMemory.readSpace, SparseMemory.readEncoding, pow_one] at hs ⊢ /-- The raw sparse-memory update is cubic in time and linear in space. -/ theorem writeRaw_hasDegree (enc : M.Encoding) (hD : 3 ≤ D) : @@ -120,8 +119,7 @@ theorem writeRaw_hasDegree (enc : M.Encoding) (hD : 3 ≤ D) : ⟨33, fun q => ?_⟩ (by omega) · have hq : (SparseMemory.queryEncoding enc.address enc.value (q.1.1, q.2)).length ≤ (SparseMemory.writeEncoding enc.address enc.value q).length := by - simp only [SparseMemory.queryEncoding, SparseMemory.writeEncoding, length_encPair] - omega + enc_len [SparseMemory.queryEncoding, SparseMemory.writeEncoding] have hp := Nat.pow_le_pow_left (Nat.add_le_add_right hq 1) 3 have ht := SparseMemory.scanTime_le_cube enc.address enc.value (q.1.1, q.2) have he : (SparseMemory.writeEncoding enc.address enc.value q).length ≤ diff --git a/Complexity/Computability/GenericRAM/Simulation/Run.lean b/Complexity/Computability/GenericRAM/Simulation/Run.lean index 3df6238539..819706cd05 100644 --- a/Complexity/Computability/GenericRAM/Simulation/Run.lean +++ b/Complexity/Computability/GenericRAM/Simulation/Run.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.GenericRAM.Simulation.Turing +import Complexity.Tactic.EncLen /-! # Clocked multi-step execution and whole-run native transport for generic RAMs @@ -949,7 +950,7 @@ theorem readCertificate_isPolynomial (enc : M.Encoding) refine ⟨.of_forall_le 32 3 fun q => ?_, .of_forall_le 32 1 fun q => ?_⟩ · have hq : (SparseMemory.queryEncoding enc.address enc.value q.1).length ≤ (SparseMemory.readEncoding enc.address enc.value q).length := by - simp only [SparseMemory.readEncoding, length_encPair]; omega + enc_len [SparseMemory.readEncoding] have hp := Nat.pow_le_pow_left (Nat.add_le_add_right hq 1) 3 have ht := SparseMemory.scanTime_le_cube enc.address enc.value q.1 have he : (SparseMemory.readEncoding enc.address enc.value q).length ≤ @@ -958,9 +959,7 @@ theorem readCertificate_isPolynomial (enc : M.Encoding) unfold SparseMemory.readTime nlinarith · have hs := SparseMemory.scanSpace_le_linear enc.address enc.value q.1 - simp only [SparseMemory.readSpace, SparseMemory.readEncoding, - length_encPair, pow_one] at hs ⊢ - omega + enc_len [SparseMemory.readSpace, SparseMemory.readEncoding, pow_one] at hs ⊢ exact comp_isPolynomial _ (prod (prod address (snd (snd (snd (fields enc c))))) (fst (snd (snd (fields enc c))))) hread (prod_isPolynomial _ _ (prod_isPolynomial _ _ ha hc) hc) @@ -978,8 +977,7 @@ theorem writeCertificate_isPolynomial (enc : M.Encoding) refine ⟨.of_forall_le 33 3 fun q => ?_, .of_forall_le 33 1 fun q => ?_⟩ · have hq : (SparseMemory.queryEncoding enc.address enc.value (q.1.1, q.2)).length ≤ (SparseMemory.writeEncoding enc.address enc.value q).length := by - simp only [SparseMemory.queryEncoding, SparseMemory.writeEncoding, length_encPair] - omega + enc_len [SparseMemory.queryEncoding, SparseMemory.writeEncoding] have hp := Nat.pow_le_pow_left (Nat.add_le_add_right hq 1) 3 have ht := SparseMemory.scanTime_le_cube enc.address enc.value (q.1.1, q.2) have he : (SparseMemory.writeEncoding enc.address enc.value q).length ≤ @@ -1194,8 +1192,7 @@ theorem runCertificateOf_isPolynomial (enc : M.Encoding) (N : M.NativePrimitives fun a j hj => by rw [iterate_round_inl] have := hOutLen a j hj - simp only [loopEncoding, length_encPair] - omega + enc_len [loopEncoding] have hInLen : PolyBounded (fun a => (ei a).length) (fun a => (runInputEncoding enc (steps a, (cfg a, initState a))).length) := ((prod cSteps (prod cCfg cInit)).polyTime @@ -1293,8 +1290,7 @@ theorem polyBounded_length_run (enc : M.Encoding) (N : M.NativePrimitives enc) (roundIterCertificate_isPolynomial enc N p cCfg cInit hN hCfg hInit j)).polyBounded_length refine hloop.mono fun a => ?_ rw [iterate_round_inl] - simp only [loopEncoding, length_encPair] - omega + enc_len [loopEncoding] /-- Automatic `ComputableInPolyTime` transport for a constant step-budget bound `∀ a, steps a ≤ K`: the intermediate outcome lengths along `0 ≤ j ≤ K` are bounded by induction on diff --git a/Complexity/Computability/GenericRAM/SparseMemory/Turing.lean b/Complexity/Computability/GenericRAM/SparseMemory/Turing.lean index 6e35dc8917..ce48d378b9 100644 --- a/Complexity/Computability/GenericRAM/SparseMemory/Turing.lean +++ b/Complexity/Computability/GenericRAM/SparseMemory/Turing.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.GenericRAM.SparseMemory.Basic public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists +import Complexity.Tactic.EncLen /-! # Native Turing-machine certificates for sparse memory @@ -154,8 +155,7 @@ theorem scanSpace_le (q : Address × SparseMemory Address Value) : have hv := le_listMax (f := fun e : Address × Value => (encV e.2).length) he change (encA e.1).length ≤ maxKeyLength encA q.2 at hk change (encV e.2).length ≤ maxValueLength encV q.2 at hv - simp only [compareSpace, length_encPair] - omega + enc_len [compareSpace] unfold scanSpace omega @@ -343,9 +343,7 @@ theorem insert_inO_cube : apply (insert_inO encA encV).mono 40 · intro q have hq : (queryEncoding encA encV (q.1.1, q.2)).length ≤ - (writeEncoding encA encV q).length := by - simp only [queryEncoding, writeEncoding, length_encPair] - omega + (writeEncoding encA encV q).length := by enc_len [queryEncoding, writeEncoding] have hp := Nat.pow_le_pow_left (Nat.add_le_add_right hq 1) 3 have ht := scanTime_le_cube encA encV (q.1.1, q.2) have he : (writeEncoding encA encV q).length ≤ @@ -354,8 +352,7 @@ theorem insert_inO_cube : nlinarith · intro q have hs := scanSpace_le_linear encA encV (q.1.1, q.2) - simp only [writeSpace, queryEncoding, writeEncoding, length_encPair] at hs ⊢ - omega + enc_len [writeSpace, queryEncoding, writeEncoding] at hs ⊢ /-- A cubic-time, linear-space specialization of the parameterized read certificate. -/ theorem read_inO_cube : @@ -367,8 +364,7 @@ theorem read_inO_cube : apply (read_inO encA encV).mono 40 · intro q have hq : (queryEncoding encA encV q.1).length ≤ (readEncoding encA encV q).length := by - simp only [readEncoding, length_encPair] - omega + enc_len [readEncoding] have hp := Nat.pow_le_pow_left (Nat.add_le_add_right hq 1) 3 have ht := scanTime_le_cube encA encV q.1 have he : (readEncoding encA encV q).length ≤ @@ -377,8 +373,7 @@ theorem read_inO_cube : nlinarith · intro q have hs := scanSpace_le_linear encA encV q.1 - simp only [readSpace, readEncoding, length_encPair] at hs ⊢ - omega + enc_len [readSpace, readEncoding] at hs ⊢ /-- Polynomial-time writes are a corollary of the native parameterized certificate. -/ @[fun_prop] diff --git a/Complexity/Computability/Kolmogorov/MINcKT.lean b/Complexity/Computability/Kolmogorov/MINcKT.lean index 8e844460dd..66772f90d8 100644 --- a/Complexity/Computability/Kolmogorov/MINcKT.lean +++ b/Complexity/Computability/Kolmogorov/MINcKT.lean @@ -14,6 +14,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bi import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Tactic.EncLen /-! # The Conditional Time-Bounded Kolmogorov Complexity Problem (`MINcKT`) @@ -135,14 +136,10 @@ theorem enc_apply (i : Instance) : rfl /-- The unary size parameter `i.size` is at most `(enc i).length`. -/ -theorem size_le_length_enc (i : Instance) : i.size ≤ (enc i).length := by - simp only [enc_apply, length_encPair, encBits_apply, encUnary_apply, List.length_replicate] - omega +theorem size_le_length_enc (i : Instance) : i.size ≤ (enc i).length := by enc_len [enc_apply] /-- The unary time parameter `i.time` is at most `(enc i).length`. -/ -theorem time_le_length_enc (i : Instance) : i.time ≤ (enc i).length := by - simp only [enc_apply, length_encPair, encBits_apply, encUnary_apply, List.length_replicate] - omega +theorem time_le_length_enc (i : Instance) : i.time ≤ (enc i).length := by enc_len [enc_apply] /-- `i ∈ MINcKT` iff `condTimeBoundedAt i.time i.string i.cond ≤ i.size`. -/ theorem mem_iff {i : Instance} : diff --git a/Complexity/Computability/MCSP/HardnessConsequences.lean b/Complexity/Computability/MCSP/HardnessConsequences.lean index 17d6891ba7..d35ce54eab 100644 --- a/Complexity/Computability/MCSP/HardnessConsequences.lean +++ b/Complexity/Computability/MCSP/HardnessConsequences.lean @@ -22,6 +22,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log import Complexity.Foundations.Data.Nat.PolynomialBound.Closure +import Complexity.Tactic.EncLen /-! # Structural consequences of the NP-hardness of MCSP @@ -138,9 +139,7 @@ private theorem length_encPair_decodePair_le : | false :: b :: v => by simp [decodePair, unframe, dropFrame] | true :: b :: v => by have ih := length_encPair_decodePair_le v - simp only [decodePair, unframe, dropFrame, length_encPair, encBits_apply, - List.length_cons] at ih ⊢ - omega + enc_len [decodePair, unframe, dropFrame] at ih ⊢ /-- If `EXP encBits ⊆ PPolyOn encBits`, then `EXP` on paired bitstrings `encPair encBits encBits` also lies in `PPolyOn (encPair encBits encBits)`. -/ @@ -414,8 +413,7 @@ theorem NEXP_subset_EXP_of_MCSP_npHard_of_EXP_subset_PPoly have harity (x : List Bool) : (R (z x)).arity ≤ m_bound x.length := by set n := x.length have h2_arity : 2 ^ (R (z x)).arity ≤ (MCSP.encInstance (R (z x))).length := by - rw [MCSP.encInstance_apply, length_encPair, encBits_apply, List.length_ofFn] - omega + enc_len [MCSP.encInstance_apply, List.length_ofFn] have hn_le : n + 1 ≤ 2 ^ f n := (Nat.lt_two_pow_self (n := n)).trans_le (Nat.pow_le_pow_right (by norm_num) (hnf n)) have hzx_len : (z x).length + 1 ≤ 2 ^ (f n + 2) := by diff --git a/Complexity/Computability/MCSP/NP.lean b/Complexity/Computability/MCSP/NP.lean index c9fe2ea485..1617b57c19 100644 --- a/Complexity/Computability/MCSP/NP.lean +++ b/Complexity/Computability/MCSP/NP.lean @@ -21,6 +21,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log import Complexity.Foundations.Data.BitString.Binary import Complexity.Foundations.Data.List.Lookup +import Complexity.Tactic.EncLen import Mathlib.Data.List.GetD /-! @@ -100,9 +101,7 @@ theorem encInstance_apply (x : Instance) : /-- The table of an instance is no longer than its encoding. -/ private theorem two_pow_le_length_encInstance (x : Instance) : - 2 ^ x.arity ≤ (encInstance x).length := by - rw [encInstance_apply, length_encPair, encBits_apply, List.length_ofFn] - omega + 2 ^ x.arity ≤ (encInstance x).length := by enc_len [encInstance_apply, List.length_ofFn] /-- The number of gates a certificate for `t` samples on `n` inputs may describe: the threshold `s`, capped at the sample-set bound `t * (2 * n + 3) + 1`. -/ @@ -518,8 +517,7 @@ theorem computableInPolyTime_checkCertificate_table {α : Type} {encT : List α set T := r.1.1.length have hT_enc : 2 * T + 1 ≤ (encIn r).length := by have h1 := hlen_le r.1.1 - simp only [encIn, length_encPair] - omega + enc_len [encIn] have hpow : 2 ^ Nat.log 2 T ≤ T + 1 := by rcases Nat.eq_zero_or_pos T with h | h · simp [h] diff --git a/Complexity/Computability/MCSP/SuccinctNP.lean b/Complexity/Computability/MCSP/SuccinctNP.lean index a95bf72b68..fb31ab8101 100644 --- a/Complexity/Computability/MCSP/SuccinctNP.lean +++ b/Complexity/Computability/MCSP/SuccinctNP.lean @@ -18,6 +18,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Li import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length +import Complexity.Tactic.EncLen /-! # Succinct MCSP is in NP @@ -272,9 +273,7 @@ private theorem length_encList_rawSamples_ofFunction {n : ℕ} (f : BooleanFunct have hconst : ((fun a => 2 * (encPair encBits encBool a).length + 1) ∘ fun y : BitString n => (List.ofFn y, f y)) = fun _ => 4 * n + 5 := by funext y - simp only [Function.comp_apply, length_encPair, encBits_apply, List.length_ofFn, - encBool_apply, List.length_singleton] - omega + enc_len [Function.comp_apply, List.length_ofFn] rw [hconst, List.map_const', List.sum_replicate, smul_eq_mul, hlen] /-- The encoded length of `Instance.ofFunction f S s` under `SuccinctMCSP.enc` depends only on the @@ -299,9 +298,7 @@ private theorem arity_and_card_le_length_enc_of_encT (encT : ℕ ↪ List Bool) x.samples.card ≤ (encPair (encPair encUnary (encList (encPair encBits encBool))) encT (toRaw x)).length := by have hcard := card_samples_le_length_encList x - rw [toRaw_apply, length_encPair, length_encPair, encUnary_apply, List.length_replicate] - dsimp only - omega + enc_len [toRaw_apply] /-! ### Verifier and correctness -/ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/ConcreteSupplierSpace.lean b/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/ConcreteSupplierSpace.lean index fff4d05b4c..60c9d8b3c4 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/ConcreteSupplierSpace.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/ConcreteSupplierSpace.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.BlockComputatio public import Complexity.Computability.Machines.Turing.MultiTape.BlockComputation.InitialVectorCorrect import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List.Size import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Pi +import Complexity.Tactic.EncLen /-! # Explicit uniform storage for concrete evaluator suppliers @@ -73,9 +74,7 @@ theorem calleeSpace_le_replaySpace {k s : ℕ} {Q : Type} (bound := Nat.card SignType) (fun _ => (length_encFinite_lt _).le) change (encNat (ScheduleRead.read k 0 2 (σ, i))).length ≤ (encNat q).length at hp change (encNat (ScheduleRead.read k 0 0 (σ, i))).length ≤ (encNat q).length at hn - simp only [Interpolation.calleeSpace, ScheduleRead.origin, Gate.encContext, - length_encPair, replaySpace] - omega + enc_len [Interpolation.calleeSpace, ScheduleRead.origin, Gate.encContext, replaySpace] private theorem interpolation_params_encoding_le (N b σ q m alphabet limit p d r i chunk : ℕ) (point : List ℕ) @@ -157,8 +156,7 @@ theorem node_reply_encoding_le {k s p r m : ℕ} {Q : Type} have hone : (encNat 1).length = 1 := rfl simp only [NodeReply.reply, hcapacity, ↓reduceIte] split - · simp only [RawController.encReply, length_encPair] - omega + · enc_len [RawController.encReply] · simp only [RawController.encReply, length_encPair] have hempty : (encList encNat []).length = 0 := rfl rw [hempty] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/GateVectorBounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/GateVectorBounds.lean index b79e390e70..833ce79c3d 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/GateVectorBounds.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/GateVectorBounds.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.BlockComputation.GateVectorCorrect import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List.Size import Complexity.Foundations.Data.List.Lookup +import Complexity.Tactic.EncLen /-! # Physical space for complete native gate vectors @@ -54,8 +55,7 @@ theorem prefixState_encoding_le (params : Params) (values : ℕ → ℕ) (j : simp only [List.length_ofFn] at hl have hmul := Nat.mul_le_mul_right (2 * (encNat p).length + 1) hj dsimp only at hc hmul - simp only [prefixState, encCaller, encParams, length_encPair, callerSpace] - omega + enc_len [prefixState, encCaller, encParams, callerSpace] /-- Every clock of one call pays for one suspended vector prefix and one actual callee. -/ theorem runFrom_one_encoding_le (M : MultiTapeTM k Bool Q) (e : Q ≃ Fin s) @@ -157,8 +157,7 @@ theorem setChunk_encoding_mono (params : QueryGate.Params Interpolation.Context) (QueryGate.encParams Interpolation.encContext (setChunk params b)).length := by rcases params with ⟨⟨N, block, σ, i, m, previous, stride⟩, parameters, point, limit⟩ have h := length_encNat_mono hab - simp only [setChunk, QueryGate.encParams, Interpolation.encContext, length_encPair] - omega + enc_len [setChunk, QueryGate.encParams, Interpolation.encContext] omit [Finite Q] in /-- The replay allowance is monotone in the binary chunk-index metadata. -/ @@ -166,8 +165,7 @@ theorem calleeSpace_chunk_mono (N block σ i m stride : ℕ) {a b : ℕ} (hab : Interpolation.calleeSpace k s Q (N, block, σ, i, m, a, stride) ≤ Interpolation.calleeSpace k s Q (N, block, σ, i, m, b, stride) := by have h := length_encNat_mono hab - simp only [Interpolation.calleeSpace, SupplierChunk.encContext, length_encPair] - omega + enc_len [Interpolation.calleeSpace, SupplierChunk.encContext] /-- The complete selected-field vector is returned with a bound at every physical clock. -/ theorem exists_runFrom_gateExtension_bounded {p q r m : ℕ} [Fact p.Prime] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/ImplicitPathSpace.lean b/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/ImplicitPathSpace.lean index eb11f086f5..09bdce639c 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/ImplicitPathSpace.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/ImplicitPathSpace.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.BlockComputatio import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeOptionPrimitives import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Degree.Bounds import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinarySizeFacts +import Complexity.Tactic.EncLen import Mathlib.Data.List.FinRange /-! @@ -138,8 +139,7 @@ theorem walk_inSpace (k : ℕ) : 16 * ((encWalkArgs a).length + 1) := by have hc := hstates a i hi.le have hm := length_le_encList_of_mem encNat (List.getElem_mem hi) - simp only [length_encPair, encWalkArgs, encProviderArgs] at * - omega + enc_len [encWalkArgs, encProviderArgs] at * have hfold := ComputableInSpace.foldlWith (encIn := encWalkArgs) (encP := encProviderArgs) (encB := encNat) (encA := encNat) (encL := encList encNat) @@ -152,8 +152,6 @@ theorem walk_inSpace (k : ℕ) : (step := fun par n j => child k (par.1, par.2, n, j)) hpar hpath hq (pathStep_inSpace k) hspace hstates - exact hfold.weaken (.of_le_linear 100 100 fun a => by - simp only [encWalkArgs, encProviderArgs, length_encPair] - omega) + exact hfold.weaken (.of_le_linear 100 100 fun a => by enc_len [encWalkArgs, encProviderArgs]) end Turing.MultiTapePTM.BlockComputation.ImplicitPath diff --git a/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/NormalizePoint.lean b/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/NormalizePoint.lean index feca9d893c..e7622e21a7 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/NormalizePoint.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/BlockComputation/NormalizePoint.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.InSpaceLib public import Mathlib.Data.ZMod.Basic import Complexity.Computability.Machines.Turing.MultiTape.Internal.BinarySizeFacts +import Complexity.Tactic.EncLen import Mathlib.Data.List.GetD import Mathlib.Data.List.OfFn @@ -94,16 +95,14 @@ theorem normalize_inSpace : rw [fold_normalize, List.nil_append] have hn := length_enc_normalize_le a.1 (a.2.take i) have ht := length_encList_take_le encNat a.2 i - simp only [encArgs, length_encPair] - omega + enc_len [encArgs] have hspace (a : Args) (i : ℕ) (hi : i < a.2.length) : (encPair (encPair encNat (encList encNat)) encNat ((a.1, (a.2.take i).foldl (fun acc v => acc ++ [v % a.1]) []), a.2[i])).length ≤ 16 * ((encArgs a).length + 1) := by have hs := hstates a i hi.le have hv := length_le_encList_of_mem encNat (List.getElem_mem hi) - simp only [encArgs, length_encPair] at * - omega + enc_len [encArgs] at * have hfold := ComputableInSpace.foldlWith (encIn := encArgs) (encP := encNat) (encA := encNat) (encL := encList encNat) (encB := encList encNat) (par := fun a : Args => a.1) (list := fun a : Args => a.2) @@ -113,9 +112,7 @@ theorem normalize_inSpace : (Si := fun a => (encArgs a).length) (Q := fun a => 16 * ((encArgs a).length + 1)) (B := fun a => (encArgs a).length) hp hl hinit hstep hspace hstates - refine hfold.weaken (.of_le_linear 100 100 fun a => by - simp only [encArgs, length_encPair] - omega) |>.of_enc_eq ?_ + refine hfold.weaken (.of_le_linear 100 100 fun a => by enc_len [encArgs]) |>.of_enc_eq ?_ intro a simp only [fold_normalize, List.nil_append] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Combinators/DivConq.lean b/Complexity/Computability/Machines/Turing/MultiTape/Combinators/DivConq.lean index 314086cf95..9e9e9fadd1 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Combinators/DivConq.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Combinators/DivConq.lean @@ -10,6 +10,7 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO import Complexity.Computability.Machines.Turing.MultiTape.Combinators.StackLoop import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Cases +import Complexity.Tactic.EncLen /-! # Divide and conquer @@ -419,13 +420,9 @@ private lemma round_inO (hisBase : ComputableTidilyInO D.isBase encA encBool Tt · simp only [Sum.elim_inl, length_encPair, encSum_inl, List.length_cons] split_ifs <;> omega · rcases o with _ | a | g <;> - simp only [Function.comp_apply, Sum.elim_inl, Sum.elim_inr, Option.elim_none, - Option.elim_some, length_encPair, encSum_inl, encSum_inr, List.length_cons, - encOption_some] <;> omega + enc_len [Function.comp_apply, Sum.elim_inl, Sum.elim_inr, Option.elim_none, Option.elim_some] · have := length_encList_toList_le (encFrame encA encG) o - simp only [Function.comp_apply, Sum.elim_inr, length_encPair, encSum_inr, - List.length_cons] at * - omega + enc_len [Function.comp_apply, Sum.elim_inr] at * /-- The halting test of the loop, in linear time. -/ private lemma halt_inO : ComputableTidilyInO D.loop.halt (encVal encA encB) encBool diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean index b45424a294..8198fde413 100644 --- a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean +++ b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean @@ -11,6 +11,7 @@ public import Complexity.Init public import Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceSemantics public import Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceStepCert public import Complexity.Computability.PolyTime.CNF.BranchedSparseCNFCounter +import Complexity.Tactic.EncLen import all Complexity.Computability.PolyTime.BooleanAnalysis.BoundedIncidenceStepCert import all Complexity.Computability.PolyTime.CNF.BranchedSparseCNFCounter import Complexity.Computability.Complexity.FineGrained.SparseBranchAsymptotics @@ -177,8 +178,7 @@ private theorem parametric_branch_step_bound {N₀_branch k_deg β C_inc C_p d_p simpa only [pow_one] using Nat.pow_le_pow_right (by omega) (by decide : 1 ≤ 2) exact (one_mul r).symm.le.trans ((Nat.mul_le_mul (by omega) hr_sq).trans hvar_bal) have hrQ_le_n : r ^ Q ≤ n' := numGroups_pow_numNodes_le_self (by omega) (by omega) - have hn_le_enc : n' ≤ (encPair encUnary encSys (n', sys')).length := by - simp only [length_encPair, encUnary_apply, List.length_replicate]; omega + have hn_le_enc : n' ≤ (encPair encUnary encSys (n', sys')).length := by enc_len generalize hL_eq : (encPair encUnary encSys (n', sys')).length = L at hn_le_enc hT_le ⊢ set S_sp := Cslib.subsetPairCount n' q; set D := ReplacementParams.auxDim n' have hS_eq : SubsetPairFold.subsetPairCount n' q = S_sp := SubsetPairFold.subsetPairCount_eq n' q @@ -359,8 +359,7 @@ private theorem exists_computableInO_signedMeasJet : omega | some y => have hiy : (encPair eMIn encJet (inp, y)).length ≤ - 2 * (eMIn inp).length + 2 * (encOption encJet (some y)).length + 1 := by - simp only [length_encPair, encOption_some, List.length_cons]; omega + 2 * (eMIn inp).length + 2 * (encOption encJet (some y)).length + 1 := by enc_len have hb := (ha (inp, y)).trans (Nat.mul_le_mul_left ca (Nat.pow_le_pow_left (Nat.add_le_add_right hiy 1) da)) simp only [Option.elim_some]; dsimp only [cAddM]; omega @@ -386,8 +385,7 @@ private theorem exists_computableInO_signedMeasJet : simp only [Option.elim_none, NativeCertificate.snd_time, NativeCertificate.linear_time]; omega | some y => have hiy : (encPair eMIn encJet (inp, y)).length ≤ - 2 * (eMIn inp).length + 2 * (encOption encJet (some y)).length + 1 := by - simp only [length_encPair, encOption_some, List.length_cons]; omega + 2 * (eMIn inp).length + 2 * (encOption encJet (some y)).length + 1 := by enc_len have hb := (ha (inp, y)).trans (Nat.mul_le_mul_left ca (Nat.pow_le_pow_left (Nat.add_le_add_right hiy 1) da)) simp only [Option.elim_some]; dsimp only [cProjWC, cAddM]; omega @@ -492,7 +490,7 @@ private theorem exists_computableInO_signedMeasJet : hj fun i _ y hy j' _ u' _ => by have hw_len := MeasurementFold.length_values_le dc.2.2.1.1 dc.2.2.1.2 i have hwc_len : (eWC (Cslib.Radix.measurementValues dc.2.2.1.1 dc.2.2.1.2 i, - mkMCtx dc)).length ≤ L_wc dc := by simp only [eWC, length_encPair, L_wc]; omega + mkMCtx dc)).length ≤ L_wc dc := by enc_len [eWC, L_wc] have hopt_len : (encOption encJet (some y)).length ≤ L_opt dc := by rw [← hy]; exact (ho1_le _).trans (Nat.mul_le_mul_left co1 (Nat.pow_le_pow_left (Nat.add_le_add_right hwc_len 1) do1)) @@ -539,7 +537,7 @@ private theorem exists_computableInO_signedMeasJet : (Cslib.Radix.measurementValues dc.2.2.1.1 dc.2.2.1.2 j, mkMCtx dc) := by rw [IndexFold.run_index, hrun_eq dc j] have hwc_len : (eWC (Cslib.Radix.measurementValues dc.2.2.1.1 dc.2.2.1.2 j, - mkMCtx dc)).length ≤ L_wc dc := by simp only [eWC, length_encPair, L_wc]; omega + mkMCtx dc)).length ≤ L_wc dc := by enc_len [eWC, L_wc] have hpay_t : cPay.time (Cslib.Radix.measurementValues st.2.1.1 st.2.1.2 st.1, st.2.2.1) ≤ (dc.2.numGroups * (2 ^ maxGroupDim dc.2.numVars dc.2.numGroups dc.2.varGroups + 1) + 1) * P_pay dc := by @@ -682,9 +680,7 @@ private theorem exists_computableInO_nodeJet : (SubsetPairFold.encDecodedPair (SubsetPairFold.unrankSubsetPair n q i)).length ≤ 6 * n + 7 := by unfold SubsetPairFold.encDecodedPair - rw [length_encPair, length_encPair, encBits_apply, encBits_apply, encBool_apply, - List.length_singleton, SubsetPairFold.length_fst_unrankSubsetPair, - SubsetPairFold.length_snd_unrankSubsetPair]; omega + enc_len [SubsetPairFold.length_fst_unrankSubsetPair, SubsetPairFold.length_snd_unrankSubsetPair] have hB : ∀ qs j, j ≤ SubsetPairFold.subsetPairCount qs.2.numVars qs.1 → (eSubAcc (SubsetPairFold.runPrefix subsetPairStepBody qs.2.numVars qs.1 j (qs.2, zeroJet qs.2.jetOrder qs.2.precision)).2.2).length ≤ B_sub qs := by @@ -709,7 +705,7 @@ private theorem exists_computableInO_nodeJet : (Nat.mul_le_mul_left 2 (Nat.mul_le_mul_left _ (Nat.add_le_add_right (Nat.mul_le_mul_left 2 (Nat.add_le_add hN_sz hM_sz)) 3))) 1)) simp only [Option.elim_some] at hjet_le - dsimp only [eSubAcc, B_sub, B_jet] at hjet_le ⊢; rw [length_encPair]; dsimp only; omega + dsimp only [eSubAcc, B_sub, B_jet] at hjet_le ⊢; enc_len let L_sub (qs : ℕ × SubsetStepCtx) := 2 * (6 * qs.2.numVars + 7) + 2 * B_sub qs + 1 have hLsub_pb : PolyBounded (fun qs => (eQS qs).length) L_sub := (((PolyBounded.const 2).mul (((PolyBounded.const 6).mul hn_pb).add (.const 7))).add @@ -1140,8 +1136,7 @@ private theorem exists_boundedIncidenceBranch_cert : have hlen : (encPair eCtx encUnary ((idPair, buildEqRowTables idPair.1.1.1 idPair.1.2.2.2 idPair.2), t)).length ≤ 2 * (eCtx (idPair, buildEqRowTables idPair.1.1.1 idPair.1.2.2.2 idPair.2)).length + - 2 * branchQ_u idPair.1 + 1 := by - simp only [length_encPair, encUnary_apply, List.length_replicate]; omega + 2 * branchQ_u idPair.1 + 1 := by enc_len have hov := (hn1_le ((idPair, buildEqRowTables idPair.1.1.1 idPair.1.2.2.2 idPair.2), t)).trans (Nat.mul_le_mul_left cn1 (Nat.pow_le_pow_left (Nat.add_le_add_right hlen 1) dn1)) diff --git a/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean b/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean index 7879b8264d..6274b7bbd4 100644 --- a/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean +++ b/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean @@ -15,6 +15,7 @@ public import Complexity.Logics.Propositional.CNF.ParityTests import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Tactic.EncLen import Mathlib.Algebra.BigOperators.Ring.List import Mathlib.Data.List.Dedup @@ -312,8 +313,7 @@ theorem exists_fin_of_lt_candidateTupleCount {m P j : ℕ} (hj : j < candidateTu (growth := fun p => 4 * (encPair (encPair encUnary encUnary) encNat p).length + 6) (((PolyBounded.const 4).mul .self).add (.const 6)) (fun p state _ _ => by - have hm_le : p.1.1 ≤ (encPair (encPair encUnary encUnary) encNat p).length := by - simp only [length_encPair, encUnary_apply, List.length_replicate]; omega + have hm_le : p.1.1 ≤ (encPair (encPair encUnary encUnary) encNat p).length := by enc_len have hd_le : (if p.1.1 = 0 then 0 else state.1 % (2 * p.1.1)) / 2 ≤ p.1.1 := by split_ifs with hm · omega @@ -321,10 +321,7 @@ theorem exists_fin_of_lt_candidateTupleCount {m P j : ℕ} (hj : j < candidateTu have hdiv_le : (encNat (state.1 / (2 * p.1.1))).length ≤ (encNat state.1).length := by simp only [encNat_apply, Nat.size_eq_bits_len] exact Nat.size_le_size (Nat.div_le_self _ _) - simp only [step, encState, encElem, length_encPair, encList_append, List.length_append, - encList_cons, encList_nil, List.append_nil, length_frame, encUnary_apply, - List.length_replicate, encBool_apply, List.length_singleton] - omega) + enc_len [step, encState, encElem, encList_append, encList_cons, encList_nil, List.append_nil]) convert (ComputableInPolyTime.snd encNat (encList encElem)).comp hfold using 1 funext p; simp only [Function.comp_apply, hfold_acc, List.nil_append] @@ -999,14 +996,12 @@ theorem length_encSelectBestAcc_run_le (countSys : List (List Bool) → ℕ) 6 * m + 2 * P + 2 * (encList encBits rows).length + V + 6 := by have hparams := run_selectBestStep_params countSys m P k rows rcases Nat.eq_zero_or_pos k with rfl | hkpos - · simp only [IndexFold.run_zero, encSelectBestAcc, length_encPair, encUnary_apply, - List.length_replicate, encOption_none, List.length_nil]; omega + · enc_len [IndexFold.run_zero, encSelectBestAcc] · obtain ⟨jStar, hjStar_lt, hopt, _, _⟩ := run_selectBestStep_spec countSys m P rows hkpos have hv := hV jStar hjStar_lt rcases r : IndexFold.run (selectBestStep countSys) k ((m, P), (rows, none)) with ⟨_, _, _, _⟩ simp only [r] at hparams hopt ⊢; rcases hparams with ⟨rfl, rfl⟩; subst hopt - simp only [encSelectBestAcc, length_encPair, encUnary_apply, List.length_replicate, - encOption_some, List.length_cons, encBits_apply, length_materializeTestRow]; omega + enc_len [encSelectBestAcc, length_materializeTestRow] private theorem selectBestIn_le (m P : ℕ) (rows : List (List Bool)) : m ≤ (encSelectBestIn (m, P, rows)).length ∧ P ≤ (encSelectBestIn (m, P, rows)).length ∧ diff --git a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean index 7f7c78bd9e..3f3598e72c 100644 --- a/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean +++ b/Complexity/Computability/PolyTime/CNF/SparseCNFLeafCounter.lean @@ -20,6 +20,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Li import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain +import Complexity.Tactic.EncLen import Mathlib.Data.List.GetD import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring @@ -501,8 +502,7 @@ private theorem polyBounded_prod_space {α β γ : Type} {ei : α ↪ List Bool} private theorem polyBounded_pair_len {α β : Type} {ei : α ↪ List Bool} {eo : β ↪ List Bool} {f : α → β} (hf : PolyBounded (fun a => (ei a).length) (fun a => (eo (f a)).length)) : PolyBounded (fun a => (ei a).length) (fun a => (encPair ei eo (a, f a)).length) := - ((((PolyBounded.const 2).mul PolyBounded.self).add hf).add (.const 2)).mono fun a => by - simp only [length_encPair]; omega + ((((PolyBounded.const 2).mul PolyBounded.self).add hf).add (.const 2)).mono fun a => by enc_len private abbrev toSysInput (k : ℕ) (q : (ℕ × CNF ℕ) × List (List Bool)) : PolySys := (q.1.1, compileParitySystemBounded k q.1.2 q.2) @@ -786,8 +786,7 @@ private theorem polyBounded_initRowsCertificate_space (initRowsCertificate hBOf).space := by have hc := NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_mbPair hBOf) have hsum : PolyBounded (fun p : ℕ × ℕ => (encPair encUnary encUnary p).length) - (fun p => p.1 + p.2) := PolyBounded.self.mono fun p => by - simp only [length_encPair, encUnary_apply, List.length_replicate]; omega + (fun p => p.1 + p.2) := PolyBounded.self.mono fun p => by enc_len exact hc.2.add (((PolyBounded.of_polynomiallyBounded id initialTestsRows_computableInO.choose_spec.choose_spec.2.1).comp hsum).comp (computableInPolyTime_mbPair hBOf).polyBounded_length) @@ -971,7 +970,7 @@ private theorem exists_compiledRowCertificate_bounds (k N₀ : ℕ) obtain ⟨hw, hsub⟩ := validDeclaredInput_eq_true_iff.mp hv have hN_le : NOf x.1 ≤ pNLen L := by simpa only [Function.comp_apply, encUnary_apply, List.length_replicate, L] using hNLen x - have hψ_le : (encCNF x.2).length ≤ L := by simp only [L, length_encPair]; omega + have hψ_le : (encCNF x.2).length ≤ L := by enc_len [L] have hm_le : x.2.length ≤ L := (show x.2.length ≤ (encCNF x.2).length from by unfold encCNF @@ -981,8 +980,7 @@ private theorem exists_compiledRowCertificate_bounds (k N₀ : ℕ) simpa only [encBits_apply, (hrprops r hr).1] using hm_le).trans (Nat.mul_le_mul_right (2 * L + 1) (hrlen.trans (Nat.mul_le_mul_left 7 hN_le))) have hcin : (encCandIn ((NOf x.1, x.2), rows)).length ≤ candInBound L := by - simp only [encCandIn, encCandCtx, length_encPair, encUnary_apply, List.length_replicate, - candInBound]; omega + enc_len [encCandIn, encCandCtx, candInBound] have hrg := (hRowG ((NOf x.1, x.2), rows)).trans (hmRowG hcin) unfold compiledRowCertificate guardedTargetOfPolyTime; rw [guardedTargetCertificate_time] by_cases h6 : rows.length ≤ 6 * NOf x.1 @@ -1209,7 +1207,7 @@ theorem exists_normalizeDeclaredLeafCertificate_bounds (fun x => (encPair encNat encNat (h x, shiftAmount NOf x)).length) := ((((PolyBounded.const 2).mul (polyBounded_output_of_space cLeaf hSpace)).add (computableInPolyTime_shiftAmount hNOf).polyBounded_length).add (.const 2)).mono fun x => by - simp only [length_encPair]; omega + enc_len have hShT := (NativeCertificate.ofPolyTime_isPolynomial (computableInPolyTime_shiftAmount hNOf)).1 have hSrT := (NativeCertificate.ofPolyTime_isPolynomial ComputableInPolyTime.binary_shiftRight).1.comp hPairLen diff --git a/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean b/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean index 245b61676f..1c924e9e20 100644 --- a/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean +++ b/Complexity/Computability/TreeEval/Reader/Cert/Offset.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.TreeEval.Reader.Encode public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.InSpaceLib +import Complexity.Tactic.EncLen /-! # Offsets of nodes within linear work space @@ -158,7 +159,7 @@ private theorem bodyLength_inSpace : .of_le fun q => by have := length_encNat_le_self q.1 have := length_encNat_le_self q.2 - simp only [length_encPair]; omega + enc_len have hstep : ComputableInSpace bodyStep (encPair encNat encNat) (encPair encNat encNat) fun q => 64 * ((encPair encNat encNat q).length + 1) := by have hl₀ : (fun q => (encPair encNat encNat q).length) ≼ @@ -214,7 +215,7 @@ private theorem three_mul_length_le (st : List Frame) : 3 * st.length ≤ induction st with | nil => simp | cons fr st ih => - have : 1 ≤ (encFrame fr).length := by rw [encFrame_apply, length_encPair]; omega + have : 1 ≤ (encFrame fr).length := by enc_len [encFrame_apply] rw [length_encList] at ih ⊢ simp only [List.length_cons, List.map_cons, List.sum_cons] omega @@ -236,8 +237,7 @@ theorem dirs_inSpace : .of_le fun _ => by omega have hd := budget_comp (frameFinite_inSpace (encB := encBool) fun y : Fin 4 × Bool × Fin 3 => y.1.val % 2 == 1) - ((snd (encList encBool) encFrame).weaken hl₀) (.of_le fun x => by - simp only [length_encPair]; omega) + ((snd (encList encBool) encFrame).weaken hl₀) (.of_le fun x => by enc_len) exact (budget_cons hd ((fst (encList encBool) encFrame).weaken hl₀)).of_enc_eq fun _ => rfl have hlen (st : List Frame) (i : ℕ) : (encList encBool ((st.take i).foldl (fun acc fr => fr.dir :: acc) [])).length ≤ @@ -253,7 +253,7 @@ theorem dirs_inSpace : (fun st i hi => by have h₁ := hlen st i have h₂ := length_le_encList_of_mem encFrame (List.getElem_mem hi) - rw [length_encPair]; dsimp only; omega) + enc_len) (fun st i _ => hlen st i) exact h.mono_le fun st => by omega @@ -315,8 +315,7 @@ theorem pathOffset_inSpace : have h₁ := length_pathOffset_le q.1.1 q.1.2 (q.2.take j) have h₂ := length_encNat_le_self q.1.1 have h₃ := length_encNat_le_self (q.1.2 - (q.2.take j).length) - simp only [length_encPair, zero_add] at * - omega + enc_len [zero_add] at * have h := foldl (encL := encList encBool) (list := fun q : (ℕ × ℕ) × List Bool => q.2) (step := pathStep') ((snd (encPair encNat encNat) (encList encBool)).weaken hl) hinit pathStep'_inSpace @@ -325,14 +324,12 @@ theorem pathOffset_inSpace : (fun q i hi => by have h₁ := hstate q i rw [foldl_pathStep', foldl_pathStep] at h₁ ⊢ - simp only [length_encPair, encBool_apply, List.length_singleton] at h₁ ⊢ - omega) + enc_len at h₁ ⊢) (fun q i _ => hstate q i) refine (snd' (snd' h)).mono_le (fun q => ?_) |>.of_enc_eq fun q => by rw [foldl_pathStep', foldl_pathStep, zero_add] have := length_encNat_le_self q.1.1 - simp only [length_encPair] at * - omega + enc_len at * end Reader diff --git a/Complexity/Crypto/Computational/OneWay/BPP.lean b/Complexity/Crypto/Computational/OneWay/BPP.lean index 690626cbc0..2c1705b475 100644 --- a/Complexity/Crypto/Computational/OneWay/BPP.lean +++ b/Complexity/Crypto/Computational/OneWay/BPP.lean @@ -19,6 +19,7 @@ import Complexity.Computability.Probabilistic.PPT.Capture import Complexity.Computability.Probabilistic.Sampling import Complexity.Probability.PMF import Complexity.Probability.PMF.Map +import Complexity.Tactic.EncLen import Cslib.Foundations.Data.Polynomial.Monotone /-! @@ -179,12 +180,9 @@ theorem half_le_succProbability_inversionGame {p : Polynomial ℕ} p.eval (encPreimagePrefix (query j)).length ≤ searchCoinLength p (n, f x) := by have hj' := length_iterate_preimageSearchStep D (n, f x) j constructor - · simp only [query, length_encPair, encUnary_apply, List.length_replicate, encBits_apply] - omega + · enc_len [query] · refine Polynomial.eval_mono p ?_ - simp only [query, length_encPair, encUnary_apply, List.length_replicate, encBits_apply, - List.length_append, hj', List.length_singleton] - omega + enc_len [query, hj'] have hbad (j : ℕ) (hj : j < n) : μ.toOuterMeasure (bad j) ≤ 1 / 2 ^ (n + 1) := by refine (toOuterMeasure_take_wrong_le hV (query j) (hlen j hj).2).trans ?_ simp only [Polynomial.eval_add, Polynomial.eval_X, Polynomial.eval_one] diff --git a/Complexity/Tactic/EncLen.lean b/Complexity/Tactic/EncLen.lean new file mode 100644 index 0000000000..be9dcd1665 --- /dev/null +++ b/Complexity/Tactic/EncLen.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +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 +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Sum +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Unary +public meta import Lean.Elab.Tactic.Omega +public meta import Lean.Elab.Tactic.Simp + +/-! +# Closing bounds on encoded lengths + +`enc_len` expands encoded lengths into the lengths of their fields, then counts with `omega`. + +The expansion is `simp only` with a fixed list of lemmas for the standard encodings, followed by +the lemmas given at the call. Local encodings stay visible there: `enc_len [eFoo_apply]`. The +location works as for `simp`, so hypotheses are expanded only when requested, as in +`enc_len at h ⊢`. + +`omega` treats a product of two lengths as an atom, which it can match only when both sides +expanded to the same term. Bound a product by a fact in its own step, and bound each component by +one context length in its own step, so that the last `enc_len` only adds. Expanding everything at +once costs more: `omega` slows sharply with the number of atoms and facts. + +The tactic fails when nothing expands, naming the plain `omega` that is then the right call, and +when `omega` cannot close the expanded goal, showing that goal. + +## Main definitions + +* `enc_len`: expand encoded lengths into their fields and close the bound with `omega`. +-/ + +public section + +namespace Cslib.Tactic.EncLen + +open Lean Parser.Tactic Elab Tactic Turing.MultiTapeTM + +/-- `enc_len` closes a linear bound on encoded lengths: it expands them into the lengths of their +fields with `simp only`, then runs `omega`. + +* `enc_len [eFoo_apply]` also unfolds the local encoding `eFoo`. +* `enc_len at h ⊢` also expands the hypothesis `h`; without a location only the goal is expanded. + +Products of lengths are atoms for `omega`. Bound them by facts in context first. -/ +syntax (name := encLen) "enc_len" (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? + (location)? : tactic + +elab_rules : tactic + | `(tactic| enc_len $[[$args,*]]? $[$loc]?) => do + let args := (args.map (·.getElems)).getD #[] + try + evalTactic (← `(tactic| simp only [length_encPair, length_frame, encUnary_apply, + List.length_replicate, encBits_apply, encBool_apply, encOption_none, encOption_some, + encSum_inl, encSum_inr, List.length_nil, List.length_cons, List.length_append, + $args,*] $[$loc]?)) + catch ex => + throwError "enc_len: the expansion failed: {ex.toMessageData}\n\ + If there is no encoded length to expand, use `omega`." + if (← getUnsolvedGoals).isEmpty then return + let goal ← getMainGoal + try + evalTactic (← `(tactic| omega)) + catch ex => + throwError "enc_len: `omega` could not close the expanded goal. Products are atoms, so \ + bound them by facts in context, and unfold local encodings with `enc_len [eFoo_apply]`.\n\ + {goal}\n{ex.toMessageData}" + +end Cslib.Tactic.EncLen + +end diff --git a/ComplexityTests/EncLenTactic.lean b/ComplexityTests/EncLenTactic.lean new file mode 100644 index 0000000000..2673130e4f --- /dev/null +++ b/ComplexityTests/EncLenTactic.lean @@ -0,0 +1,114 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +module +-- upstream: local-only (tests of the enc_len tactic) + +public import Complexity.Tactic.EncLen + +/-! +# Tests for `enc_len` +-/ + +public section + +open Turing.MultiTapeTM + +variable {α β : Type} {eA : α ↪ List Bool} {eB : β ↪ List Bool} + +/-- A local encoding, unfolded by name at the call. -/ +@[expose] def eLocal : ℕ × Bool ↪ List Bool := encPair encUnary encBool + +theorem eLocal_apply (p : ℕ × Bool) : eLocal p = encPair encUnary encBool p := rfl + +/-! Nested pairs expand to their fields, with projections of literal pairs reduced. -/ + +example (a : α) (b : β) (n : ℕ) : + (eA a).length ≤ (encPair eA (encPair eB encUnary) (a, b, n)).length := by + enc_len + +example (a : α) (b : β) (n : ℕ) : + n + (eB b).length < (encPair eA (encPair eB encUnary) (a, b, n)).length := by + enc_len + +/-- Variable pairs keep their projections as atoms. -/ +example (p : α × β) : (eB p.2).length ≤ (encPair eA eB p).length := by + enc_len + +/-! The standard leaf encodings. -/ + +example (b : Bool) (w : List Bool) (x : α) : + (encPair encBool encBits (b, w)).length = 3 + w.length ∧ + (encOption eA (some x)).length = (eA x).length + 1 ∧ + (encOption eA (none : Option α)).length = 0 ∧ + (encSum eA eB (Sum.inl x : α ⊕ β)).length = (eA x).length + 1 := by + refine ⟨?_, ?_, ?_, ?_⟩ <;> enc_len + +/-! Local encodings are named at the call. -/ + +example (p : ℕ × Bool) : p.1 ≤ (eLocal p).length := by + enc_len [eLocal_apply] + +/-! Locations work as for `simp`, and hypotheses stay unexpanded otherwise. -/ + +example (a : α) (b : β) (T : ℕ) (h : (encPair eA eB (a, b)).length ≤ T) : (eA a).length ≤ T := by + enc_len at h ⊢ + +example (a : α) (b : β) (T : ℕ) (h : (encPair eA eB (a, b)).length ≤ T) : (eB b).length ≤ T := by + enc_len at * + +/-! A product is an atom, which the expansion rewrites everywhere it is asked to. -/ + +example (a : α) (b : β) (k T : ℕ) (hk : k * (encPair eA eB (a, b)).length ≤ T) : + k * (encPair eA eB (a, b)).length + (eA a).length ≤ T + (encPair eA eB (a, b)).length := by + enc_len at hk ⊢ + +/-- The tactic also closes a goal that the expansion alone proves. -/ +example (n : ℕ) : (encUnary n).length = n := by + enc_len + +/-! Failures. -/ + +/-- +error: enc_len: the expansion failed: `simp` made no progress +If there is no encoded length to expand, use `omega`. +-/ +#guard_msgs in +example (a b : ℕ) (h : a ≤ b) : a ≤ b + 1 := by + enc_len + +/-- enc_len: `omega` could not close the expanded goal. -/ +#guard_msgs (substring := true) in +example (a : α) (b : β) : (encPair eA eB (a, b)).length ≤ (eA a).length := by + enc_len + +/-! A false bound shows the expanded form, not the original encoding. -/ + +/-- ⊢ 2 * (eA a).length + 1 + (eB b).length ≤ (eA a).length -/ +#guard_msgs (substring := true) in +example (a : α) (b : β) : (encPair eA eB (a, b)).length ≤ (eA a).length := by + enc_len + +/-! Products stay atoms, so this needs a scaling fact. -/ + +/-- enc_len: `omega` could not close the expanded goal. -/ +#guard_msgs (substring := true) in +example (a : α) (b : β) (k : ℕ) : + k * (eA a).length ≤ k * (encPair eA eB (a, b)).length := by + enc_len + +/-- With the scaling fact in context, the same goal only adds. -/ +example (a : α) (b : β) (k : ℕ) : + k * (eA a).length ≤ k * (encPair eA eB (a, b)).length := by + have h := Nat.mul_le_mul_left k (length_le_encPair_left eA eB (a, b)) + enc_len at h ⊢ + +/-! A bad lemma name reports the real error. -/ + +/-- error: Unknown identifier `noSuchLemma` -/ +#guard_msgs in +example (n : ℕ) : (encUnary n).length ≤ n := by + enc_len [noSuchLemma] From 58e592bf960041b353f2b246f3aa1ba35484b1e1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Tue, 3 Nov 2026 19:13:26 -0500 Subject: [PATCH 2/2] fix(EncLen): keep encoded-length automation on its original goal Bounded coordinator fix for #2224 under root delegation and #2209#6618723309 by codex-enc-len-goal-scope-1651-20261104. Reuse the independent original36-file review5756806689 while obtaining fresh narrow outside review of the tactic behavior/regression/manual delta. Preserve Christian Reitwiessner and Samuel Schlesinger source credit, all33 migrated client files, public computational statements/definitions/bounds, existing tests, syntax and diagnostics. AI-assisted preparation by Codex; no self-approval or broader #2209/#2184 completion. Use the pinned Lean Tactic.focus around the existing elaborator. A real pre-fix probe fails after simp closes the original goal and omega advances to the unrelated NonemptyNat sibling. The same fixture succeeds after the change; retain it unbulleted in the complete test file, with only that intentionally multigoal example exempted from the style warning. No heartbeat or recursion budget changes. The manual adds import, selective expansion/local lemma/scaling/diagnostic and recovery routes before Proof style as interface maintenance, preserving the separate #2215/#2223 insertion anchors. Validation before this checkpoint: strict affected library and complete test pass3656jobs, baseline failure and fixed success saved, manual links/excerpts plus37tooltests and targeted hygiene/whitespace pass. All other source bytes and33 whole client entries are exact original; the ordinary fixed-main merge retains unrelated main/pins and canonical imports. One scheduled default all-six, actual manual PDF inspection and fresh independent outside delta review remain before publication. Agent manual roles/procedures and selected abstract statements/catalogue/rendering are unaffected. --- Complexity/Tactic/EncLen.lean | 2 +- ComplexityTests/EncLenTactic.lean | 9 +++++++++ manual/design-and-assurance/automation.md | 24 +++++++++++++++++++++++ 3 files changed, 34 insertions(+), 1 deletion(-) diff --git a/Complexity/Tactic/EncLen.lean b/Complexity/Tactic/EncLen.lean index be9dcd1665..e818f264d9 100644 --- a/Complexity/Tactic/EncLen.lean +++ b/Complexity/Tactic/EncLen.lean @@ -55,7 +55,7 @@ syntax (name := encLen) "enc_len" (" [" (simpStar <|> simpErase <|> simpLemma),* (location)? : tactic elab_rules : tactic - | `(tactic| enc_len $[[$args,*]]? $[$loc]?) => do + | `(tactic| enc_len $[[$args,*]]? $[$loc]?) => focus do let args := (args.map (·.getElems)).getD #[] try evalTactic (← `(tactic| simp only [length_encPair, length_frame, encUnary_apply, diff --git a/ComplexityTests/EncLenTactic.lean b/ComplexityTests/EncLenTactic.lean index 2673130e4f..9c11669091 100644 --- a/ComplexityTests/EncLenTactic.lean +++ b/ComplexityTests/EncLenTactic.lean @@ -70,6 +70,15 @@ example (a : α) (b : β) (k T : ℕ) (hk : k * (encPair eA eB (a, b)).length example (n : ℕ) : (encUnary n).length = n := by enc_len +-- Closing the original goal by expansion must leave its sibling pending; focusing the caller +-- would hide the regression. +set_option linter.style.multiGoal false in +example (n : ℕ) : + (encUnary n).length = n ∧ Nonempty ℕ := by + constructor + enc_len + exact ⟨0⟩ + /-! Failures. -/ /-- diff --git a/manual/design-and-assurance/automation.md b/manual/design-and-assurance/automation.md index 8742be8cbb..7822bf738e 100644 --- a/manual/design-and-assurance/automation.md +++ b/manual/design-and-assurance/automation.md @@ -64,6 +64,30 @@ This contract answers a recurrent concern in the transcript: removing proof book [`FOOperator.lean`](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Tactic/FOOperator.lean#L14) similarly synthesizes a single uniform formula for a family through `fo_definable`, with `fo_wf` handling supported well-formedness/positivity obligations. This does not mean a different formula may be selected separately for each structure. Fixed-point operators, positivity and interpretation legality remain mathematical constraints. The [logic survey](../circuits-logic-and-other-models/index.md) records the distinction between interpretation, quantifier-free reduction and projection. +## Close encoded-length arithmetic + +Import `Complexity.Tactic.EncLen` and use `enc_len` to expand standard encoded lengths with +a fixed `simp only` list, then close the resulting arithmetic with `omega`. The complete +[checked clients](../../ComplexityTests/EncLenTactic.lean) cover nested and variable pairs, +leaf encodings, local encodings, locations, scaling facts and diagnostics. This proves encoding +arithmetic; it does not construct a computation or resource certificate. + +By default only the current goal is expanded. Supply a local encoding lemma explicitly with +`enc_len [eFoo_apply]`. Use `enc_len at h ⊢` to expand one hypothesis and the goal, or `enc_len at *` +when expansion of every hypothesis is useful. Each call handles its original goal: if expansion +closes it, unrelated sibling goals remain for the caller. The checked multi-goal client exercises +that case without bullets or `<;>`. + +Variable products remain atoms for `omega`. Supply a scaling fact, such as +`Nat.mul_le_mul_left k h`, before the final call; expanding a product's factors does not prove +its monotonicity. Prefer the selective location form when hypotheses already state bounds in +the encoding's original form. + +If nothing expands, the diagnostic recommends plain `omega`. If the expanded goal remains, +inspect its bounds, supply missing arithmetic facts or name a local encoding lemma. An unknown +lemma reports the underlying name-resolution error; check its spelling, namespace and import. +The tactic neither invents a growth bound nor searches for an encoding definition to unfold. + ## Proof style as interface maintenance The project asks for nonterminal `simp only` where later steps depend on the resulting normal form, forbids global simplification attributes on machine transitions, and requires comments and reviewed allowlisting for unusually large heartbeat bounds. These policies address predictable search explosions and fragile proofs. They complement semantic lemmas and named certificates; they do not prove maintainability by themselves. [Proof hygiene](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/AGENTS.md#proof-hygiene)