List functions in polynomial time for the repeated tailored verifier

The pure stages of the repeated programs (issue #280) cut questions and answers into blocks and put the coordinates' outputs together. The functions they need, as PolyTimeFuns:

• flattenF, the concatenation of a list of lists;
• blocksF, the k blocks of s elements of a list (blocks), with s and k in unary;
• cutF, a list cut into consecutive pieces of given lengths (cut), the lengths in unary.

theorem MIPRE.Tailored.RepProg.esize_drop_le {α : Type u_1} [Cost.SizedEncoding α] (l : List α) (n : ℕ) : Cost.esize (List.drop n l) ≤ Cost.esize l

theorem MIPRE.Tailored.RepProg.esize_take_le {α : Type u_1} [Cost.SizedEncoding α] (l : List α) (n : ℕ) : Cost.esize (List.take n l) ≤ Cost.esize l

Concatenation

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

The concatenation of a list of lists.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.flattenF_apply {α : Type u_1} [Cost.SizedEncoding α] (l : List (List α)) : flattenF.toFun l = l.flatten

Blocks of equal length

def MIPRE.Tailored.RepProg.blocks {α : Type u_1} (l : List α) (s k : ℕ) : List (List α)

The k blocks of s elements of l: its i-th block is chunk s i l.

Equations

• MIPRE.Tailored.RepProg.blocks l s k = List.ofFn fun (i : Fin k) => MIPRE.Cost.Data.chunk s (↑i) l

@[simp]

theorem MIPRE.Tailored.RepProg.length_blocks {α : Type u_1} [Cost.SizedEncoding α] (l : List α) (s k : ℕ) : (blocks l s k).length = k

noncomputable def MIPRE.Tailored.RepProg.dropStepF {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun (List α × Cost.Unary) (List α × Cost.Unary)

The step of the block cutter: drop a block.

Equations

• MIPRE.Tailored.RepProg.dropStepF = MIPRE.Cost.PolyTimeFun.drop.pair MIPRE.Cost.PolyTimeFun.snd

@[simp]

theorem MIPRE.Tailored.RepProg.dropStepF_apply {α : Type u_1} [Cost.SizedEncoding α] (p : List α × Cost.Unary) : dropStepF.toFun p = (List.drop (List.length p.2) p.1, p.2)

theorem MIPRE.Tailored.RepProg.iterate_dropStepF {α : Type u_1} [Cost.SizedEncoding α] (p : List α × Cost.Unary) (i : ℕ) : dropStepF.toFun^[i] p = (List.drop (i * List.length p.2) p.1, p.2)

noncomputable def MIPRE.Tailored.RepProg.blocksF {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun ((List α × Cost.Unary) × Cost.Unary) (List (List α))

The k blocks of s elements, with s and k in unary.

Equations

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

@[simp]

theorem MIPRE.Tailored.RepProg.blocksF_apply {α : Type u_1} [Cost.SizedEncoding α] (l : List α) (us uk : Cost.Unary) : blocksF.toFun ((l, us), uk) = blocks l (List.length us) (List.length uk)

Consecutive pieces of given lengths

def MIPRE.Tailored.RepProg.cut {α : Type u_1} (l : List α) : List ℕ → List (List α)

l cut into consecutive pieces of the lengths ns; the pieces past the end of l are short or empty.

Equations

• MIPRE.Tailored.RepProg.cut l [] = []
• MIPRE.Tailored.RepProg.cut l (n :: ns) = List.take n l :: MIPRE.Tailored.RepProg.cut (List.drop n l) ns