alternatives to tactic.omega

Stream: maths

[Jakub Kądziołka]

I have the following goal, which is easily solved by omega:

example (n k : ℕ) (h1 : n ≤ k + 2) (h2 : n ≠ k + 2) (h3 : n ≠ k + 1) : n ≤ k := by omega

However, as the CI has made me aware, this tactic is being phased out (btw, where can I read more about the rationale for this?). What is the best way of proving this goal without omega?

[Bhavik Mehta]

You can use docs#lt_of_le_of_ne and docs#nat.lt_add_one_iff

[Yaël Dillies]

Actually, there's better

[Yaël Dillies]

The hands on approach is to do cases on h1

[Yaël Dillies]

The higher powered approach is to use docs#succ_order.le_succ_iff_lt_or_eq (yes, it's misnamed). Unfortunately, we don't seem to have the specialization to ℕ but you can use docs#nat.lt_succ_iff followed by docs#nat.lt_succ_iff_lt_or_eq

[Scott Morrison]

The rationale for phasing out omega is that is was written by someone who has not subsequently contributed, and the existing code base for omega is considered unmaintainable. (We would love to have a replacement, but it should be written for Lean4, not Lean3, so the problem wouldn't go away immediately in any case.)

[Chris B]

Jakub Kądziołka said:

where can I read more about the rationale for this?

Users figured out that omega was producing very large proofs which were ~30-100 times the size of other large declarations. For whatever revision of mathlib I was using to run the numbers pre-ban, the raw proof term for the largest item using omega took ~7.5 seconds to check, while average for other large declarations was ~120 milliseconds.

There's some background and stats in this thread:
https://leanprover.zulipchat.com/#narrow/stream/236449-Program-verification/topic/Arena.20allocation.20for.20ITPs/near/206635753

[Chris B]

You can see the dovetail into Scott's point at the end of the thread.

[Chris B]

Fwiw Coq is apparently ditching omega altogether : https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Multiplication.20on.20int.20is.20well-defined/near/202302824