omega errs

Stream: lean4

[Michael Stoll]

import Mathlib

/-- error: omega could not prove the goal:
it is false -/
#guard_msgs in
example : Odd 3 := by
  omega

I guess it is OK that omega claims that it cannot prove that 3 is odd, but claiming in addition that 3 is in fact not odd goes a bit far...

[Ruben Van de Velde]

On live.lean-lang.org , with the button in your code snippet, it does work

[Kyle Miller]

I'm seeing the error on the most recent master branch of mathlib.

[Kyle Miller]

@Ruben Van de Velde When you say "it does work" do you mean that omega works, or that Michael's example really does show the error? I'm seeing the latter on live.lean-lang.org, but I interpreted you as saying the former.

[Ruben Van de Velde]

Oh no, I missed the guard messages and misinterpreted the output. Never mind me

[Kyle Miller]

@Kim Morrison The error message in Lean.Elab.Tactic.Omega.formatErrorMessage is a bit strong. It seems like "it is false" is correct for the problem that omega created from the local context, but it discarded not (Odd 3) itself, so it's presumptuous of it to say it's not possible at all. Maybe it could report what facts it ended up being able to use, and that with these facts the problem is impossible?

[Kim Morrison]

Yes, I think we could just remove it is false.

Better would be to say "could not prove the goal from the relevant hypotheses:" and then list the facts it pulled from the context. Then the user could see that it ignored Odd 3.

[Kim Morrison]

lean#4264

[Joachim Breitner]

My bad, when I changed the error message it seems I didn't think this through as much as I thought I did.

[Kim Morrison]

All good. This was just a corner case of a massive improvement over my original messages. :-)