Zero is not odd

Stream: Is there code for X?

[Eric Wieser]

Surely this should be handled by a single tactic?

import Mathlib

example (h : Odd 0) : False := by
   sorry

[Yaël Dillies]

I've tried quite hard to get it to a single tactic a few weeks ago and I didn't manage

[Andrew Yang]

example (h : Odd 0) : False := by
rcases h with ⟨_, ⟨⟩⟩

Does this count?

[Eric Wieser]

I think simp at h used to work in 4.10.0

[Damiano Testa]

Does simp_all [Odd] count? Also simp [Odd] at h seems enough.

[Heather Macbeth]

If you reorganize,

example : Odd 0 → False := by decide

[Heather Macbeth]

In Lean 3 the decide equivalent, dec_trivial, had a variant dec_trivial! which ran "revert" first -- that would do it here!

[Moritz Firsching]

tauto works

[Moritz Firsching]

Maybe having ¬ Odd 0 as a theorem wouldn't be so bad. At least there is one occurrence where it is used

[Mario Carneiro]

are you saying that it's not already a theorem?

[Mario Carneiro]

obviously it should exist, I thought the question was about finding a proof of it automatically

[Bhavik Mehta]

I'd be very surprised if simp [parity_simps] at h can't do this

[Moritz Firsching]

ok, I didn't find it, grepping Odd 0 (and Even 0 for that matter) does not give the desired results

[Zhang Qinchuan]

I have similiar problem that contradiction tactic didn't recognize Odd n and Even n is contradictory.

import Mathlib

example (n : ℕ) (hodd : Odd n) (heven : Even n) : False := by
  -- ↓ failed before rewrite
  -- contradiction

  rw [← Nat.not_odd_iff_even] at heven

  -- ↓ success after rewrite
  contradiction

[Ruben Van de Velde]

I think that counts as "works as intended". contradiction should not (cannot) find any possible contradiction, only the ones that are pure logic

[Moritz Firsching]

I looked a bit and we have :

• docs#Int.not_even_one
• docs#Nat.not_even_one
• even_zero: docs#even_zero
• odd_one: docs#odd_one
  So the thing missing is not_odd_zero and I think the right generality is probably to add it for Int and Nat, since it is of course not true for Ring:

example : Odd (0 : ZMod 3) := ⟨1, rfl⟩
example : Even (1 : ZMod 3) := ⟨2, rfl⟩

mathlib#17419 adds these