The constraint forms of the introspection processor, in polynomial time

The linear-constraints processor of the tailored introspection verifier writes its constraints through a handful of forms (Forms.lean, RegCons.lean, SourceCons.lean, AuxCons.lean). This file builds each of them as a Cost.PolyTimeFun from already computed data: lengths and offsets in unary, so that the output, of about Q constraints of about 2Q + 2R bits, is polynomial in the size of the input; readable conditions as Booleans; coordinate sets S ⊆ Fin s as their bit masks maskOf S; vectors of 𝔽₂^s as their bits CL.toBits.

• placeOf, rejectF: the vector place n off w and the rejecting constraint;
• unitsF: the unit vectors units m, as the orbit of a shift;
• pairFormF: the form place la oa e ++ place lb ob e ++ [false];
• eqConsF, guardConsF, projEqConsF, dualConsF: eqCons, guardCons, projEqCons, dualCons;
• reindexF, swapConF, swapConsF: reindex, swapCon and its map over a list.

Each comes with its _apply lemma on arbitrary inputs, and the _spec lemma stating that on the encoding of the semantic data it outputs the semantic list.

Pieces on a generic input

noncomputable def MIPRE.Tailored.Intro.catF {ι : Type} [Cost.SizedEncoding ι] {α : Type} [Cost.SizedEncoding α] (F G : Cost.PolyTimeFun ι (List α)) : Cost.PolyTimeFun ι (List α)

Concatenation of two computed lists.

Equations

• MIPRE.Tailored.Intro.catF F G = MIPRE.Cost.PolyTimeFun.append.comp (F.pair G)

@[simp]

theorem MIPRE.Tailored.Intro.catF_apply {ι : Type} [Cost.SizedEncoding ι] {α : Type} [Cost.SizedEncoding α] (F G : Cost.PolyTimeFun ι (List α)) (a : ι) : (catF F G).toFun a = F.toFun a ++ G.toFun a

noncomputable def MIPRE.Tailored.Intro.zerosOf {ι : Type} [Cost.SizedEncoding ι] (u : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.BitStr

u zeros.

Equations

• MIPRE.Tailored.Intro.zerosOf u = MIPRE.Cost.PolyTimeFun.replicate.comp (u.pair (MIPRE.Cost.PolyTimeFun.const false))

@[simp]

theorem MIPRE.Tailored.Intro.zerosOf_apply {ι : Type} [Cost.SizedEncoding ι] (u : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : (zerosOf u).toFun a = List.replicate (List.length (u.toFun a)) false

noncomputable def MIPRE.Tailored.Intro.subOf {ι : Type} [Cost.SizedEncoding ι] (u v : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

Truncated subtraction of unary numbers.

Equations

• MIPRE.Tailored.Intro.subOf u v = MIPRE.Cost.PolyTimeFun.drop.comp (u.pair v)

@[simp]

theorem MIPRE.Tailored.Intro.subOf_apply {ι : Type} [Cost.SizedEncoding ι] (u v : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : (subOf u v).toFun a = List.drop (List.length (v.toFun a)) (u.toFun a)

noncomputable def MIPRE.Tailored.Intro.lenOf {ι : Type} [Cost.SizedEncoding ι] {α : Type} [Cost.SizedEncoding α] (l : Cost.PolyTimeFun ι (List α)) : Cost.PolyTimeFun ι Cost.Unary

The length of a computed list, in unary.

Equations

• MIPRE.Tailored.Intro.lenOf l = MIPRE.Cost.PolyTimeFun.length.comp l

@[simp]

theorem MIPRE.Tailored.Intro.lenOf_apply {ι : Type} [Cost.SizedEncoding ι] {α : Type} [Cost.SizedEncoding α] (l : Cost.PolyTimeFun ι (List α)) (a : ι) : (lenOf l).toFun a = Cost.unary (l.toFun a).length

noncomputable def MIPRE.Tailored.Intro.takeOf {ι : Type} [Cost.SizedEncoding ι] (l : Cost.PolyTimeFun ι Cost.BitStr) (u : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.BitStr

A prefix of a computed bit string.

Equations

• MIPRE.Tailored.Intro.takeOf l u = MIPRE.Cost.PolyTimeFun.take.comp (l.pair u)

@[simp]

theorem MIPRE.Tailored.Intro.takeOf_apply {ι : Type} [Cost.SizedEncoding ι] (l : Cost.PolyTimeFun ι Cost.BitStr) (u : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : (takeOf l u).toFun a = List.take (List.length (u.toFun a)) (l.toFun a)

noncomputable def MIPRE.Tailored.Intro.dropOf {ι : Type} [Cost.SizedEncoding ι] (l : Cost.PolyTimeFun ι Cost.BitStr) (u : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.BitStr

A suffix of a computed bit string.

Equations

• MIPRE.Tailored.Intro.dropOf l u = MIPRE.Cost.PolyTimeFun.drop.comp (l.pair u)

@[simp]

theorem MIPRE.Tailored.Intro.dropOf_apply {ι : Type} [Cost.SizedEncoding ι] (l : Cost.PolyTimeFun ι Cost.BitStr) (u : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : (dropOf l u).toFun a = List.drop (List.length (u.toFun a)) (l.toFun a)

noncomputable def MIPRE.Tailored.Intro.placeOf {ι : Type} [Cost.SizedEncoding ι] (n off : Cost.PolyTimeFun ι Cost.Unary) (w : Cost.PolyTimeFun ι Cost.BitStr) : Cost.PolyTimeFun ι Cost.BitStr

The placed vector place n off w.

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.placeOf_apply {ι : Type} [Cost.SizedEncoding ι] (n off : Cost.PolyTimeFun ι Cost.Unary) (w : Cost.PolyTimeFun ι Cost.BitStr) (a : ι) : (placeOf n off w).toFun a = place (List.length (n.toFun a)) (List.length (off.toFun a)) (w.toFun a)

noncomputable def MIPRE.Tailored.Intro.isNilOf {ι : Type} [Cost.SizedEncoding ι] {α : Type} [Cost.SizedEncoding α] (l : Cost.PolyTimeFun ι (List α)) : Cost.PolyTimeFun ι Bool

Whether a list is empty.

Equations

• MIPRE.Tailored.Intro.isNilOf l = ((MIPRE.Cost.PolyTimeFun.const true).casesList (MIPRE.Cost.PolyTimeFun.const false)).comp ((MIPRE.Cost.PolyTimeFun.const ()).pair l)

@[simp]

theorem MIPRE.Tailored.Intro.isNilOf_apply {ι : Type} [Cost.SizedEncoding ι] {α : Type} [Cost.SizedEncoding α] (l : Cost.PolyTimeFun ι (List α)) (a : ι) : (isNilOf l).toFun a = (l.toFun a).isEmpty

noncomputable def MIPRE.Tailored.Intro.andOf {ι : Type} [Cost.SizedEncoding ι] (b c : Cost.PolyTimeFun ι Bool) : Cost.PolyTimeFun ι Bool

Conjunction of two computed Booleans.

Equations

• MIPRE.Tailored.Intro.andOf b c = b.ite c (MIPRE.Cost.PolyTimeFun.const false)

@[simp]

theorem MIPRE.Tailored.Intro.andOf_apply {ι : Type} [Cost.SizedEncoding ι] (b c : Cost.PolyTimeFun ι Bool) (a : ι) : (andOf b c).toFun a = (b.toFun a && c.toFun a)

noncomputable def MIPRE.Tailored.Intro.eqUOf {ι : Type} [Cost.SizedEncoding ι] (u v : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Bool

Equality of two unary numbers.

Equations

• MIPRE.Tailored.Intro.eqUOf u v = MIPRE.Tailored.Intro.andOf (MIPRE.Tailored.Intro.isNilOf (MIPRE.Tailored.Intro.subOf u v)) (MIPRE.Tailored.Intro.isNilOf (MIPRE.Tailored.Intro.subOf v u))

@[simp]

theorem MIPRE.Tailored.Intro.eqUOf_apply {ι : Type} [Cost.SizedEncoding ι] (u v : Cost.PolyTimeFun ι Cost.Unary) (a : ι) : (eqUOf u v).toFun a = decide (List.length (u.toFun a) = List.length (v.toFun a))

Unit vectors

def MIPRE.Tailored.Intro.shift (w : Cost.BitStr) : Cost.BitStr

The shift: a zero in front, the last bit dropped.

Equations

• MIPRE.Tailored.Intro.shift w = false :: List.dropLast w

noncomputable def MIPRE.Tailored.Intro.shiftF : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

The shift in polynomial time.

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.shiftF_apply (w : Cost.BitStr) : shiftF.toFun w = shift w

theorem MIPRE.Tailored.Intro.length_iterate_shift_le (w : Cost.BitStr) (n : ℕ) : List.length (shift^[n] w) ≤ List.length w + 1

theorem MIPRE.Tailored.Intro.esize_iterate_shift_le (n : ℕ) (w : Cost.BitStr) : Cost.esize (shiftF.toFun^[n] w) ≤ Polynomial.eval (Cost.esize w) (Polynomial.C 4 * Polynomial.X + Polynomial.C 5)

theorem MIPRE.Tailored.Intro.unit_eq {m i : ℕ} : unit m i = List.replicate i false ++ [true] ++ List.replicate (m - i - 1) false

theorem MIPRE.Tailored.Intro.shift_unit {m i : ℕ} (h : i + 1 < m) : shift (unit m i) = unit m (i + 1)

theorem MIPRE.Tailored.Intro.iterate_shift_unit {m : ℕ} (i : ℕ) : i < m → shift^[i] (unit m 0) = unit m i

def MIPRE.Tailored.Intro.units (m : ℕ) : List Cost.BitStr

The unit vectors of length m, in order.

Equations

• MIPRE.Tailored.Intro.units m = List.map (MIPRE.Tailored.Intro.unit m) (List.range m)

noncomputable def MIPRE.Tailored.Intro.unitsF : Cost.PolyTimeFun Cost.Unary (List Cost.BitStr)

The unit vectors, as the orbit of the first under the shift.

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.unitsF_apply (u : Cost.Unary) : unitsF.toFun u = units (List.length u)

theorem MIPRE.Tailored.Intro.unit_eq_ofFn {m i : ℕ} (hi : i < m) : unit m i = List.ofFn fun (j : Fin m) => decide (↑j = i)

theorem MIPRE.Tailored.Intro.toBits_single {s : ℕ} (i : Fin s) : CL.toBits (Pi.single i 1) = unit s ↑i

theorem MIPRE.Tailored.Intro.units_eq_map_finRange (s : ℕ) : units s = List.map (fun (i : Fin s) => CL.toBits (Pi.single i 1)) (List.finRange s)

The two-sided form

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.Lay : Type

The layout of a two-sided form: the lengths and offsets ((la, oa), (lb, ob)).

Equations

• MIPRE.Tailored.Intro.Lay = ((MIPRE.Cost.Unary × MIPRE.Cost.Unary) × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

def MIPRE.Tailored.Intro.lay (la oa lb ob : ℕ) : Lay

The layout of (la, oa, lb, ob).

Equations

• MIPRE.Tailored.Intro.lay la oa lb ob = ((MIPRE.Cost.unary la, MIPRE.Cost.unary oa), MIPRE.Cost.unary lb, MIPRE.Cost.unary ob)

def MIPRE.Tailored.Intro.pairForm (la oa lb ob : ℕ) (e : Cost.BitStr) : Cost.BitStr

The constraint ⟨e, a_{oa..}⟩ + ⟨e, b_{ob..}⟩ = 0.

Equations

• MIPRE.Tailored.Intro.pairForm la oa lb ob e = MIPRE.Tailored.Intro.place la oa e ++ MIPRE.Tailored.Intro.place lb ob e ++ [false]

noncomputable def MIPRE.Tailored.Intro.pairFormF : Cost.PolyTimeFun (Cost.BitStr × Lay) Cost.BitStr

The two-sided form in polynomial time, on (e, layout).

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.pairFormF_apply (e : Cost.BitStr) (L : Lay) : pairFormF.toFun (e, L) = pairForm (List.length L.1.1) (List.length L.1.2) (List.length L.2.1) (List.length L.2.2) e

Equality of windows

theorem MIPRE.Tailored.Intro.eqCons_eq_units (la lb oa ob m : ℕ) : eqCons la lb oa ob m = List.map (pairForm la oa lb ob) (units m)

noncomputable def MIPRE.Tailored.Intro.eqConsF : Cost.PolyTimeFun (Lay × Cost.Unary) (List Cost.BitStr)

The window equality constraints eqCons, on (layout, m).

Equations

• MIPRE.Tailored.Intro.eqConsF = MIPRE.Tailored.Intro.pairFormF.mapWith.comp ((MIPRE.Tailored.Intro.unitsF.comp MIPRE.Cost.PolyTimeFun.snd).pair MIPRE.Cost.PolyTimeFun.fst)

@[simp]

theorem MIPRE.Tailored.Intro.eqConsF_apply (L : Lay) (m : Cost.Unary) : eqConsF.toFun (L, m) = eqCons (List.length L.1.1) (List.length L.2.1) (List.length L.1.2) (List.length L.2.2) (List.length m)

theorem MIPRE.Tailored.Intro.eqConsF_spec (la lb oa ob m : ℕ) : eqConsF.toFun (lay la oa lb ob, Cost.unary m) = eqCons la lb oa ob m

Readable guards

noncomputable def MIPRE.Tailored.Intro.rejectF : Cost.PolyTimeFun Cost.Unary Cost.BitStr

The rejecting constraint rejectConstraint d, d in unary.

Equations

• MIPRE.Tailored.Intro.rejectF = MIPRE.Tailored.Intro.catF (MIPRE.Tailored.Intro.zerosOf (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Unary)) (MIPRE.Cost.PolyTimeFun.const [true])

@[simp]

theorem MIPRE.Tailored.Intro.rejectF_apply (u : Cost.Unary) : rejectF.toFun u = rejectConstraint (List.length u)

noncomputable def MIPRE.Tailored.Intro.guardConsF : Cost.PolyTimeFun (Bool × Cost.Unary) (List Cost.BitStr)

The readable guard guardCons, on (b, d).

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.guardConsF_apply (b : Bool) (d : Cost.Unary) : guardConsF.toFun (b, d) = guardCons b (List.length d)

theorem MIPRE.Tailored.Intro.guardConsF_spec (b : Bool) (d : ℕ) : guardConsF.toFun (b, Cost.unary d) = guardCons b d

Equality on a coordinate set

def MIPRE.Tailored.Intro.maskOf {s : ℕ} (S : Finset (Fin s)) : Cost.BitStr

The bit mask of a coordinate set.

Equations

• MIPRE.Tailored.Intro.maskOf S = List.ofFn fun (i : Fin s) => decide (i ∈ S)

@[simp]

theorem MIPRE.Tailored.Intro.length_maskOf {s : ℕ} (S : Finset (Fin s)) : List.length (maskOf S) = s

def MIPRE.Tailored.Intro.selectL {α : Type} (l : List α) (m : Cost.BitStr) : List α

The entries of l selected by the mask m.

Equations

• MIPRE.Tailored.Intro.selectL l m = (List.map (fun (p : α × Bool) => if p.2 = true then [p.1] else []) (l.zip m)).flatten

theorem MIPRE.Tailored.Intro.selectL_map {α β : Type} (f : β → α) (p : β → Bool) (l : List β) : selectL (List.map f l) (List.map p l) = List.map f (List.filter p l)

noncomputable def MIPRE.Tailored.Intro.selectF {α : Type} [Cost.SizedEncoding α] : Cost.PolyTimeFun (List α × Cost.BitStr) (List α)

The selection by a mask in polynomial time, on (l, m).

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.selectF_apply {α : Type} [Cost.SizedEncoding α] (l : List α) (m : Cost.BitStr) : selectF.toFun (l, m) = selectL l m

theorem MIPRE.Tailored.Intro.projEqCons_eq_select {s : ℕ} (la lb oa ob : ℕ) (S : Finset (Fin s)) : projEqCons la lb oa ob S = List.map (pairForm la oa lb ob) (selectL (units s) (maskOf S))

noncomputable def MIPRE.Tailored.Intro.projEqConsF : Cost.PolyTimeFun (Lay × Cost.BitStr) (List Cost.BitStr)

The coordinate-set equality constraints projEqCons, on (layout, mask).

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.projEqConsF_apply (L : Lay) (m : Cost.BitStr) : projEqConsF.toFun (L, m) = List.map (pairForm (List.length L.1.1) (List.length L.1.2) (List.length L.2.1) (List.length L.2.2)) (selectL (units (List.length m)) m)

theorem MIPRE.Tailored.Intro.projEqConsF_spec {s : ℕ} (la lb oa ob : ℕ) (S : Finset (Fin s)) : projEqConsF.toFun (lay la oa lb ob, maskOf S) = projEqCons la lb oa ob S

Equality of duals

def MIPRE.Tailored.Intro.andMask (g m : Cost.BitStr) : Cost.BitStr

The bits of g masked by m.

Equations

• MIPRE.Tailored.Intro.andMask g m = List.map (fun (p : Bool × Bool) => p.1 && p.2) (List.zip g m)

noncomputable def MIPRE.Tailored.Intro.andMaskF : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

The masking in polynomial time, on (g, m).

Equations

• MIPRE.Tailored.Intro.andMaskF = (MIPRE.Tailored.Intro.andOf MIPRE.Cost.PolyTimeFun.fst MIPRE.Cost.PolyTimeFun.snd).map.comp MIPRE.Cost.PolyTimeFun.zip

@[simp]

theorem MIPRE.Tailored.Intro.andMaskF_apply (g m : Cost.BitStr) : andMaskF.toFun (g, m) = andMask g m

theorem MIPRE.Tailored.Intro.toBits_proj {s : ℕ} (S : Finset (Fin s)) (z : Fin s → CL.𝔽₂) : CL.toBits ((CL.proj S) z) = andMask (CL.toBits z) (maskOf S)

theorem MIPRE.Tailored.Intro.dualCons_eq_map {s : ℕ} (la lb oa ob : ℕ) (S : Finset (Fin s)) (gens : List (Fin s → CL.𝔽₂)) : dualCons la lb oa ob S gens = List.map (pairForm la oa lb ob) (List.map (fun (g : Cost.BitStr) => andMask g (maskOf S)) (List.map CL.toBits gens))

noncomputable def MIPRE.Tailored.Intro.dualConsF : Cost.PolyTimeFun (Lay × Cost.BitStr × List Cost.BitStr) (List Cost.BitStr)

The dual equality constraints dualCons, on (layout, mask, generators).

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.dualConsF_apply (L : Lay) (m : Cost.BitStr) (gs : List Cost.BitStr) : dualConsF.toFun (L, m, gs) = List.map (pairForm (List.length L.1.1) (List.length L.1.2) (List.length L.2.1) (List.length L.2.2)) (List.map (fun (g : Cost.BitStr) => andMask g m) gs)

theorem MIPRE.Tailored.Intro.dualConsF_spec {s : ℕ} (la lb oa ob : ℕ) (S : Finset (Fin s)) (gens : List (Fin s → CL.𝔽₂)) : dualConsF.toFun (lay la oa lb ob, maskOf S, List.map CL.toBits gens) = dualCons la lb oa ob S gens

Re-indexed input constraints

@[reducible, inline]

abbrev MIPRE.Tailored.Intro.RParams : Type

The parameters of a re-indexing: ((Q, R), ((lRa, lLa), (lRb, lLb)), (la, lb)).

Equations

• MIPRE.Tailored.Intro.RParams = ((MIPRE.Cost.Unary × MIPRE.Cost.Unary) × ((MIPRE.Cost.Unary × MIPRE.Cost.Unary) × MIPRE.Cost.Unary × MIPRE.Cost.Unary) × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

def MIPRE.Tailored.Intro.rparams (Q R lRa lLa lRb lLb la lb : ℕ) : RParams

The parameters of reindex Q R lRa lLa lRb lLb la lb.

Equations

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

noncomputable def MIPRE.Tailored.Intro.place2Of {ι : Type} [Cost.SizedEncoding ι] (n o₁ : Cost.PolyTimeFun ι Cost.Unary) (w₁ : Cost.PolyTimeFun ι Cost.BitStr) (o₂ : Cost.PolyTimeFun ι Cost.Unary) (w₂ : Cost.PolyTimeFun ι Cost.BitStr) : Cost.PolyTimeFun ι Cost.BitStr

The vector place2 n o₁ w₁ o₂ w₂.

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.place2Of_apply {ι : Type} [Cost.SizedEncoding ι] (n o₁ : Cost.PolyTimeFun ι Cost.Unary) (w₁ : Cost.PolyTimeFun ι Cost.BitStr) (o₂ : Cost.PolyTimeFun ι Cost.Unary) (w₂ : Cost.PolyTimeFun ι Cost.BitStr) (a : ι) : (place2Of n o₁ w₁ o₂ w₂).toFun a = place2 (List.length (n.toFun a)) (List.length (o₁.toFun a)) (w₁.toFun a) (List.length (o₂.toFun a)) (w₂.toFun a)

noncomputable def MIPRE.Tailored.Intro.rQ : Cost.PolyTimeFun (Cost.BitStr × RParams) Cost.Unary

The projections of the input (c, params) of the re-indexing.

Equations

• MIPRE.Tailored.Intro.rQ = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Tailored.Intro.rR : Cost.PolyTimeFun (Cost.BitStr × RParams) Cost.Unary

Equations

• MIPRE.Tailored.Intro.rR = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.Tailored.Intro.rRa : Cost.PolyTimeFun (Cost.BitStr × RParams) Cost.Unary

Equations

• MIPRE.Tailored.Intro.rRa = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.Tailored.Intro.rLa : Cost.PolyTimeFun (Cost.BitStr × RParams) Cost.Unary

Equations

• MIPRE.Tailored.Intro.rLa = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.Tailored.Intro.rRb : Cost.PolyTimeFun (Cost.BitStr × RParams) Cost.Unary

Equations

• MIPRE.Tailored.Intro.rRb = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.Tailored.Intro.rLb : Cost.PolyTimeFun (Cost.BitStr × RParams) Cost.Unary

Equations

• MIPRE.Tailored.Intro.rLb = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd)))

noncomputable def MIPRE.Tailored.Intro.rla : Cost.PolyTimeFun (Cost.BitStr × RParams) Cost.Unary

Equations

• MIPRE.Tailored.Intro.rla = MIPRE.Cost.PolyTimeFun.fst.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.Intro.rlb : Cost.PolyTimeFun (Cost.BitStr × RParams) Cost.Unary

Equations

• MIPRE.Tailored.Intro.rlb = MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp (MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd))

noncomputable def MIPRE.Tailored.Intro.reindexF : Cost.PolyTimeFun (Cost.BitStr × RParams) Cost.BitStr

The re-indexing reindex, on (c, params).

Equations

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

theorem MIPRE.Tailored.Intro.getD_eq_headD_drop (c : Cost.BitStr) (k : ℕ) : List.getD c k false = (List.drop k c).headD false

@[simp]

theorem MIPRE.Tailored.Intro.reindexF_apply (c : Cost.BitStr) (P : RParams) : reindexF.toFun (c, P) = reindex (List.length P.1.1) (List.length P.1.2) (List.length P.2.1.1.1) (List.length P.2.1.1.2) (List.length P.2.1.2.1) (List.length P.2.1.2.2) (List.length P.2.2.1) (List.length P.2.2.2) c

theorem MIPRE.Tailored.Intro.reindexF_spec (Q R lRa lLa lRb lLb la lb : ℕ) (c : Cost.BitStr) : reindexF.toFun (c, rparams Q R lRa lLa lRb lLb la lb) = reindex Q R lRa lLa lRb lLb la lb c

The other orientation

noncomputable def MIPRE.Tailored.Intro.swapConF : Cost.PolyTimeFun (Cost.BitStr × Cost.Unary × Cost.Unary) Cost.BitStr

The swapped constraint swapCon, on (c, (la, lb)).

Equations

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

@[simp]

theorem MIPRE.Tailored.Intro.swapConF_apply (c : Cost.BitStr) (la lb : Cost.Unary) : swapConF.toFun (c, la, lb) = swapCon (List.length la) (List.length lb) c

noncomputable def MIPRE.Tailored.Intro.swapConsF : Cost.PolyTimeFun (List Cost.BitStr × Cost.Unary × Cost.Unary) (List Cost.BitStr)

The swapped constraints of a list, on (cs, (la, lb)).

Equations

• MIPRE.Tailored.Intro.swapConsF = MIPRE.Tailored.Intro.swapConF.mapWith

@[simp]

theorem MIPRE.Tailored.Intro.swapConsF_apply (cs : List Cost.BitStr) (la lb : Cost.Unary) : swapConsF.toFun (cs, la, lb) = List.map (swapCon (List.length la) (List.length lb)) cs

theorem MIPRE.Tailored.Intro.swapConsF_spec (cs : List Cost.BitStr) (la lb : ℕ) : swapConsF.toFun (cs, Cost.unary la, Cost.unary lb) = List.map (swapCon la lb) cs