Mod 2 alternating truth value

Stream: maths

[Mark Andrew Gerads]

I need this lemma, and do not know how to prove it. I wrote an induction lemma about hyperoperators that depends on this lemma.

lemma mod_two_alternates (k : ℕ) : (k.succ % 2 = 0) = ¬(k % 2 = 0):=

[Mark Andrew Gerads]

I don't know how to deal with mods. My best try is this:

lemma mod_two_alternates (k : ℕ) : (k.succ % 2 = 0) = ¬(k % 2 = 0):=
begin
  rw eq_iff_iff,
  split,
  intros h0,
  sorry,
  intros h1,
  sorry,
end

[Patrick Johnson]

import data.nat.parity

example {k : ℕ} : (k.succ % 2 = 0) = ¬(k % 2 = 0) :=
by simp_rw [←nat.even_iff, nat.even_add_one]

[Mark Andrew Gerads]

Because you helped, I added you as an author here: https://github.com/leanprover-community/mathlib/pull/18116

[Eric Rodriguez]

Usually these types of lemmas are written using iff, instead of equality - why do you need the equality?

[Eric Wieser]

Note that in the end the answer was to use even and docs#nat.even_add_one directly

[Mark Andrew Gerads]

Eric Rodriguez said:

Usually these types of lemmas are written using iff, instead of equality - why do you need the equality?

I needed it for a lemma hyperoperation_ge_four_zero in https://github.com/leanprover-community/mathlib/pull/18116/files .
The lemma has been rewritten, like @Eric Wieser mentioned.

[Eric Wieser]

That answers "why do I need a result with (k.succ % 2 = 0) on the LHS and ¬(k % 2 = 0) on the right", but it doesn't answer the question "why does it need = in the middle instead of iff"

[Eric Wieser]

The answer to that second question is "it doesn't", and I think that's Eric's point

[Mark Andrew Gerads]

Ah. I have it that way because I was using simp_rw to rewrite it in an ite, and was not aware of the method of rewriting when it is in iff form, but knew it would rewrite as an equality.

[Eric Wieser]

simp, simp_rw, and rw, among most other tactics, do not care about the difference