Failure of omega

Stream: lean4

[Kyle Miller]

Here's something that ring can solve but omega cannot:

import Mathlib.Tactic.Ring

example {a b : ℤ} : (a - b) * (a + b) = a^2 - b^2 := by
  -- omega -- fails
  ring

Is this expected?

[Shreyas Srinivas]

I thought omega was only useful for nat. Is it not?

[Kyle Miller]

I was going to say "be sure to read the first line of the docstring," but I guess I need to read it too:

The omega tactic, for resolving integer and natural linear arithmetic problems

This is nonlinear arithmetic, so I guess I shouldn't be surprised it failed!

[Kyle Miller]

(Not only is omega useful for Int, but my understanding is that it converts everything from Nat to Int internally.)

[Henrik Böving]

Omega the decision procedure is a complete procedure for quantifier free linear integer arithmetic (or QF_LIA in SMT speak) our omega is an implementation of that procedure (not a complete implementation, it misses handling for some special cases) + lean specific things on top like the Nat reasoning etc.

[Shreyas Srinivas]

Oh right. I recall reading that omega is a decision procedure for quantifier free portion of presburger arithmetic which I thought was first order theory of natural numbers with addition. TIL integers are included.

[Shreyas Srinivas]

(deleted)

[Kim Morrison]

Multiplications are just treated as atoms by omega.