The row-proof arithmetic layer, deep-embedded

This is step A of the proof-data source: affine forms, contexts, and the entailment checker of the format spec §4.1 / §13.4, as Bool functions over List ℤ, proved sound once.

Representation discipline

Everything generated is List ℤ addressed with List.getD. No ![…], no Fin-indexed functions, no Matrix.cons. This is not a style preference: the accompanying analysis §5 measured 198 s of kernel type-checking for one rfl through ![…] at a Fin numeral against 15 ms for the same goal by decide, and the accompanying analysis records 189,527 unfoldings of instDecidableEqSum.decEq from the same family of mistake.

The one design decision worth recording

A form c + Σ aᵢ xᵢ is stored as the single list c :: a, and evaluated as dot g (1 :: x) — the constant is just the coefficient of a leading 1 coordinate. Evaluation is then literally a dot product, so it is additive and homogeneous in the form by two three-line inductions, and every soundness step downstream is linear algebra rather than case analysis on the head.

Out-of-range certificate indices need no bounds check. List.getD returns [] there, eval [] x = 0, and a zero row is harmless on both sides: with a nonnegative multiplier it contributes 0 ≥ 0 to the inequality part, and any multiplier contributes 0 to the equality part. So the checker is fail-closed on malformed indices without spending a comparison on them.

@[reducible, inline]

abbrev Utilities.Subdivision.ClosedRowProof.Form : Type

An affine form c + Σ aᵢ xᵢ, stored as c :: a.

Equations

• Utilities.Subdivision.ClosedRowProof.Form = List ℤ

def Utilities.Subdivision.ClosedRowProof.dot : List ℤ → List ℤ → ℤ

Dot product, truncating at the shorter list.

Equations

• Utilities.Subdivision.ClosedRowProof.dot [] x✝ = 0
• Utilities.Subdivision.ClosedRowProof.dot x✝ [] = 0
• Utilities.Subdivision.ClosedRowProof.dot (a :: as) (b :: bs) = a * b + Utilities.Subdivision.ClosedRowProof.dot as bs

def Utilities.Subdivision.ClosedRowProof.eval (g : Form) (x : List ℤ) : ℤ

Evaluate a form at a point. The constant term is the coefficient of the leading 1, which makes eval a dot product and hence linear in the form.

Equations

• Utilities.Subdivision.ClosedRowProof.eval g x = Utilities.Subdivision.ClosedRowProof.dot g (1 :: x)

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.dot_nil_left (y : List ℤ) : dot [] y = 0

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.dot_nil_right (l : List ℤ) : dot l [] = 0

@[simp]

theorem Utilities.Subdivision.ClosedRowProof.eval_nil (x : List ℤ) : eval [] x = 0

def Utilities.Subdivision.ClosedRowProof.addForm : Form → Form → Form

Sum of two forms, aligned at the constant term.

Equations

• Utilities.Subdivision.ClosedRowProof.addForm [] x✝ = x✝
• Utilities.Subdivision.ClosedRowProof.addForm x✝ [] = x✝
• Utilities.Subdivision.ClosedRowProof.addForm (a :: as) (b :: bs) = (a + b) :: Utilities.Subdivision.ClosedRowProof.addForm as bs

def Utilities.Subdivision.ClosedRowProof.smulForm (k : ℤ) (f : Form) : Form

Scalar multiple of a form.

Equations

• Utilities.Subdivision.ClosedRowProof.smulForm k f = List.map (fun (a : ℤ) => k * a) f

def Utilities.Subdivision.ClosedRowProof.subForm (f g : Form) : Form

Difference of two forms.

Equations

• Utilities.Subdivision.ClosedRowProof.subForm f g = Utilities.Subdivision.ClosedRowProof.addForm f (Utilities.Subdivision.ClosedRowProof.smulForm (-1) g)

theorem Utilities.Subdivision.ClosedRowProof.dot_addForm (f g : Form) (y : List ℤ) : dot (addForm f g) y = dot f y + dot g y

theorem Utilities.Subdivision.ClosedRowProof.dot_smulForm (k : ℤ) (f : Form) (y : List ℤ) : dot (smulForm k f) y = k * dot f y

theorem Utilities.Subdivision.ClosedRowProof.eval_addForm (f g : Form) (x : List ℤ) : eval (addForm f g) x = eval f x + eval g x

theorem Utilities.Subdivision.ClosedRowProof.eval_smulForm (k : ℤ) (f : Form) (x : List ℤ) : eval (smulForm k f) x = k * eval f x

theorem Utilities.Subdivision.ClosedRowProof.eval_subForm (f g : Form) (x : List ℤ) : eval (subForm f g) x = eval f x - eval g x

theorem Utilities.Subdivision.ClosedRowProof.dot_eq_zero_of_all_zero {l : List ℤ} (h : ∀ a ∈ l, a = 0) (y : List ℤ) : dot l y = 0

A form all of whose coefficients vanish evaluates to 0.

def Utilities.Subdivision.ClosedRowProof.formEq (f g : Form) : Bool

Syntactic equality of forms, up to padding: their difference is zero in every coordinate.

Equations

• Utilities.Subdivision.ClosedRowProof.formEq f g = List.all (Utilities.Subdivision.ClosedRowProof.subForm f g) fun (a : ℤ) => a == 0

theorem Utilities.Subdivision.ClosedRowProof.eval_eq_of_formEq {f g : Form} (h : formEq f g = true) (x : List ℤ) : eval f x = eval g x

Contexts

structure Utilities.Subdivision.ClosedRowProof.Context : Type

A context: forms asserted ≥ 0 and forms asserted = 0.

• ge : List Form

  Forms asserted nonnegative.

• eq : List Form

  Forms asserted zero.

def Utilities.Subdivision.ClosedRowProof.Context.Holds (Γ : Context) (x : List ℤ) : Prop

The point x satisfies the context.

Equations

• Γ.Holds x = ((∀ g ∈ Γ.ge, 0 ≤ Utilities.Subdivision.ClosedRowProof.eval g x) ∧ ∀ g ∈ Γ.eq, Utilities.Subdivision.ClosedRowProof.eval g x = 0)

Entailment certificates

A certificate for Γ ⊢ g ≥ 0 is (k; λ; μ; c) with k ≥ 1, λ sparse nonnegative weights into Γ.ge, μ sparse weights into Γ.eq, c ≥ 0, and

k · g  =  Σ λᵢ Γ.geᵢ  +  Σ μⱼ Γ.eqⱼ  +  c

as an identity of forms. Nothing searches for λ; the generator supplies it.

def Utilities.Subdivision.ClosedRowProof.combineRows (rows : List Form) (w : List (ℕ × ℤ)) : Form

A sparse combination of context rows.

Equations

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

structure Utilities.Subdivision.ClosedRowProof.Cert : Type

An entailment certificate.

• k : ℤ

  The positive scaling k.

• lam : List (ℕ × ℤ)

  Sparse nonnegative weights on the inequality rows.

• mu : List (ℕ × ℤ)

  Sparse weights on the equality rows.

• c : ℤ

  The nonnegative slack constant.

def Utilities.Subdivision.ClosedRowProof.Cert.combination (w : Cert) (Γ : Context) : Form

The form the certificate claims equals k · g.

Equations

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

def Utilities.Subdivision.ClosedRowProof.Cert.check (w : Cert) (Γ : Context) (g : Form) : Bool

The checker of spec §4.1. One pass over the sparse lists and one vector comparison; no rounding, deliberately (§13.4).

Equations

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

theorem Utilities.Subdivision.ClosedRowProof.eval_getD_nonneg {rows : List Form} {x : List ℤ} (hrows : ∀ g ∈ rows, 0 ≤ eval g x) (i : ℕ) : 0 ≤ eval (rows.getD i []) x

A getD into a list of nonnegative-valued forms is nonnegative-valued: out of range it is [], which evaluates to 0.

theorem Utilities.Subdivision.ClosedRowProof.eval_getD_eq_zero {rows : List Form} {x : List ℤ} (hrows : ∀ g ∈ rows, eval g x = 0) (i : ℕ) : eval (rows.getD i []) x = 0

The same for a list of zero-valued forms.

theorem Utilities.Subdivision.ClosedRowProof.combineRows_nonneg {rows : List Form} {w : List (ℕ × ℤ)} {x : List ℤ} (hrows : ∀ g ∈ rows, 0 ≤ eval g x) (hw : ∀ p ∈ w, 0 ≤ p.2) : 0 ≤ eval (combineRows rows w) x

theorem Utilities.Subdivision.ClosedRowProof.combineRows_eq_zero {rows : List Form} {w : List (ℕ × ℤ)} {x : List ℤ} (hrows : ∀ g ∈ rows, eval g x = 0) : eval (combineRows rows w) x = 0

theorem Utilities.Subdivision.ClosedRowProof.Cert.check_sound {w : Cert} {Γ : Context} {g : Form} (h : w.check Γ g = true) {x : List ℤ} (hx : Γ.Holds x) : 0 ≤ eval g x

Soundness of the entailment layer.

If the checker accepts, the form really is nonnegative everywhere on the context. This is the only thing the rest of the lowering may assume about certificates.