intlinarith

ilNegLe

def ilNegLe (x : Nat) (y : Nat) (h : or (Nat.blt y x) (Nat.beq x y) = true) : Nat.ble y x = true

Rewrites the order test between two negative integers into leNat y x.

ilNegLeBack

def ilNegLeBack (x : Nat) (y : Nat) (h : Nat.ble y x = true) : or (Nat.blt y x) (Nat.beq x y) = true

Converts leNat y x back into the order test between two negative integers.

ilLtToLe

def ilLtToLe (a : Nat) (b : Nat) (h : Nat.blt a b = true) : Nat.ble (succ a) b = true

A strict Nat comparison a < b gives succ a <= b.

ilLeToLt

def ilLeToLt (a : Nat) (b : Nat) (h : Nat.ble (succ a) b = true) : Nat.blt a b = true

succ a <= b gives the strict Nat comparison a < b.

ilLtSuccToLe

def ilLtSuccToLe (y : Nat) (x : Nat) (h : Nat.blt y (succ x) = true) : Nat.ble y x = true

y < succ x on Nat gives y <= x.

ilLeToLtSucc

def ilLeToLtSucc (y : Nat) (x : Nat) (h : Nat.ble y x = true) : Nat.blt y (succ x) = true

y <= x on Nat gives y < succ x.

ilOrTrueR

def ilOrTrueR (b : Bool) : or b true = true

A boolean disjunction with true on the right is true.

ilLeZero

def ilLeZero (y : Nat) : Nat.ble zero y = true

Zero is at most every natural number.

ilNegPos

theorem ilNegPos (p : Int) (y : Int) : Int.add (Int.neg p) (Int.add p y) = y

Ring identity: -p + (p + y) = y.

ilNegNeg

theorem ilNegNeg (p : Int) (k : Int) : Int.add (Int.neg (Int.add p k)) k = Int.neg p

Ring identity: -(p + k) + k = -p.

ilNegPosW

def ilNegPosW (x : Nat) (y : Nat) : Int.add (negsucc x) (pos (add (succ x) y)) = pos y

Adding pos (succ x + y) to negsucc x gives pos y.

ilNegNegW

def ilNegNegW (y : Nat) (k : Nat) : Int.add (negsucc (add y k)) (pos k) = negsucc y

Adding pos k to negsucc (y + k) gives negsucc y.

ileW

def ileW (a : Int) (b : Int) : Int.ble a b = true -> (k : Nat) × (Int.add a (pos k) = b)

Turns a <= b on Int into a witness k with a + k = b.

ileRefl

def ileRefl (a : Int) : Int.ble a a = true

The Int order is reflexive.

ileSucR

def ileSucR (a : Int) (c : Int) : Int.ble a c = true -> Int.ble a (Int.succ c) = true

If a <= c then a <= c + 1 on Int.

ileSubst

def ileSubst (a : Int) (b : Int) (c : Int) (p : b = c) (h : Int.ble a b = true) : Int.ble a c = true

Transports a <= b along an equality b = c.

ileAdd

def ileAdd (a : Int) (k : Nat) : Int.ble a (Int.add a (pos k)) = true

Every integer is at most itself plus a natural number.

ileOf

def ileOf (a : Int) (b : Int) (k : Nat) (p : Int.add a (pos k) = b) : Int.ble a b = true

A witness a + k = b gives a <= b on Int.

ileOfEq

def ileOfEq (a : Int) (b : Int) (p : a = b) : (k : Nat) × (Int.add a (pos k) = b)

An equality a = b gives the witness 0 for a <= b.

ileOfEqSym

def ileOfEqSym (a : Int) (b : Int) (p : a = b) : (k : Nat) × (Int.add b (pos k) = a)

An equality a = b gives the witness 0 for b <= a.

iltToLe

def iltToLe (a : Int) (b : Int) : Int.blt a b = true -> Int.ble (Int.succ a) b = true

A strict Int inequality a < b gives a + 1 <= b.

iltOfLe

def iltOfLe (a : Int) (b : Int) : Int.ble (Int.succ a) b = true -> Int.blt a b = true

a + 1 <= b on Int gives the strict inequality a < b.

ILinHyp

data ILinHyp

A hypothesis for the Int linarith certificate: two expressions with a witness that the first plus k equals the second, and its coefficient.

ilHolds

def ilHolds (ρ : List Int) (l : List ILinHyp) : Type

The proposition that every hypothesis in the list holds under the environment.

ilSum

def ilSum (l : List ILinHyp) : IntExpr

The expression for the weighted sum of hypothesis gaps, the sum of c * (b - a).

ilK

def ilK (l : List ILinHyp) : Nat

The natural number summing c * k over the hypotheses, the value of their weighted gap sum.

ilDiff

theorem ilDiff (a : Int) (k : Int) : Int.add (Int.add a k) (Int.neg a) = k

Ring identity: (a + k) - a = k.

ilDiffAt

def ilDiffAt (a : Int) (b : Int) (k : Nat) (h : Int.add a (pos k) = b) : Int.add b (Int.neg a) = pos k

A witness a + k = b gives b - a = k.

ilSumEval

def ilSumEval (ρ : List Int) (l : List ILinHyp) (pf : ilHolds ρ l) : intEval ρ (ilSum l) = pos (ilK l)

Under holding hypotheses, the weighted gap sum evaluates to the nonnegative integer ilK.

ilPosOfMul

def ilPosOfMul (L : Nat) (x : Int) (K : Nat) : Int.mul (pos (succ L)) x = pos K -> (k : Nat) × (x = pos k)

If a positive multiple of x is a nonnegative integer, x is nonnegative.

ilAddSub

theorem ilAddSub (a : Int) (b : Int) : Int.add a (Int.add b (Int.neg a)) = b

Ring identity: a + (b - a) = b.

intLinMul

def intLinMul (ρ : List Int) (l : List ILinHyp) (pf : ilHolds ρ l) (a : IntExpr) (b : IntExpr) (L : Nat) (c : Nat) (cert : intCheckL (imul (inum (succ L)) (iadd b (ineg a))) (iadd (ilSum l) (inum c)) = intCheckR (imul (inum (succ L)) (iadd b (ineg a))) (iadd (ilSum l) (inum c))) : Int.mul (pos (succ L)) (Int.add (intEval ρ b) (Int.neg (intEval ρ a))) = pos (add (ilK l) c)

Checked by the certificate, M times (b - a) equals the weighted hypothesis sum plus a constant, a nonnegative integer.

intLinW

def intLinW (ρ : List Int) (l : List ILinHyp) (pf : ilHolds ρ l) (a : IntExpr) (b : IntExpr) (L : Nat) (c : Nat) (cert : intCheckL (imul (inum (succ L)) (iadd b (ineg a))) (iadd (ilSum l) (inum c)) = intCheckR (imul (inum (succ L)) (iadd b (ineg a))) (iadd (ilSum l) (inum c))) : (k : Nat) × (Int.add (intEval ρ b) (Int.neg (intEval ρ a)) = pos k)

Under a valid certificate, b - a is a nonnegative integer.

ilLeOfDiff

def ilLeOfDiff (x : Int) (y : Int) (w : (k : Nat) × (Int.add y (Int.neg x) = pos k)) : Int.ble x y = true

A nonnegative difference y - x gives x <= y on Int.

intLinLe

def intLinLe (ρ : List Int) (l : List ILinHyp) (pf : ilHolds ρ l) (a : IntExpr) (b : IntExpr) (L : Nat) (c : Nat) (cert : intCheckL (imul (inum (succ L)) (iadd b (ineg a))) (iadd (ilSum l) (inum c)) = intCheckR (imul (inum (succ L)) (iadd b (ineg a))) (iadd (ilSum l) (inum c))) : Int.ble (intEval ρ a) (intEval ρ b) = true

Soundness of the Int linarith checker for a <= goal: a valid Farkas certificate over the hypotheses proves a <= b.

intLinLt

def intLinLt (ρ : List Int) (l : List ILinHyp) (pf : ilHolds ρ l) (a : IntExpr) (b : IntExpr) (L : Nat) (c : Nat) (cert : intCheckL (imul (inum (succ L)) (iadd b (ineg (iadd (inum (succ zero)) a)))) (iadd (ilSum l) (inum c)) = intCheckR (imul (inum (succ L)) (iadd b (ineg (iadd (inum (succ zero)) a)))) (iadd (ilSum l) (inum c))) : Int.blt (intEval ρ a) (intEval ρ b) = true

Soundness of the Int linarith checker for a strict goal: a certificate for a + 1 <= b proves a < b.

intLinTestTrans

def intLinTestTrans (x : Int) (y : Int) (z : Int) (h1 : Int.ble x y = true) (h2 : Int.ble y z = true) : Int.ble x z = true

Example use of intLinLe: from x <= y and y <= z conclude x <= z.

ilCancel

theorem ilCancel (a : Int) (p : Int) : p = Int.add (Int.add a p) (Int.neg a)

Ring identity: p = (a + p) - a.

ilNatAddZero

def ilNatAddZero (k1 : Nat) (k2 : Nat) : add k1 k2 = zero -> k1 = zero

If a sum of two natural numbers is zero, the first is zero.

ilAntisymW

def ilAntisymW (a : Int) (b : Int) (k1 : Nat) (k2 : Nat) (p1 : Int.add a (pos k1) = b) (p2 : Int.add b (pos k2) = a) : a = b

Antisymmetry of the Int order from explicit witnesses a + k1 = b and b + k2 = a.

ilUseLe

def ilUseLe (a : Int) (b : Int) (C : Type) (w : (k : Nat) × (Int.add a (pos k) = b)) (f : (k : Nat) -> Int.add a (pos k) = b -> C) : C

Eliminates an Int order witness into an arbitrary type by passing its components to a continuation.

ileAntisym

def ileAntisym (a : Int) (b : Int) (h1 : Int.ble a b = true) (h2 : Int.ble b a = true) : a = b

The Int order is antisymmetric: a <= b and b <= a imply a = b.

intLinFalse

def intLinFalse (ρ : List Int) (l : List ILinHyp) (pf : ilHolds ρ l) (c : Nat) (cert : intCheckL (iadd (ilSum l) (inum (succ c))) (inum zero) = intCheckR (iadd (ilSum l) (inum (succ c))) (inum zero)) : Empty

Soundness of the Int linarith contradiction checker: hypotheses whose weighted sum plus a positive constant is identically zero are inconsistent.

intLinAbsurd

def intLinAbsurd (A : Type) (ρ : List Int) (l : List ILinHyp) (pf : ilHolds ρ l) (c : Nat) (cert : intCheckL (iadd (ilSum l) (inum (succ c))) (inum zero) = intCheckR (iadd (ilSum l) (inum (succ c))) (inum zero)) : A

Proves any goal from inconsistent hypotheses certified by intLinFalse.