Connecting `Nat.bodd` and `Odd`

Stream: mathlib4

[Johannes Tantow]

Hi,
I think it would be beneficial to have two lemmas that connect Nat.bodd and Odd/Even.
One of them I already have below:

import Mathlib.Algebra.Ring.Parity
import Mathlib.Data.Nat.Bits

theorem bodd_eq_true_iff_odd (n: ℕ): n.bodd = true ↔ Odd n := by
  induction n with
  | zero => simp
  | succ m ih =>
    simp [Nat.odd_add_one]
    constructor
    · intro h
      by_contra p
      simp [← ih, h] at p
    · intro h
      by_contra p
      simp [ih, ← Nat.not_even_iff_odd] at p
      contradiction

The other lemma would combine this with Even in the false case.

---

Why would that be useful? I wanted to formally prove the correctness of the multiplication algorithm below:

def f (x: ℕ)(y: ℕ): ℕ :=
  if y = 0
  then 0
  else
    let z:= f x (y/2)
    if y % 2 = 0
    then 2*z
    else 2*z + x
termination_by y
decreasing_by
  rename_i h
  exact Nat.bitwise_rec_lemma h

Nat.bodd was needed as I wanted to use the Nat.div2_succ lemma and I used Nat.odd_iff to rewrite the modulo. I used the lemma above to combine it .

---

If I am not overlooking something, I would like to have write access to add this to mathlib. If there are further useful lemmas connected to this, I am also open to add them to it. If that would be the case, which file would be more appropriate of the two I currently import?

Or is there another different way to do this?

[Daniel Weber]

This can be proven using docs#Nat.bodd_eq_one_and_ne_zero

import Mathlib.Algebra.Ring.Parity
import Mathlib.Data.Nat.Bits

theorem bodd_eq_true_iff_odd (n: ℕ): n.bodd = true ↔ Odd n := by
  simp [Nat.bodd_eq_one_and_ne_zero, Nat.odd_iff]

theorem bodd_eq_false_iff_even (n: ℕ): n.bodd = false ↔ Even n := by
  simp [Nat.bodd_eq_one_and_ne_zero, Nat.even_iff]

[Johannes Tantow]

Okay, that is simpler. Is it still useful to have it directly?

[Ruben Van de Velde]

I guess mathlib doesn't really use Nat.bodd, but it seems fine to add

[Kim Morrison]

How is Nat.bodd being used? Could we remove it instead?

[Eric Wieser]

#13649 might be relevant here

[Kim Morrison]

I left a comment on #19666, which #13649 is waiting on.

[Kim Morrison]

But redefining bodd doesn't seem relevant to whether we want/need it in the first place. :-)

[Johannes Tantow]

Kim Morrison schrieb:

How is Nat.bodd being used? Could we remove it instead?

I required it to use docs#Nat.div2_succ . It would also be fine and simpler for me, if the lemma does directly use mod2. I guess that replacement would always be possible, but perhaps this implementation of testing for oddness is faster.

[Johan Commelin]

If the goal is to verify the multiplication algorithm, then I think it would be nice to do this in an arbitrary base, using docs#Nat.digits

[Johannes Tantow]

In principle yes, but adding this algorithm, which is essentially peasant multiplication, to mathlib wasn't my intent. It was an exercise in a course I teach the exercise sessions and one of my students was interested how we would be able to formalize the proof. One could also try to do it with digits, but this gets probably more complicated While doing the formal proof I noticed that such a lemma as on top might be helpful

[Johan Commelin]

Aha, understood