linarith

LinUnit

data LinUnit

A one-element type used as the trivial target of transports and as the empty hypothesis list’s proof.

linAbsurd

def linAbsurd {A : Type} (h : false = true) : A

Eliminates an impossible equation false = true into any type.

linZeroNeqSucc

def linZeroNeqSucc {A : Type} (n : Nat) (h : succ n = zero) : A

Eliminates an impossible equation succ n = zero into any type.

linPred

def linPred (n : Nat) : Nat

Predecessor on Nat with pred zero = zero, used to derive injectivity of succ.

linSuccInj

def linSuccInj (a : Nat) (b : Nat) (p : succ a = succ b) : a = b

Injectivity of succ: succ a = succ b implies a = b.

linCancelL

def linCancelL (x : Nat) (m : Nat) (n : Nat) (p : add x m = add x n) : m = n

Left cancellation of addition on Nat: x + m = x + n implies m = n.

linLeW

def linLeW (a : Nat) (b : Nat) (h : Nat.ble a b = true) : (k : Nat) × (add a k = b)

Turns a true Nat.ble a b into a witness k with a + k = b.

linBleAdd

def linBleAdd (a : Nat) (k : Nat) : Nat.ble a (add a k) = true

Nat.ble a (a + k) always evaluates to true.

linBleOf

def linBleOf (a : Nat) (b : Nat) (k : Nat) (p : add a k = b) : Nat.ble a b = true

Turns a witness a + k = b into a proof that Nat.ble a b is true.

linLtW

def linLtW (a : Nat) (b : Nat) (h : Nat.blt a b = true) : (k : Nat) × (add (succ a) k = b)

Turns a true Nat.blt a b into a witness k with succ a + k = b.

linBltAdd

def linBltAdd (a : Nat) (k : Nat) : Nat.blt a (add (succ a) k) = true

Nat.blt a (succ a + k) always evaluates to true.

linBltOf

def linBltOf (a : Nat) (b : Nat) (k : Nat) (p : add (succ a) k = b) : Nat.blt a b = true

Turns a witness succ a + k = b into a proof that Nat.blt a b is true.

linBleOfW

def linBleOfW (a : Nat) (b : Nat) (w : (k : Nat) × (add a k = b)) : Nat.ble a b = true

Like linBleOf but takes the witness as a single pair, so the caller computes it only once.

linBltOfW

def linBltOfW (a : Nat) (b : Nat) (w : (k : Nat) × (add (succ a) k = b)) : Nat.blt a b = true

Like linBltOf but takes the witness as a single pair, so the caller computes it only once.

LinHyp

data LinHyp

A linarith hypothesis lin a b c k: eval a + k = eval b, used with coefficient c.

linHolds

def linHolds (ρ : List Nat) (l : List LinHyp) : Type

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

linA

def linA (l : List LinHyp) : RingExpr

The coefficient-weighted sum of the hypotheses’ left-hand sides as a ring expression.

linB

def linB (l : List LinHyp) : RingExpr

The coefficient-weighted sum of the hypotheses’ right-hand sides as a ring expression.

linK

def linK (l : List LinHyp) : Nat

The coefficient-weighted sum of the hypotheses’ slack witnesses.

linStepRearr

theorem linStepRearr (x : Nat) (y : Nat) (sa : Nat) (sk : Nat) : add (add x y) (add sa sk) = add (add x sa) (add y sk)

Rearranges (x + y) + (sa + sk) into (x + sa) + (y + sk); a step lemma for linBEq.

linBEq

def linBEq (ρ : List Nat) (l : List LinHyp) (pf : linHolds ρ l) : ringEval ρ (linB l) = add (ringEval ρ (linA l)) (linK l)

Given the hypotheses hold, the weighted right-hand sum equals the weighted left-hand sum plus the weighted slacks.

linRearr

theorem linRearr (a : Nat) (s : Nat) (sa : Nat) (sk : Nat) : add (add a s) (add sa sk) = add sa (add a (add s sk))

Rearranges (a + s) + (sa + sk) into sa + (a + (s + sk)); a step lemma for linarithCert.

linarithCert

def linarithCert (ρ : List Nat) (l : List LinHyp) (pf : linHolds ρ l) (a : RingExpr) (b : RingExpr) (s : RingExpr) (cert : ringNorm (radd b (linA l)) = ringNorm (radd (radd a s) (linB l))) : add (ringEval ρ a) (add (ringEval ρ s) (linK l)) = ringEval ρ b

Core of the Farkas certificate check: a polynomial identity between the goal and the weighted hypotheses yields a + (s + slacks) = b.

linMulCancel

def linMulCancel (L : Nat) (a : Nat) (b : Nat) (k : Nat) (p : add (mul a (succ L)) k = mul b (succ L)) : (k2 : Nat) × (add a k2 = b)

Cancels a positive multiplier: a·(L+1) + k = b·(L+1) yields a witness that a <= b.

linarithLe

def linarithLe (ρ : List Nat) (l : List LinHyp) (pf : linHolds ρ l) (a : RingExpr) (b : RingExpr) (s : RingExpr) (L : Nat) (cert : ringNorm (radd (rmul b (rnum (succ L))) (linA l)) = ringNorm (radd (radd (rmul a (rnum (succ L))) s) (linB l))) : Nat.ble (ringEval ρ a) (ringEval ρ b) = true

The certificate the linarith tactic produces for a <= goals over Nat: a Farkas certificate checked by ringNorm proves Nat.ble a b.

linarithLt

def linarithLt (ρ : List Nat) (l : List LinHyp) (pf : linHolds ρ l) (a : RingExpr) (b : RingExpr) (s : RingExpr) (L : Nat) (cert : ringNorm (radd (rmul b (rnum (succ L))) (linA l)) = ringNorm (radd (radd (rmul (radd (rnum (succ zero)) a) (rnum (succ L))) s) (linB l))) : Nat.blt (ringEval ρ a) (ringEval ρ b) = true

The certificate the linarith tactic produces for a < goals over Nat: a Farkas certificate checked by ringNorm proves Nat.blt a b.

linarithTestTrans

def linarithTestTrans (x : Nat) (y : Nat) (z : Nat) (h1 : Nat.ble x y = true) (h2 : Nat.ble y z = true) : Nat.ble x z = true

Example of using linarithLe directly to prove transitivity of <= without the tactic.

linEqW

def linEqW (a : Nat) (b : Nat) (p : a = b) : (k : Nat) × (add a k = b)

Turns an equation a = b into a <= witness from a to b with slack zero.

linEqWSym

def linEqWSym (a : Nat) (b : Nat) (p : a = b) : (k : Nat) × (add b k = a)

Turns an equation a = b into a <= witness from b to a with slack zero.

linFalseRearr

theorem linFalseRearr (a : Nat) (k : Nat) (s : Nat) (l : Nat) : add (add (add a k) s) (succ l) = add a (succ (add k (add s l)))

Rearranges ((a + k) + s) + succ l into a + succ (k + (s + l)); a step lemma for linarithFalse.

linarithFalse

def linarithFalse (ρ : List Nat) (l : List LinHyp) (pf : linHolds ρ l) (s : RingExpr) (L : Nat) (cert : ringNorm (radd (radd (linB l) s) (rnum (succ L))) = ringNorm (linA l)) : Empty

Derives a contradiction from hypotheses whose weighted sums would force a strictly positive number to be zero.

linarithAbsurd

def linarithAbsurd (A : Type) (ρ : List Nat) (l : List LinHyp) (pf : linHolds ρ l) (s : RingExpr) (L : Nat) (cert : ringNorm (radd (radd (linB l) s) (rnum (succ L))) = ringNorm (linA l)) : A

Proves any goal from a contradictory set of linear hypotheses, via linarithFalse.