bit0/bit1 and mod

Stream: Is there code for X?

[Michael Stoll]

It seems that the following are not in mathlib.

lemma nat.bit0_mod_bit0 (m n : nat) : (bit0 m) % (bit0 n) = bit0 (m % n) := ...
lemma nat.bit1_mod_bit0 (m n : nat) : (bit1 m) % (bit0 n) = bit1 (m % n) := ...

Their counterparts docs#nat.bit0_div_bit0 and docs#nat.bit1_div_bit0 do exist, however.

These lemmas are useful, e.g., for proving things like (bit1 (bit0 (bit1 n))) % 8 = 5 for n : nat.
Are there objections to adding them to mathlib?

[Michael Stoll]

My proof for the second one looks a bit longer than necessary:

import data.nat.parity
namespace nat
variables {n m : ℕ}

@[simp] lemma bit1_mod_bit0 : bit1 n % bit0 m = bit1 (n % m) :=
begin
  have h₁ := congr_arg bit1 (nat.div_add_mod n m),
  -- `∀ m n : ℕ, bit0 m * n = bit0 (m * n)` seems to be missing...
  rw [bit1_add, bit0_eq_two_mul, ← mul_assoc, ← bit0_eq_two_mul] at h₁,
  have h₂ := nat.div_add_mod (bit1 n) (bit0 m),
  rw [bit1_div_bit0] at h₂,
  exact add_left_cancel (h₂.trans h₁.symm),
end

Suggestions for improvements are welcome!

[Michael Stoll]

This is #16396.
I have tagged the lemmas @[simp], since docs#nat.bit0_div_bit0 and docs#nat.bit1_div_bit0 are, but this may be debatable.

[Mauricio Collares]

#16396 would have been a great #16384

[Eric Rodriguez]

#16384 was sniped by the bot lmfao

[Yaël Dillies]

I would write them the other way around, so that it reads as a distributivity law.

[Michael Stoll]

The advantage of this direction is that it is compatible with docs#nat.bit0_mod_two / docs#nat.bit1_mod_two.

[Michael Stoll]

One could also argue that the rhs is simpler, since it contains one fewer function application...

[Michael Stoll]

Plus, docs#nat.bit0_div_bit0 and docs#nat.bit1_div_bit0 have the corresponding direction.