Skip to content

refactor(machines): retire superseded tidy list combinators #2008

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 1 commit into from
Oct 31, 2026
Merged

refactor(machines): retire superseded tidy list combinators #2008

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
206 changes: 2 additions & 204 deletions Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ Authors: Christian Reitwiessner
module
-- upstream: vendored crei:crei/tidy-universal @7f7c0696 (unsubmitted)
-- vendored: use core's fold homomorphism law for the captured-parameter identity.
-- vendored: retire superseded tidy list combinators; plain rules live in BigO/Lists.

public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Bounds
public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
Expand Down Expand Up @@ -39,9 +40,7 @@ space. The encoded value counts towards the space since a combinator keeps it on
## Main results

* `Turing.MultiTapeTM.ComputableTidilyInO.comp`, `.ite`, `.prod`: closure properties.
* `Turing.MultiTapeTM.ComputableTidilyInO.foldl`, `.foldlWith`: left folds.
* `Turing.MultiTapeTM.ComputableTidilyInO.findWith`, `.filterWith`, `.mapWith`: list operations
with a parameter.
* `Turing.MultiTapeTM.ComputableTidilyInO.foldl`, `.foldlWith`: left folds with a parameter.
* `Turing.MultiTapeTM.ComputableTidilyInDegree.inO`: bounds of a given degree.
-/

Expand Down Expand Up @@ -367,207 +366,6 @@ public theorem foldlWith [ListEncoding encA encL] [hS : SizedListEncoding encA e

end Fold

/-! ### Finding, filtering and mapping -/

section Lists

open ComputableTidilyInDegree (findStep foldl_findStep filterStep foldl_filterStep mapStep
foldl_mapStep length_encList_filter_le isSome optionSome snoc)

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`. -/
public theorem findWith {t : π × α → Bool} {Tt St : π × α → ℕ}
(ht : ComputableTidilyInO t (encPair encP enc) encBool Tt St)
(hpar : ComputableTidilyInO par encIn encP Tp Sp)
(hlist : ComputableTidilyInO list encIn (encList enc) Tl Sl) :
ComputableTidilyInO (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
-- the step, as a function of `((p, acc), a)`
have hq := fst (encPair encP (encOption enc)) enc
have hel := snd (encPair encP (encOption enc)) enc
have hisSome := (isSome enc).inO_one.comp_linear hq.snd'
have h := hisSome.ite hq.snd' ((ht.comp (hq.fst'.prod hel)).ite
((optionSome (enc₁ := enc)).inO_one.comp_linear hel) (const none))
have hstep : ComputableTidilyInO (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 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_findStep, Option.none_or]

/-- The elements of `list x` passing the test `t` with the parameter `par x`. -/
public theorem filterWith {t : π × α → Bool} {Tt St : π × α → ℕ}
(ht : ComputableTidilyInO t (encPair encP enc) encBool Tt St)
(hpar : ComputableTidilyInO par encIn encP Tp Sp)
(hlist : ComputableTidilyInO list encIn (encList enc) Tl Sl) :
ComputableTidilyInO (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
((snoc enc).inO_one.comp_linear (hq.snd'.prod hel)) hq.snd'
have hstep : ComputableTidilyInO
(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 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_filterStep, List.nil_append]

/-- Mapping `f` with the parameter `par x` over `list x`. -/
public theorem mapWith {f : π × α → β} {Tf Sf : π × α → ℕ}
(hf : ComputableTidilyInO f (encPair encP enc) encB Tf Sf)
(hpar : ComputableTidilyInO par encIn encP Tp Sp)
(hlist : ComputableTidilyInO list encIn (encList enc) Tl Sl) :
ComputableTidilyInO (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 := (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 : ComputableTidilyInO (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 Lists

end ComputableTidilyInO

end Turing.MultiTapeTM
7 changes: 3 additions & 4 deletions Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Lists.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,7 @@ 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
One left fold over `list x` 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.

Expand All @@ -28,8 +27,8 @@ the accumulator and the largest cost of the test or function on an element.

## References

Restates Christian Reitwiessner's tidy list combinators
(`Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean`) in the plain calculus.
Derived from Christian Reitwiessner's original list-combinator construction, using the plain
fold rules and independent time and workspace bounds.
-/

public section
Expand Down
57 changes: 5 additions & 52 deletions Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ module
public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.InSpace.Plain
public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Lists
public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length
import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Lists
import Complexity.Computability.Machines.Turing.MultiTape.Internal.DegreeOptionPrimitives
import Complexity.Computability.Machines.Turing.MultiTape.Internal.EqualityPrimitives

Expand Down Expand Up @@ -511,43 +512,10 @@ theorem mapWith {π κ : Type} {encP : π ↪ List Bool} {encK : κ ↪ List Boo
(encList enc (list x)).length +
(encList encK ((list x).map fun a => f (par x, a))).length +
listMax (fun a => Sf (par x, a)) (list x) := by
have hfold_eq (p : π) (l : List ε) (acc : List κ) :
l.foldl (fun acc a => acc ++ [f (p, a)]) acc = acc ++ l.map (fun a => f (p, a)) := by
induction l generalizing acc with
| nil => simp
| cons a l ih => simp [ih, List.append_assoc]
have hq := fst (encPair encP (encList encK)) enc
have hel := snd (encPair encP (encList encK)) enc
obtain ⟨c, hc⟩ := hf.length_le
have hstep : ComputableInSpace (fun q : (π × List κ) × ε => q.1.2 ++ [f (q.1.1, q.2)])
(encPair (encPair encP (encList encK)) enc) (encList encK)
fun q => (encPair (encPair encP (encList encK)) enc q).length + Sf (q.1.1, q.2) :=
((snoc encK).comp ((snd' hq).prod (hf.comp ((fst' hq).prod hel)))).weaken
⟨2 * c + 6, fun q => by
have := hc (q.1.1, q.2)
simp only [length_encPair] at this ⊢
nlinarith⟩
have hst (x : α) (i : ℕ) :
(encList encK (((list x).take i).foldl (fun acc a => acc ++ [f (par x, a)]) [])).length ≤
(encList encK ((list x).map fun a => f (par x, a))).length := by
rw [hfold_eq, List.nil_append, List.map_take]
exact length_encList_take_le encK _ _
have hfold := foldlWith (encL := encList enc) (encB := encList encK)
(step := fun p acc a => acc ++ [f (p, a)]) hpar hlist (const []) hstep
(Q := fun x => 4 * (encP (par x)).length +
3 * (encList enc (list x)).length +
3 * (encList encK ((list x).map fun a => f (par x, a))).length + 5 +
listMax (fun a => Sf (par x, a)) (list x))
(B := fun x => (encList encK ((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 => Sf (par x, a)) (List.getElem_mem hi)
have h₃ := hst x i
simp only [length_encPair] at h₂ ⊢
omega)
(fun x i _ => hst x i)
refine (hfold.weaken ⟨6, fun x => by dsimp only; omega⟩).of_enc_eq fun x => ?_
rw [hfold_eq, List.nil_append]
obtain ⟨_, hf⟩ := hf.exists_inO
obtain ⟨_, hpar⟩ := hpar.exists_inO
obtain ⟨_, hlist⟩ := hlist.exists_inO
exact of_inO (ComputableInO.mapWith hf hpar hlist)

end Generic

Expand Down Expand Up @@ -872,21 +840,6 @@ theorem length :
fun l => 8 * ((encList enc l).length + 1) :=
ComputableInSpace.length.tidy

theorem mapWith {π κ : Type} {encP : π ↪ List Bool} {encK : κ ↪ List Bool} {f : π × ε → κ}
{Sf : π × ε → ℕ} {par : α → π} {list : α → List ε} {Sp Sl : α → ℕ}
(hf : ComputableTidilyInSpace f (encPair encP enc) encK Sf)
(hpar : ComputableTidilyInSpace par encIn encP Sp)
(hlist : ComputableTidilyInSpace list encIn (encList enc) Sl) :
ComputableTidilyInSpace (fun x => (list x).map fun a => f (par x, a)) encIn (encList encK)
fun x => (encIn x).length + Sp x + Sl x + (encP (par x)).length +
(encList enc (list x)).length +
(encList encK ((list x).map fun a => f (par x, a))).length +
listMax (fun a => Sf (par x, a)) (list x) :=
let ⟨_, hf⟩ := hf
let ⟨_, hpar⟩ := hpar
let ⟨_, hlist⟩ := hlist
⟨_, ComputableTidilyInO.mapWith hf hpar hlist⟩

end Generic

section BudgetOps
Expand Down
21 changes: 21 additions & 0 deletions ComplexityTests/InSpacePlain.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,4 +114,25 @@ theorem countUp_polySpace : ComputableInPolySpace countUp encNat encNat := by
example (n : ℕ) : countUp n = n := by
simp [countUp, ComputableInO.iterate_succ_eq]

/-- Mapping may use a captured parameter; the resulting list remains charged to space. -/
def fill (p : Bool × List Bool) : List Bool := p.2.map fun _ => p.1

theorem fill_inSpace :
ComputableInSpace fill (encPair encBool (encList encBool)) (encList encBool)
fun p => 8 * ((encPair encBool (encList encBool) p).length + 1) := by
have hlen (xs : List Bool) : (encList encBool xs).length = 3 * xs.length := by
simp [length_encList, encBool_apply, Nat.mul_comm]
apply (ComputableInSpace.mapWith (ComputableInSpace.fst encBool encBool)
(ComputableInSpace.fst encBool (encList encBool))
(ComputableInSpace.snd encBool (encList encBool))).mono_le
intro p
have hmax : listMax (fun a : Bool => (encPair encBool encBool (p.1, a)).length) p.2 ≤ 5 :=
listMax_le fun a _ => by simp [encBool_apply]
simp only [length_encPair, encBool_apply, List.length_singleton, hlen, List.length_map] at hmax ⊢
omega

example : fill (true, [false, true, false]) = [true, true, true] := rfl
example : fill (false, [true, false]) = [false, false] := rfl
example : fill (true, []) = [] := rfl

end ComplexityTests.InSpacePlain
4 changes: 2 additions & 2 deletions scripts/tidy_surface_baseline.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,14 @@
"Complexity/Computability/Machines/ReadMachine/Tidy.lean": 2,
"Complexity/Computability/Machines/Turing/MultiTape/Combinators/Encoding.lean": 8,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/Arith.lean": 2,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean": 32,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO.lean": 29,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Plain.lean": 2,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree.lean": 24,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/Fold.lean": 2,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean": 16,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Bit.lean": 1,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean": 3,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 45,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 44,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean": 12,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace.lean": 2,
"Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean": 11,
Expand Down
Loading