The associated test is primitive recursive

primrec_assocTest: the map from a tailored game description to the description of its associated subgroup test (assocTest, Definition I:2086) is primitive recursive, so it composes with the halting reduction. Each of its constructions is a composition of list operations with a Primrec lemma in Mathlib; three are rewritten first into a form those lemmas cover: allBits as an iterate (allBits_eq_iterate), List.dedup as a fold (dedup_eq_foldr), and the enumeration of the fixed literals by List.range (zipIdx_map_eq).

Rewritings

def MIPRE.Tailored.Sofic.allBitsStep (acc : List (List Bool)) : List (List Bool)

One step of allBits.

Equations

• MIPRE.Tailored.Sofic.allBitsStep acc = List.flatMap (fun (r : List Bool) => [false :: r, true :: r]) acc

theorem MIPRE.Tailored.Sofic.allBits_eq_iterate (n : ℕ) : allBits n = allBitsStep^[n] [[]]

def MIPRE.Tailored.Sofic.dedupStep {α : Type u_1} [DecidableEq α] (a : α) (acc : List α) : List α

Deduplication as a fold: keep an element unless it occurs later.

Equations

• MIPRE.Tailored.Sofic.dedupStep a acc = if List.idxOf a acc < acc.length then acc else a :: acc

theorem MIPRE.Tailored.Sofic.dedup_eq_foldr {α : Type u_1} [DecidableEq α] (l : List α) : l.dedup = List.foldr dedupStep [] l

theorem MIPRE.Tailored.Sofic.zipIdx_map_eq {α : Type u_1} (l : List (α × Bool)) (d : α × Bool) : List.map (fun (p : (α × Bool) × ℕ) => (p.2, p.1.2)) l.zipIdx = List.map (fun (i : ℕ) => (i, (l.getD i d).2)) (List.range l.length)

theorem MIPRE.Tailored.Sofic.filter_eq_filterMap {α : Type u_1} (p : α → Bool) (l : List α) : List.filter p l = List.filterMap (fun (a : α) => if p a = true then some a else none) l

Primitive recursion

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.Q : Type

The arguments (g, x, y) of the per-pair constructions.

Equations

• MIPRE.Tailored.Sofic.Q = (TailoredGameValue.TailoredGameData × ℕ × ℕ)

theorem MIPRE.Tailored.Sofic.primrec_ansLen : Primrec fun (g : TailoredGameValue.TailoredGameData) => g.ansLen

theorem MIPRE.Tailored.Sofic.primrec_genW : Primrec genW

theorem MIPRE.Tailored.Sofic.primrec_invW : Primrec invW

theorem MIPRE.Tailored.Sofic.primrec_commW : Primrec₂ commW

theorem MIPRE.Tailored.Sofic.primrec_wJ : Primrec fun (x : Q) => wJ

theorem MIPRE.Tailored.Sofic.primrec_genX : Primrec fun (q : Q) => genX q.1 q.2.1 q.2.2

genX, on (g, x, i).

theorem MIPRE.Tailored.Sofic.primrec_wX : Primrec fun (q : Q) => wX q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.primrec_wX₂ : Primrec₂ fun (q : TailoredGameValue.TailoredGameData × ℕ) (i : ℕ) => wX q.1 q.2 i

wX g x applied to i, with (g, x) in context.

theorem MIPRE.Tailored.Sofic.primrec_varsAt : Primrec₂ fun (g : TailoredGameValue.TailoredGameData) (x : ℕ) => varsAt g x

theorem MIPRE.Tailored.Sofic.pg : Primrec fun (q : Q) => q.1

g of the arguments.

theorem MIPRE.Tailored.Sofic.px : Primrec fun (q : Q) => q.2.1

x of the arguments.

theorem MIPRE.Tailored.Sofic.py : Primrec fun (q : Q) => q.2.2

y of the arguments.

theorem MIPRE.Tailored.Sofic.primrec_varsX : Primrec fun (q : Q) => varsAt q.1 q.2.1

theorem MIPRE.Tailored.Sofic.primrec_varsY : Primrec fun (q : Q) => varsAt q.1 q.2.2

theorem MIPRE.Tailored.Sofic.primrec_fixedLits : Primrec fun (q : Q) => fixedLits q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.primrec_readVars : Primrec fun (q : Q) => readVars q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.primrec_readWords : Primrec fun (q : Q) => readWords q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.primrec_consAt : Primrec fun (q : Q) => consAt q.1 q.2.1 q.2.2

@[reducible, inline]

abbrev MIPRE.Tailored.Sofic.Q₂ (β : Type) : Type

(g, x, y) of a pair whose first component is the arguments.

Equations

• MIPRE.Tailored.Sofic.Q₂ β = (MIPRE.Tailored.Sofic.Q × β)

theorem MIPRE.Tailored.Sofic.primrec_consWord : Primrec₂ fun (q : Q) (c : List Bool) => consWord q.1 q.2.1 q.2.2 c

theorem MIPRE.Tailored.Sofic.primrec_dedupStep {α : Type} [Primcodable α] [DecidableEq α] : Primrec₂ dedupStep

theorem MIPRE.Tailored.Sofic.idxOf_word (l : List SubgroupTestValue.Word) (w : SubgroupTestValue.Word) : List.idxOf w l = List.idxOf w l

List.idxOf on words, with the structural BEq of lists, is the one with the BEq of decidable equality, which Mathlib's Primrec.list_idxOf is stated for.

theorem MIPRE.Tailored.Sofic.primrec_consWords : Primrec fun (q : Q) => consWords q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.primrec_words : Primrec fun (q : Q) => words q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.primrec_fixedLen : Primrec fun (p : Q × List Bool) => (fixedLits p.1.1 p.1.2.1 p.1.2.2).length

theorem MIPRE.Tailored.Sofic.primrec_readLen : Primrec fun (p : Q × List Bool) => (readWords p.1.1 p.1.2.1 p.1.2.2).length

def MIPRE.Tailored.Sofic.clauseFixed (p : Q × List Bool) : List (ℕ × Bool)

The fixed literals of a clause, enumerated.

Equations

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

def MIPRE.Tailored.Sofic.clauseRead (p : Q × List Bool) : List (ℕ × Bool)

The readable literals of a clause.

Equations

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

def MIPRE.Tailored.Sofic.clauseCons (p : Q × List Bool) : List (ℕ × Bool)

The constraint literals of a clause.

Equations

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

theorem MIPRE.Tailored.Sofic.clause_eq (q : Q) (r : List Bool) : clause q.1 q.2.1 q.2.2 r = clauseFixed (q, r) ++ clauseRead (q, r) ++ clauseCons (q, r)

theorem MIPRE.Tailored.Sofic.primrec_clauseFixed : Primrec clauseFixed

theorem MIPRE.Tailored.Sofic.primrec_clauseRead : Primrec clauseRead

theorem MIPRE.Tailored.Sofic.primrec_clauseCons : Primrec clauseCons

theorem MIPRE.Tailored.Sofic.primrec_clause : Primrec₂ fun (q : Q) (r : List Bool) => clause q.1 q.2.1 q.2.2 r

theorem MIPRE.Tailored.Sofic.primrec_allBitsStep : Primrec allBitsStep

theorem MIPRE.Tailored.Sofic.primrec_allBits : Primrec allBits

theorem MIPRE.Tailored.Sofic.primrec_clauses : Primrec fun (q : Q) => clauses q.1 q.2.1 q.2.2

theorem MIPRE.Tailored.Sofic.primrec_challenge : Primrec fun (p : ℕ × Q) => challenge p.2.1 p.1 p.2.2.1 p.2.2.2

theorem MIPRE.Tailored.Sofic.primrec_questionWeight : Primrec fun (q : Q) => (wts q.1).questionWeight q.2.1 q.2.2

def MIPRE.Tailored.Sofic.totalWeightL (g : TailoredGameValue.TailoredGameData) : ℕ

The total weight, as a sum over lists.

Equations

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

theorem MIPRE.Tailored.Sofic.sum_fin_eq_sum_range (n : ℕ) (f : ℕ → ℕ) : ∑ x : Fin (n + 1), f ↑x = (List.map f (List.range (n + 1))).sum

theorem MIPRE.Tailored.Sofic.sum_flatMap_nat {α : Type u_1} (L : List α) (f : α → List ℕ) : (List.flatMap f L).sum = (List.map (fun (x : α) => (f x).sum) L).sum

theorem MIPRE.Tailored.Sofic.totalWeight_eq (g : TailoredGameValue.TailoredGameData) : (wts g).totalWeight = totalWeightL g

theorem MIPRE.Tailored.Sofic.primrec_totalWeightL : Primrec totalWeightL

theorem MIPRE.Tailored.Sofic.primrec_nGen : Primrec nGen

theorem MIPRE.Tailored.Sofic.primrec_assocTest : Primrec assocTest

The associated test is primitive recursive.