unexpected failures with omega

[robertylewis]

omega fails when there are things in the context that are not linear inequalities and depend on the nat/int atoms. This makes it way less convenient than one would hope, since it's pretty common to have hypotheses like these floating around, and clearing them manually is a pain.

All of the following fail:

import tactic.omega

example (a b : ℕ) (h : a < b + 1) (ha : a.prime) : a ≤ b := 
by omega

example (a b c : ℕ) (h : a < b + 1) (ha : c.prime) : a ≤ b := 
by omega

example (a b : ℕ) (h : a < b + 1) (p : fin a) : a ≤ b := 
by omega

@skbaek would it be possible to improve the hypothesis filtering? I don't think it would be hard to check whether an expression is in the language omega understands.

[robertylewis]

Additionally, tactic.interactive.omega is missing a doc string, which makes it hard to find the options omega manual, omega int, etc.

[robertylewis]

Another example of strange behavior: the first one succeeds, the second fails. In other cases, omega doesn't care whether variables and hypotheses are in the context or the goal.

lemma int.pred_ne_self (n : ℤ) : n - 1 ≠ n :=
by intro h; omega

lemma int.pred_ne_self' (n : ℤ) : n - 1 ≠ n :=
by omega

[mukeshtiwari]

I believe that I have also found a case where omega fails to solve the goal. I got error for the lemma: lemma three_le_four : 3 < 4 := by omega
The error message is tactic failed, there is no goals to be solved. In general, it fails when the difference is 1, i.e. 3 < 4, 4 < 5, or 5 < 6. Interestingly, it solves a more general form happily lemma three_le_four (n : ℕ): n < n + 1 := by omega .

Version: 1.39.2
Commit: 6ab598523be7a800d7f3eb4d92d7ab9a66069390
Date: 2019-10-15T15:33:00.827Z
Electron: 4.2.10
Chrome: 69.0.3497.128
Node.js: 10.11.0
V8: 6.9.427.31-electron.0
OS: Darwin x64 19.0.0
Lean: 3.4.2

[robertylewis]

Indeed, that's a bug. Note that norm_num is the more appropriate tactic there -- omega is mainly for goals with variables -- but omega should still succeed.

omega is a very big tactic and I'd rather not try to fix these things myself. @skbaek do you think you'll have a chance any time soon to investigate these issues?

[robertylewis]

@kbuzzard mentioned this example on Zulip:

example {X : Type} [fintype X] (n k : ℕ) (hk : k + 1 ≤ n) : n - k = n - (k + 1) + 1 := 
begin
  omega
end

omega tries to clear X, which fails because of the instance argument. @skbaek any thoughts? I'm not sure why these have to be cleared at all; can't they just be left alone in the local context?

[fpvandoorn]

here is another failure

1 goal
n : ℕ,
G_C G_L : list ℤ,
hG : length G_C + length G_L = n + 1,
iv : ℕ,
hi : iv < length G_C
⊢ iv + (length G_C - iv - 1) + length G_L = n

[robertylewis]

I'm not sure what the expected behavior of omega is on goals with nat division (by constants). It seems not to treat m / 3 as an atom, but also doesn't treat it correctly. There's a bug here but I don't know in which direction.

-- omega isn't happy with nat division
lemma foo1 (m : ℕ) : m / 3 ≤ m :=
by omega -- failed 

-- it's even less happy when you try to help it out.
lemma foo2 (m : ℕ) : m / 3 ≤ m :=
by { have h : m % 3 + 3 * (m / 3) = m := nat.mod_add_div m 3, 
     omega } -- invalid eval_expr, expression must be closed

-- if you generalize the `/` in `h` it succeeds
lemma foo3 (m p : ℕ) (h : m % 3 + 3 * p = m) : p ≤ m :=
by omega -- succeeds

lemma foo4 (m p : ℕ) (h : m % 3 + 3 * p = m) (h2 : p = m / 3) : m / 3 ≤ m :=
by omega -- succeeds

[robertylewis]

Another problem: this one seems easier to fix.

example (h : 0 > 1) : false := by omega -- Cannot reify expr : false

[robertylewis]

And from #2376 :

import tactic.omega

set_option profiler true

example (m : ℕ)
(hm5 : m % 5 < 5)
(lh : m % 5 = 3)
(hm3 : m % 5 = 3 % 5)
(hm4 : m * 3 % 5 = 4)
(h : m * 3 = 7) :
  9 ≤ 7 :=
begin
  -- ⊢ 9 ≤ 7
  omega -- <- finishes almost instantly
end

example (m : ℕ)
(hm5 : m % 5 < 5)
(lh : m % 5 = 3)
(hm3 : m % 5 = 3 % 5)
(hm4 : m * 3 % 5 = 4)
(h : m * 3 = 7) :
  9 ≤ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ (nat.succ nat.zero))))))) :=
begin
  -- ⊢ 9 ≤ 7
  omega -- <- takes three seconds
end

The contradiction is coming from h. In the bad case, each time I delete a hypothesis other than h, runtime halves. The same behaviour is not observed in the good case.

[kbuzzard]

Gabriel pointed out that as a preprocessing step

mathlib/src/tactic/omega/nat/main.lean

Line 24 in f723f37

nat.succ_eq_add_one

omega tries succ_eq_add_one, turning the bad 7 into 0 + 1 + 1 + 1 + 1 + 1 + 1 + 1. If add_assoc and zero_add and add_zero were also added, the 7 would become a much nicer 7.

[robertylewis]

This is an expected failure, but with an unexpected message:

import tactic.omega
example (p : ℕ) : p = p*p := by omega
-- invalid eval_expr, expression must be closed

[semorrison]

(omega will need a complete reimplementation in Lean4, hence the wontfix here. Perhaps when this happens, this issue can be re-incarnated as test cases.)