Linear forms on windows of the answers

The linear-constraints processor of the tailored question reduction writes its constraints as linear forms on fixed windows of the two answers: a register sits at a known offset of the re-encoded answer (MIPRE.Tailored.Intro.enc). This file is the arithmetic of that:

• dotL c v, the F₂ inner product of two bit strings, and satisfies_append_iff: the constraint α ++ β ++ [γ] holds of a ++ b ++ [true] exactly when ⟨α, a⟩ + ⟨β, b⟩ = γ;
• place n off w, the vector of length n carrying w at offset off, and dotL_place: its inner product with a is that of w with the window of a at off;
• eqCons: the constraints that a window of a equals a window of b, bit by bit, and eqCons_iff;
• guardCons b: no constraint when the readable condition b holds, the rejecting one otherwise.

The inner product

def MIPRE.Tailored.Intro.dotL : Cost.BitStr → Cost.BitStr → Bool

The F₂ inner product of two bit strings, on their common prefix.

Equations

• MIPRE.Tailored.Intro.dotL (x_2 :: c) (y :: v) = (x_2 && y ^^ MIPRE.Tailored.Intro.dotL c v)
• MIPRE.Tailored.Intro.dotL x✝¹ x✝ = false

@[simp]

theorem MIPRE.Tailored.Intro.dotL_nil_left (v : Cost.BitStr) : dotL [] v = false

@[simp]

theorem MIPRE.Tailored.Intro.dotL_cons_cons (x y : Bool) (c v : Cost.BitStr) : dotL (x :: c) (y :: v) = (x && y ^^ dotL c v)

theorem MIPRE.Tailored.Intro.dotL_eq_odd (c v : Cost.BitStr) : dotL c v = decide (Odd (List.count true (List.zipWith (fun (x1 x2 : Bool) => x1 && x2) c v)))

theorem MIPRE.Tailored.Intro.satisfies_iff_dotL {c v : Cost.BitStr} (h : List.length c = List.length v) : Satisfies c v ↔ dotL c v = false

theorem MIPRE.Tailored.Intro.dotL_append {c c' v v' : Cost.BitStr} : List.length c = List.length v → dotL (c ++ c') (v ++ v') = (dotL c v ^^ dotL c' v')

theorem MIPRE.Tailored.Intro.satisfies_append_iff {α β a b : Cost.BitStr} (γ : Bool) (ha : List.length α = List.length a) (hb : List.length β = List.length b) : Satisfies (α ++ β ++ [γ]) (a ++ b ++ [true]) ↔ (dotL α a ^^ dotL β b) = γ

A constraint on the two answers and the affine coordinate, read.

theorem MIPRE.Tailored.Intro.dotL_replicate_false (m : ℕ) (v : Cost.BitStr) : dotL (List.replicate m false) v = false

Vectors placed at an offset

def MIPRE.Tailored.Intro.place (n off : ℕ) (w : Cost.BitStr) : Cost.BitStr

The vector of length n with w at offset off and zeros elsewhere (when it fits).

Equations

• MIPRE.Tailored.Intro.place n off w = List.replicate off false ++ w ++ List.replicate (n - off - List.length w) false

theorem MIPRE.Tailored.Intro.length_place {n off : ℕ} {w : Cost.BitStr} (h : off + List.length w ≤ n) : List.length (place n off w) = n

theorem MIPRE.Tailored.Intro.dotL_place {n off : ℕ} {w a : Cost.BitStr} (h : off + List.length w ≤ n) (ha : List.length a = n) : dotL (place n off w) a = dotL w (List.take (List.length w) (List.drop off a))

The inner product with a placed vector is that with the window.

Equality of windows

def MIPRE.Tailored.Intro.unit (m i : ℕ) : Cost.BitStr

The unit vector eᵢ of length m.

Equations

• MIPRE.Tailored.Intro.unit m i = MIPRE.Tailored.Intro.place m i [true]

theorem MIPRE.Tailored.Intro.length_unit {m i : ℕ} (hi : i < m) : List.length (unit m i) = m

theorem MIPRE.Tailored.Intro.dotL_unit {m i : ℕ} (hi : i < m) {w : Cost.BitStr} (hw : List.length w = m) : dotL (unit m i) w = w[i]

def MIPRE.Tailored.Intro.eqCons (la lb oa ob m : ℕ) : List Cost.BitStr

The constraints a_{oa+i} = b_{ob+i} for i < m, on answers of lengths la, lb.

Equations

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

theorem MIPRE.Tailored.Intro.eqCons_iff {la lb oa ob m : ℕ} {a b : Cost.BitStr} (ha : List.length a = la) (hb : List.length b = lb) (hoa : oa + m ≤ la) (hob : ob + m ≤ lb) : (∀ c ∈ eqCons la lb oa ob m, Satisfies c (a ++ b ++ [true])) ↔ List.take m (List.drop oa a) = List.take m (List.drop ob b)

The window equality constraints hold exactly when the windows are equal.

Readable guards

def MIPRE.Tailored.Intro.guardCons (b : Bool) (d : ℕ) : List Cost.BitStr

No constraint when the readable condition holds, the rejecting one otherwise.

Equations

• MIPRE.Tailored.Intro.guardCons b d = if b = true then [] else [MIPRE.Tailored.rejectConstraint d]

theorem MIPRE.Tailored.Intro.guardCons_iff {b : Bool} {d : ℕ} {v : Cost.BitStr} : (∀ c ∈ guardCons b d, Satisfies c (v ++ [true])) ↔ b = true