bit mod two

Stream: Is there code for X?

[Johan Commelin]

Do we have these? I couldn't find them, but I'm a bit surprised.

namespace nat

variables (n : ℕ)

@[simp] lemma bit0_mod_two : bit0 n % 2 = 0 :=
show (n + n) % 2 = 0, by rw [← two_mul, mul_mod, mod_self, zero_mul, zero_mod]

@[simp] lemma bit1_mod_two : bit1 n % 2 = 1 :=
by rw [bit1, add_mod, bit0_mod_two, zero_add, mod_mod, one_mod]

end nat

[Gabriel Ebner]

The closest I could find is bodd_bit:

variables (n : ℕ)

@[simp] lemma bodd_bit0 : (bit0 n).bodd = ff := nat.bodd_bit ff _
@[simp] lemma bodd_bit1 : (bit1 n).bodd = tt := nat.bodd_bit tt _
@[simp] lemma bit0_mod_two : bit0 n % 2 = 0 := by rw nat.mod_two_of_bodd; simp
@[simp] lemma bit1_mod_two : bit1 n % 2 = 1 := by rw nat.mod_two_of_bodd; simp

[Johan Commelin]

@Gabriel Ebner Thanks! You managed to prove twice as many simp-lemmas in about the same number of characters.

[Johan Commelin]

Shall I PR these to nat.basic?

[Gabriel Ebner]

Apparently bodd_bit0 is already in nat.basic. So yes, that seems like the right place.

[Johan Commelin]

#4343