The answer-reduced decision, as a program

Piece AR-3e of planning/answer-reduction.md: polynomial-time functions computing the decision on blocks of MIPRE/Background/AnswerReduction/DecideSpec, each with the law that it computes its specification (verdictP_apply for the whole). The type-dependent control is a finite table of the type pair (PolyTimeFun.finiteFunction); the field arithmetic is the introspection stage programs'.

Cutting a list into runs

noncomputable def MIPRE.AnswerReduction.chunkStep : Cost.PolyTimeFun ((List Cost.BitStr × List (List Cost.BitStr)) × Cost.Unary) (List Cost.BitStr × List (List Cost.BitStr))

Equations

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

theorem MIPRE.AnswerReduction.chunkStep_apply (v : List Cost.BitStr) (vs : List (List Cost.BitStr)) (w : Cost.Unary) : chunkStep.toFun ((v, vs), w) = (List.drop (List.length w) v, List.take (List.length w) v :: vs)

theorem MIPRE.AnswerReduction.chunkStep_fold (n : ℕ) (w : Cost.Unary) (v : List Cost.BitStr) (vs : List (List Cost.BitStr)) : (List.foldl chunkStep.step (v, vs) (List.replicate n w)).2 = (chunks (List.length w) n v).reverse ++ vs

noncomputable def MIPRE.AnswerReduction.chunksProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × List Cost.BitStr) (List (List Cost.BitStr))

Cutting into runs, as a program: (n, w, l) ↦ chunks w n l.

Equations

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

@[simp]

theorem MIPRE.AnswerReduction.chunksProg_apply (n w : Cost.Unary) (l : List Cost.BitStr) : chunksProg.toFun (n, w, l) = chunks (List.length w) (List.length n) l

Reading a finite type

def MIPRE.AnswerReduction.decodeAmong {α : Type u_1} [Cost.SizedEncoding α] [Inhabited α] : List α → Cost.PolyTimeFun Cost.Data α

Reading a value among a list of candidates, by comparing encodings; the default otherwise.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.AnswerReduction.decodeAmong [] = MIPRE.Cost.PolyTimeFun.const default

theorem MIPRE.AnswerReduction.decodeAmong_encode {α : Type u_1} [Cost.SizedEncoding α] [Inhabited α] (l : List α) (a : α) (h : a ∈ l) : (decodeAmong l).toFun (Cost.encode a) = a

noncomputable def MIPRE.AnswerReduction.readFinite {α : Type u_1} [Cost.SizedEncoding α] [Inhabited α] [Fintype α] : Cost.PolyTimeFun Cost.Data α

Reading a value of a finite type off any datum.

Equations

• MIPRE.AnswerReduction.readFinite = MIPRE.AnswerReduction.decodeAmong Finset.univ.toList

@[simp]

theorem MIPRE.AnswerReduction.readFinite_encode {α : Type u_1} [Cost.SizedEncoding α] [Inhabited α] [Fintype α] (a : α) : readFinite.toFun (Cost.encode a) = a

The line-versus-point check

@[reducible, inline]

abbrev MIPRE.AnswerReduction.LvpIn : Type

The line, the point, the polynomials and the values.

Equations

• MIPRE.AnswerReduction.LvpIn = ((MIPRE.Cost.Unary × List MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr × List MIPRE.Cost.BitStr) × List (List MIPRE.Cost.BitStr) × List MIPRE.Cost.BitStr)

noncomputable def MIPRE.AnswerReduction.lvpBP : Cost.PolyTimeFun LvpIn Bool

lvpB, as a program.

Equations

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

@[simp]

theorem MIPRE.AnswerReduction.lvpBP_apply (kU : Cost.Unary) (base dir pt : List Cost.BitStr) (polys : List (List Cost.BitStr)) (vals : List Cost.BitStr) : lvpBP.toFun ((kU, base, dir, pt), polys, vals) = lvpB kU base dir pt polys vals

The low-degree subtest of a copy

@[reducible, inline]

abbrev MIPRE.AnswerReduction.LdIn : Type

Width, copy, test type, the two runs of blocks, polynomials and values.

Equations

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

noncomputable def MIPRE.AnswerReduction.kL : Cost.PolyTimeFun LdIn Cost.Unary

Equations

• MIPRE.AnswerReduction.kL = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.AnswerReduction.dL : Cost.PolyTimeFun LdIn StageProg.Desc

Equations

• MIPRE.AnswerReduction.dL = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.AnswerReduction.τL : Cost.PolyTimeFun LdIn ℕ

Equations

• MIPRE.AnswerReduction.τL = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.AnswerReduction.xL : Cost.PolyTimeFun LdIn StageProg.Blocks

Equations

• MIPRE.AnswerReduction.xL = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.AnswerReduction.yL : Cost.PolyTimeFun LdIn StageProg.Blocks

Equations

• MIPRE.AnswerReduction.yL = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.AnswerReduction.polysL : Cost.PolyTimeFun LdIn (List (List Cost.BitStr))

Equations

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

noncomputable def MIPRE.AnswerReduction.valsL : Cost.PolyTimeFun LdIn (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.AnswerReduction.oL : Cost.PolyTimeFun LdIn Cost.Unary

Equations

• MIPRE.AnswerReduction.oL = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.AnswerReduction.dL

noncomputable def MIPRE.AnswerReduction.szL : Cost.PolyTimeFun LdIn Cost.Unary

Equations

• MIPRE.AnswerReduction.szL = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.AnswerReduction.dL)

noncomputable def MIPRE.AnswerReduction.jwL : Cost.PolyTimeFun LdIn Cost.Unary

Equations

• MIPRE.AnswerReduction.jwL = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.AnswerReduction.dL))

noncomputable def MIPRE.AnswerReduction.cL : Cost.PolyTimeFun LdIn Cost.Unary

Equations

• MIPRE.AnswerReduction.cL = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.AnswerReduction.dL))

noncomputable def MIPRE.AnswerReduction.sliceLd (l : Cost.PolyTimeFun LdIn (List Cost.BitStr)) : Cost.PolyTimeFun LdIn (List Cost.BitStr)

Equations

• MIPRE.AnswerReduction.sliceLd l = MIPRE.AnswerReduction.StageProg.sliceP.comp (MIPRE.AnswerReduction.oL.pair (MIPRE.AnswerReduction.szL.pair l))

noncomputable def MIPRE.AnswerReduction.seedLd : Cost.PolyTimeFun LdIn Cost.BitStr

Equations

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

noncomputable def MIPRE.AnswerReduction.isτL (t : ℕ) : Cost.PolyTimeFun LdIn Bool

Equations

• MIPRE.AnswerReduction.isτL t = MIPRE.SAT.ArrayProg.eqNat.ap₂ MIPRE.AnswerReduction.τL (MIPRE.Cost.PolyTimeFun.const t)

noncomputable def MIPRE.AnswerReduction.dirLd : Cost.PolyTimeFun LdIn (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.AnswerReduction.baseLd : Cost.PolyTimeFun LdIn (List Cost.BitStr)

Equations

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

noncomputable def MIPRE.AnswerReduction.ldBP : Cost.PolyTimeFun LdIn Bool

ldB, as a program.

Equations

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

@[simp]

theorem MIPRE.AnswerReduction.ldBP_apply (kU : Cost.Unary) (d : StageProg.Desc) (τ : ℕ) (X Y : StageProg.Blocks) (polys : List (List Cost.BitStr)) (vals : List Cost.BitStr) : ldBP.toFun (kU, d, τ, X, Y, polys, vals) = ldB kU d τ X Y polys vals

The bounded parse

theorem MIPRE.AnswerReduction.decode_listBits_eq_some {d : Cost.Data} {bs : List Cost.BitStr} : Cost.decode d = some bs ↔ d = Cost.encode bs

theorem MIPRE.AnswerReduction.readBits_rawList_encode (bs : List Cost.BitStr) : List.map CL.Detyping.Program.readBits.toFun (CL.Detyping.Program.rawList (Cost.encode bs)) = bs

noncomputable def MIPRE.AnswerReduction.rawBlocks (s : Cost.BitStr) : List Cost.BitStr

The blocks a serialized answer lists, whether or not it is well formed.

Equations

• MIPRE.AnswerReduction.rawBlocks s = List.map MIPRE.CL.Detyping.Program.readBits.toFun (MIPRE.CL.Detyping.Program.rawList (MIPRE.Cost.Data.parse s))

noncomputable def MIPRE.AnswerReduction.parseBP : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.BitStr) (Bool × List Cost.BitStr)

The bounded parse, as a program: (k, c, s) to whether s parses to c blocks of k bits, and the blocks.

Equations

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

theorem MIPRE.AnswerReduction.parseBP_apply (kU cU : Cost.Unary) (s : Cost.BitStr) : parseBP.toFun (kU, cU, s) = ((parseB (List.length kU) (List.length cU) s).isSome, rawBlocks s) ∧ ∀ (bs : List Cost.BitStr), parseB (List.length kU) (List.length cU) s = some bs → rawBlocks s = bs

The number of elements

noncomputable def MIPRE.AnswerReduction.cntP : Cost.PolyTimeFun ((Cost.Unary × Cost.Unary) × Pcp.PcpTy) Cost.Unary

cntB, in unary, as a program.

Equations

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

@[simp]

theorem MIPRE.AnswerReduction.cntP_apply (mU m'U : Cost.Unary) (t : Pcp.PcpTy) : cntP.toFun ((mU, m'U), t) = Cost.unary (cntB (List.length mU) (List.length m'U) t)

One side

@[reducible, inline]

abbrev MIPRE.AnswerReduction.SideIn : Type

The parameters, the game check's verdict, the types, the blocks of the questions and of the answers.

Equations

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

noncomputable def MIPRE.AnswerReduction.kS : Cost.PolyTimeFun SideIn Cost.Unary

Equations

• MIPRE.AnswerReduction.kS = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.AnswerReduction.m'S : Cost.PolyTimeFun SideIn Cost.Unary

Equations

• MIPRE.AnswerReduction.m'S = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.fst)

noncomputable def MIPRE.AnswerReduction.descsS : Cost.PolyTimeFun SideIn (List StageProg.Desc)

Equations

• MIPRE.AnswerReduction.descsS = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.fst)

noncomputable def MIPRE.AnswerReduction.chkS : Cost.PolyTimeFun SideIn Bool

Equations

• MIPRE.AnswerReduction.chkS = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.AnswerReduction.tysS : Cost.PolyTimeFun SideIn (ArTy × ArTy)

Equations

• MIPRE.AnswerReduction.tysS = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.AnswerReduction.xS : Cost.PolyTimeFun SideIn StageProg.Blocks

Equations

• MIPRE.AnswerReduction.xS = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.AnswerReduction.yS : Cost.PolyTimeFun SideIn StageProg.Blocks

Equations

• MIPRE.AnswerReduction.yS = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.AnswerReduction.aS : Cost.PolyTimeFun SideIn (List Cost.BitStr)

Equations

• MIPRE.AnswerReduction.aS = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.AnswerReduction.bS : Cost.PolyTimeFun SideIn (List Cost.BitStr)

Equations

• MIPRE.AnswerReduction.bS = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.AnswerReduction.onTys {β : Type u_1} [Cost.SizedEncoding β] (f : ArTy × ArTy → β) : Cost.PolyTimeFun SideIn β

Equations

• MIPRE.AnswerReduction.onTys f = (MIPRE.Cost.PolyTimeFun.finiteFunction f).comp MIPRE.AnswerReduction.tysS

noncomputable def MIPRE.AnswerReduction.eqPart : Cost.PolyTimeFun SideIn Bool

Equations

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

noncomputable def MIPRE.AnswerReduction.widthP : Cost.PolyTimeFun SideIn Cost.Unary

Equations

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

noncomputable def MIPRE.AnswerReduction.ldPart : Cost.PolyTimeFun SideIn Bool

Equations

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

noncomputable def MIPRE.AnswerReduction.sideBP : Cost.PolyTimeFun SideIn Bool

sideB, as a program.

Equations

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

@[simp]

theorem MIPRE.AnswerReduction.sideBP_apply (kU m'U : Cost.Unary) (descs : List StageProg.Desc) (chk : Bool) (p q : ArTy) (X Y : StageProg.Blocks) (A B : List Cost.BitStr) : sideBP.toFun ((kU, m'U, descs), chk, (p, q), (X, Y), A, B) = sideB kU m'U descs chk p q X Y A B

The predicate

@[reducible, inline]

abbrev MIPRE.AnswerReduction.VerdictIn : Type

The parameters, the two game checks' verdicts, the types, the blocks of the questions and the answers.

Equations

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

noncomputable def MIPRE.AnswerReduction.parV : Cost.PolyTimeFun VerdictIn (Cost.Unary × Cost.Unary × List StageProg.Desc)

Equations

• MIPRE.AnswerReduction.parV = MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.AnswerReduction.chksV : Cost.PolyTimeFun VerdictIn (Bool × Bool)

Equations

• MIPRE.AnswerReduction.chksV = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.AnswerReduction.tysV : Cost.PolyTimeFun VerdictIn (ArTy × ArTy)

Equations

• MIPRE.AnswerReduction.tysV = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.AnswerReduction.blocksVP : Cost.PolyTimeFun VerdictIn (StageProg.Blocks × StageProg.Blocks)

Equations

• MIPRE.AnswerReduction.blocksVP = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.AnswerReduction.ansV : Cost.PolyTimeFun VerdictIn (Cost.BitStr × Cost.BitStr)

Equations

• MIPRE.AnswerReduction.ansV = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.AnswerReduction.parseV (ty : Cost.PolyTimeFun VerdictIn ArTy) (s : Cost.PolyTimeFun VerdictIn Cost.BitStr) : Cost.PolyTimeFun VerdictIn (Bool × List Cost.BitStr)

The parse of one answer, at the type the selector names.

Equations

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

noncomputable def MIPRE.AnswerReduction.verdictP : Cost.PolyTimeFun VerdictIn Bool

verdictB, as a program.

Equations

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

theorem MIPRE.AnswerReduction.verdictP_apply (kU m'U : Cost.Unary) (descs : List StageProg.Desc) (chkP chkQ : Bool) (p q : ArTy) (X Y : StageProg.Blocks) (a b : Cost.BitStr) : verdictP.toFun ((kU, m'U, descs), (chkP, chkQ), (p, q), (X, Y), a, b) = verdictB kU m'U descs chkP chkQ p q X Y a b