Omega failing due to terms with power?

Stream: lean4

[Sabbir Rahman]

(edited to make mathlib independent)

Hi, I was working on a proof related to natural numbers and noticed omega failing in a place where I was expecting it to succeed. I have been able to reduce it to following minimal reproduction:

example (a b : Nat) : a  = a + b - b := by
  omega

example (a b : Int) : a = a + b - b := by
  omega

example (a b : Nat) : a = a + 2^b - 2^b := by
  omega

example (a b : Nat) : 2^a = 2^a + b - b := by
  omega -- this one fails with following message
/-
omega could not prove the goal:
a possible counterexample may satisfy the constraints
  d ≥ 0
  c ≤ -1
  c ≤ -1
where
 c := ↑2 ^ a
 d := ↑b
-/

as you can see, omega is for some reasone treating 2^a and b as integers and even then the counterexample still doesn't make sense to me. I've only been using lean for a month or so. So I am not sure how to trace a tactic like omega and to me it feels like omega should handle the 4th example too, unless I am missing some fact. If anyone can clear up if this is a bug or feature, will be great.

btw I am aware that this simple example can be solved by theorems in mathlib. But like I said I faced my original problem in a different place with powered terms.

[Kevin Buzzard]

I think the naive answer is "omega doesn't deal with powers" but I'm surprised it's not treating 2^a as an atom.

[Sabbir Rahman]

At first I assumed that too, but 3rd example has 2^b and that worked without issues

[Kevin Buzzard]

I would change \N to Nat and repost without any imports in #lean4 to get some expert eyes on this. As for the integer suggestion, I think this is just part of the algorithm, I wouldn't take these things too seriously. Or edit your original post to be mathlib-free and I can move the thread to that channel.

[Sabbir Rahman]

changed the code to be mathlib free, could you move it please?

also I was not aware that omega is defined in lean and not in mathlib, I keep learning new facts in lean everyday.

[Notification Bot]

This topic was moved here from #general > Omega failing due to terms with power? by Frédéric Dupuis.

[Frédéric Dupuis]

I also tried that last example with grind (an experimental tactic that should also close goals like this) and it crashed on Lean 4.19.0-rc2.