List operations with bounds of given degrees

Operations on lists encoded by Turing.MultiTapeTM.encList, with explicit degrees (Turing.MultiTapeTM.ComputableTidilyInDegree): adding an element at either end and concatenation in linear time; finding the first element that passes a test and keeping the elements that pass a test, one degree above the test. The tests may depend on a parameter.

Main results

• Turing.MultiTapeTM.ComputableTidilyInDegree.cons, .snoc, .listAppend.
• Turing.MultiTapeTM.ComputableTidilyInDegree.findWith: the first element passing a test.
• Turing.MultiTapeTM.ComputableTidilyInDegree.filterWith: the elements passing a test.

@[simp]

theorem Turing.MultiTapeTM.encList_append {α : Type} (enc : α ↪ List Bool) (l₁ l₂ : List α) : (encList enc) (l₁ ++ l₂) = (encList enc) l₁ ++ (encList enc) l₂

theorem Turing.MultiTapeTM.length_encList_take_le {α : Type} (enc : α ↪ List Bool) (l : List α) (i : ℕ) : ((encList enc) (List.take i l)).length ≤ ((encList enc) l).length

A prefix is no longer than the list.

theorem Turing.MultiTapeTM.length_le_encList_of_mem {α : Type} (enc : α ↪ List Bool) {l : List α} {a : α} (h : a ∈ l) : (enc a).length ≤ ((encList enc) l).length

An element is no longer than the encoded list.

theorem Turing.MultiTapeTM.length_le_length_encList {α : Type u_1} (enc : α ↪ List Bool) (l : List α) : l.length ≤ ((encList enc) l).length

The number of elements is at most the length of the encoded list.

theorem Turing.MultiTapeTM.length_encOption_find?_le {α : Type} (enc : α ↪ List Bool) (p : α → Bool) (l : List α) : ((encOption enc) (List.find? p l)).length ≤ ((encList enc) l).length + 1

The element found in a list is no longer than the encoded list.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.cons {α : Type} (enc : α ↪ List Bool) : ComputableTidilyInDegree (fun (p : α × List α) => p.1 :: p.2) (encPair enc (encList enc)) (encList enc) 1 1

Adding an element in front: the identity on encoded words.

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

Adding an element at the end.

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

Concatenation.

Finding and filtering

def Turing.MultiTapeTM.ComputableTidilyInDegree.findStep {α π : Type} (t : π × α → Bool) (p : π) (acc : Option α) (a : α) : Option α

One step of finding the first element passing the test t.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.foldl_findStep {α π : Type} (t : π × α → Bool) (p : π) (l : List α) (acc : Option α) : List.foldl (findStep t p) acc l = acc.or (List.find? (fun (a : α) => t (p, a)) l)

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.findWith {α γ : Type} {encIn : γ ↪ List Bool} {π : Type} {encP : π ↪ List Bool} {enc : α ↪ List Bool} {dt et dP eP dL : ℕ} {t : π × α → Bool} {par : γ → π} {list : γ → List α} (ht : ComputableTidilyInDegree t (encPair encP enc) encBool dt et) (hpar : ComputableTidilyInDegree par encIn encP dP eP) (hlist : ComputableTidilyInDegree list encIn (encList enc) dL 1) : ComputableTidilyInDegree (fun (x : γ) => List.find? (fun (a : α) => t (par x, a)) (list x)) encIn (encOption enc) (max (max dL dP) (1 + max 1 dt * max 1 eP)) 1

The first element of list x passing the test t with the parameter par x, for a list of linear size.

def Turing.MultiTapeTM.ComputableTidilyInDegree.filterStep {α π : Type} (t : π × α → Bool) (p : π) (acc : List α) (a : α) : List α

One step of keeping the elements that pass the test t.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.foldl_filterStep {α π : Type} (t : π × α → Bool) (p : π) (l acc : List α) : List.foldl (filterStep t p) acc l = acc ++ List.filter (fun (a : α) => t (p, a)) l

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.length_encList_filter_le {α : Type} (enc : α ↪ List Bool) (f : α → Bool) (l : List α) : ((encList enc) (List.filter f l)).length ≤ ((encList enc) l).length

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.filterWith {α γ : Type} {encIn : γ ↪ List Bool} {π : Type} {encP : π ↪ List Bool} {enc : α ↪ List Bool} {dt et dP eP dL : ℕ} {t : π × α → Bool} {par : γ → π} {list : γ → List α} (ht : ComputableTidilyInDegree t (encPair encP enc) encBool dt et) (hpar : ComputableTidilyInDegree par encIn encP dP eP) (hlist : ComputableTidilyInDegree list encIn (encList enc) dL 1) : ComputableTidilyInDegree (fun (x : γ) => List.filter (fun (a : α) => t (par x, a)) (list x)) encIn (encList enc) (max (max dL dP) (1 + max 1 dt * max 1 eP)) 1

The elements of list x passing the test t with the parameter par x, for a list of linear size.

def Turing.MultiTapeTM.ComputableTidilyInDegree.mapStep {α π β : Type} (f : π × α → β) (p : π) (acc : List β) (a : α) : List β

One step of mapping with the parameter p.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.foldl_mapStep {α π β : Type} (f : π × α → β) (p : π) (l : List α) (acc : List β) : List.foldl (mapStep f p) acc l = acc ++ List.map (fun (a : α) => f (p, a)) l

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.mapWith {α γ : Type} {encIn : γ ↪ List Bool} {π : Type} {encP : π ↪ List Bool} {enc : α ↪ List Bool} {dP dL : ℕ} {β : Type} {encB : β ↪ List Bool} {f : π × α → β} {par : γ → π} {list : γ → List α} {df ef : ℕ} (hf : ComputableTidilyInDegree f (encPair encP enc) encB df ef) (hpar : ComputableTidilyInDegree par encIn encP dP 1) (hlist : ComputableTidilyInDegree list encIn (encList enc) dL 1) : ComputableTidilyInDegree (fun (x : γ) => List.map (fun (a : α) => f (par x, a)) (list x)) encIn (encList encB) (max (max dL dP) (1 + max 1 (max df ef) * (ef + 1))) (ef + 1)

Mapping f with the parameter par x over list x, for a parameter and a list of linear size.

Arithmetic on unary numbers and integers

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.unary_sub : ComputableTidilyInDegree (fun (p : ℕ × ℕ) => p.1 - p.2) (encPair encUnary encUnary) encUnary 2 1

Truncated subtraction of unary numbers.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.unary_min : ComputableTidilyInDegree (fun (p : ℕ × ℕ) => min p.1 p.2) (encPair encUnary encUnary) encUnary 2 1

The minimum of unary numbers.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.int_pos : ComputableTidilyInDegree (fun (z : ℤ) => decide (0 < z)) encIntUnary encBool 1 0

Whether an integer is positive.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.int_neg : ComputableTidilyInDegree (fun (z : ℤ) => decide (z < 0)) encIntUnary encBool 1 1

Whether an integer is negative.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.isSome {α : Type} (enc : α ↪ List Bool) : ComputableTidilyInDegree (fun (o : Option α) => o.isSome) (encOption enc) encBool 1 0

Whether an option holds a value.

theorem Turing.MultiTapeTM.ComputableTidilyInDegree.replicate {α : Type} (enc : α ↪ List Bool) : ComputableTidilyInDegree (fun (p : ℕ × α) => List.replicate p.1 p.2) (encPair encUnary enc) (encList enc) 3 2

A list of n copies of an element.