The closure library, part IV: folds over lists

The generic iteration combinator of the library, PolyTimeFun.foldl: a fold of a polynomial-time body over a list is polynomial-time provided the accumulator grows by at most an additive polynomial in the element at each step (the Cobham condition esize (F (s, a)) ≤ esize s + B (esize a)), and from it cons, casesList, map, zip, append, replicate and reverse (planning/succinct-cook-levin.md, S3). Every combinator's toFun is the corresponding List function, so that a program assembled from them is defined by its mathematical meaning and only its time bound is inherited.

Lists of an arbitrary encodable type encode as cons-chains of the encodings (instSizedEncodingList, at low priority so that the existing instances for bit strings and gate lists are still found first; they agree definitionally).

Lists of encodable values

@[instance_reducible, instance 100]

instance MIPRE.Cost.instSizedEncodingList {α : Type u_1} [SizedEncoding α] : SizedEncoding (List α)

Lists encode elementwise, as cons-chains.

Equations

• MIPRE.Cost.instSizedEncodingList = { encode := MIPRE.Cost.Data.ofList MIPRE.Cost.encode, decode := MIPRE.Cost.Data.toList? MIPRE.Cost.decode, decode_encode := ⋯ }

theorem MIPRE.Cost.encode_list_nil {α : Type u_1} [SizedEncoding α] : encode [] = Data.nil

theorem MIPRE.Cost.encode_list_cons {α : Type u_1} [SizedEncoding α] (a : α) (l : List α) : encode (a :: l) = (encode a).cons (encode l)

theorem MIPRE.Cost.encode_list_eq_list {α : Type u_1} [SizedEncoding α] (l : List α) : encode l = Data.list (List.map encode l)

@[simp]

theorem MIPRE.Cost.esize_list_nil {α : Type u_1} [SizedEncoding α] : esize [] = 1

@[simp]

theorem MIPRE.Cost.esize_list_cons {α : Type u_1} [SizedEncoding α] (a : α) (l : List α) : esize (a :: l) = esize a + esize l + 1

theorem MIPRE.Cost.esize_mem_le {α : Type u_1} [SizedEncoding α] {a : α} {l : List α} (h : a ∈ l) : esize a + 1 ≤ esize l

theorem MIPRE.Cost.length_le_esize_list {α : Type u_1} [SizedEncoding α] (l : List α) : l.length ≤ esize l

theorem MIPRE.Cost.esize_list_append {α : Type u_1} [SizedEncoding α] (l₁ l₂ : List α) : esize (l₁ ++ l₂) + 1 = esize l₁ + esize l₂

theorem MIPRE.Cost.esize_list_reverse {α : Type u_1} [SizedEncoding α] (l : List α) : esize l.reverse = esize l

Program layer: the fold loop

def MIPRE.Cost.Prog.foldBody (F : Prog) : Prog

The body of the fold loop of F: on the state cons xs acc, stop with acc if xs is empty; otherwise bind acc' := F (acc, head xs) and continue with cons (tail xs) acc'.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Cost.Prog.foldBody_wellScoped {F : Prog} (hF : WellScoped 1 F) : WellScoped 1 F.foldBody

theorem MIPRE.Cost.Prog.foldBody_stop {F : Prog} (acc : Data) : Eval [Data.nil.cons acc] F.foldBody (Data.nil.cons acc) (acc.size + 5)

theorem MIPRE.Cost.Prog.foldBody_step {F : Prog} (hF : WellScoped 1 F) (h rest acc acc' : Data) (t : ℕ) (hrun : Eval [acc.cons h] F acc' t) : Eval [(h.cons rest).cons acc] F.foldBody ((Data.nil.cons Data.nil).cons (rest.cons acc')) (acc.size + h.size + rest.size + acc'.size + t + 14)

Function layer

@[reducible, inline]

abbrev MIPRE.Cost.PolyTimeFun.step {α : Type u_1} {σ : Type u_4} [SizedEncoding α] [SizedEncoding σ] (F : PolyTimeFun (σ × α) σ) (s : σ) (a : α) : σ

The step function of a fold, as a binary function.

Equations

• F.step s a = F.toFun (s, a)

theorem MIPRE.Cost.PolyTimeFun.foldl_esize_le {α : Type u_1} {σ : Type u_4} [SizedEncoding α] [SizedEncoding σ] (F : PolyTimeFun (σ × α) σ) (B : Polynomial ℕ) (hB : ∀ (s : σ) (a : α), esize (F.toFun (s, a)) ≤ esize s + Polynomial.eval (esize a) B) (l : List α) (s₀ : σ) (pre : List α) : pre ⊆ l → esize (List.foldl F.step s₀ pre) ≤ esize s₀ + pre.length * Polynomial.eval (esize l) B

The size bound along a fold under the additive Cobham condition: after consuming pre, the accumulator has size at most esize s₀ + |pre| · B (esize l) whenever the elements of pre are elements of l.

def MIPRE.Cost.PolyTimeFun.FoldBounded {α : Type u_1} {σ : Type u_4} [SizedEncoding α] [SizedEncoding σ] (F : PolyTimeFun (σ × α) σ) (B : Polynomial ℕ) : Prop

The Cobham condition for folding F over a list: along the fold of any list l from any s₀, the accumulator has size at most B (esize (l, s₀)).

Equations

• F.FoldBounded B = ∀ (l : List α) (s₀ : σ) (pre xs : List α), l = pre ++ xs → MIPRE.Cost.esize (List.foldl F.step s₀ pre) ≤ Polynomial.eval (MIPRE.Cost.esize (l, s₀)) B

theorem MIPRE.Cost.PolyTimeFun.foldBounded_of_additive {α : Type u_1} {σ : Type u_4} [SizedEncoding α] [SizedEncoding σ] (F : PolyTimeFun (σ × α) σ) (B : Polynomial ℕ) (hB : ∀ (s : σ) (a : α), esize (F.toFun (s, a)) ≤ esize s + Polynomial.eval (esize a) B) : F.FoldBounded (Polynomial.X + Polynomial.X * B)

The additive condition — each step grows the accumulator by at most B (esize a) — is a Cobham condition with the bound X + X · B.

noncomputable def MIPRE.Cost.PolyTimeFun.foldStepBound {α : Type u_1} {σ : Type u_4} [SizedEncoding α] [SizedEncoding σ] (F : PolyTimeFun (σ × α) σ) (B : Polynomial ℕ) : Polynomial ℕ

The per-iteration cost bound of the fold loop, as a polynomial in esize (l, s₀).

Equations

• F.foldStepBound B = F.timeBound.comp (B + Polynomial.X + 1) + 2 * B + 3 * Polynomial.X + Polynomial.C 14

noncomputable def MIPRE.Cost.PolyTimeFun.foldl {α : Type u_1} {σ : Type u_4} [SizedEncoding α] [SizedEncoding σ] (F : PolyTimeFun (σ × α) σ) (B : Polynomial ℕ) (hB : F.FoldBounded B) : PolyTimeFun (List α × σ) σ

Folding a polynomial-time body over a list, under the Cobham condition FoldBounded F B: foldl F B hB (l, s₀) = l.foldl (fun s a => F (s, a)) s₀. The loop state is the input pair itself.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.foldl_apply {α : Type u_1} {σ : Type u_4} [SizedEncoding α] [SizedEncoding σ] (F : PolyTimeFun (σ × α) σ) (B : Polynomial ℕ) (hB : F.FoldBounded B) (l : List α) (s₀ : σ) : (F.foldl B hB).toFun (l, s₀) = List.foldl (fun (s : σ) (a : α) => F.toFun (s, a)) s₀ l

noncomputable def MIPRE.Cost.PolyTimeFun.foldlAdd {α : Type u_1} {σ : Type u_4} [SizedEncoding α] [SizedEncoding σ] (F : PolyTimeFun (σ × α) σ) (B : Polynomial ℕ) (hB : ∀ (s : σ) (a : α), esize (F.toFun (s, a)) ≤ esize s + Polynomial.eval (esize a) B) : PolyTimeFun (List α × σ) σ

Folding under the additive condition.

Equations

• F.foldlAdd B hB = F.foldl (Polynomial.X + Polynomial.X * B) ⋯

@[simp]

theorem MIPRE.Cost.PolyTimeFun.foldlAdd_apply {α : Type u_1} {σ : Type u_4} [SizedEncoding α] [SizedEncoding σ] (F : PolyTimeFun (σ × α) σ) (B : Polynomial ℕ) (hB : ∀ (s : σ) (a : α), esize (F.toFun (s, a)) ≤ esize s + Polynomial.eval (esize a) B) (l : List α) (s₀ : σ) : (F.foldlAdd B hB).toFun (l, s₀) = List.foldl (fun (s : σ) (a : α) => F.toFun (s, a)) s₀ l

Derived combinators

noncomputable def MIPRE.Cost.PolyTimeFun.congr {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) (f : α → β) (h : ∀ (a : α), F.toFun a = f a) : PolyTimeFun α β

Replacing the function of a PolyTimeFun by an extensionally equal one.

Equations

• F.congr f h = { toFun := f, code := F.code, closed := ⋯, timeBound := F.timeBound, computes := ⋯ }

@[simp]

theorem MIPRE.Cost.PolyTimeFun.congr_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) (f : α → β) (h : ∀ (a : α), F.toFun a = f a) (a : α) : (F.congr f h).toFun a = f a

noncomputable def MIPRE.Cost.PolyTimeFun.ofEncodeEq {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (f : α → β) (h : ∀ (a : α), encode (f a) = encode a) : PolyTimeFun α β

A function whose output encodes exactly as its input is computed by var 0.

Equations

• MIPRE.Cost.PolyTimeFun.ofEncodeEq f h = { toFun := f, code := MIPRE.Cost.Prog.var 0, closed := Nat.zero_lt_one, timeBound := Polynomial.X + 1, computes := ⋯ }

@[simp]

theorem MIPRE.Cost.PolyTimeFun.ofEncodeEq_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (f : α → β) (h : ∀ (a : α), encode (f a) = encode a) (a : α) : (ofEncodeEq f h).toFun a = f a

noncomputable def MIPRE.Cost.PolyTimeFun.cast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun α β) (f : α → γ) (h : ∀ (a : α), encode (f a) = encode (F.toFun a)) : PolyTimeFun α γ

Retyping the output: a function whose values encode as the values of F is computed by the program of F.

Equations

• F.cast f h = { toFun := f, code := F.code, closed := ⋯, timeBound := F.timeBound, computes := ⋯ }

@[simp]

theorem MIPRE.Cost.PolyTimeFun.cast_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun α β) (f : α → γ) (h : ∀ (a : α), encode (f a) = encode (F.toFun a)) (a : α) : (F.cast f h).toFun a = f a

noncomputable def MIPRE.Cost.PolyTimeFun.cons {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) (G : PolyTimeFun α (List β)) : PolyTimeFun α (List β)

Consing.

Equations

• F.cons G = { toFun := fun (a : α) => F.toFun a :: G.toFun a, code := F.code.cons G.code, closed := ⋯, timeBound := F.timeBound + G.timeBound + 1, computes := ⋯ }

@[simp]

theorem MIPRE.Cost.PolyTimeFun.cons_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) (G : PolyTimeFun α (List β)) (a : α) : (F.cons G).toFun a = F.toFun a :: G.toFun a

noncomputable def MIPRE.Cost.PolyTimeFun.reverse {α : Type u_1} [SizedEncoding α] : PolyTimeFun (List α) (List α)

Reversal.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.reverse_apply {α : Type u_1} [SizedEncoding α] (l : List α) : reverse.toFun l = l.reverse

def MIPRE.Cost.PolyTimeFun.casesListFun {α : Type u_1} {β : Type u_2} {γ : Type u_3} (N : α → β) (K : α × γ × List γ → β) : α × List γ → β

Case analysis on a list: the function of casesList.

Equations

• MIPRE.Cost.PolyTimeFun.casesListFun N K (a, []) = N a
• MIPRE.Cost.PolyTimeFun.casesListFun N K (a, h :: t) = K (a, h, t)

noncomputable def MIPRE.Cost.PolyTimeFun.casesList {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (N : PolyTimeFun α β) (K : PolyTimeFun (α × γ × List γ) β) : PolyTimeFun (α × List γ) β

Case analysis on a list component: casesList N K (a, []) is N a and casesList N K (a, h :: t) is K (a, (h, t)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.casesList_nil {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (N : PolyTimeFun α β) (K : PolyTimeFun (α × γ × List γ) β) (a : α) : (N.casesList K).toFun (a, []) = N.toFun a

@[simp]

theorem MIPRE.Cost.PolyTimeFun.casesList_cons {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (N : PolyTimeFun α β) (K : PolyTimeFun (α × γ × List γ) β) (a : α) (h : γ) (t : List γ) : (N.casesList K).toFun (a, h :: t) = K.toFun (a, h, t)

The list functions underlying the combinators

theorem MIPRE.Cost.foldl_cons_map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) (init : List β) : (List.foldl (fun (acc : List β) (a : α) => f a :: acc) init l).reverse = init.reverse ++ List.map f l

The fold underlying map.

theorem MIPRE.Cost.foldl_cons_reverse {α : Type u_1} (l₁ l₂ : List α) : List.foldl (fun (acc : List α) (a : α) => a :: acc) l₂ l₁.reverse = l₁ ++ l₂

The fold underlying append.

def MIPRE.Cost.zipStep {α : Type u_1} {β : Type u_2} (s : List β × List (α × β)) (a : α) : List β × List (α × β)

The step of the zip fold: on the state (l₂, acc) and the element a, consume the head of l₂.

Equations

• MIPRE.Cost.zipStep s a = match s.1 with | [] => ([], s.2) | b :: l₂ => (l₂, (a, b) :: s.2)

theorem MIPRE.Cost.foldl_zipStep_nil {α : Type u_1} {β : Type u_2} (l : List α) (acc : List (α × β)) : List.foldl zipStep ([], acc) l = ([], acc)

theorem MIPRE.Cost.foldl_zipStep {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) (acc : List (α × β)) : (List.foldl zipStep (l₂, acc) l₁).2.reverse = acc.reverse ++ l₁.zip l₂

theorem MIPRE.Cost.foldl_replicate {β : Type u_2} (u : List Unit) (acc : List β) (b : β) : List.foldl (fun (s : List β × β) (x : Unit) => (s.2 :: s.1, s.2)) (acc, b) u = (List.replicate u.length b ++ acc, b)

The fold underlying replicate: the state carries the value to replicate.

noncomputable def MIPRE.Cost.PolyTimeFun.map {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) : PolyTimeFun (List α) (List β)

Mapping a polynomial-time function over a list.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.map_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (F : PolyTimeFun α β) (l : List α) : F.map.toFun l = List.map F.toFun l

noncomputable def MIPRE.Cost.PolyTimeFun.append {α : Type u_1} [SizedEncoding α] : PolyTimeFun (List α × List α) (List α)

Appending.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.append_apply {α : Type u_1} [SizedEncoding α] (p : List α × List α) : append.toFun p = p.1 ++ p.2

noncomputable def MIPRE.Cost.PolyTimeFun.zipStepF {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] : PolyTimeFun ((List β × List (α × β)) × α) (List β × List (α × β))

The zip step as a polynomial-time function.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.zipStepF_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (p : (List β × List (α × β)) × α) : zipStepF.toFun p = zipStep p.1 p.2

noncomputable def MIPRE.Cost.PolyTimeFun.zip {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] : PolyTimeFun (List α × List β) (List (α × β))

Zipping two lists.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.zip_apply {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (p : List α × List β) : zip.toFun p = p.1.zip p.2

Unary numerals as lists of units

@[instance_reducible]

instance MIPRE.Cost.instSizedEncodingUnit : SizedEncoding Unit

The unit encodes as the atom, so that a list of n units is the unary numeral Data.ofNat n.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev MIPRE.Cost.Unary : Type

Unary numerals: lists of units.

Equations

• MIPRE.Cost.Unary = List Unit

def MIPRE.Cost.unary (n : ℕ) : Unary

The unary numeral of n.

Equations

• MIPRE.Cost.unary n = List.replicate n ()

@[simp]

theorem MIPRE.Cost.length_unary (n : ℕ) : List.length (unary n) = n

theorem MIPRE.Cost.encode_unary (n : ℕ) : encode (unary n) = Data.ofNat n

@[simp]

theorem MIPRE.Cost.esize_unary (n : ℕ) : esize (unary n) = 2 * n + 1

theorem MIPRE.Cost.unary_add (a b : ℕ) : unary (a + b) = unary a ++ unary b

theorem MIPRE.Cost.unary_length (u : Unary) : unary (List.length u) = u

noncomputable def MIPRE.Cost.PolyTimeFun.length {α : Type u_1} [SizedEncoding α] : PolyTimeFun (List α) Unary

The length of a list, in unary.

Equations

• MIPRE.Cost.PolyTimeFun.length = (MIPRE.Cost.PolyTimeFun.const ()).map.congr (fun (l : List α) => MIPRE.Cost.unary l.length) ⋯

@[simp]

theorem MIPRE.Cost.PolyTimeFun.length_apply {α : Type u_1} [SizedEncoding α] (l : List α) : length.toFun l = unary l.length

noncomputable def MIPRE.Cost.PolyTimeFun.replicate {β : Type u_2} [SizedEncoding β] : PolyTimeFun (Unary × β) (List β)

replicate (u, b) = List.replicate |u| b, by a fold over the unary numeral u whose state carries b.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.replicate_apply {β : Type u_2} [SizedEncoding β] (p : Unary × β) : replicate.toFun p = List.replicate (List.length p.1) p.2

noncomputable def MIPRE.Cost.PolyTimeFun.mapWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun (α × β) γ) : PolyTimeFun (List α × β) (List γ)

Mapping with a parameter: mapWith F (l, c) = l.map (fun a => F (a, c)), by zipping l with copies of c.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.Cost.PolyTimeFun.mapWith_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SizedEncoding α] [SizedEncoding β] [SizedEncoding γ] (F : PolyTimeFun (α × β) γ) (p : List α × β) : F.mapWith.toFun p = List.map (fun (a : α) => F.toFun (a, p.2)) p.1