Zulip Chat Archive

Stream: Is there code for X?

Topic: bit mod two


view this post on Zulip Johan Commelin (Oct 01 2020 at 07:57):

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

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 08:09):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 08:27):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 08:29):

Shall I PR these to nat.basic?

view this post on Zulip Gabriel Ebner (Oct 01 2020 at 08:30):

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

view this post on Zulip Johan Commelin (Oct 01 2020 at 08:35):

#4343


Last updated: May 17 2021 at 15:13 UTC