Direct plain list primitives

Finite-state word transducers implement unary successor and append a framed element to a list. Their machine clocks are linear and use no work tapes. The proofs do not invoke a tidy computability calculus.

theorem Turing.MultiTapeTM.foldlMap {α β : Type} (f : α → β) (list : List α) (acc : List β) : List.foldl (fun (mapped : List β) (value : α) => mapped ++ [f value]) acc list = acc ++ List.map f list

Appending mapped elements in a left fold retains the initial output prefix.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_succ : ComputableInPolyTime (fun (x : ℕ) => x + 1) encUnary encUnary

Unary successor is a direct finite-state transduction, including the empty word for zero.

theorem Turing.MultiTapeTM.ComputableInPolyTime.snoc {α : Type} (enc : α ↪ List Bool) : ComputableInPolyTime (fun (p : List α × α) => p.1 ++ [p.2]) (encPair (encList enc) enc) (encList enc)

Append one element to a framed list, for an arbitrary fixed element encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsCons {γ : Type} {input : γ ↪ List Bool} {head : γ → Bool} {tail : γ → List Bool} (hhead : ComputableInPolyTime head input encBool) (htail : ComputableInPolyTime tail input encBits) : ComputableInPolyTime (fun (x : γ) => head x :: tail x) input encBits

Prepend a computed bit to a computed word, retaining both input certificates.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsReverse : ComputableInPolyTime List.reverse encBits encBits

Reverse arbitrary bit strings with the direct prefix-bounded fold.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsTail : ComputableInPolyTime List.tail encBits encBits

Drop one symbol of an arbitrary word, reusing the existing word-codec machine.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsIsEmpty : ComputableInPolyTime List.isEmpty encBits encBool

Test whether the complete raw word is empty, with the Boolean result encoding fixed.

theorem Turing.MultiTapeTM.ComputableInPolyTime.range : ComputableInPolyTime List.range encUnary (encList encUnary)

Enumerate all naturals below a unary bound. Both the bound and each list element remain unary; the reachable framed output has quadratic length.

theorem Turing.MultiTapeTM.ComputableInPolyTime.allWithInput {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} {test : γ → α → Bool} {list : γ → List α} (hlist : ComputableInPolyTime list encIn (encList encA)) (htest : ComputableInPolyTime (fun (p : γ × α) => test p.1 p.2) (encPair encIn encA) encBool) : ComputableInPolyTime (fun (x : γ) => (list x).all (test x)) encIn encBool

Test all elements of a computed framed list with the full original input captured by the uniform callback machine. No finite-element assumption is needed.

theorem Turing.MultiTapeTM.ComputableInPolyTime.allConst {γ : Type} {encIn : γ ↪ List Bool} {ι : Type u_1} (l : List ι) {test : γ → ι → Bool} (htest : ∀ i ∈ l, ComputableInPolyTime (fun (x : γ) => test x i) encIn encBool) : ComputableInPolyTime (fun (x : γ) => l.all (test x)) encIn encBool

For a fixed list, only its members need callback certificates. The index type may live in any universe and needs neither an encoding nor a finite-type instance.

theorem Turing.MultiTapeTM.ComputableInPolyTime.map {α β : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {f : α → β} (hf : ComputableInPolyTime f encA encB) : ComputableInPolyTime (List.map f) (encList encA) (encList encB)

Mapping a uniform encoded function over a runtime framed list is polynomial-time. The callback's output bound follows from its actual machine, rather than an extra list premise.

theorem Turing.MultiTapeTM.ComputableInPolyTime.bitsReverseWithInput {γ : Type} {encIn : γ ↪ List Bool} {word : γ → List Bool} (hword : ComputableInPolyTime word encIn encBits) : ComputableInPolyTime (fun (a : γ) => (word a).reverse) encIn encBits

Reverse a computed word, fixing its raw intermediate encoding before proof search. The input certificate may itself convert from another representation.

theorem Turing.MultiTapeTM.ComputableInPolyTime.cons' {γ α : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {head : γ → α} {tail : γ → List α} (hhead : ComputableInPolyTime head encIn encA) (htail : ComputableInPolyTime tail encIn (encList encA)) : ComputableInPolyTime (fun (x : γ) => head x :: tail x) encIn (encList encA)

Prepend computed data. The result encoding determines the element encoding before fun_prop searches for the two component certificates.

theorem Turing.MultiTapeTM.ComputableInPolyTime.listAppend' {γ α : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {left right : γ → List α} (hleft : ComputableInPolyTime left encIn (encList encA)) (hright : ComputableInPolyTime right encIn (encList encA)) : ComputableInPolyTime (fun (x : γ) => left x ++ right x) encIn (encList encA)

Concatenate computed lists, inferring their shared encoding from the result.

theorem Turing.MultiTapeTM.ComputableInPolyTime.listReverseWithInput {γ α : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {list : γ → List α} (hlist : ComputableInPolyTime list encIn (encList encA)) : ComputableInPolyTime (fun (a : γ) => (list a).reverse) encIn (encList encA)

Reverse a computed framed list, inferring its element encoding from the result.

theorem Turing.MultiTapeTM.ComputableInPolyTime.unary_range' {α : Type} {input : α ↪ List Bool} {n : α → ℕ} (hn : ComputableInPolyTime n input encUnary) : ComputableInPolyTime (fun (a : α) => List.range (n a)) input (encList encUnary)

Enumerate 0, …, n a - 1 for a computed unary bound, fixing the intermediate encoding.