Zero Not Odd

Stream: Is there code for X?

[Sophia C]

Is there a library lemma somewhere that proves 0 is not odd? It feels weird to have to write my own proposition for this, especially when it's so simple to do this:

theorem zero_not_odd {x : ℕ} (hx : Odd x) : x ≠ 0 := by
  by_contra
  rcases hx with ⟨y, hy⟩
  linarith

The main issue I'm running into is that I don't know if there's a good search tool that would let me find the names of lemmas like this?

[Mario Carneiro]

you can prove simple propositions like that by decide:

theorem zero_not_odd : ¬Odd 0 := by decide

[Sophia C]

How does that work? decide seems like magic.

[Yakov Pechersky]

docs#Nat.instDecidablePredOdd. A DecidablePred instance means that for a predicate P : Nat -> Prop, if you're given a statement of P n, there is an algorithm to determine whether P n is true or false.

[Yakov Pechersky]

In this case, that algorithm says "well, Odd means the same as determining that n % 2 = 1. And we have a decidable algorithm of determining that two Nats are the same. So we can rely on that algorithm." And then it takes your 0, plugs it into 0 % 2 = 1 which reduces to 0 = 1 which is false (because of how Nats are constructed), so the negation of it is true. BTW, through docs#Not.decidable.

[Ruben Van de Velde]

I wonder in what generality it's true - at least for Nat and Int; clearly not for ZMod n (n odd)

[Damiano Testa]

I seem to remember that it is false exactly when 2 is invertible and 1 has an opposite.

[Kevin Buzzard]

Opposite := additive inverse :-)