omega regression

Stream: lean4

[David Renshaw]

example (a b c : Nat) (h : a + b = c * 1) : a + b = c := by omega

This succeeded on lean v4.10.0, and now fails on lean v4.11.0-rc1 with the error:

omega could not prove the goal:
a possible counterexample may satisfy the constraints
  f ≥ 0
  e ≥ 0
  e - f ≤ -1
  d ≥ 0
  d - e ≤ 0
where
 d := ↑b
 e := ↑(c * 1)
 f := ↑c

[David Renshaw]

I've reported this as lean4#4916.

[Damiano Testa]

I do not know if it is the same regression, but this also fails:

example (a : Nat) : a * 1 = a := by omega

[Kim Morrison]

Sorry, this is a regression from lean#4695

[Kim Morrison]

And fixed properly, or at least better, at lean#4989. I'll roll this into v4.11.0-rc2, which is coming shortly in any case.