Correct query branches of the executable detyping router #
theorem
MIPRE.CL.Detyping.Program.route_query
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(E : T → T → Prop)
[DecidableRel E]
(n : ℕ)
(q : Sampler.Query)
:
(route E).toFun (Cost.encode (n, q)) = routeResult (graphDim T)
(Cost.encode n, q.toTuple.1, q.toTuple.2.1.toBool, q.toTuple.2.2.1, q.toTuple.2.2.2.1, q.toTuple.2.2.2.2)
(graphResult E
(q.toTuple.2.1.toBool, decide (q.toTuple.2.2.1 = 1), ofBits (graphDim T) q.toTuple.2.2.2.1, ofBits (graphDim T) q.toTuple.2.2.2.2))
theorem
MIPRE.CL.Detyping.Program.route_dimension
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(E : T → T → Prop)
[DecidableRel E]
(n : ℕ)
:
theorem
MIPRE.CL.Detyping.Program.route_marginal_early
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(E : T → T → Prop)
[DecidableRel E]
(n : ℕ)
(w : Player)
(j : ℕ)
(z : Cost.BitStr)
(hj : 1 ≤ j)
(hj' : j ≤ 2)
:
(route E).toFun (Cost.encode (n, Sampler.Query.marginal w j z)) = directResult
(graphBits ((CLFun.truncate j (Graph.presentation E w.toBool)).eval (graphOfBits z)) ++ pad false (content (graphDim T) z))
theorem
MIPRE.CL.Detyping.Program.route_linear_early
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(E : T → T → Prop)
[DecidableRel E]
(n : ℕ)
(w : Player)
(j : ℕ)
(u y : Cost.BitStr)
(hj : 1 ≤ j)
(hj' : j ≤ 2)
:
(route E).toFun (Cost.encode (n, Sampler.Query.linear w j u y)) = directResult
(graphBits (((Graph.presentation E w.toBool).mapOfPrefix (j - 1) (graphOfBits u)) (graphOfBits y)) ++ pad false (content (graphDim T) y))
theorem
MIPRE.CL.Detyping.Program.route_factor_early
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(E : T → T → Prop)
[DecidableRel E]
(n : ℕ)
(w : Player)
(j : ℕ)
(u : Cost.BitStr)
(hj : 1 ≤ j)
(hj' : j ≤ 2)
:
(route E).toFun (Cost.encode (n, Sampler.Query.factor w j u)) = directResult
(indicatorBits
(Finset.map graphEquiv.toEmbedding ((Graph.presentation E w.toBool).factorOfPrefix (j - 1) (graphOfBits u))) ++ pad false (content (graphDim T) u))
theorem
MIPRE.CL.Detyping.Program.route_marginal_late
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(E : T → T → Prop)
[DecidableRel E]
(n : ℕ)
(w : Player)
(j : ℕ)
(z : Cost.BitStr)
(hj : 2 < j)
:
(route E).toFun (Cost.encode (n, Sampler.Query.marginal w j z)) = match select E w.toBool (graphOfBits z) with
| none =>
directResult
(graphBits ((Graph.presentation E w.toBool).eval (graphOfBits z)) ++ pad false (content (graphDim T) z))
| some t =>
callResult
(Cost.encode (n, TypedSampler.Query.atType t (Sampler.Query.marginal w (j - 2) (content (graphDim T) z))))
(withPrefix (graphBits ((Graph.presentation E w.toBool).eval (graphOfBits z))))
theorem
MIPRE.CL.Detyping.Program.route_linear_late
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(E : T → T → Prop)
[DecidableRel E]
(n : ℕ)
(w : Player)
(j : ℕ)
(u y : Cost.BitStr)
(hj : 2 < j)
:
(route E).toFun (Cost.encode (n, Sampler.Query.linear w j u y)) = match select E w.toBool (graphOfBits u) with
| none => directResult (List.replicate (graphDim T) false ++ pad false (content (graphDim T) y))
| some t =>
callResult
(Cost.encode
(n, TypedSampler.Query.atType t
(Sampler.Query.linear w (j - 2) (content (graphDim T) u) (content (graphDim T) y))))
(withPrefix (List.replicate (graphDim T) false))
theorem
MIPRE.CL.Detyping.Program.route_factor_late
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(E : T → T → Prop)
[DecidableRel E]
(n : ℕ)
(w : Player)
(j : ℕ)
(u : Cost.BitStr)
(hj : 2 < j)
:
(route E).toFun (Cost.encode (n, Sampler.Query.factor w j u)) = match select E w.toBool (graphOfBits u) with
| none => directResult (List.replicate (graphDim T) false ++ pad (decide (j = 3)) (content (graphDim T) u))
| some t =>
callResult (Cost.encode (n, TypedSampler.Query.atType t (Sampler.Query.factor w (j - 2) (content (graphDim T) u))))
(withPrefix (List.replicate (graphDim T) false))
theorem
MIPRE.CL.Detyping.Program.content_length
{g s : ℕ}
(z : Cost.BitStr)
(hz : List.length z = g + s)
:
theorem
MIPRE.CL.Detyping.Program.pad_content
{g s : ℕ}
(b : Bool)
(z : Cost.BitStr)
(hz : List.length z = g + s)
: