From b725dc5207fc91da59e36e87bcc98476fb7538b3 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 17:08:49 +0000 Subject: [PATCH 1/3] refactor(Universal): dedupe encodings and extract proof fragments in Universal/Complexity Move encSign and encUnit to Encodings/Bool (replacing the identical encMove and a test-local encUnit), move the encInt successor/predecessor length bounds next to length_encInt, and extract repeated size arguments of the step complexity proof into lemmas. Co-Authored-By: Claude Opus 5.5 --- .../FineGrained/CountingNativeEndpoint.lean | 4 +- .../Machines/ReadMachine/Tidy.lean | 6 +- .../MultiTape/Complexity/Primitives.lean | 8 ++ .../Turing/MultiTape/Encodings/Bool.lean | 21 +++- .../MultiTape/Encodings/StepMachineComp.lean | 44 +++---- .../Internal/StepMachineCompiler.lean | 39 +++---- .../MultiTape/Universal/Complexity.lean | 109 +++++++----------- .../CNF/BranchedSparseCNFCounter.lean | 3 +- .../BoundedIncidenceCounter.lean | 4 +- .../CNF/BranchedSparseCNFCounter.lean | 1 - ComplexityTests/FiniteCSP.lean | 5 +- ComplexityTests/Space/Savitch.lean | 3 +- 12 files changed, 118 insertions(+), 129 deletions(-) diff --git a/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean index a1cdd4e02..d94ad11a1 100644 --- a/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean +++ b/Complexity/Computability/Complexity/FineGrained/CountingNativeEndpoint.lean @@ -12,7 +12,7 @@ import Complexity.Computability.Complexity.FineGrained.CountingSparsificationUni import Complexity.Computability.Complexity.FineGrained.CountingParameterBounds import Complexity.Computability.PolyTime.FineGrained.ParameterCheck import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParametersPolyTime -import Complexity.Computability.Machines.Turing.MultiTape.Universal.Complexity +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bounds import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat @@ -71,7 +71,6 @@ namespace Cslib.Complexity.CountingNativeEndpointPrep open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification open Cslib.Logic.PL.CNF (validDeclaredInput validDeclaredInput_eq_true_iff) open Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM -open Turing.MultiTapeTM.Universal (encUnit encUnit_apply) open CountingSparsify SubexponentialSAT SubexponentialSAT.ReplacementParams open SubexponentialSAT.SparseCountingScale Filter @@ -426,7 +425,6 @@ namespace Cslib.Complexity.CountingNativeEndpointPrep open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.CNF.Sparsification open Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM Cslib.GenericRAM -open Turing.MultiTapeTM.Universal (encUnit encUnit_apply) open CountingSparsify SubexponentialSAT SubexponentialSAT.SparsePolyCounter open BranchedSparseCNFCounter diff --git a/Complexity/Computability/Machines/ReadMachine/Tidy.lean b/Complexity/Computability/Machines/ReadMachine/Tidy.lean index 60828dc5c..f5aad4528 100644 --- a/Complexity/Computability/Machines/ReadMachine/Tidy.lean +++ b/Complexity/Computability/Machines/ReadMachine/Tidy.lean @@ -279,16 +279,16 @@ theorem toStepMachine_resourceCertificate (hhalt : ComputableInO m.halt encS enc (budget_prod hisN (budget_prod he (budget_prod hl (budget_prod ha hz)))) hst -- the three results have hres₁ := budget_prod (encB := encPair encS encNat) (budget_prod (fst' hr) hpos) - (budget_prod (encB := encMove) (budget_const (0 : SignType) hin hst) (snd' hr)) + (budget_prod (encB := encSign) (budget_const (0 : SignType) hin hst) (snd' hr)) have hres₂ := budget_prod (encB := encPair encS encNat) (budget_prod hq (budget_comp natSucc hpos (sq_bigOLe hpos.length_le) (.add hpos.length_le (.const 1 _)))) - (budget_prod (encB := encMove) (budget_const (1 : SignType) hin hst) + (budget_prod (encB := encSign) (budget_const (1 : SignType) hin hst) (budget_const (encB := encBits) ([] : List Bool) hin hst)) have hres₃ := budget_prod (encB := encPair encS encNat) (budget_prod hq (budget_comp natPred hpos (sq_bigOLe hpos.length_le) (.add hpos.length_le (.const 1 _)))) - (budget_prod (encB := encMove) (budget_const (-1 : SignType) hin hst) + (budget_prod (encB := encSign) (budget_const (-1 : SignType) hin hst) (budget_const (encB := encBits) ([] : List Bool) hin hst)) have hall := budget_ite hc hres₁ (budget_ite hl hres₂ hres₃) refine ((hall.of_enc_eq fun p => by rw [← stepBy_eq]; rfl).mono 4 (fun p => ?_) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean index 5a6a6d76e..68c387f5f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Primitives.lean @@ -82,6 +82,14 @@ public lemma length_encInt (z : ℤ) : (encInt z).length = if z < 0 then (-z).toNat else z.toNat + 1 := by rcases z with n | n <;> simp [Int.negSucc_lt_zero] +public lemma length_encInt_add_one_le (z : ℤ) : + (encInt (z + 1)).length ≤ (encInt z).length + 1 := by + rw [length_encInt, length_encInt]; split_ifs <;> omega + +public lemma length_encInt_sub_one_le (z : ℤ) : + (encInt (z - 1)).length ≤ (encInt z).length + 1 := by + rw [length_encInt, length_encInt]; split_ifs <;> omega + namespace EncInt /-- Adds one to an encoded integer. -/ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Bool.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Bool.lean index e8a1cead5..30b0f7e6b 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Bool.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Bool.lean @@ -8,10 +8,17 @@ module -- upstream: vendored crei:crei/tidy-universal @7f7c0696 (unsubmitted) public import Complexity.Init +public import Mathlib.Basic.Sign.Defs public import Mathlib.Data.List.Basic public import Mathlib.Logic.Embedding.Basic -/-! # The single-symbol encoding of Booleans -/ +/-! +# Encodings of Booleans, signs and the unit type + +`Turing.MultiTapeTM.encBool` encodes a Boolean by one symbol, `Turing.MultiTapeTM.encSign` a sign, +such as a head move, by at most one symbol, and `Turing.MultiTapeTM.encUnit` the unit by the empty +word. +-/ namespace Turing.MultiTapeTM @@ -22,4 +29,16 @@ namespace Turing.MultiTapeTM @[simp] public lemma encBool_apply (b : Bool) : encBool b = [b] := rfl +/-- Signs: `0 ↦ []`, `-1 ↦ [false]` and `1 ↦ [true]`. -/ +@[expose] public def encSign : SignType ↪ List Bool := + ⟨fun m => match m with | .zero => [] | .neg => [false] | .pos => [true], by + intro a b h + cases a <;> cases b <;> simp_all⟩ + +/-- The unit type, encoded by the empty word. -/ +@[expose] public def encUnit : Unit ↪ List Bool := ⟨fun _ => [], fun _ _ _ => rfl⟩ + +@[simp] +public lemma encUnit_apply (u : Unit) : encUnit u = [] := rfl + end Turing.MultiTapeTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/StepMachineComp.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/StepMachineComp.lean index c6827e2bc..ed42a6105 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/StepMachineComp.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/StepMachineComp.lean @@ -213,23 +213,23 @@ lemma moveOn_eq (n p : ℕ) (d : SignType) : /-- **The head of `g` after a move**, in quadratic time and linear space. -/ lemma moveOn_inO : ComputableInO (fun q : ℕ × ℕ × SignType => moveOn q.1 q.2.1 q.2.2) - (encPair encNat (encPair encNat encMove)) encNat - (fun q => ((encPair encNat (encPair encNat encMove) q).length + 1) ^ 2) - fun q => (encPair encNat (encPair encNat encMove) q).length + 1 := by - have hn := fst encNat (encPair encNat encMove) - have hp := (snd encNat (encPair encNat encMove)).fst' - have hd := (snd encNat (encPair encNat encMove)).snd' - have hdz := (ComputableInDegree.of_finite (encIn := encMove) (encMid := encBool) + (encPair encNat (encPair encNat encSign)) encNat + (fun q => ((encPair encNat (encPair encNat encSign) q).length + 1) ^ 2) + fun q => (encPair encNat (encPair encNat encSign) q).length + 1 := by + have hn := fst encNat (encPair encNat encSign) + have hp := (snd encNat (encPair encNat encSign)).fst' + have hd := (snd encNat (encPair encNat encSign)).snd' + have hdz := (ComputableInDegree.of_finite (encIn := encSign) (encMid := encBool) fun d : SignType => decide (d = 0)).inO_one.comp_linear hd - have hdn := (ComputableInDegree.of_finite (encIn := encMove) (encMid := encBool) + have hdn := (ComputableInDegree.of_finite (encIn := encSign) (encMid := encBool) fun d : SignType => decide (d = -1)).inO_one.comp_linear hd have heq := (eq encNat).comp (hp.prod (natSucc.comp hn)) have h := hdz.ite hp (hdn.ite (natPred.comp hp) (heq.ite hp (natSucc.comp hp))) refine (h.of_enc_eq fun q => ?_).mono 16 (fun q => ?_) fun q => ?_ · simp only [moveOn_eq, Function.comp_apply, decide_eq_true_eq] all_goals - have h₁ := length_encPair (enc₁ := encNat) (enc₂ := encPair encNat encMove) q - have h₂ := length_encPair (enc₁ := encNat) (enc₂ := encMove) q.2 + have h₁ := length_encPair (enc₁ := encNat) (enc₂ := encPair encNat encSign) q + have h₂ := length_encPair (enc₁ := encNat) (enc₂ := encSign) q.2 have h₃ := (show (encNat (q.2.1 - 1)).length ≤ (encNat q.2.1).length from by simpa [Nat.size_eq_bits_len] using Nat.size_le_size (Nat.sub_le q.2.1 1)) have h₄ := ComputableTidilyInO.length_encNat_add_le q.1 1 @@ -324,7 +324,7 @@ variable {f : StepMachine σf Bool Bool} {g : StepMachine σg Bool Bool} {Tf Sf local notation "encArg" => encPair (encCompState encF encG) (encOption encBool) /-- The encoding of the results of a step. -/ -local notation "encRes" => encPair (encCompState encF encG) (encPair encMove encBits) +local notation "encRes" => encPair (encCompState encF encG) (encPair encSign encBits) lemma length_encArg_le (p : CompState σf σg × Option Bool) : (encArg p).length ≤ 2 * (encCompState encF encG p.1).length + 3 := by @@ -403,8 +403,8 @@ lemma stepF_inO (hf : f.ResourceCertificate encF Tf Sf) : have hn : (fun p : CompState σf σg × Option Bool => (f.step p.1.f p.2).2.2.length) ≼ fun p => Sf p.1.f + (encCompState encF encG p.1).length := .of_le_linear cf cf fun p => by have := hcf (p.1.f, p.2) - have := length_le_encPair_right encF (encPair encMove encBits) (f.step p.1.f p.2) - have := length_le_encPair_right encMove encBits (f.step p.1.f p.2).2 + have := length_le_encPair_right encF (encPair encSign encBits) (f.step p.1.f p.2) + have := length_le_encPair_right encSign encBits (f.step p.1.f p.2).2 simp only [encBits_apply] at * nlinarith have hA := (encArg_bigO (encF := encF) (encG := encG)).trans @@ -431,7 +431,7 @@ lemma stepF_inO (hf : f.ResourceCertificate encF Tf Sf) : lemma stepG_round_inO (hg : g.ResourceCertificate encG Tg Sg) : ComputableInO (fun p : CompState σf σg × Option Bool => g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)) - encArg (encPair encG (encPair encMove encBits)) + encArg (encPair encG (encPair encSign encBits)) (fun p => 4 * (encArg p).length + Tg p.1.g.1) (fun p => 4 * (encArg p).length + Sg p.1.g.1) := by have hs := fst (encCompState encF encG) (encOption encBool) @@ -456,10 +456,10 @@ lemma stepG_head_inO (hg : g.ResourceCertificate encG Tg Sg) : moveOn p.1.cd.len p.1.g.2 (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1) encArg encNat (fun p => 6 * (encArg p).length + Tg p.1.g.1 + - ((encPair encNat (encPair encNat encMove) + ((encPair encNat (encPair encNat encSign) (p.1.cd.len, p.1.g.2, (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1)).length + 1) ^ 2) (fun p => 6 * (encArg p).length + Sg p.1.g.1 + - (encPair encNat (encPair encNat encMove) + (encPair encNat (encPair encNat encSign) (p.1.cd.len, p.1.g.2, (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1)).length + 1) := by have hs := fst (encCompState encF encG) (encOption encBool) have hgp := CompState.g_inO.comp_linear hs @@ -492,11 +492,11 @@ lemma stepG_inO (hg : g.ResourceCertificate encG Tg Sg) : obtain ⟨hgs, hpg, hlen, -⟩ := parts_bigO (encF := encF) (encG := encG) have hA := encArg_bigO (encF := encF) (encG := encG) have hmv : (fun p : CompState σf σg × Option Bool => - (encMove (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1).length) ≼ + (encSign (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1).length) ≼ fun p => (encCompState encF encG p.1).length := .of_le_linear 0 1 fun p => by - cases (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1 <;> simp [encMove] - have hsq : (fun p : CompState σf σg × Option Bool => ((encPair encNat (encPair encNat encMove) + cases (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1 <;> simp [encSign] + have hsq : (fun p : CompState σf σg × Option Bool => ((encPair encNat (encPair encNat encSign) (p.1.cd.len, p.1.g.2, (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1)).length + 1) ^ 2) ≼ fun p => ((encCompState encF encG p.1).length + 1) ^ 3 := BigOLe.pow_le (by simp only [length_encPair]; bigO) @@ -508,11 +508,11 @@ lemma stepG_inO (hg : g.ResourceCertificate encG Tg Sg) : (BigOLe.of_le fun p => Nat.pow_le_pow_left (by omega) 3).trans hT have hAt := hA.trans hL have hAs := hA.trans hLs - have hlin : (fun p : CompState σf σg × Option Bool => (encPair encNat (encPair encNat encMove) + have hlin : (fun p : CompState σf σg × Option Bool => (encPair encNat (encPair encNat encSign) (p.1.cd.len, p.1.g.2, (g.step p.1.g.1 (p.1.cd.symbol p.1.g.2)).2.1)).length) ≼ fun p => compSpace encF encG Sf Sg p.1 := BigOLe.trans (by simp only [length_encPair]; bigO) hLs - refine (hst.prod ((const (0 : SignType) (encMid := encMove)).prod hr.snd'.snd')).weaken ?_ ?_ <;> + refine (hst.prod ((const (0 : SignType) (encMid := encSign)).prod hr.snd'.snd')).weaken ?_ ?_ <;> · bigO lemma le_compTime (s : CompState σf σg) : @@ -557,7 +557,7 @@ lemma rewind_inO : ComputableInO (fun p : CompState σf σg × Option Bool => (⟨p.1.g, p.1.phase, p.1.f, p.1.cd⟩ : CompState σf σg)) fun p => rfl have hres {st : CompState σf σg × Option Bool → CompState σf σg} {T S} (h : ComputableInO st encArg (encCompState encF encG) T S) (d : SignType) := - h.prod ((const d (encMid := encMove)).prod (const ([] : List Bool) (encMid := encBits))) + h.prod ((const d (encMid := encSign)).prod (const ([] : List Bool) (encMid := encBits))) have hAt := (encArg_bigO (encF := encF) (encG := encG)).trans (time_bigO (Tf := Tf) (Sf := Sf) (Tg := Tg)).2.1 have hAs := (encArg_bigO (encF := encF) (encG := encG)).trans (space_bigO (Sf := Sf) (Sg := Sg)).1 diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/StepMachineCompiler.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/StepMachineCompiler.lean index 9f01d6ad2..8a7fde3ac 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/StepMachineCompiler.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/StepMachineCompiler.lean @@ -15,6 +15,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Ste public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCombinators 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.Bool public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OnWords public import Complexity.Computability.Machines.Turing.MultiTape.StepMachine.Basic public import Cslib.Computability.Machines.Turing.MultiTape.Combinators.AlmostConstant @@ -34,7 +35,7 @@ an unbounded output with constant workspace; no bound on the whole output is add ## Main definitions -* `Turing.MultiTapeTM.encMove`, `.encPeek`: the unchanged encodings used by the compiler. +* `Turing.MultiTapeTM.encPeek`: the unchanged encoding used by the compiler. * `Turing.StepMachine.ResourceCertificate`: charged plain certificates for halt and step. ## Main results @@ -55,13 +56,7 @@ public lemma linear_stepFlagWord : ComputableInLinearTimeAndSpace stepFlagWord encBool encBits := .of_finite stepFlagWord -/-- Moves of the input head: none, to the left, to the right. -/ -@[expose] public def encMove : SignType ↪ List Bool := - ⟨fun m => match m with | .zero => [] | .neg => [false] | .pos => [true], by - intro a b h - cases a <;> cases b <;> simp_all⟩ - -@[simp] public lemma moveOfCell_encMove (m : SignType) : moveOfCell (encMove m).head? = m := by +@[simp] public lemma moveOfCell_encSign (m : SignType) : moveOfCell (encSign m).head? = m := by cases m <;> rfl public lemma peekWord_injective : Function.Injective peekWord := by @@ -164,14 +159,14 @@ variable {σ : Type} {encS : σ ↪ List Bool} {halt : σ → Bool} {TS SS : σ × Option Bool → ℕ} /-- The state and its pending move. -/ -public abbrev encAug (encS : σ ↪ List Bool) : σ × SignType ↪ List Bool := encPair encS encMove +public abbrev encAug (encS : σ ↪ List Bool) : σ × SignType ↪ List Bool := encPair encS encSign /-- The step, read from the state behind the symbol under the input head. -/ lemma step_peek_inO (hstep : ComputableInO (fun p : σ × Option Bool => step p.1 p.2) - (encPair encS (encOption encBool)) (encPair encS (encPair encMove encBits)) TS SS) : + (encPair encS (encOption encBool)) (encPair encS (encPair encSign encBits)) TS SS) : ComputableInO (fun p : Option Bool × (σ × SignType) => step p.2.1 p.1) - (encPeek (encAug encS)) (encPair encS (encPair encMove encBits)) + (encPeek (encAug encS)) (encPair encS (encPair encSign encBits)) (fun p => (encPeek (encAug encS) p).length + (encPeek (encAug encS) p).length + TS (p.2.1, p.1)) fun p => (encPeek (encAug encS) p).length + (encPeek (encAug encS) p).length + @@ -247,7 +242,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis (hinit : ComputableInO init encIn encS TI SI) (hhalt : ComputableInO halt encS encBool TH SH) (hstep : ComputableInO (fun p : σ × Option Bool => step p.1 p.2) - (encPair encS (encOption encBool)) (encPair encS (encPair encMove encBits)) TS SS) + (encPair encS (encOption encBool)) (encPair encS (encPair encSign encBits)) TS SS) (hrounds : ∀ x, (StepMachine.mk (init x) halt step).HaltsAt (encIn x) (rounds x)) (hg : ∀ x, encOut (g x) = ((StepMachine.mk (init x) halt step).run (encIn x) (rounds x)).out) @@ -337,16 +332,16 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis have hP (b : Option Bool) (n : ℕ) (hn : n ≤ R) (mm : SignType) : (encPeek (encAug encS) (b, (q n, mm))).length ≤ 2 * L + 4 := by have : (encS (q n)).length ≤ L := hlMax x n hn - cases b <;> cases mm <;> simp [peekWord, encMove] <;> omega + cases b <;> cases mm <;> simp [peekWord, encSign] <;> omega have hst (n : ℕ) (hn : n ≤ R) : TS (q n, a n) + TH (q n) ≤ Tm ∧ SS (q n, a n) + SH (q n) ≤ Sm := ⟨htMax x n hn, hsMax x n hn⟩ have hfl (n : ℕ) : (stepFlagWord (!halt (q n))).length ≤ 1 := by unfold stepFlagWord; split_ifs <;> simp - have hmv (mm : SignType) : (encMove mm).length ≤ 1 := by cases mm <;> simp [encMove] + have hmv (mm : SignType) : (encSign mm).length ≤ 1 := by cases mm <;> simp [encSign] have h := computesTidily_stepTM hVN hVF hNF hVC hVM w R (fun n => encAug encS (q n, mv n)) - (fun n => (st n).2.2) (fun n => encMove (st n).2.1) (fun n => stepFlagWord (!halt (q n))) + (fun n => (st n).2.2) (fun n => encSign (st n).2.1) (fun n => stepFlagWord (!halt (q n))) (fun n => (m.run w n).pos) rfl - (fun n hn => by simp only [hrun n hn, moveOfCell_encMove]) + (fun n hn => by simp only [hrun n hn, moveOfCell_encSign]) (fun n hn => by simp [hnh n hn, stepFlagWord]) (by simpa [stepFlagWord] using (hrounds x).1) ((hI x).imp (fun _ _ h => h) (fun _ _ _ _ _ ⟨h, he⟩ => ⟨h.trans rfl, he⟩) le_rfl le_rfl) @@ -371,7 +366,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis (fun n hn => (hN (a n, (q n, mv n))).imp (fun _ _ h => h) (fun _ _ _ _ _ ⟨h, he⟩ => ⟨by rw [h]; simp [hq n hn, mv, st, peekWord, slot], he⟩) (by have := hP (a n) n hn.le (mv n); have := (hst n hn.le).1 - have : (encPeek (encPair encS encMove) (none, (step (q n) (a n)).1, + have : (encPeek (encPair encS encSign) (none, (step (q n) (a n)).1, (step (q n) (a n)).2.1)).length ≤ 2 * L + 4 := by have := hP none (n + 1) hn (step (q n) (a n)).2.1 rw [hq n hn] at this @@ -384,7 +379,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis 2 * Tm + 8 * L + 20 by omega) dsimp -zeta only; simp only [Function.comp_apply]; omega) (by have := hP (a n) n hn.le (mv n); have := (hst n hn.le).2 - have : (encPeek (encPair encS encMove) (none, (step (q n) (a n)).1, + have : (encPeek (encPair encS encSign) (none, (step (q n) (a n)).1, (step (q n) (a n)).2.1)).length ≤ 2 * L + 4 := by have := hP none (n + 1) hn (step (q n) (a n)).2.1 rw [hq n hn] at this @@ -437,7 +432,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis -- the bounds have hround (n : ℕ) (hn : n < R) : stepRoundTime (stepFlagWord (!halt (q n))).length (peekWord (a n) ++ encAug encS (q n, mv n)).length - (slot ++ encAug encS (q (n + 1), mv (n + 1))).length (encMove (st n).2.1).length + (slot ++ encAug encS (q (n + 1), mv (n + 1))).length (encSign (st n).2.1).length (D * (Tm + 4 * L + 10) + 4) (D * (2 * Tm + 8 * L + 20) + 2 * L + 10) (D * (2 * L + 5) + 7) (D * (Tm + 2 * L + 5) + 7) + 1 ≤ 100 * (D * (Tm + L + 1)) := by have h₁ := hP (a n) n hn.le (mv n) @@ -457,7 +452,7 @@ private theorem Internal.compileStepMachine {σ γ ω : Type} {encS : σ ↪ Lis omega have hS : ∑ n ∈ Finset.range R, (stepRoundTime (stepFlagWord (!halt (q n))).length (peekWord (a n) ++ encAug encS (q n, mv n)).length - (slot ++ encAug encS (q (n + 1), mv (n + 1))).length (encMove (st n).2.1).length + (slot ++ encAug encS (q (n + 1), mv (n + 1))).length (encSign (st n).2.1).length (D * (Tm + 4 * L + 10) + 4) (D * (2 * Tm + 8 * L + 20) + 2 * L + 10) (D * (2 * L + 5) + 7) (D * (Tm + 2 * L + 5) + 7) + 1) ≤ R * (100 * (D * (Tm + L + 1))) := (Finset.sum_le_sum fun n hn => hround n (Finset.mem_range.mp hn)).trans (by simp) @@ -495,7 +490,7 @@ public structure ResourceCertificate {σ : Type} (m : StepMachine σ Bool Bool) (T S : σ → ℕ) : Prop where computable_halt : ComputableInO m.halt encS encBool T S computable_step : ComputableInO (fun p : σ × Option Bool => m.step p.1 p.2) - (encPair encS (encOption encBool)) (encPair encS (encPair encMove encBits)) + (encPair encS (encOption encBool)) (encPair encS (encPair encSign encBits)) (fun p => T p.1) fun p => S p.1 /-- The step machine `m` started in the state `s`. -/ @@ -535,7 +530,7 @@ public theorem ResourceCertificate.computableInBigO_of_init {σ γ ω : Type} {e rw [(m.withInit (init x)).run_succ_of_not_halt hh] have h₁ := hcS (((m.withInit (init x)).run (encIn x) i).state, inputSymbolAt (encIn x) ((m.withInit (init x)).run (encIn x) i).pos) - have h₂ := length_le_encPair_left encS (encPair encMove encBits) + have h₂ := length_le_encPair_left encS (encPair encSign encBits) (m.step ((m.withInit (init x)).run (encIn x) i).state (inputSymbolAt (encIn x) ((m.withInit (init x)).run (encIn x) i).pos)) have h₃ := Nat.mul_le_mul_left cS (Nat.add_le_add_right (hmax x i (by omega)).2 1) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean index 0f5ac5e9a..0d96f3221 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean @@ -11,6 +11,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO public import Complexity.Computability.Machines.Turing.MultiTape.Internal.OCountedIteration public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.IterateWhile public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Basic +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool import Complexity.Computability.Machines.Turing.MultiTape.Universal.Input import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative import Mathlib.Tactic.Linarith @@ -52,12 +53,6 @@ namespace Turing.MultiTapeTM.Universal /-! ### Encodings -/ -/-- Moves, by their sign. -/ -@[expose] public def encSign : SignType ↪ List Bool := - ⟨fun m => match m with | .zero => [] | .neg => [false] | .pos => [true], by - intro a b h - cases a <;> cases b <;> simp_all⟩ - /-- Symbols and blanks. -/ public abbrev eSym : Option ℕ ↪ List Bool := encOption encUnary @@ -69,12 +64,6 @@ public abbrev eSym : Option ℕ ↪ List Bool := encOption encUnary /-- An action on a work tape. -/ public abbrev TapeAct := Option (Option ℕ) × SignType -/-- The unit type, encoded by the empty word. -/ -@[expose] public def encUnit : Unit ↪ List Bool := ⟨fun _ => [], fun _ _ _ => rfl⟩ - -@[simp] -public lemma encUnit_apply (u : Unit) : encUnit u = [] := rfl - /-- Actions on a work tape. -/ public abbrev eTA : Option (Option ℕ) × SignType ↪ List Bool := encPair (encOption eSym) encSign @@ -250,12 +239,6 @@ lemma length_encList_eq_le (l : List (Option ℕ)) : (encList eSym l).length := by cases l <;> simp -lemma length_encInt_add_one (z : ℤ) : (encInt (z + 1)).length ≤ (encInt z).length + 1 := by - rw [length_encInt, length_encInt]; split_ifs <;> omega - -lemma length_encInt_sub_one (z : ℤ) : (encInt (z - 1)).length ≤ (encInt z).length + 1 := by - rw [length_encInt, length_encInt]; split_ifs <;> omega - /-- Applying an action at most doubles a work tape, up to the length of the action. -/ lemma length_eTape_apply (t : Tape) (a : Option (Option ℕ) × SignType) : (eTape (t.apply a)).length ≤ 2 * (eTape t).length + 2 * (eTA a).length + 8 := by @@ -263,8 +246,8 @@ lemma length_eTape_apply (t : Tape) (a : Option (Option ℕ) × SignType) : obtain ⟨w, m⟩ := a have := length_encList_eq_le l have := length_encList_eq_le r - have := length_encInt_add_one h - have := length_encInt_sub_one h + have := length_encInt_add_one_le h + have := length_encInt_sub_one_le h rcases w with _ | o <;> rcases m with _ | _ | _ <;> simp only [Tape.apply, Tape.move, Tape.write, Tape.read, Option.elim, eTape_apply, length_encPair, encList_cons, List.length_append, length_frame, encOption_some, @@ -296,6 +279,16 @@ lemma length_read_le (t : Tape) : (eSym t.read).length ≤ (eTape t).length := b simp only [Tape.read, eTape_apply, length_encPair] at * omega +/-- The symbols under the heads are no longer than the work tapes. -/ +lemma length_encList_map_read_le (ts : List Tape) : + (encList eSym (ts.map Tape.read)).length ≤ (encList eTape ts).length := by + induction ts with + | nil => simp + | cons t ts ih => + have := length_read_le t + simp only [List.map_cons, encList_cons, List.length_append, length_frame] at * + omega + /-! ### All work tapes -/ open ComputableTidilyInO @@ -350,19 +343,11 @@ public theorem reads_inO : ComputableTidilyInO (fun ts : List Tape => ts.map Tape.read) (encList eTape) (encList eSym) (fun ts => (ts.length + 1) * ((encList eTape ts).length + 1)) fun ts => (encList eTape ts).length := by - have hmap (ts : List Tape) : (encList eSym (ts.map fun t => t.read)).length ≤ - (encList eTape ts).length := by - induction ts with - | nil => simp - | cons t ts ih => - have := length_read_le t - simp only [List.map_cons, encList_cons, List.length_append, length_frame] at * - omega refine ((mapWith (encP := encUnit) (f := fun p : Unit × Tape => p.2.read) (read_deg.inO_one.comp_linear (snd encUnit eTape)) (const ()) (of_linear (.of_eq fun _ => rfl))).mono 8 (fun ts => ?_) fun ts => ?_) all_goals - have h₁ := hmap ts + have h₁ : (encList eSym (ts.map fun t => t.read)).length ≤ _ := length_encList_map_read_le ts have h₂ : listMax (fun t => (encPair encUnit eTape ((), t)).length) ts ≤ (encList eTape ts).length + 1 := listMax_le fun t ht => by @@ -464,29 +449,26 @@ lemma length_wTable_le : (encList (encPair eKey eAct) c.1.1.table).length ≤ (eWCtx c).length := by rw [length_eWCtx]; simp only [eDesc_apply, length_encPair]; omega -lemma length_le_wTime {A B : ℕ} - (hA : A ≤ c.1.2.workTapes.length + c.1.1.table.length) - (hB : B ≤ (eWCtx c).length) : - (A + 1) * ((eDesc c.1.1).length + 1) * (B + 1) ≤ wTime c := - (Nat.mul_le_mul (Nat.mul_le_mul_right _ (by omega)) (by omega)).trans - (Nat.le_add_right _ _) - -lemma length_le_wTime' {A B : ℕ} +lemma length_le_wTime {A B k : ℕ} (hA : A ≤ c.1.2.workTapes.length + c.1.1.table.length) - (hB : B ≤ (eWCtx c).length) : (A + 1) * (B + 1) ≤ wTime c := - (Nat.mul_le_mul_right (B + 1) - (Nat.le_mul_of_pos_right (A + 1) (Nat.succ_pos _))).trans - (length_le_wTime c hA hB) + (hB : B ≤ (eWCtx c).length) (hk : k ≤ (eDesc c.1.1).length + 1) : + (A + 1) * k * (B + 1) ≤ wTime c := + (Nat.mul_le_mul (Nat.mul_le_mul (by omega) hk) (by omega)).trans (Nat.le_add_right _ _) + +/-- An entry of the table is no longer than the context. -/ +lemma length_le_of_mem_table {e : Key × Act} (he : e ∈ c.1.1.table) : + (encPair eKey eAct e).length ≤ (eWCtx c).length := + (length_le_encList_of_mem (encPair eKey eAct) he).trans (length_wTable_le c) + +/-- An entry of the table is no longer than the description. -/ +lemma length_le_eDesc_of_mem_table {e : Key × Act} (he : e ∈ c.1.1.table) : + (encPair eKey eAct e).length ≤ (eDesc c.1.1).length := by + have := length_le_encList_of_mem (encPair eKey eAct) he + simp only [eDesc_apply, length_encPair] at * + omega lemma length_wKey_le : (eKey (wKey c)).length ≤ 4 * (eWCtx c).length + 4 := by - have h₂ : (encList eSym (c.1.2.workTapes.map Tape.read)).length ≤ - (encList eTape c.1.2.workTapes).length := by - induction c.1.2.workTapes with - | nil => simp - | cons t ts ih => - have := length_read_le t - simp only [List.map_cons, encList_cons, List.length_append, length_frame] at * - omega + have h₂ := length_encList_map_read_le c.1.2.workTapes have h₃ : (c.1.2.state.getD 0) ≤ (eSym c.1.2.state).length := by cases c.1.2.state <;> simp rw [length_eWCtx] simp only [wKey, eKey_apply, length_encPair, encUnary_apply, List.length_replicate] @@ -513,7 +495,7 @@ abbrev WPart {β : Type} (f : WCtx → β) (enc : β ↪ List Bool) : Prop := ComputableTidilyInO f eWCtx enc wTime fun c => (eWCtx c).length lemma le_wTime (c : WCtx) : (eWCtx c).length + 1 ≤ wTime c := - by simpa using length_le_wTime' c (A := 0) (Nat.zero_le _) le_rfl + by simpa using length_le_wTime c (A := 0) (Nat.zero_le _) le_rfl (k := 1) (by omega) /-- One step of the simulation without the input, within the time `wTime` and linear space. -/ public theorem stepWith_inO : @@ -533,9 +515,9 @@ public theorem stepWith_inO : all_goals have h₁ := length_eWCtx c have h₂ := le_wTime c - have h₃ := length_le_wTime' c (A := c.1.2.workTapes.length) (by omega) - (B := (encList eTape c.1.2.workTapes).length) (by omega) - dsimp only [eWCtx, Function.comp_apply] at * + have h₃ := length_le_wTime c (A := c.1.2.workTapes.length) (by omega) + (B := (encList eTape c.1.2.workTapes).length) (by omega) (k := 1) (by omega) + simp only [eWCtx, Nat.mul_one] at * omega have hsym : WPart (fun c => c.2) eSym := (snd (encPair eDesc eCfg) eSym).mono 1 (fun c => by @@ -557,14 +539,6 @@ public theorem stepWith_inO : have hk := length_wKey_le c have ht := length_wTable_le c have hst := le_wTime c - have hentry (e : Key × Act) (he : e ∈ c.1.1.table) : - (encPair eKey eAct e).length ≤ (eWCtx c).length := - (length_le_encList_of_mem (encPair eKey eAct) he).trans ht - have hentryD (e : Key × Act) (he : e ∈ c.1.1.table) : - (encPair eKey eAct e).length ≤ (eDesc c.1.1).length := by - have := length_le_encList_of_mem (encPair eKey eAct) he - simp only [eDesc_apply, length_encPair] at * - omega have hlinear : (eWCtx c).length + 1 ≤ ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) := by nlinarith have hlen := length_le_length_encList (encPair eKey eAct) c.1.1.table @@ -574,16 +548,16 @@ public theorem stepWith_inO : ((eKey (e.1, wKey c).1).length + (eKey (e.1, wKey c).2).length + 1)) c.1.1.table ≤ 32 * ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) := listMax_le fun e he => by - have h₁ := hentry e he + have h₁ := length_le_of_mem_table c he have h₂ := length_le_encPair_left eKey eAct e - have hD := hentryD e he + have hD := length_le_eDesc_of_mem_table c he have h₃ : ((eKey e.1).length + 1) * ((eKey e.1).length + (eKey (wKey c)).length + 1) ≤ ((eDesc c.1.1).length + 1) * (5 * ((eWCtx c).length + 1)) := Nat.mul_le_mul (by omega) (by omega) simp only [length_encPair] at * nlinarith have h₂ := length_le_wTime c (A := c.1.1.table.length) (by omega) - (B := (eWCtx c).length) le_rfl + (B := (eWCtx c).length) le_rfl le_rfl have h₃ := Nat.mul_le_mul_left (c.1.1.table.length + 1) (Nat.add_le_add (Nat.add_le_add (hk.trans (show 4 * (eWCtx c).length + 4 ≤ 4 * ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) by nlinarith)) @@ -597,7 +571,7 @@ public theorem stepWith_inO : (encPair eKey eKey (e.1, wKey c)).length) c.1.1.table ≤ 32 * ((eWCtx c).length + 1) := listMax_le fun e he => by - have h₁ := hentry e he + have h₁ := length_le_of_mem_table c he have h₂ := length_le_encPair_left eKey eAct e simp only [length_encPair] at * omega @@ -643,8 +617,9 @@ public theorem stepWith_inO : have := length_eWCtx c simp only [eAct_apply, length_encPair] at * omega - have h₂ := length_le_wTime' c (A := c.1.2.workTapes.length) (by omega) - (B := (eWCtx c).length) le_rfl + have h₂ := length_le_wTime c (A := c.1.2.workTapes.length) (by omega) + (B := (eWCtx c).length) le_rfl (k := 1) (by omega) + rw [Nat.mul_one] at h₂ · have h₁ := Nat.mul_le_mul_left (c.1.2.workTapes.length + 1) (Nat.add_le_add_right hp 1) dsimp only [eWCtx, Function.comp_apply] at * nlinarith diff --git a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean index a09c43261..100ae21c7 100644 --- a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean +++ b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean @@ -12,7 +12,7 @@ public import Complexity.Computability.Complexity.FineGrained.CountingSparsifica public import Complexity.Computability.Complexity.FineGrained.GeneralCNFBranchSchedule public import Complexity.Computability.Complexity.FineGrained.SparseBranchAsymptotics public import Complexity.Computability.Complexity.FineGrained.SparseCountingScale -public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Complexity +public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool public import Complexity.Computability.PolyTime.BooleanAnalysis.SparsePolyCounter public import Complexity.Computability.PolyTime.CNF.SparseCNFLeafCounter public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParametersPolyTime @@ -79,7 +79,6 @@ open Cslib.Complexity.SubexponentialSAT Cslib.Complexity.SubexponentialSAT.Spars open Cslib.GenericRAM Cslib.GenericRAM.ExhaustiveCountFallback open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.ClauseSet.Sparsification open Turing.MultiTapeTM -open Turing.MultiTapeTM.Universal (encUnit) local notation "encSys" => encList (encList (encList encNat)) local notation "encLeafCtx" => encPair encUnit encUnary diff --git a/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean b/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean index ff29b2797..6701ea171 100644 --- a/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean +++ b/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean @@ -59,11 +59,11 @@ example : ∃ N₀_leaf N₀_top C_t d_t A_t : ℕ, 1 ≤ A_t ∧ ∀ x : (Unit × ℕ) × Logic.PL.CNF ℕ, x.2.length ≤ leafOccBound 3 x.1.2 * x.1.2 + 1 → ((branchedSparseCNFDeclaredCertificate 3 N₀_leaf N₀_top 16384 boundedIncidenceBranchCertificate branchBound16384).time x : ℝ) ≤ - (C_t : ℝ) * ((encPair (encPair Universal.encUnit encUnary) encCNF x).length + 1 : ℝ) ^ + (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t * (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) ∧ ((branchedSparseCNFLeafCertificate 3 N₀_leaf N₀_top 16384 boundedIncidenceBranchCertificate branchBound16384).time x : ℝ) ≤ - (C_t : ℝ) * ((encPair (encPair Universal.encUnit encUnary) encCNF x).length + 1 : ℝ) ^ + (C_t : ℝ) * ((encPair (encPair encUnit encUnary) encCNF x).length + 1 : ℝ) ^ d_t * (2 : ℝ) ^ ((A_t : ℝ) * interpolationScale x.1.2) := exists_branchedSparseCNF_time_bound 3 16384 boundedIncidenceBranchCertificate branchBound16384 polyBounded_boundedIncidenceBranchCertificate_space diff --git a/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean index c8e3427fc..8185a562c 100644 --- a/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean +++ b/ComplexityTests/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean @@ -20,7 +20,6 @@ open Cslib.Complexity Cslib.Complexity.BranchedSparseCNFCounter Cslib.GenericRAM open Cslib.Complexity.SparseCNFLeafCounter Cslib.Complexity.SubexponentialSAT open Cslib.Complexity.SubexponentialSAT.SparsePolyCounter Cslib.GenericRAM.ExhaustiveCountFallback open Cslib.Logic.PL Cslib.Logic.PL.CNF Cslib.Logic.PL.ClauseSet.Sparsification Turing.MultiTapeTM -open Turing.MultiTapeTM.Universal (encUnit) local notation "encLeafIn" => encPair (encPair encUnit encUnary) encCNF diff --git a/ComplexityTests/FiniteCSP.lean b/ComplexityTests/FiniteCSP.lean index 30c200f5f..d7429b577 100644 --- a/ComplexityTests/FiniteCSP.lean +++ b/ComplexityTests/FiniteCSP.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger import Complexity.Logics.Propositional.CSP.ToBoolean import Complexity.Computability.Complexity.FineGrained.CountingFiniteCSP +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool /-! # Finite-domain CSP unit tests @@ -101,10 +102,6 @@ example : example : (triangleCSP.toBoolean 3 3).numVars ≤ 3 * CSP.bitWidth 3 := CSP.numVars_toBoolean_le (by decide) -/-- Trivial encoding for the singleton relation alphabet `Unit`. -/ -def encUnit : Unit ↪ List Bool := - ⟨fun _ => [], fun _ _ _ => rfl⟩ - -- Polynomial-time compilation and compiled encoding length bound example : ComputableInPolyTime (fun x : ℕ × CSP Unit ℕ => x.2.toBoolean 3 x.1) diff --git a/ComplexityTests/Space/Savitch.lean b/ComplexityTests/Space/Savitch.lean index 06c37d8d8..0a9571d59 100644 --- a/ComplexityTests/Space/Savitch.lean +++ b/ComplexityTests/Space/Savitch.lean @@ -6,7 +6,7 @@ Authors: Bolton Bailey, Samuel Schlesinger import Complexity.Algorithms.Reachability.Savitch import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Space.Reachability -import Complexity.Computability.Machines.Turing.MultiTape.Universal.Complexity +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Bool import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives /-! @@ -22,7 +22,6 @@ polynomial-space form for a family of depths, so that their hypotheses are satis namespace ComplexityTests.Savitch open Cslib Cslib.Reachability Turing.MultiTapeTM -open Turing.MultiTapeTM.Universal (encUnit) /-! ### The binary counter -/ From da5055c4d9ee93803fbaec10d9c5f933e43bed03 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 17:14:37 +0000 Subject: [PATCH 2/3] feat(BigO): plain findWith, filterWith and mapWith Move the private plain findWith/filterWith of SparseMemory/Turing to a public module Complexity/BigO/Lists and add the plain mapWith, so that clients of the tidy list combinators can migrate to the plain calculus. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../GenericRAM/SparseMemory/Turing.lean | 126 +--------- .../MultiTape/Complexity/BigO/Lists.lean | 235 ++++++++++++++++++ 3 files changed, 237 insertions(+), 125 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Lists.lean diff --git a/Complexity.lean b/Complexity.lean index 9735d61c9..2f82825eb 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1503,6 +1503,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Arit public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Bounds public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.NatPolynomial public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Option public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Pi diff --git a/Complexity/Computability/GenericRAM/SparseMemory/Turing.lean b/Complexity/Computability/GenericRAM/SparseMemory/Turing.lean index d7c2868d9..6e35dc891 100644 --- a/Complexity/Computability/GenericRAM/SparseMemory/Turing.lean +++ b/Complexity/Computability/GenericRAM/SparseMemory/Turing.lean @@ -10,7 +10,7 @@ module 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.Internal.OLoops +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists /-! # Native Turing-machine certificates for sparse memory @@ -208,130 +208,6 @@ theorem scanSpace_le_linear (q : Address × SparseMemory Address Value) : variable [DecidableEq Address] -open ComputableTidilyInDegree - (findStep foldl_findStep filterStep foldl_filterStep length_encList_filter_le) - -private theorem findWith {γ α π : Type} {encIn : γ ↪ List Bool} {enc : α ↪ List Bool} - {encP : π ↪ List Bool} {par : γ → π} {list : γ → List α} {Tp Tl Sp Sl : γ → ℕ} - {t : π × α → Bool} {Tt St : π × α → ℕ} - (ht : ComputableInO t (encPair encP enc) encBool Tt St) - (hpar : ComputableInO par encIn encP Tp Sp) - (hlist : ComputableInO list encIn (encList enc) Tl Sl) : - ComputableInO (fun x => (list x).find? fun a => t (par x, a)) encIn (encOption enc) - (fun x => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * - ((encP (par x)).length + (encList enc (list x)).length + - listMax (fun a => Tt (par x, a)) (list x))) - fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length + - (encList enc (list x)).length + listMax (fun a => St (par x, a)) (list x) := by - have hq := fst (encPair encP (encOption enc)) enc - have hel := snd (encPair encP (encOption enc)) enc - have hisSome := (ComputableInDegree.isSome enc).inO_one.comp_linear hq.snd' - have h := hisSome.ite hq.snd' ((ht.comp (hq.fst'.prod hel)).ite - ((ComputableInDegree.optionSome (enc₁ := enc)).inO_one.comp_linear hel) (const none)) - have hstep : ComputableInO (fun q : (π × Option α) × α => findStep t q.1.1 q.1.2 q.2) - (encPair (encPair encP (encOption enc)) enc) (encOption enc) - (fun q => (encPair (encPair encP (encOption enc)) enc q).length + Tt (q.1.1, q.2)) - fun q => (encPair (encPair encP (encOption enc)) enc q).length + St (q.1.1, q.2) := by - refine (h.mono 4 (fun q => ?_) fun q => ?_).of_enc_eq fun ⟨⟨p, acc⟩, a⟩ => ?_ - · split_ifs <;> omega - · split_ifs <;> omega - · cases acc <;> simp [findStep] - have hst (x : γ) (i : ℕ) : - (encOption enc (((list x).take i).foldl (findStep t (par x)) none)).length ≤ - (encList enc (list x)).length + 1 := by - rw [foldl_findStep, Option.none_or] - exact (length_encOption_find?_le enc _ _).trans - (Nat.add_le_add_right (length_encList_take_le enc _ _) 1) - have hfold := foldlWith (encL := encList enc) (encB := encOption enc) hpar hlist - (const none) hstep (R := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + 5 + listMax (fun a => Tt (par x, a)) (list x)) - (Q := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + 5 + listMax (fun a => St (par x, a)) (list x)) - (B := fun x => (encList enc (list x)).length + 1) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => Tt (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => St (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i _ => by have := hst x i; omega) - refine (hfold.mono 16 (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ - · have h₁ := length_le_length_encList enc (list x) - have h₂ : (list x).length ≤ (list x).length * (encList enc (list x)).length := by - rcases Nat.eq_zero_or_pos (list x).length with h | h - · simp [h] - · exact Nat.le_mul_of_pos_right _ (by omega) - ring_nf - omega - · omega - · rw [foldl_findStep, Option.none_or] - -private theorem filterWith {γ α π : Type} {encIn : γ ↪ List Bool} {enc : α ↪ List Bool} - {encP : π ↪ List Bool} {par : γ → π} {list : γ → List α} {Tp Tl Sp Sl : γ → ℕ} - {t : π × α → Bool} {Tt St : π × α → ℕ} - (ht : ComputableInO t (encPair encP enc) encBool Tt St) - (hpar : ComputableInO par encIn encP Tp Sp) - (hlist : ComputableInO list encIn (encList enc) Tl Sl) : - ComputableInO (fun x => (list x).filter fun a => t (par x, a)) encIn (encList enc) - (fun x => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * - ((encP (par x)).length + (encList enc (list x)).length + - listMax (fun a => Tt (par x, a)) (list x))) - fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length + - (encList enc (list x)).length + listMax (fun a => St (par x, a)) (list x) := by - have hq := fst (encPair encP (encList enc)) enc - have hel := snd (encPair encP (encList enc)) enc - have h := (ht.comp (hq.fst'.prod hel)).ite - ((ComputableInDegree.snoc enc).inO_one.comp_linear (hq.snd'.prod hel)) hq.snd' - have hstep : ComputableInO - (fun q : (π × List α) × α => filterStep t q.1.1 q.1.2 q.2) - (encPair (encPair encP (encList enc)) enc) (encList enc) - (fun q => (encPair (encPair encP (encList enc)) enc q).length + Tt (q.1.1, q.2)) - fun q => (encPair (encPair encP (encList enc)) enc q).length + St (q.1.1, q.2) := by - refine (h.mono 4 (fun q => ?_) fun q => ?_).of_enc_eq fun ⟨⟨p, acc⟩, a⟩ => ?_ - · split_ifs <;> omega - · split_ifs <;> omega - · simp [filterStep] - have hst (x : γ) (i : ℕ) : - (encList enc (((list x).take i).foldl (filterStep t (par x)) [])).length ≤ - (encList enc (list x)).length := by - rw [foldl_filterStep, List.nil_append] - exact (length_encList_filter_le enc _ _).trans (length_encList_take_le enc _ _) - have hfold := foldlWith (encL := encList enc) (encB := encList enc) hpar hlist - (const []) hstep (R := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + 5 + listMax (fun a => Tt (par x, a)) (list x)) - (Q := fun x => 4 * (encP (par x)).length + - 3 * (encList enc (list x)).length + 5 + listMax (fun a => St (par x, a)) (list x)) - (B := fun x => (encList enc (list x)).length + 1) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => Tt (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i hi => by - have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) - have h₂ := le_listMax (f := fun a => St (par x, a)) (List.getElem_mem hi) - have h₃ := hst x i - simp only [length_encPair] at h₂ ⊢ - omega) - (fun x i _ => by have := hst x i; omega) - refine (hfold.mono 16 (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ - · have h₁ := length_le_length_encList enc (list x) - have h₂ : (list x).length ≤ (list x).length * (encList enc (list x)).length := by - rcases Nat.eq_zero_or_pos (list x).length with h | h - · simp [h] - · exact Nat.le_mul_of_pos_right _ (by omega) - ring_nf - omega - · omega - · rw [foldl_filterStep, List.nil_append] - private theorem compare_inO : ComputableInO (fun q : Address × (Address × Value) => decide (q.1 = q.2.1)) (encPair encA (encPair encA encV)) encBool (compareTime encA encV) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Lists.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Lists.lean new file mode 100644 index 000000000..e06cf3bb9 --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Lists.lean @@ -0,0 +1,235 @@ +/- +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.Complexity.Quantitative +import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# Finding, filtering and mapping with parameters + +Plain counterparts of `Turing.MultiTapeTM.ComputableTidilyInO.findWith`, `.filterWith` and +`.mapWith`: one left fold over `list x` whose step applies a test or function to the parameter +`par x` and the current element. The time bound charges each round for the parameter, the list, +the accumulator and the largest cost of the test or function on an element. + +## Main results + +* `Turing.MultiTapeTM.ComputableInO.findWith`: the first element passing a test. +* `Turing.MultiTapeTM.ComputableInO.filterWith`: the elements passing a test. +* `Turing.MultiTapeTM.ComputableInO.mapWith`: the images of the elements. + +## References + +Restates Christian Reitwiessner's tidy list combinators +(`Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean`) in the plain calculus. +-/ + +public section + +namespace Turing.MultiTapeTM.ComputableInO + +open ComputableTidilyInDegree (findStep foldl_findStep filterStep foldl_filterStep mapStep + foldl_mapStep length_encList_filter_le) + +variable {γ α β π : Type} {encIn : γ ↪ List Bool} {enc : α ↪ List Bool} {encB : β ↪ List Bool} + {encP : π ↪ List Bool} {par : γ → π} {list : γ → List α} {Tp Tl Sp Sl : γ → ℕ} + + +/-- The first element of `list x` passing the test `t` with the parameter `par x`. -/ +theorem findWith {t : π × α → Bool} {Tt St : π × α → ℕ} + (ht : ComputableInO t (encPair encP enc) encBool Tt St) + (hpar : ComputableInO par encIn encP Tp Sp) + (hlist : ComputableInO list encIn (encList enc) Tl Sl) : + ComputableInO (fun x => (list x).find? fun a => t (par x, a)) encIn (encOption enc) + (fun x => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * + ((encP (par x)).length + (encList enc (list x)).length + + listMax (fun a => Tt (par x, a)) (list x))) + fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length + + (encList enc (list x)).length + listMax (fun a => St (par x, a)) (list x) := by + have hq := fst (encPair encP (encOption enc)) enc + have hel := snd (encPair encP (encOption enc)) enc + have hisSome := (ComputableInDegree.isSome enc).inO_one.comp_linear hq.snd' + have h := hisSome.ite hq.snd' ((ht.comp (hq.fst'.prod hel)).ite + ((ComputableInDegree.optionSome (enc₁ := enc)).inO_one.comp_linear hel) (const none)) + have hstep : ComputableInO (fun q : (π × Option α) × α => findStep t q.1.1 q.1.2 q.2) + (encPair (encPair encP (encOption enc)) enc) (encOption enc) + (fun q => (encPair (encPair encP (encOption enc)) enc q).length + Tt (q.1.1, q.2)) + fun q => (encPair (encPair encP (encOption enc)) enc q).length + St (q.1.1, q.2) := by + refine (h.mono 4 (fun q => ?_) fun q => ?_).of_enc_eq fun ⟨⟨p, acc⟩, a⟩ => ?_ + · split_ifs <;> omega + · split_ifs <;> omega + · cases acc <;> simp [findStep] + have hst (x : γ) (i : ℕ) : + (encOption enc (((list x).take i).foldl (findStep t (par x)) none)).length ≤ + (encList enc (list x)).length + 1 := by + rw [foldl_findStep, Option.none_or] + exact (length_encOption_find?_le enc _ _).trans + (Nat.add_le_add_right (length_encList_take_le enc _ _) 1) + have hfold := foldlWith (encL := encList enc) (encB := encOption enc) hpar hlist + (const none) hstep (R := fun x => 4 * (encP (par x)).length + + 3 * (encList enc (list x)).length + 5 + listMax (fun a => Tt (par x, a)) (list x)) + (Q := fun x => 4 * (encP (par x)).length + + 3 * (encList enc (list x)).length + 5 + listMax (fun a => St (par x, a)) (list x)) + (B := fun x => (encList enc (list x)).length + 1) + (fun x i hi => by + have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) + have h₂ := le_listMax (f := fun a => Tt (par x, a)) (List.getElem_mem hi) + have h₃ := hst x i + simp only [length_encPair] at h₂ ⊢ + omega) + (fun x i hi => by + have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) + have h₂ := le_listMax (f := fun a => St (par x, a)) (List.getElem_mem hi) + have h₃ := hst x i + simp only [length_encPair] at h₂ ⊢ + omega) + (fun x i _ => by have := hst x i; omega) + refine (hfold.mono 16 (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ + · have h₁ := length_le_length_encList enc (list x) + have h₂ : (list x).length ≤ (list x).length * (encList enc (list x)).length := by + rcases Nat.eq_zero_or_pos (list x).length with h | h + · simp [h] + · exact Nat.le_mul_of_pos_right _ (by omega) + ring_nf + omega + · omega + · rw [foldl_findStep, Option.none_or] + +/-- The elements of `list x` passing the test `t` with the parameter `par x`. -/ +theorem filterWith {t : π × α → Bool} {Tt St : π × α → ℕ} + (ht : ComputableInO t (encPair encP enc) encBool Tt St) + (hpar : ComputableInO par encIn encP Tp Sp) + (hlist : ComputableInO list encIn (encList enc) Tl Sl) : + ComputableInO (fun x => (list x).filter fun a => t (par x, a)) encIn (encList enc) + (fun x => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * + ((encP (par x)).length + (encList enc (list x)).length + + listMax (fun a => Tt (par x, a)) (list x))) + fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length + + (encList enc (list x)).length + listMax (fun a => St (par x, a)) (list x) := by + have hq := fst (encPair encP (encList enc)) enc + have hel := snd (encPair encP (encList enc)) enc + have h := (ht.comp (hq.fst'.prod hel)).ite + ((ComputableInDegree.snoc enc).inO_one.comp_linear (hq.snd'.prod hel)) hq.snd' + have hstep : ComputableInO + (fun q : (π × List α) × α => filterStep t q.1.1 q.1.2 q.2) + (encPair (encPair encP (encList enc)) enc) (encList enc) + (fun q => (encPair (encPair encP (encList enc)) enc q).length + Tt (q.1.1, q.2)) + fun q => (encPair (encPair encP (encList enc)) enc q).length + St (q.1.1, q.2) := by + refine (h.mono 4 (fun q => ?_) fun q => ?_).of_enc_eq fun ⟨⟨p, acc⟩, a⟩ => ?_ + · split_ifs <;> omega + · split_ifs <;> omega + · simp [filterStep] + have hst (x : γ) (i : ℕ) : + (encList enc (((list x).take i).foldl (filterStep t (par x)) [])).length ≤ + (encList enc (list x)).length := by + rw [foldl_filterStep, List.nil_append] + exact (length_encList_filter_le enc _ _).trans (length_encList_take_le enc _ _) + have hfold := foldlWith (encL := encList enc) (encB := encList enc) hpar hlist + (const []) hstep (R := fun x => 4 * (encP (par x)).length + + 3 * (encList enc (list x)).length + 5 + listMax (fun a => Tt (par x, a)) (list x)) + (Q := fun x => 4 * (encP (par x)).length + + 3 * (encList enc (list x)).length + 5 + listMax (fun a => St (par x, a)) (list x)) + (B := fun x => (encList enc (list x)).length + 1) + (fun x i hi => by + have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) + have h₂ := le_listMax (f := fun a => Tt (par x, a)) (List.getElem_mem hi) + have h₃ := hst x i + simp only [length_encPair] at h₂ ⊢ + omega) + (fun x i hi => by + have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) + have h₂ := le_listMax (f := fun a => St (par x, a)) (List.getElem_mem hi) + have h₃ := hst x i + simp only [length_encPair] at h₂ ⊢ + omega) + (fun x i _ => by have := hst x i; omega) + refine (hfold.mono 16 (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ + · have h₁ := length_le_length_encList enc (list x) + have h₂ : (list x).length ≤ (list x).length * (encList enc (list x)).length := by + rcases Nat.eq_zero_or_pos (list x).length with h | h + · simp [h] + · exact Nat.le_mul_of_pos_right _ (by omega) + ring_nf + omega + · omega + · rw [foldl_filterStep, List.nil_append] + + +/-- Mapping `f` with the parameter `par x` over `list x`. -/ +theorem mapWith {f : π × α → β} {Tf Sf : π × α → ℕ} + (hf : ComputableInO f (encPair encP enc) encB Tf Sf) + (hpar : ComputableInO par encIn encP Tp Sp) + (hlist : ComputableInO list encIn (encList enc) Tl Sl) : + ComputableInO (fun x => (list x).map fun a => f (par x, a)) encIn (encList encB) + (fun x => (encIn x).length + Tp x + Tl x + ((list x).length + 1) * + ((encP (par x)).length + (encList enc (list x)).length + + (encList encB ((list x).map fun a => f (par x, a))).length + + listMax (fun a => Tf (par x, a)) (list x))) + fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length + + (encList enc (list x)).length + + (encList encB ((list x).map fun a => f (par x, a))).length + + listMax (fun a => Sf (par x, a)) (list x) := by + have hq := fst (encPair encP (encList encB)) enc + have hel := snd (encPair encP (encList encB)) enc + have h := (ComputableInDegree.snoc encB).inO_one.comp (hq.snd'.prod (hf.comp (hq.fst'.prod hel))) + obtain ⟨c, hc⟩ := hf.length_le + obtain ⟨d, hd⟩ := hf.length_le_time + have hstep : ComputableInO (fun q : (π × List β) × α => mapStep f q.1.1 q.1.2 q.2) + (encPair (encPair encP (encList encB)) enc) (encList encB) + (fun q => (encPair (encPair encP (encList encB)) enc q).length + Tf (q.1.1, q.2)) + fun q => (encPair (encPair encP (encList encB)) enc q).length + Sf (q.1.1, q.2) := + h.mono (2 * c + 2 * d + 6) (fun q => by + have := hd (q.1.1, q.2) + simp only [length_encPair, Function.comp_apply] at this ⊢ + nlinarith) fun q => by + have := hc (q.1.1, q.2) + simp only [length_encPair, Function.comp_apply] at this ⊢ + nlinarith + have hst (x : γ) (i : ℕ) : + (encList encB (((list x).take i).foldl (mapStep f (par x)) [])).length ≤ + (encList encB ((list x).map fun a => f (par x, a))).length := by + rw [foldl_mapStep, List.nil_append, List.map_take] + exact length_encList_take_le encB _ _ + have hfold := foldlWith (encL := encList enc) (encB := encList encB) hpar hlist + (const []) hstep (R := fun x => 4 * (encP (par x)).length + + 3 * (encList enc (list x)).length + + 3 * (encList encB ((list x).map fun a => f (par x, a))).length + 5 + + listMax (fun a => Tf (par x, a)) (list x)) + (Q := fun x => 4 * (encP (par x)).length + + 3 * (encList enc (list x)).length + + 3 * (encList encB ((list x).map fun a => f (par x, a))).length + 5 + + listMax (fun a => Sf (par x, a)) (list x)) + (B := fun x => (encList encB ((list x).map fun a => f (par x, a))).length) + (fun x i hi => by + have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) + have h₂ := le_listMax (f := fun a => Tf (par x, a)) (List.getElem_mem hi) + have h₃ := hst x i + simp only [length_encPair] at h₂ ⊢ + omega) + (fun x i hi => by + have h₁ := length_le_encList_of_mem enc (List.getElem_mem hi) + have h₂ := le_listMax (f := fun a => Sf (par x, a)) (List.getElem_mem hi) + have h₃ := hst x i + simp only [length_encPair] at h₂ ⊢ + omega) + (fun x i hi => by have := hst x i; omega) + refine (hfold.mono 16 (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ + · have h₁ := length_le_length_encList enc (list x) + have h₂ : (list x).length ≤ (list x).length * (encList enc (list x)).length := by + rcases Nat.eq_zero_or_pos (list x).length with h | h + · simp [h] + · exact Nat.le_mul_of_pos_right _ (by omega) + ring_nf + omega + · omega + · rw [foldl_mapStep, List.nil_append] + +end Turing.MultiTapeTM.ComputableInO From 8cbebb0100084c6e6d66fc3317a838006ee37b72 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 17:23:41 +0000 Subject: [PATCH 3/3] refactor(Universal): state the step complexity in the plain calculus Universal/Complexity now states and proves the tape operations, applyTapes_inO, reads_inO, moveInput_inO, stepWith_inO and step_inO with ComputableInDegree and ComputableInO. Its tidy clients derive what they need with .tidy, marked as bridges for #862. Public statements and definitions use named parts of the step contexts instead of projection chains (#1764). Co-Authored-By: Claude Opus 5.5 --- .../Turing/MultiTape/Universal/Bound.lean | 2 +- .../MultiTape/Universal/Complexity.lean | 206 ++++++++++-------- .../Turing/MultiTape/Universal/Compose.lean | 12 +- .../Turing/MultiTape/Universal/InPlace.lean | 8 +- .../Turing/MultiTape/Universal/Machine.lean | 6 +- .../MultiTape/Universal/SpaceBudget.lean | 3 +- scripts/tidy_surface_baseline.json | 1 - 7 files changed, 135 insertions(+), 103 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean index 292d05d43..09e06559b 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Bound.lean @@ -305,7 +305,7 @@ public theorem stepTime_iterate_le (x : List ℕ) (j : ℕ) : have hbits := ComputableTidilyInO.length_encNat_mono (show cfg.inputPos ≤ (encList encUnary x).length + 1 by omega) unfold stepTime stepBound - dsimp only + dsimp only [Ctx.desc, Ctx.input, Ctx.cfg] exact Nat.add_le_add (Nat.mul_le_mul (Nat.mul_le_mul_right _ (by omega)) (by omega)) (Nat.mul_le_mul (by omega) (by gcongr)) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean index 0d96f3221..f72978176 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean @@ -18,6 +18,7 @@ import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives import Complexity.Computability.Machines.Turing.MultiTape.Internal.OLoops +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists /-! # The cost of a step of the simulation @@ -26,7 +27,8 @@ States, symbols and moves are encoded in unary (`Turing.MultiTapeTM.encUnary`), the work tapes as integers (`Turing.MultiTapeTM.encInt`), the position of the input head in binary (`Turing.MultiTapeTM.encNat`), and a structure as the framed tuple of its fields. -Reading, writing and moving on a zipper are tidily computable in linear time and space. A step of +Reading, writing and moving on a zipper are computable in linear time and space +(`Turing.MultiTapeTM.ComputableInDegree` with degrees one). A step of the simulation (`Turing.MultiTapeTM.Universal.step_inO`) takes space linear in the length `L` of the encoded context (the description, the input and the configuration). Its time bound separates the configuration length from description lookup and input scanning: for `K` work tapes, `E` @@ -41,12 +43,16 @@ copied each round; this bound does not implement the buffered Hennie–Stearns s ## Main definitions * `Turing.MultiTapeTM.Universal.eDesc`, `.eCfg`: the encodings of descriptions and configurations. +* `Turing.MultiTapeTM.Universal.Ctx`, `.WCtx`: the contexts of a step, with and without the input, + and their named parts (`Ctx.desc`, `Ctx.input`, `Ctx.cfg`, `WCtx.desc`, `WCtx.cfg`, `WCtx.sym`). * `Turing.MultiTapeTM.Universal.stepTime`: the time bound of a step. ## Main results -* `Turing.MultiTapeTM.Universal.step_inO`: a step is tidily computable within the time `stepTime` - and linear space. +* `Turing.MultiTapeTM.Universal.step_inO`: a step is computable (`Turing.MultiTapeTM.ComputableInO`) + within the time `stepTime` and linear space. +* `Turing.MultiTapeTM.Universal.stepWith_inO`, `.applyTapes_inO`, `.reads_inO`, `.moveInput_inO`: + its parts. -/ namespace Turing.MultiTapeTM.Universal @@ -110,7 +116,7 @@ public abbrev eCfgFields : Option ℕ × ℕ × List Tape ↪ List Bool := eCfg c = eCfgFields (c.state, c.inputPos, c.workTapes) := rfl /-- The state of a configuration, in linear time. -/ -public lemma state_inO : ComputableTidilyInO SCfg.state eCfg eSym (fun c => (eCfg c).length) +public lemma state_inO : ComputableInO SCfg.state eCfg eSym (fun c => (eCfg c).length) fun c => (eCfg c).length := .of_linear (.of_unframe fun c => by simp [eCfg_apply]) @@ -118,39 +124,39 @@ public lemma state_inO : ComputableTidilyInO SCfg.state eCfg eSym (fun c => (eCf section Tape -open ComputableTidilyInDegree +open ComputableInDegree -lemma tapeFields_deg : ComputableTidilyInDegree (fun t : Tape => (t.head, t.left, t.right)) eTape +lemma tapeFields_deg : ComputableInDegree (fun t : Tape => (t.head, t.left, t.right)) eTape eTapeFields 1 1 := of_eq fun _ => rfl @[local fun_prop] -lemma tapeMk_deg : ComputableTidilyInDegree +lemma tapeMk_deg : ComputableInDegree (fun p : ℤ × List (Option ℕ) × List (Option ℕ) => Tape.mk p.1 p.2.1 p.2.2) eTapeFields eTape 1 1 := of_eq fun _ => rfl @[local fun_prop] -lemma tapeHead_deg : ComputableTidilyInDegree Tape.head eTape encInt 1 1 := +lemma tapeHead_deg : ComputableInDegree Tape.head eTape encInt 1 1 := tapeFields_deg.fst' @[local fun_prop] -lemma tapeLeft_deg : ComputableTidilyInDegree Tape.left eTape (encList eSym) 1 1 := +lemma tapeLeft_deg : ComputableInDegree Tape.left eTape (encList eSym) 1 1 := tapeFields_deg.snd'.fst' @[local fun_prop] -lemma tapeRight_deg : ComputableTidilyInDegree Tape.right eTape (encList eSym) 1 1 := +lemma tapeRight_deg : ComputableInDegree Tape.right eTape (encList eSym) 1 1 := tapeFields_deg.snd'.snd' /-- The symbol under the head. -/ @[local fun_prop] -lemma read_deg : ComputableTidilyInDegree Tape.read eTape eSym 1 1 := by +lemma read_deg : ComputableInDegree Tape.read eTape eSym 1 1 := by unfold Tape.read fun_prop (disch := lia) /-- Writing under the head. -/ @[local fun_prop] -lemma write_deg : ComputableTidilyInDegree (fun p : Tape × Option ℕ => p.1.write p.2) +lemma write_deg : ComputableInDegree (fun p : Tape × Option ℕ => p.1.write p.2) (encPair eTape eSym) eTape 1 1 := by unfold Tape.write fun_prop (disch := lia) @@ -158,20 +164,20 @@ lemma write_deg : ComputableTidilyInDegree (fun p : Tape × Option ℕ => p.1.wr /-- A right move. -/ @[local fun_prop] lemma movePos_deg : - ComputableTidilyInDegree (fun t : Tape => t.move .pos) eTape eTape 1 1 := by + ComputableInDegree (fun t : Tape => t.move .pos) eTape eTape 1 1 := by simp only [Tape.move] fun_prop (disch := lia) /-- A left move. -/ @[local fun_prop] lemma moveNeg_deg : - ComputableTidilyInDegree (fun t : Tape => t.move .neg) eTape eTape 1 1 := by + ComputableInDegree (fun t : Tape => t.move .neg) eTape eTape 1 1 := by simp only [Tape.move] fun_prop (disch := lia) /-- Moving the head. -/ @[local fun_prop] -lemma move_deg : ComputableTidilyInDegree (fun p : Tape × SignType => p.1.move p.2) +lemma move_deg : ComputableInDegree (fun p : Tape × SignType => p.1.move p.2) (encPair eTape encSign) eTape 1 1 := by have ht := fst eTape encSign have hm := snd eTape encSign @@ -185,9 +191,9 @@ lemma move_deg : ComputableTidilyInDegree (fun p : Tape × SignType => p.1.move /-- Applying an action to a work tape: write, then move. -/ @[local fun_prop] -lemma apply_deg : ComputableTidilyInDegree (fun p : Tape × TapeAct => +lemma apply_deg : ComputableInDegree (fun p : Tape × TapeAct => p.1.apply p.2) (encPair eTape eTA) eTape 1 1 := by - convert (show ComputableTidilyInDegree (fun p : Tape × TapeAct => + convert (show ComputableInDegree (fun p : Tape × TapeAct => (if p.2.1.isSome then p.1.write (p.2.1.getD none) else p.1).move p.2.2) (encPair eTape eTA) eTape 1 1 by fun_prop (disch := first | apply le_refl | lia)) using 1 funext ⟨t, w, m⟩ @@ -214,11 +220,11 @@ lemma foldl_applyStep (ts : List Tape) (as : List TapeAct) (acc : List Tape) : | nil => simp [applyStep, ih, applyTapes, applyTapes_nil_right] | cons a as => simp [applyStep, ih, applyTapes] -lemma applyStep_deg : ComputableTidilyInDegree +lemma applyStep_deg : ComputableInDegree (fun q : (List TapeAct × List Tape) × Tape => applyStep q.1 q.2) (encPair (encPair (encList eTA) (encList eTape)) eTape) (encPair (encList eTA) (encList eTape)) 1 1 := by - convert (show ComputableTidilyInDegree (fun q : (List TapeAct × List Tape) × Tape => + convert (show ComputableInDegree (fun q : (List TapeAct × List Tape) × Tape => (q.1.1.tail, q.1.2 ++ [if q.1.1.isEmpty then q.2 else q.2.apply (q.1.1.headD (none, 0))])) (encPair (encPair (encList eTA) (encList eTape)) eTape) (encPair (encList eTA) (encList eTape)) 1 1 by @@ -291,12 +297,12 @@ lemma length_encList_map_read_le (ts : List Tape) : /-! ### All work tapes -/ -open ComputableTidilyInO +open ComputableInO /-- Applying actions to the work tapes, within time the number of work tapes times the length of the arguments, and linear space. -/ public theorem applyTapes_inO : - ComputableTidilyInO (fun p : List Tape × List TapeAct => applyTapes p.1 p.2) + ComputableInO (Function.uncurry applyTapes) (encPair (encList eTape) (encList eTA)) (encList eTape) (fun p => (p.1.length + 1) * ((encPair (encList eTape) (encList eTA) p).length + 1)) fun p => (encPair (encList eTape) (encList eTA) p).length := by @@ -312,9 +318,9 @@ public theorem applyTapes_inO : omega have hfold := (ComputableInO.foldl (encL := encList eTape) (encB := encPair (encList eTA) (encList eTape)) - (fst (encList eTape) (encList eTA)).computableInO - ((snd (encList eTape) (encList eTA)).prod (const [])).computableInO - applyStep_deg.inO_one.computableInO + (fst (encList eTape) (encList eTA)) + ((snd (encList eTape) (encList eTA)).prod (const [])) + applyStep_deg.inO_one (R := fun p => 14 * (encPair (encList eTape) (encList eTA) p).length + 1) (Q := fun p => 14 * (encPair (encList eTape) (encList eTA) p).length + 1) (B := fun p => 6 * (encPair (encList eTape) (encList eTA) p).length) @@ -328,19 +334,19 @@ public theorem applyTapes_inO : have h₂ := length_le_encList_of_mem eTape (List.getElem_mem hi) simp only [length_encPair] at h₁ h₂ ⊢ omega) - (fun p i hi => hlen p i)).tidy + (fun p i hi => hlen p i)) refine (((snd (encList eTA) (encList eTape)).comp_linear hfold).mono 32 (fun p => ?_) fun p => ?_).of_enc_eq fun p => ?_ · simp only [length_encPair] nlinarith · simp only [length_encPair] omega - · simp [foldl_applyStep] + · simp [foldl_applyStep, Function.uncurry] /-- The symbols under the heads of the work tapes, within time the number of work tapes times their length, and linear space. -/ public theorem reads_inO : - ComputableTidilyInO (fun ts : List Tape => ts.map Tape.read) (encList eTape) (encList eSym) + ComputableInO (fun ts : List Tape => ts.map Tape.read) (encList eTape) (encList eSym) (fun ts => (ts.length + 1) * ((encList eTape ts).length + 1)) fun ts => (encList eTape ts).length := by refine ((mapWith (encP := encUnit) (f := fun p : Unit × Tape => p.2.read) @@ -362,7 +368,7 @@ public theorem reads_inO : /-- Moving the input head, charging binary arithmetic only to the encoded position length. -/ public theorem moveInput_inO : - ComputableTidilyInO (fun q : ℕ × Option ℕ × SignType => moveInput q.1 q.2.1 q.2.2) + ComputableInO (fun (p, a, m) => moveInput p a m) (encPair encNat (encPair eSym encSign)) encNat (fun q => (encPair encNat (encPair eSym encSign) q).length + ((encNat q.1).length + 1) ^ 2) @@ -370,14 +376,14 @@ public theorem moveInput_inO : have hp := fst encNat (encPair eSym encSign) have ha := (snd encNat (encPair eSym encSign)).fst' have hm := (snd encNat (encPair eSym encSign)).snd' - have hsign (s : SignType) := (ComputableTidilyInDegree.of_finite (encIn := encSign) + have hsign (s : SignType) := (ComputableInDegree.of_finite (encIn := encSign) (encMid := encBool) fun m : SignType => decide (m = s)).inO_one.comp_linear hm - have hright := (ComputableTidilyInDegree.of_finite (encIn := encPair encBool encBool) + have hright := (ComputableInDegree.of_finite (encIn := encPair encBool encBool) (encMid := encBool) fun b : Bool × Bool => b.1 || b.2).inO_one.comp_linear - ((ComputableInO.natIsZero.tidy.comp_linear hp).prod - ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear ha)) - refine (((hsign .zero).ite hp ((hsign .neg).ite (ComputableInO.natPred.tidy.comp hp) - (hright.ite (ComputableInO.natSucc.tidy.comp hp) hp))).mono 8 (fun q => ?_) + ((ComputableInO.natIsZero.comp_linear hp).prod + ((ComputableInDegree.isSome encUnary).inO_one.comp_linear ha)) + refine (((hsign .zero).ite hp ((hsign .neg).ite (ComputableInO.natPred.comp hp) + (hright.ite (ComputableInO.natSucc.comp hp) hp))).mono 8 (fun q => ?_) fun q => ?_).of_enc_eq fun ⟨p, a, m⟩ => ?_ · have h₁ : (encNat q.1).length ≤ (encPair encNat (encPair eSym encSign) q).length := by rw [length_encPair]; omega @@ -400,13 +406,22 @@ public abbrev WCtx := (Desc × SCfg) × Option ℕ /-- The encoding of contexts without the input. -/ public abbrev eWCtx : WCtx ↪ List Bool := encPair (encPair eDesc eCfg) eSym +/-- The description of a context without the input. -/ +public abbrev WCtx.desc (c : WCtx) : Desc := c.1.1 + +/-- The configuration of a context without the input. -/ +public abbrev WCtx.cfg (c : WCtx) : SCfg := c.1.2 + +/-- The symbol under the input head, in a context without the input. -/ +public abbrev WCtx.sym (c : WCtx) : Option ℕ := c.2 + /-- The key of the transition to take. -/ @[expose] public def wKey (c : WCtx) : Key := - ⟨c.1.2.state.getD 0, c.2, c.1.2.workTapes.map Tape.read⟩ + ⟨c.cfg.state.getD 0, c.sym, c.cfg.workTapes.map Tape.read⟩ /-- The transition to take, if any. -/ @[expose] public def wFound (c : WCtx) : Option (Key × Act) := - c.1.1.table.find? (·.1 = wKey c) + c.desc.table.find? (·.1 = wKey c) /-- The default transition, never taken. -/ @[expose] public def defaultEntry : Key × Act := (⟨0, none, []⟩, ⟨0, [], none, none⟩) @@ -414,13 +429,13 @@ public abbrev eWCtx : WCtx ↪ List Bool := encPair (encPair eDesc eCfg) eSym /-- The action of the transition to take. -/ @[expose] public def wAct (c : WCtx) : Act := ((wFound c).getD defaultEntry).2 -public lemma stepWith_eq (c : WCtx) : stepWith c.1.1 c.1.2 c.2 = - if c.1.2.state.isSome then +public lemma stepWith_eq (c : WCtx) : stepWith c.desc c.cfg c.sym = + if c.cfg.state.isSome then (if (wFound c).isSome then - (⟨(wAct c).state, moveInput c.1.2.inputPos c.2 (wAct c).inputTape, - applyTapes c.1.2.workTapes (wAct c).workTapes⟩, (wAct c).output) - else (⟨none, c.1.2.inputPos, c.1.2.workTapes⟩, none)) - else (c.1.2, none) := by + (⟨(wAct c).state, moveInput c.cfg.inputPos c.sym (wAct c).inputTape, + applyTapes c.cfg.workTapes (wAct c).workTapes⟩, (wAct c).output) + else (⟨none, c.cfg.inputPos, c.cfg.workTapes⟩, none)) + else (c.cfg, none) := by obtain ⟨⟨d, ⟨_ | q, ip, ts⟩⟩, a⟩ := c · rfl · simp only [stepWith, Option.isSome_some, ↓reduceIte] @@ -433,43 +448,43 @@ public lemma stepWith_eq (c : WCtx) : stepWith c.1.1 c.1.2 c.2 = /-- A step without input lookup: tape passes and description comparisons are linear in context length; only binary input-head arithmetic is quadratic in its own encoded length. -/ @[expose] public def wTime (c : WCtx) : ℕ := - (c.1.2.workTapes.length + c.1.1.table.length + 1) * ((eDesc c.1.1).length + 1) * - ((eWCtx c).length + 1) + ((encNat c.1.2.inputPos).length + 1) ^ 2 + (c.cfg.workTapes.length + c.desc.table.length + 1) * ((eDesc c.desc).length + 1) * + ((eWCtx c).length + 1) + ((encNat c.cfg.inputPos).length + 1) ^ 2 section Lengths variable (c : WCtx) -lemma length_eWCtx : (eWCtx c).length = 2 * (2 * (eDesc c.1.1).length + 1 + - (2 * (eSym c.1.2.state).length + 1 + (2 * (encNat c.1.2.inputPos).length + 1 + - (encList eTape c.1.2.workTapes).length))) + 1 + (eSym c.2).length := by +lemma length_eWCtx : (eWCtx c).length = 2 * (2 * (eDesc c.desc).length + 1 + + (2 * (eSym c.cfg.state).length + 1 + (2 * (encNat c.cfg.inputPos).length + 1 + + (encList eTape c.cfg.workTapes).length))) + 1 + (eSym c.sym).length := by simp only [eWCtx, eCfg_apply, length_encPair] lemma length_wTable_le : - (encList (encPair eKey eAct) c.1.1.table).length ≤ (eWCtx c).length := by + (encList (encPair eKey eAct) c.desc.table).length ≤ (eWCtx c).length := by rw [length_eWCtx]; simp only [eDesc_apply, length_encPair]; omega lemma length_le_wTime {A B k : ℕ} - (hA : A ≤ c.1.2.workTapes.length + c.1.1.table.length) - (hB : B ≤ (eWCtx c).length) (hk : k ≤ (eDesc c.1.1).length + 1) : + (hA : A ≤ c.cfg.workTapes.length + c.desc.table.length) + (hB : B ≤ (eWCtx c).length) (hk : k ≤ (eDesc c.desc).length + 1) : (A + 1) * k * (B + 1) ≤ wTime c := (Nat.mul_le_mul (Nat.mul_le_mul (by omega) hk) (by omega)).trans (Nat.le_add_right _ _) /-- An entry of the table is no longer than the context. -/ -lemma length_le_of_mem_table {e : Key × Act} (he : e ∈ c.1.1.table) : +lemma length_le_of_mem_table {e : Key × Act} (he : e ∈ c.desc.table) : (encPair eKey eAct e).length ≤ (eWCtx c).length := (length_le_encList_of_mem (encPair eKey eAct) he).trans (length_wTable_le c) /-- An entry of the table is no longer than the description. -/ -lemma length_le_eDesc_of_mem_table {e : Key × Act} (he : e ∈ c.1.1.table) : - (encPair eKey eAct e).length ≤ (eDesc c.1.1).length := by +lemma length_le_eDesc_of_mem_table {e : Key × Act} (he : e ∈ c.desc.table) : + (encPair eKey eAct e).length ≤ (eDesc c.desc).length := by have := length_le_encList_of_mem (encPair eKey eAct) he simp only [eDesc_apply, length_encPair] at * omega lemma length_wKey_le : (eKey (wKey c)).length ≤ 4 * (eWCtx c).length + 4 := by - have h₂ := length_encList_map_read_le c.1.2.workTapes - have h₃ : (c.1.2.state.getD 0) ≤ (eSym c.1.2.state).length := by cases c.1.2.state <;> simp + have h₂ := length_encList_map_read_le c.cfg.workTapes + have h₃ : (c.cfg.state.getD 0) ≤ (eSym c.cfg.state).length := by cases c.cfg.state <;> simp rw [length_eWCtx] simp only [wKey, eKey_apply, length_encPair, encUnary_apply, List.length_replicate] omega @@ -492,38 +507,38 @@ end Lengths /-- A part of a step within the time `wTime` and linear space. -/ abbrev WPart {β : Type} (f : WCtx → β) (enc : β ↪ List Bool) : Prop := - ComputableTidilyInO f eWCtx enc wTime fun c => (eWCtx c).length + ComputableInO f eWCtx enc wTime fun c => (eWCtx c).length lemma le_wTime (c : WCtx) : (eWCtx c).length + 1 ≤ wTime c := by simpa using length_le_wTime c (A := 0) (Nat.zero_le _) le_rfl (k := 1) (by omega) /-- One step of the simulation without the input, within the time `wTime` and linear space. -/ public theorem stepWith_inO : - ComputableTidilyInO (fun c : WCtx => stepWith c.1.1 c.1.2 c.2) eWCtx (encPair eCfg eSym) + ComputableInO (fun c : WCtx => stepWith c.desc c.cfg c.sym) eWCtx (encPair eCfg eSym) wTime fun c => (eWCtx c).length := by -- the parts of the context have hd := (fst (encPair eDesc eCfg) eSym).fst' have hc := (fst (encPair eDesc eCfg) eSym).snd' have hf := hc.of_enc_eq (encOut := eCfgFields) - (g := fun c : WCtx => (c.1.2.state, c.1.2.inputPos, c.1.2.workTapes)) fun _ => rfl + (g := fun c : WCtx => (c.cfg.state, c.cfg.inputPos, c.cfg.workTapes)) fun _ => rfl have htable := (hd.of_enc_eq (encOut := encPair encUnary (encPair encUnary - (encList (encPair eKey eAct)))) (g := fun c : WCtx => (c.1.1.tapes, c.1.1.q₀, c.1.1.table)) + (encList (encPair eKey eAct)))) (g := fun c : WCtx => (c.desc.tapes, c.desc.q₀, c.desc.table)) fun _ => rfl).snd'.snd' -- the key - have hreads : WPart (fun c => c.1.2.workTapes.map Tape.read) (encList eSym) := by + have hreads : WPart (fun c => c.cfg.workTapes.map Tape.read) (encList eSym) := by refine (reads_inO.comp hf.snd'.snd').mono 2 (fun c => ?_) fun c => ?_ all_goals have h₁ := length_eWCtx c have h₂ := le_wTime c - have h₃ := length_le_wTime c (A := c.1.2.workTapes.length) (by omega) - (B := (encList eTape c.1.2.workTapes).length) (by omega) (k := 1) (by omega) + have h₃ := length_le_wTime c (A := c.cfg.workTapes.length) (by omega) + (B := (encList eTape c.cfg.workTapes).length) (by omega) (k := 1) (by omega) simp only [eWCtx, Nat.mul_one] at * omega - have hsym : WPart (fun c => c.2) eSym := + have hsym : WPart (fun c => c.sym) eSym := (snd (encPair eDesc eCfg) eSym).mono 1 (fun c => by have := le_wTime c; dsimp only [eWCtx] at *; omega) fun c => by dsimp only [eWCtx]; omega have hkey : WPart wKey eKey := by - refine ((((ComputableTidilyInDegree.getD (enc₁ := encUnary) 0).inO_one.comp_linear + refine ((((ComputableInDegree.getD (enc₁ := encUnary) 0).inO_one.comp_linear hf.fst').prod (hsym.prod hreads)).mono 4 (fun c => ?_) fun c => ?_).of_enc_eq fun _ => rfl all_goals @@ -531,7 +546,7 @@ public theorem stepWith_inO : dsimp only [eWCtx, Function.comp_apply] at * omega -- the transition - have htest := (ComputableInO.eq eKey).tidy.comp ((snd eKey (encPair eKey eAct)).fst'.prod + have htest := (ComputableInO.eq eKey).comp ((snd eKey (encPair eKey eAct)).fst'.prod (fst eKey (encPair eKey eAct))) have hfound : WPart wFound (encOption (encPair eKey eAct)) := by refine (findWith htest hkey htable).mono 64 (fun c => ?_) fun c => ?_ @@ -540,35 +555,35 @@ public theorem stepWith_inO : have ht := length_wTable_le c have hst := le_wTime c have hlinear : (eWCtx c).length + 1 ≤ - ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) := by nlinarith - have hlen := length_le_length_encList (encPair eKey eAct) c.1.1.table + ((eDesc c.desc).length + 1) * ((eWCtx c).length + 1) := by nlinarith + have hlen := length_le_length_encList (encPair eKey eAct) c.desc.table · have h₁ : listMax (fun e => (encPair eKey (encPair eKey eAct) (wKey c, e)).length + (encPair eKey (encPair eKey eAct) (wKey c, e)).length + ((eKey (e.1, wKey c).1).length + 1) * ((eKey (e.1, wKey c).1).length + (eKey (e.1, wKey c).2).length + 1)) - c.1.1.table ≤ 32 * ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) := + c.desc.table ≤ 32 * ((eDesc c.desc).length + 1) * ((eWCtx c).length + 1) := listMax_le fun e he => by have h₁ := length_le_of_mem_table c he have h₂ := length_le_encPair_left eKey eAct e have hD := length_le_eDesc_of_mem_table c he have h₃ : ((eKey e.1).length + 1) * ((eKey e.1).length + (eKey (wKey c)).length + 1) - ≤ ((eDesc c.1.1).length + 1) * (5 * ((eWCtx c).length + 1)) := + ≤ ((eDesc c.desc).length + 1) * (5 * ((eWCtx c).length + 1)) := Nat.mul_le_mul (by omega) (by omega) simp only [length_encPair] at * nlinarith - have h₂ := length_le_wTime c (A := c.1.1.table.length) (by omega) + have h₂ := length_le_wTime c (A := c.desc.table.length) (by omega) (B := (eWCtx c).length) le_rfl le_rfl - have h₃ := Nat.mul_le_mul_left (c.1.1.table.length + 1) (Nat.add_le_add + have h₃ := Nat.mul_le_mul_left (c.desc.table.length + 1) (Nat.add_le_add (Nat.add_le_add (hk.trans (show 4 * (eWCtx c).length + 4 ≤ - 4 * ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) by nlinarith)) + 4 * ((eDesc c.desc).length + 1) * ((eWCtx c).length + 1) by nlinarith)) (ht.trans (show (eWCtx c).length ≤ - ((eDesc c.1.1).length + 1) * ((eWCtx c).length + 1) by omega))) + ((eDesc c.desc).length + 1) * ((eWCtx c).length + 1) by omega))) h₁) dsimp only [eWCtx, Function.comp_apply] at * nlinarith · have h₁ : listMax (fun e => (encPair eKey (encPair eKey eAct) (wKey c, e)).length + (encPair eKey (encPair eKey eAct) (wKey c, e)).length + - (encPair eKey eKey (e.1, wKey c)).length) c.1.1.table ≤ + (encPair eKey eKey (e.1, wKey c)).length) c.desc.table ≤ 32 * ((eWCtx c).length + 1) := listMax_le fun e he => by have h₁ := length_le_of_mem_table c he @@ -578,12 +593,12 @@ public theorem stepWith_inO : dsimp only [eWCtx, Function.comp_apply] at * omega -- the action and the new configuration - have hact := (((ComputableTidilyInDegree.getD (enc₁ := encPair eKey eAct) + have hact := (((ComputableInDegree.getD (enc₁ := encPair eKey eAct) (enc := encOption (encPair eKey eAct)) defaultEntry).inO_one.comp_linear hfound).snd').of_enc_eq (encOut := encPair encSign (encPair (encList eTA) (encPair eSym eSym))) (g := fun c => ((wAct c).inputTape, (wAct c).workTapes, (wAct c).output, (wAct c).state)) fun _ => rfl - have hmove : WPart (fun c => moveInput c.1.2.inputPos (wKey c).input (wAct c).inputTape) + have hmove : WPart (fun c => moveInput c.cfg.inputPos (wKey c).input (wAct c).inputTape) encNat := by have hinput := (hkey.of_enc_eq (encOut := encPair encUnary (encPair eSym (encList eSym))) (g := fun c => ((wKey c).state, (wKey c).input, (wKey c).work)) fun _ => rfl) @@ -594,48 +609,48 @@ public theorem stepWith_inO : have hk := length_wKey_le c have ha := length_wAct_le c have hst := le_wTime c - have hp : (encPair encNat (encPair eSym encSign) (c.1.2.inputPos, (wKey c).input, + have hp : (encPair encNat (encPair eSym encSign) (c.cfg.inputPos, (wKey c).input, (wAct c).inputTape)).length ≤ 8 * ((eWCtx c).length + 1) := by have := length_eWCtx c simp only [eKey_apply, eAct_apply, length_encPair] at * omega - have h₂ : ((encNat c.1.2.inputPos).length + 1) ^ 2 ≤ wTime c := + have h₂ : ((encNat c.cfg.inputPos).length + 1) ^ 2 ≤ wTime c := Nat.le_add_left _ _ · dsimp only [eWCtx, Function.comp_apply] at * omega · dsimp only [eWCtx, Function.comp_apply] at * omega - have happ : WPart (fun c => applyTapes c.1.2.workTapes (wAct c).workTapes) + have happ : WPart (fun c => applyTapes c.cfg.workTapes (wAct c).workTapes) (encList eTape) := by refine (applyTapes_inO.comp (hf.snd'.snd'.prod hact.snd'.fst')).mono 16 (fun c => ?_) fun c => ?_ all_goals have ha := length_wAct_le c have hst := le_wTime c - have hp : (encPair (encList eTape) (encList eTA) (c.1.2.workTapes, + have hp : (encPair (encList eTape) (encList eTA) (c.cfg.workTapes, (wAct c).workTapes)).length ≤ 4 * ((eWCtx c).length + 1) := by have := length_eWCtx c simp only [eAct_apply, length_encPair] at * omega - have h₂ := length_le_wTime c (A := c.1.2.workTapes.length) (by omega) + have h₂ := length_le_wTime c (A := c.cfg.workTapes.length) (by omega) (B := (eWCtx c).length) le_rfl (k := 1) (by omega) rw [Nat.mul_one] at h₂ - · have h₁ := Nat.mul_le_mul_left (c.1.2.workTapes.length + 1) (Nat.add_le_add_right hp 1) + · have h₁ := Nat.mul_le_mul_left (c.cfg.workTapes.length + 1) (Nat.add_le_add_right hp 1) dsimp only [eWCtx, Function.comp_apply] at * nlinarith · dsimp only [eWCtx, Function.comp_apply] at * omega -- the result have hlive := (((hact.snd'.snd'.snd'.prod (hmove.prod happ)).of_enc_eq (encOut := eCfg) - (g := fun c => (⟨(wAct c).state, moveInput c.1.2.inputPos (wKey c).input - (wAct c).inputTape, applyTapes c.1.2.workTapes (wAct c).workTapes⟩ : SCfg)) + (g := fun c => (⟨(wAct c).state, moveInput c.cfg.inputPos (wKey c).input + (wAct c).inputTape, applyTapes c.cfg.workTapes (wAct c).workTapes⟩ : SCfg)) fun _ => rfl).prod hact.snd'.snd'.fst') have hhalt := ((((const (encMid := eSym) none).prod hf.snd').of_enc_eq (encOut := eCfg) - (g := fun c : WCtx => (⟨none, c.1.2.inputPos, c.1.2.workTapes⟩ : SCfg)) fun _ => rfl).prod + (g := fun c : WCtx => (⟨none, c.cfg.inputPos, c.cfg.workTapes⟩ : SCfg)) fun _ => rfl).prod (const (encMid := eSym) none)) have hidle := hc.prod (const (encMid := eSym) none) - refine ((((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear hf.fst').ite - (((ComputableTidilyInDegree.isSome (encPair eKey eAct)).inO_one.comp_linear hfound).ite + refine ((((ComputableInDegree.isSome encUnary).inO_one.comp_linear hf.fst').ite + (((ComputableInDegree.isSome (encPair eKey eAct)).inO_one.comp_linear hfound).ite hlive hhalt) hidle).mono 16 (fun c => ?_) fun c => ?_).of_enc_eq fun c => ?_ · have := le_wTime c dsimp only [eWCtx, Function.comp_apply] at * @@ -653,12 +668,21 @@ public abbrev Ctx := (Desc × List ℕ) × SCfg /-- The encoding of contexts. -/ public abbrev eCtx : Ctx ↪ List Bool := encPair (encPair eDesc (encList encUnary)) eCfg +/-- The description of a context. -/ +public abbrev Ctx.desc (c : Ctx) : Desc := c.1.1 + +/-- The input of a context. -/ +public abbrev Ctx.input (c : Ctx) : List ℕ := c.1.2 + +/-- The configuration of a context. -/ +public abbrev Ctx.cfg (c : Ctx) : SCfg := c.2 + /-- The step bound separates linear configuration passes from a streaming input lookup with binary countdown arithmetic. In particular, the whole configuration length is never squared. -/ @[expose] public def stepTime (c : Ctx) : ℕ := - (c.2.workTapes.length + c.1.1.table.length + 1) * ((eDesc c.1.1).length + 1) * + (c.cfg.workTapes.length + c.desc.table.length + 1) * ((eDesc c.desc).length + 1) * ((eCtx c).length + 1) + - ((encList encUnary c.1.2).length + 1) * ((encNat c.2.inputPos).length + 1) ^ 2 + ((encList encUnary c.input).length + 1) * ((encNat c.cfg.inputPos).length + 1) ^ 2 lemma le_stepTime_ctx (c : Ctx) : (eCtx c).length + 1 ≤ stepTime c := (Nat.le_mul_of_pos_left _ (Nat.mul_pos (Nat.succ_pos _) (Nat.succ_pos _))).trans @@ -667,7 +691,7 @@ lemma le_stepTime_ctx (c : Ctx) : (eCtx c).length + 1 ≤ stepTime c := /-- One step of the simulation, on contexts, within the time `stepTime` and linear space: the symbol under the input head, and the step without the input. -/ public theorem step_inO : - ComputableTidilyInO (fun c : Ctx => step c.1.1 c.1.2 c.2) eCtx (encPair eCfg eSym) + ComputableInO (fun c : Ctx => step c.desc c.input c.cfg) eCtx (encPair eCfg eSym) stepTime fun c => (eCtx c).length := by have hd := (fst (encPair eDesc (encList encUnary)) eCfg).fst' have hx := (fst (encPair eDesc (encList encUnary)) eCfg).snd' @@ -675,7 +699,7 @@ public theorem step_inO : have hip := (hc.of_enc_eq (encOut := eCfgFields) (g := fun c : Ctx => (c.2.state, c.2.inputPos, c.2.workTapes)) fun _ => rfl).snd'.fst' refine ((stepWith_inO.comp - ((hd.prod hc).prod (inputSymbol_stream_inO.tidy.comp (hx.prod hip)))).mono 32 + ((hd.prod hc).prod (inputSymbol_stream_inO.comp (hx.prod hip)))).mono 32 (fun c => ?_) fun c => ?_).of_enc_eq fun c => by rw [step_eq_stepWith]; rfl all_goals have h₁ : (eSym (inputSymbol c.1.2 c.2.inputPos)).length ≤ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean index e313f253c..87086cd03 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean @@ -382,7 +382,8 @@ lemma halted_inO {α : Type} {enc : α ↪ List Bool} {c : α → SCfg} {T S : ((ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool) fun b : Bool => !b).inO_one.comp_linear ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear - (state_inO.comp_linear h))).of_enc_eq fun a => by + -- bridge for #862: tidy client of the plain `state_inO` + (state_inO.tidy.comp_linear h))).of_enc_eq fun a => by simp only [Function.comp_apply] cases (c a).state <;> rfl @@ -435,7 +436,8 @@ public lemma stepG_inO : have hc := fst eCtl (encPair encNat encUnary) have hg := hc.fst'.fst' have hsym := countSym_inO (inputPos_inO hg.snd') hc.snd'.fst' hc.snd'.snd' - refine (stepWith_inO.comp (hg.prod (hsym.of_enc_eq (g := fun s : CSt => gSym s.1) + -- bridge for #862: tidy client of the plain `stepWith_inO` + refine (stepWith_inO.tidy.comp (hg.prod (hsym.of_enc_eq (g := fun s : CSt => gSym s.1) fun _ => rfl))).mono 100 (fun s => ?_) fun s => ?_ all_goals have hw := wTime_le' (s.1.1.1, gSym s.1) @@ -464,7 +466,8 @@ public lemma stepF_inO : ComputableTidilyInO (fun s : CSt => stepWith s.1.1.2.1 have hn := snd eCtl (encPair encNat encUnary) have hg := hc.fst'.snd' have hsym := countSym_inO (inputPos_inO hg.snd') hn.fst' hn.snd' - refine (stepWith_inO.comp (hg.prod (hsym.of_enc_eq (g := xSym) + -- bridge for #862: tidy client of the plain `stepWith_inO` + refine (stepWith_inO.tidy.comp (hg.prod (hsym.of_enc_eq (g := xSym) fun _ => rfl))).mono 100 (fun s => ?_) fun s => ?_ all_goals have hw := wTime_le' (s.1.1.2, xSym s) @@ -619,7 +622,8 @@ public lemma cEmit_inO : ComputableTidilyInO (fun s : CSt => gEmit s.1) eCSt enc public lemma cCont_inO : ComputableTidilyInO (fun s : CSt => s.1.1.1.2.state.isSome) eCSt encBool (fun s => ((eCSt s).length + 1) ^ 3) fun s => (eCSt s).length + 1 := (((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear - (state_inO.comp_linear (fst eCtl (encPair encNat encUnary)).fst'.fst'.snd'))).mono 1 + -- bridge for #862: tidy client of the plain `state_inO` + (state_inO.tidy.comp_linear (fst eCtl (encPair encNat encUnary)).fst'.fst'.snd'))).mono 1 (fun s => by have hL : (eCSt s).length + 1 ≤ ((eCSt s).length + 1) ^ 3 := Nat.le_self_pow (by norm_num) _ dsimp only [eCSt] at * diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean index 99dd2094b..bd5ab2cc9 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean @@ -423,7 +423,7 @@ lemma wTime_le (s : St) : wTime (s.1, symAt s) ≤ 9 * ((eSt s).length + 1) ^ 3 Nat.mul_le_mul (Nat.mul_le_mul hl (by omega)) (by omega) have hdigits := Nat.pow_le_pow_left (Nat.succ_le_succ hpos) 2 unfold wTime - dsimp only at hproduct hdigits ⊢ + dsimp only [WCtx.desc, WCtx.cfg] at hproduct hdigits ⊢ nlinarith [Nat.le_self_pow (show 2 ≠ 0 by decide) ((eSt s).length + 1)] /-- The step at the end of a pass. -/ @@ -446,7 +446,8 @@ public lemma stepAt_inO : ComputableTidilyInO stepAt eSt (encPair eCfg eSym) (enc := eSym)).inO_one.comp_linear hcur)).of_enc_eq fun s => by simp only [symAt, Function.comp_apply] split_ifs <;> simp_all - have hstep := stepWith_inO.comp (hdc.prod hsym) + -- bridge for #862: tidy client of the plain `stepWith_inO` + have hstep := stepWith_inO.tidy.comp (hdc.prod hsym) have hidle := hc.prod (const (encMid := eSym) none) refine (((ComputableInO.natIsZero.tidy.comp_linear hr).ite hidle hstep).of_enc_eq (g := stepAt) fun s => ?_).mono 100 (fun s => ?_) fun s => ?_ @@ -527,7 +528,8 @@ public lemma foldFinish_inO : ComputableTidilyInO foldFinish eSt eHalted refine (((ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := eHalted) fun b : Bool => !b).inO_one.comp_linear ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear - (state_inO.comp_linear hc))).of_enc_eq (g := foldFinish) fun s => by + -- bridge for #862: tidy client of the plain `state_inO` + (state_inO.tidy.comp_linear hc))).of_enc_eq (g := foldFinish) fun s => by simp only [foldFinish, Function.comp_apply] cases s.1.2.state <;> rfl).mono 1 (fun s => ?_) fun s => ?_ <;> · have hL : (eSt s).length + 1 ≤ ((eSt s).length + 1) ^ 3 := Nat.le_self_pow (by norm_num) _ diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean index 0e31d1e17..d256c024b 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/Machine.lean @@ -75,7 +75,8 @@ lemma round_inO : ComputableTidilyInO round eRun eRun (fun s => stepTime s.1 + ( fun s => (eRun s).length := by have hctx := fst eCtx (encList encUnary) have hout := snd eCtx (encList encUnary) - have hstep := step_inO.comp hctx + -- bridge for #862: tidy client of the plain `step_inO` + have hstep := step_inO.tidy.comp hctx have hnewout := ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear hstep.snd').ite ((ComputableTidilyInDegree.snoc encUnary).inO_one.comp_linear (hout.prod ((ComputableTidilyInDegree.getD (enc₁ := encUnary) 0).inO_one.comp_linear @@ -206,7 +207,8 @@ public theorem computableTidilyInO_universal : exact length_eRun_le i.1 i.2.1 hk)).tidy have hhalted := (ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool) (fun b : Bool => !b)).inO_one.comp_linear ((ComputableTidilyInDegree.isSome encUnary).inO_one - |>.comp_linear (state_inO.comp_linear hiter.fst'.snd')) + -- bridge for #862: tidy client of the plain `state_inO` + |>.comp_linear (state_inO.tidy.comp_linear hiter.fst'.snd')) refine ((hiter.snd'.prod hhalted).mono 16 (fun i => ?_) fun i => ?_).of_enc_eq fun i => ?_ · have h₁ : (eDesc i.1).length ≤ (eIn i).length := length_le_encPair_left _ _ i have h₂ := Nat.pow_le_pow_left (Nat.add_le_add_right h₁ 1) 2 diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean index 0d137351e..2f45c6174 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean @@ -516,7 +516,8 @@ private lemma foldFinishS_inO : ComputableTidilyInO foldFinishS eSSt eOut (fun s => ((eSSt s).length + 1) ^ 3) fun s => (eSSt s).length + 1 := by have h₁ := fst eSt (encPair encUnary (encList encUnary)) have h₂ := snd eSt (encPair encUnary (encList encUnary)) - have hst := state_inO.comp_linear h₁.fst'.snd' + -- bridge for #862: tidy client of the plain `state_inO` + have hst := state_inO.tidy.comp_linear h₁.fst'.snd' have hnone := (ComputableTidilyInDegree.of_finite (encIn := encBool) (encMid := encBool) fun b : Bool => !b).inO_one.comp_linear ((ComputableTidilyInDegree.isSome encUnary).inO_one.comp_linear hst) diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index b68c38f04..80955f025 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -53,7 +53,6 @@ "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 5, "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/QueryTake.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean": 6, "Complexity/Computability/Machines/Turing/MultiTape/Universal/Compose.lean": 7, "Complexity/Computability/Machines/Turing/MultiTape/Universal/Decode.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Universal/InPlace.lean": 9,