Skip to content

feat(BigO): plain findWith, filterWith and mapWith #1773

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 30, 2026
Merged

feat(BigO): plain findWith, filterWith and mapWith #1773

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
1 change: 1 addition & 0 deletions Complexity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
126 changes: 1 addition & 125 deletions Complexity/Computability/GenericRAM/SparseMemory/Turing.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
Loading
Loading