omega

omegaNotLtOf

def omegaNotLtOf (g : Nat) (n : Nat) (r : Nat) (p : add (succ g) n = r) (hr : Nat.blt r (succ g) = true) : Empty

(g+1) + n = r and r < g+1 cannot both hold; the arithmetic fact behind the integer cut.

omegaCutW

def omegaCutW (g : Nat) (r : Nat) (hr : Nat.blt r (succ g) = true) (X : Nat) (Y : Nat) (k : Nat) (p : add (mul X (succ g)) k = add (mul Y (succ g)) r) : (k2 : Nat) × (add X k2 = Y)

The integer cutting-plane step: (g+1)·X + k = (g+1)·Y + r with r < g+1 yields a witness that X <= Y.

omegaStep

def omegaStep (ρ : List Nat) (l : List LinHyp) (pf : linHolds ρ l) (X : RingExpr) (Y : RingExpr) (s : RingExpr) (g : Nat) (r : Nat) (hr : Nat.blt r (succ g) = true) (cert : ringNorm (radd (radd (rmul Y (rnum (succ g))) (rnum r)) (linA l)) = ringNorm (radd (radd (rmul X (rnum (succ g))) s) (linB l))) : (k : Nat) × (add (ringEval ρ X) k = ringEval ρ Y)

One omega derivation step: a Farkas combination of the hypotheses gives (g+1)·X <= (g+1)·Y + r, which the cut tightens to X <= Y.

omegaLeFalse

def omegaLeFalse (a : Nat) (b : Nat) (h : Nat.ble a b = false) : Nat.blt b a = true

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

omegaLtFalse

def omegaLtFalse (a : Nat) (b : Nat) (h : Nat.blt a b = false) : Nat.ble b a = true

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

omegaLeByContra

def omegaLeByContra (a : Nat) (b : Nat) (f : Nat.blt b a = true -> Empty) : Nat.ble a b = true

Proves a <= b by refuting b < a.

omegaLtByContra

def omegaLtByContra (a : Nat) (b : Nat) (f : Nat.ble b a = true -> Empty) : Nat.blt a b = true

Proves a < b by refuting b <= a.

omegaAntisym

def omegaAntisym (a : Nat) (b : Nat) (h1 : Nat.ble a b = true) (h2 : Nat.ble b a = true) : a = b

Antisymmetry of Nat.ble: a <= b and b <= a imply a = b.

omegaEqByContra

def omegaEqByContra (a : Nat) (b : Nat) (f1 : Nat.blt b a = true -> Empty) (f2 : Nat.blt a b = true -> Empty) : a = b

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

omegaSubAdd

def omegaSubAdd (a : Nat) (b : Nat) (h : Nat.ble b a = true) : add (sub a b) b = a

When b <= a, subtracting b and adding it back gives a.

omegaSubZero

def omegaSubZero (a : Nat) (b : Nat) (h : Nat.ble b a = false) : sub a b = zero

When a < b, truncated subtraction a - b is zero.

omegaSubCases

def omegaSubCases (a : Nat) (b : Nat) (s : Nat) (hs : s = sub a b) (P : Type) (k1 : Nat.ble b a = true -> add s b = a -> P) (k2 : Nat.ble b a = false -> s = zero -> P) : P

The two cases of a truncated subtraction s = a - b: either b <= a and s + b = a, or a < b and s = 0.

omegaPredSub

def omegaPredSub (a : Nat) : Nat.pred a = sub a 1

The predecessor is subtraction of one.

omegaPredCases

def omegaPredCases (a : Nat) (s : Nat) (hs : s = Nat.pred a) (P : Type) (k1 : Nat.ble 1 a = true -> add s 1 = a -> P) (k2 : Nat.ble 1 a = false -> s = zero -> P) : P

The two cases of s = pred a, as for a - 1.

omegaEqRefl

def omegaEqRefl (x : Nat) : x = x

Reflexivity at a given number; the omega tactic applies it to an atom in the core term.

omegaAbsurd

def omegaAbsurd (A : Type) (e : Empty) : A

Proves any goal from Empty; the omega tactic applies it with the goal type made explicit.

omegaTestCut

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

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