omega failed in simple case

Stream: new members

[Zhang Qinchuan]

omega failed in the following examle without the rw [mul_comm]. Is this expected/ by design?

import Mathlib

example (a b c : ℕ) (ha : 1 ≤ a) (ha_sub_one : a - 1 = b * c) : c * b + 1 = a := by
  --rw [mul_comm]
  omega -- failed!

[Bjørn Kjos-Hanssen]

It doesn't seem to like "nonlinear" multiplication in general.

import Mathlib

example (b : ℕ) : b * 57 = 57 * b  := by
  omega -- works

example (b c : ℕ) : b * c = c * b  := by
  omega -- failed!

[Johan Commelin]

Yup, that's by design. Otherwise you take on yourself the burden of writing a tactic that can decide a^3 + b^3 = c^3. And such problems are pretty hard.

[Kyle Miller]

In this case, replacing the rw line with ring_nf at * works. Or you can have have := mul_comm b c to give omega an additional fact.