intomega

iomMove

theorem iomMove (a : Int) (r : Int) : r = Int.add a (Int.add (Int.neg a) r)

r = a + (−a + r) over Int; a rearrangement used by iomPosOfMulR.

iomRearr

theorem iomRearr (G : Nat) (j : Nat) (K : Nat) : add (mul (succ G) (succ j)) K = add (succ G) (add (mul (succ G) j) K)

(G+1)·(j+1) + K = (G+1) + ((G+1)·j + K) over Nat; a rearrangement used by iomPosOfMulR.

iomPosOfMulR

def iomPosOfMulR (G : Nat) (r : Nat) (hr : Nat.blt r (succ G) = true) (x : Int) (K : Nat) : Int.add (Int.mul (pos (succ G)) x) (pos r) = pos K -> (k : Nat) × (x = pos k)

The integer cut over Int: (G+1)·x + r = K with 0 <= r < G+1 and K ≥ 0 forces x to be non-negative.

iomW

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

Turns a non-negative difference y − x = k into the witness x + k = y.

iomStep

def iomStep (ρ : List Int) (l : List ILinHyp) (pf : ilHolds ρ l) (X : IntExpr) (Y : IntExpr) (G : Nat) (r : Nat) (c : Nat) (hr : Nat.blt r (succ G) = true) (cert : intCheckL (iadd (imul (inum (succ G)) (iadd Y (ineg X))) (inum r)) (iadd (ilSum l) (inum c)) = intCheckR (iadd (imul (inum (succ G)) (iadd Y (ineg X))) (inum r)) (iadd (ilSum l) (inum c))) : (k : Nat) × (Int.add (intEval ρ X) (pos k) = intEval ρ Y)

One integer omega derivation step: a Farkas combination of the hypotheses plus the integer cut yields a witness that X <= Y.

iomLeFalse

def iomLeFalse (a : Int) (b : Int) (h : Int.ble a b = false) : Int.blt b a = true

If Int.ble a b is false then Int.blt b a is true.

iomLtFalse

def iomLtFalse (a : Int) (b : Int) (h : Int.blt a b = false) : Int.ble b a = true

If Int.blt a b is false then Int.ble b a is true.

iomLeByContra

def iomLeByContra (a : Int) (b : Int) (f : Int.blt b a = true -> Empty) : Int.ble a b = true

Proves a <= b over Int by refuting b < a.

iomLtByContra

def iomLtByContra (a : Int) (b : Int) (f : Int.ble b a = true -> Empty) : Int.blt a b = true

Proves a < b over Int by refuting b <= a.

iomEqByContra

def iomEqByContra (a : Int) (b : Int) (f1 : Int.blt b a = true -> Empty) (f2 : Int.blt a b = true -> Empty) : a = b

Proves a = b over Int by refuting both b < a and a < b.

intOmegaTestCut

def intOmegaTestCut (x : Int) (h : Int.ble (Int.mul (pos 2) x) (pos 5) = true) : (k : Nat) × (Int.add x (pos k) = pos 2)

Example of using iomStep directly to derive x <= 2 from 2x <= 5 over Int without the tactic.