A tailored game description as a game description

TailoredGameData.toGameData turns a tailored game description into a HaltingGameValue.GameData with the same game: the questions are the same vertices, the answers the bit vectors of length Λ named by the numbers below 2 ^ Λ (bit i of the number is coordinate i, vecEquiv), the weights the same list, and the acceptance table every tuple the canonical decider accepts (acceptsN, the decider on numbers). So the machinery written for game descriptions applies to tailored ones: the quantum value is the same (quantumValue_toGameData), and it is r.e. from below along a computable family (ValueApprox.rePred_lt_quantumValue), because the conversion is primitive recursive (primrec_toGameData).

Answers as numbers

def TailoredGameValue.TailoredGameData.vecEquiv (L : ℕ) : Fin (2 ^ L) ≃ (Fin L → Bool)

The bit vectors of length L as the numbers below 2 ^ L: coordinate i is bit i.

Equations

• TailoredGameValue.TailoredGameData.vecEquiv L = finFunctionFinEquiv.symm.trans ((Equiv.refl (Fin L)).arrowCongr finTwoEquiv)

theorem TailoredGameValue.TailoredGameData.vecEquiv_apply (L : ℕ) (a : Fin (2 ^ L)) (i : Fin L) : (vecEquiv L) a i = (↑a).testBit ↑i

The answer length and the canonical decider, on numbers

def TailoredGameValue.TailoredGameData.ansLenL (g : TailoredGameData) : ℕ

The answer length Λ, computed by a fold over the vertices.

Equations

• g.ansLenL = List.foldr max 0 (List.map g.lenAt (List.range (g.nV + 1)))

theorem TailoredGameValue.TailoredGameData.le_foldr_max {l : List ℕ} {a : ℕ} (h : a ∈ l) : a ≤ List.foldr max 0 l

theorem TailoredGameValue.TailoredGameData.foldr_max_le {l : List ℕ} {B : ℕ} (h : ∀ a ∈ l, a ≤ B) : List.foldr max 0 l ≤ B

theorem TailoredGameValue.TailoredGameData.lenAt_le_ansLen (g : TailoredGameData) (x : Fin (g.nV + 1)) : g.lenAt ↑x ≤ g.ansLen

theorem TailoredGameValue.TailoredGameData.ansLenL_eq (g : TailoredGameData) : g.ansLenL = g.ansLen

def TailoredGameValue.TailoredGameData.rdN (g : TailoredGameData) (x a : ℕ) : List Bool

The readable part of an answer given as a number.

Equations

• g.rdN x a = List.map a.testBit (List.range (g.lenRAt x))

def TailoredGameValue.TailoredGameData.flN (g : TailoredGameData) (x a : ℕ) : List Bool

The full answer, given as a number.

Equations

• g.flN x a = List.map a.testBit (List.range (g.lenAt x))

def TailoredGameValue.TailoredGameData.parityB (l : List Bool) : Bool

The parity of a list of bits, by a fold.

Equations

• TailoredGameValue.TailoredGameData.parityB l = List.foldr (fun (b acc : Bool) => !decide (b = acc)) false l

theorem TailoredGameValue.TailoredGameData.parityB_eq_false_iff (l : List Bool) : parityB l = false ↔ Even (List.count true l)

def TailoredGameValue.TailoredGameData.satB (c v : List Bool) : Bool

Satisfaction of a linear constraint, as a Boolean function.

Equations

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

theorem TailoredGameValue.TailoredGameData.zipWith_eq_range (c v : List Bool) (h : c.length = v.length) : List.zipWith (fun (x1 x2 : Bool) => x1 && x2) c v = List.map (fun (i : ℕ) => c.getD i false && v.getD i false) (List.range c.length)

theorem TailoredGameValue.TailoredGameData.satB_iff (c v : List Bool) : satB c v = true ↔ Satisfies c v

def TailoredGameValue.TailoredGameData.acceptsN (g : TailoredGameData) (x y a b : ℕ) : Bool

The canonical decider on numbers: answers given as numbers, read as bit vectors.

Equations

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

def TailoredGameValue.TailoredGameData.accN (g : TailoredGameData) : List (ℕ × ℕ × ℕ × ℕ)

The acceptance table: every tuple of numbers in range that the decider accepts.

Equations

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

def TailoredGameValue.TailoredGameData.toGameData (g : TailoredGameData) : HaltingGameValue.GameData

A tailored game description as a game description.

Equations

• g.toGameData = { nX := g.nV, nA := 2 ^ g.ansLenL - 1, w := g.w, acc := g.accN }

theorem TailoredGameValue.TailoredGameData.mem_accN (g : TailoredGameData) (x y a b : ℕ) : (x, y, a, b) ∈ g.accN ↔ x < g.nV + 1 ∧ y < g.nV + 1 ∧ a < 2 ^ g.ansLenL ∧ b < 2 ^ g.ansLenL ∧ g.acceptsN x y a b = true

The canonical decider on numbers is the canonical decider

theorem TailoredGameValue.TailoredGameData.wellFormatted_iff (g : TailoredGameData) (x : Fin (g.nV + 1)) (a : Fin (2 ^ g.ansLen)) : g.WellFormatted x ((vecEquiv g.ansLen) a) ↔ ↑a < 2 ^ g.lenAt ↑x

theorem TailoredGameValue.TailoredGameData.bit_vecEquiv (g : TailoredGameData) (a : Fin (2 ^ g.ansLen)) {i : ℕ} (hi : i < g.ansLen) : bit ((vecEquiv g.ansLen) a) i = (↑a).testBit i

theorem TailoredGameValue.TailoredGameData.readable_vecEquiv (g : TailoredGameData) (x : Fin (g.nV + 1)) (a : Fin (2 ^ g.ansLen)) : g.readable x ((vecEquiv g.ansLen) a) = g.rdN ↑x ↑a

theorem TailoredGameValue.TailoredGameData.full_vecEquiv (g : TailoredGameData) (x : Fin (g.nV + 1)) (a : Fin (2 ^ g.ansLen)) : g.full x ((vecEquiv g.ansLen) a) = g.flN ↑x ↑a

theorem TailoredGameValue.TailoredGameData.elem_iff (A B C : Prop) [Decidable A] [Decidable B] [Decidable C] (s : Bool) : (!(decide A && decide B && decide C) || s) = true ↔ A → B → C → s = true

theorem TailoredGameValue.TailoredGameData.acceptsN_iff (g : TailoredGameData) (x y : Fin (g.nV + 1)) (a b : Fin (2 ^ g.ansLen)) : g.acceptsN ↑x ↑y ↑a ↑b = true ↔ g.Accepts x y ((vecEquiv g.ansLen) a) ((vecEquiv g.ansLen) b)

The canonical decider on numbers is the canonical decider.

The same game

theorem TailoredGameValue.TailoredGameData.toGameData_nA_succ (g : TailoredGameData) : g.toGameData.nA + 1 = 2 ^ g.ansLen

def TailoredGameValue.TailoredGameData.ansIdx (g : TailoredGameData) : Fin (g.toGameData.nA + 1) ≃ (Fin g.ansLen → Bool)

The answers of the game description, as bit vectors.

Equations

• g.ansIdx = (finCongr ⋯).trans (TailoredGameValue.TailoredGameData.vecEquiv g.ansLen)

theorem TailoredGameValue.TailoredGameData.toGameData_μ (g : TailoredGameData) (x y : Fin (g.nV + 1)) : g.toGameData.game.μ x y = g.game.μ x y

theorem TailoredGameValue.TailoredGameData.toGameData_D (g : TailoredGameData) (x y : Fin (g.nV + 1)) (a b : Fin (g.toGameData.nA + 1)) : g.toGameData.game.D x y a b = g.game.D x y (g.ansIdx a) (g.ansIdx b)

theorem TailoredGameValue.TailoredGameData.quantumValue_toGameData (g : TailoredGameData) : MIPRE.quantumValue g.toGameData.game = MIPRE.quantumValue g.game

The game description has the quantum value of the tailored one.

The conversion is primitive recursive

theorem TailoredGameValue.TailoredGameData.primrec_tuple : Primrec ⇑equivTuple

theorem TailoredGameValue.TailoredGameData.primrec_nV : Primrec fun (g : TailoredGameData) => g.nV

theorem TailoredGameValue.TailoredGameData.primrec_lenR : Primrec fun (g : TailoredGameData) => g.lenR

theorem TailoredGameValue.TailoredGameData.primrec_lenL : Primrec fun (g : TailoredGameData) => g.lenL

theorem TailoredGameValue.TailoredGameData.primrec_w : Primrec fun (g : TailoredGameData) => g.w

theorem TailoredGameValue.TailoredGameData.primrec_cons : Primrec fun (g : TailoredGameData) => g.cons

theorem TailoredGameValue.TailoredGameData.primrec_lenRAt : Primrec₂ fun (g : TailoredGameData) (x : ℕ) => g.lenRAt x

theorem TailoredGameValue.TailoredGameData.primrec_lenLAt : Primrec₂ fun (g : TailoredGameData) (x : ℕ) => g.lenLAt x

theorem TailoredGameValue.TailoredGameData.primrec_lenAt : Primrec₂ fun (g : TailoredGameData) (x : ℕ) => g.lenAt x

theorem TailoredGameValue.TailoredGameData.primrec_ansLenL : Primrec fun (g : TailoredGameData) => g.ansLenL

theorem TailoredGameValue.TailoredGameData.primrec_testBit : Primrec₂ fun (a i : ℕ) => a.testBit i

theorem TailoredGameValue.TailoredGameData.primrec_rdN : Primrec fun (q : TailoredGameData × ℕ × ℕ) => q.1.rdN q.2.1 q.2.2

theorem TailoredGameValue.TailoredGameData.primrec_flN : Primrec fun (q : TailoredGameData × ℕ × ℕ) => q.1.flN q.2.1 q.2.2

theorem TailoredGameValue.TailoredGameData.primrec_parityB : Primrec parityB

theorem TailoredGameValue.TailoredGameData.primrec_satB : Primrec₂ satB

def TailoredGameValue.TailoredGameData.consTest (q : TailoredGameData × ℕ × ℕ × ℕ × ℕ) (e : ℕ × ℕ × List Bool × List Bool) : Bool

The per-constraint test of acceptsN, as a function of the description, the tuple and the constraint entry.

Equations

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

theorem TailoredGameValue.TailoredGameData.primrec_consTest : Primrec₂ consTest

theorem TailoredGameValue.TailoredGameData.all_eq_foldr {α : Type u_1} (l : List α) (f : α → Bool) : l.all f = List.foldr (fun (e : α) (b : Bool) => f e && b) true l

theorem TailoredGameValue.TailoredGameData.primrec_acceptsN : Primrec fun (q : TailoredGameData × ℕ × ℕ × ℕ × ℕ) => q.1.acceptsN q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2

theorem TailoredGameValue.TailoredGameData.primrec_accN : Primrec accN

theorem TailoredGameValue.TailoredGameData.primrec_toGameData : Primrec toGameData

The conversion is primitive recursive.