Counterexample for omega

Stream: metaprogramming / tactics

[Mirek Olšák]

Is it possible to extract an integer counterexample when the tactic omega fails? Similarly as SMT solvers can output a solution when it exists. For example given

example (a : ℤ) :
  3*a > 4 → 3*a ≤ 11 → a < 3 → false := by
  intros
  omega

I would like omega to tell

tactic omega failed, possible evaluation: a = 2

I have found the option

set_option trace.omega true

but honestly, I don't understand much what is going on -- I know basics of linear programming, but not anything deeper, e.g. how to get from the domain of rational numbers to integers.

[Henrik Böving]

Iirc the omega test is capable of producing a counter example so if the omega tactic cant do it right now it should hopefully be possible to get there if someone puts in the effort.

[Kim Morrison]

It's in the roadmap, but not quite yet! Note that the current implementation of omega is still missing the "dark and grey shadows" part of the algorithm, so it is not a complete decision procedure, and can sometimes fail without identifying a counterexample.

Once I put out a few more immediate fires I will improve the trace output for omega, and hopefully not too long after that implement the dark and grey shadows, and from there provide counterexamples.

[Mario Carneiro]

there is also the issue that counterexamples may not be true counterexamples because omega generalizes anything it doesn't understand to a variable, so it might e.g say that sin x ^ 2 + cos x ^ 2 = 1 is false if you consider sin x ^ 2 = 0 and cos x ^ 2 = 0

[Mirek Olšák]

@Scott Morrison Thanks for clarifying the current state. I didn't know it is not a complete procedure yet. And of course I know the counterexample doesn't have to be a full counterexample, only a partial one suggesting that (in iProver's terminology) more refinement is needed.

[Mario Carneiro]

I wonder how much this overlaps with slim_check. It's possible that in most small cases of this you can already get slim_check to give you a counterexample:

import Mathlib.Tactic.SlimCheck

example (a : ℤ) :
  3*a > 4 → 3*a ≤ 11 → a < 3 → false := by
  intros
  slim_check

-- Found problems!
-- a := 2
-- guard: 4 < 6
-- guard: 6 ≤ 11
-- guard: 2 < 3
-- issue: false does not hold
-- (0 shrinks)