omega doesn’t know Even or Odd

Stream: metaprogramming / tactics

[Geoffrey Irving]

Currently omega doesn’t understand Even or Odd, which makes the rw in the following required:

import Mathlib

lemma not_3 (n : ℕ) (e : Even n) : n ≠ 3 := by
  rw [Nat.even_iff] at e  -- Needed, alas
  omega

Is there an alternative tactic which is “omega + extensions”, or is it reasonable to extend omega itself to translate Even and Odd?

[Kim Morrison]

We're trying to avoid accumulating ad-hoc extensions to omega. You can write a preprocessor for now. Hopefully once grind subsumes omega there will be really nice ways to do this. :-)