linsys

dot

def dot (u : List Int) (x : List Int) : Int

Dot product of two integer vectors, truncated to the shorter one.

vecAdd

def vecAdd (u : List Int) (v : List Int) : List Int

Componentwise sum of two integer vectors, keeping the tail of the longer one.

vecScale

def vecScale (c : Int) (u : List Int) : List Int

Scales every component of an integer vector by a constant.

linMix4

theorem linMix4 (a : Int) (b : Int) (y : Int) (p : Int) (q : Int) : Int.add (Int.mul (Int.add a b) y) (Int.add p q) = Int.add (Int.add (Int.mul a y) p) (Int.add (Int.mul b y) q)

Ring identity used to split the dot product of a vector sum into two dot products.

linMix2

theorem linMix2 (c : Int) (a : Int) (y : Int) (d : Int) : Int.add (Int.mul (Int.mul c a) y) (Int.mul c d) = Int.mul c (Int.add (Int.mul a y) d)

Ring identity used to pull a scalar factor out of a dot product.

dotAdd

def dotAdd (u : List Int) (v : List Int) (x : List Int) : dot (vecAdd u v) x = Int.add (dot u x) (dot v x)

Dot product distributes over vector addition on the left.

dotScale

def dotScale (c : Int) (u : List Int) (x : List Int) : dot (vecScale c u) x = Int.mul c (dot u x)

Scaling the left vector scales the dot product by the same constant.

Solves

def Solves (sys : List ((List Int) × Int)) (x : List Int) (f : Int) : Type

The proposition that x / f solves the system: every row satisfies dot a x = f * b.

combCoeffs

def combCoeffs (y : List Int) (sys : List ((List Int) × Int)) : List Int

Coefficient vector of the linear combination of the rows weighted by y.

combRhs

def combRhs (y : List Int) (sys : List ((List Int) × Int)) : Int

Right-hand side of the linear combination of the rows weighted by y.

linMix3

theorem linMix3 (c : Int) (f : Int) (b : Int) (rest : Int) : Int.add (Int.mul c (Int.mul f b)) (Int.mul f rest) = Int.mul f (Int.add (Int.mul c b) rest)

Ring identity used to factor the denominator out of a combined right-hand side.

combSound

def combSound (y : List Int) (sys : List ((List Int) × Int)) (x : List Int) (f : Int) : Solves sys x f -> dot (combCoeffs y sys) x = Int.mul f (combRhs y sys)

Any solution of the system also satisfies every linear combination of its rows.

boolCode

def boolCode (b : Bool) : Type

Maps true to Unit and false to Empty, used to separate the two booleans.

falseNeTrue

def falseNeTrue (p : false = true) : Empty

The boolean false is not equal to true.

isZeroVec

def isZeroVec (v : List Int) : Bool

Decides whether every component of an integer vector is zero.

isZeroIntSound

def isZeroIntSound (c : Int) : Int.isZero c = true -> c = pos zero

Soundness of Int.isZero: if it returns true the integer is zero.

andTrueL

def andTrueL (b : Bool) (c : Bool) : and b c = true -> b = true

If a boolean conjunction is true, its left operand is true.

andTrueElimR

def andTrueElimR (b : Bool) (c : Bool) : and b c = true -> c = true

If a boolean conjunction is true, its right operand is true.

isZeroVecDot

def isZeroVecDot (v : List Int) (x : List Int) : isZeroVec v = true -> dot v x = pos zero

A vector recognized as zero by isZeroVec has zero dot product with any vector.

mulPosSuccZero

def mulPosSuccZero (d : Nat) (c : Int) : Int.mul (pos (succ d)) c = pos zero -> c = pos zero

If a positive integer times c is zero, then c is zero.

linNoSolution

def linNoSolution (sys : List ((List Int) × Int)) (y : List Int) (h1 : isZeroVec (combCoeffs y sys) = true) (h2 : Int.isZero (combRhs y sys) = false) (x : List Int) (d : Nat) (s : Solves sys x (pos (succ d))) : Empty

Soundness of the no-solution certificate: a row combination with zero coefficients and nonzero right-hand side rules out every rational solution.

LinNoSolution

def LinNoSolution (sys : List ((List Int) × Int)) : Type

The statement that the system has no rational solution with a positive denominator.

linMix5

theorem linMix5 (a : Int) (x : Int) (z : Int) (p : Int) (q : Int) : Int.add (Int.mul a (Int.add x z)) (Int.add p q) = Int.add (Int.add (Int.mul a x) p) (Int.add (Int.mul a z) q)

Ring identity used to split a dot product over a sum on the right.

linMix6

theorem linMix6 (t : Int) (a : Int) (z : Int) (d : Int) : Int.add (Int.mul a (Int.mul t z)) (Int.mul t d) = Int.mul t (Int.add (Int.mul a z) d)

Ring identity used to pull a scalar factor out of the right vector of a dot product.

dotAddR

def dotAddR (u : List Int) (x : List Int) (z : List Int) : dot u (vecAdd x z) = Int.add (dot u x) (dot u z)

Dot product distributes over vector addition on the right.

dotScaleR

def dotScaleR (u : List Int) (t : Int) (z : List Int) : dot u (vecScale t z) = Int.mul t (dot u z)

Scaling the right vector scales the dot product by the same constant.

linShift

def linShift (sys : List ((List Int) × Int)) (x : List Int) (f : Int) (k : List Int) (t : Int) : Solves sys x f -> Solves sys k (pos zero) -> Solves sys (vecAdd x (vecScale t k)) f

Moving a solution any multiple t along a direction in the kernel of the system yields another solution.

LinUnderdetermined

def LinUnderdetermined (sys : List ((List Int) × Int)) : Type

Underdetermined certificate: a rational solution together with a nonzero direction k satisfying Ak = 0.

linSubEq

theorem linSubEq (a : Int) (c : Int) : a = Int.add (Int.add a (Int.neg c)) c

Ring identity rewriting a as (a - c) + c.

subZeroEq

def subZeroEq (a : Int) (c : Int) (p : Int.isZero (Int.sub a c) = true) : a = c

If Int.isZero recognizes a - c as zero, then a equals c.

isScaledUnit

def isScaledUnit (v : List Int) (j : Nat) (c : Int) : Bool

Decides whether a vector is c times the j-th unit vector (and has a j-th position).

scaledUnitDot

def scaledUnitDot (v : List Int) (j : Nat) (c : Int) (z : List Int) : isScaledUnit v j c = true -> dot v z = Int.mul c (intNth z j)

A vector that is c times the j-th unit vector has dot product with z equal to c times the j-th component of z.

linUniqueCoord

def linUniqueCoord (sys : List ((List Int) × Int)) (m : List Int) (j : Nat) (e : Nat) (h : isScaledUnit (combCoeffs m sys) j (pos (succ e)) = true) (z : List Int) (f : Int) (s : Solves sys z f) : Int.mul (pos (succ e)) (intNth z j) = Int.mul f (combRhs m sys)

If a row combination turns the coefficients into (e+1) times the j-th unit vector, it pins down the j-th component of every solution.

linPos

def linPos (i : Nat) (j : Nat) : Nat

Computes i + j by moving i onto j, the position handled by the i-th combination.

linPosZero

def linPosZero (i : Nat) (j : Nat) : linPos i j = add i j

linPos i j equals the ordinary sum i + j.

allUnitsFrom

def allUnitsFrom (ms : List (List Int)) (j : Nat) (sys : List ((List Int) × Int)) (e : Nat) : Bool

Checks that each successive combination in the list yields a scaled unit vector at consecutive positions starting from j.

listNthL

def listNthL (ms : List (List Int)) (i : Nat) : List Int

The i-th vector of a list of integer vectors, or the empty vector when out of range.

allUnitsNth

def allUnitsNth (ms : List (List Int)) (j : Nat) (sys : List ((List Int) × Int)) (e : Nat) (i : Nat) : allUnitsFrom ms j sys e = true -> Nat.blt i (length ms) = true -> isScaledUnit (combCoeffs (listNthL ms i) sys) (linPos i j) (pos (succ e)) = true

Extracts from allUnitsFrom that the i-th combination yields the scaled unit vector at position linPos i j.

linWidth

def linWidth (sys : List ((List Int) × Int)) : Nat

Number of variables of the system, the length of its longest coefficient row.

LinUnique

def LinUnique (sys : List ((List Int) × Int)) : Type

Unique-solution certificate: a rational solution plus one row combination per variable that pins that variable down.

linUniqueAt

def linUniqueAt (sys : List ((List Int) × Int)) (ms : List (List Int)) (e : Nat) (h : allUnitsFrom ms zero sys e = true) (i : Nat) (lt : Nat.blt i (length ms) = true) (z : List Int) (f : Int) (s : Solves sys z f) : Int.mul (pos (succ e)) (intNth z i) = Int.mul f (combRhs (listNthL ms i) sys)

Reads a unique-solution certificate: the i-th combination determines the i-th component of every solution.

BoundOp

data BoundOp

Comparison kinds for bounding a component of the unique solution: le, lt, ge, gt, eq, and absolute value at most.

boundCmp

def boundCmp (op : BoundOp) (l : Int) (r : Int) : Bool

Evaluates a bound comparison on two integers that already share a common denominator.

boundHolds

def boundHolds (op : BoundOp) (x : Int) (d : Nat) (num : Int) (den : Nat) : Bool

Checks whether x / (d+1) compares to num / (den+1) as the bound operator demands, by cross-multiplying.

LinBound

def LinBound (sys : List ((List Int) × Int)) (k : Nat) (op : BoundOp) (num : Int) (den : Nat) : Type

Bound certificate: the system has a unique solution and its k-th component satisfies the given rational bound.