Improving proofs about `Nat.xor`

Stream: new members

[tjf801]

I've proved a few basic theorems about the ^^^ operator on natural numbers, but I feel like most (if not all) of these proofs are way more clunky and verbose than they need to be. Does anyone have any advice for condensing them down or making them more readable?

@[simp] theorem Nat.zero_xor (a : Nat) : 0 ^^^ a = a := by
  simp [HXor.hXor, Xor.xor, xor, bitwise]

@[simp] theorem Nat.xor_zero (x : Nat) : a ^^^ 0 = a := by
  simp only [HXor.hXor, Xor.xor, xor]
  unfold bitwise
  simp [@eq_comm _ 0]

@[simp] theorem Nat.xor_self (a : Nat) : a ^^^ a = 0 := by
  simp [HXor.hXor, Xor.xor, xor]
  unfold bitwise
  simp
  split
  · trivial
  · simp [Nat.add_eq_zero_iff]
    exact xor_self _

theorem Nat.xor_comm (a b : Nat) : a ^^^ b = b ^^^ a := by
  simp [HXor.hXor, Xor.xor, xor]
  unfold bitwise
  simp
  split
  · split <;> simp_all
  · split
    · rfl
    · split
      · split
        · have p := Nat.xor_comm (a/2) (b/2)
          simp [HXor.hXor, Xor.xor, xor] at p
          simp [p]
        · next h not_h =>
          exact absurd h.symm not_h
      · split
        · next not_h h =>
          exact absurd h.symm not_h
        · have p := Nat.xor_comm (a/2) (b/2)
          simp [HXor.hXor, Xor.xor, xor] at p
          simp [p]

[Eric Wieser]

import Mathlib.Data.Nat.Bitwise will let you delete all of those

[tjf801]

I figured Mathlib would have something like that, but I'm trying to do it myself so I can personally get more familiar with using tactics and writing proofs, even if it is reinventing the wheel a bit if that makes any sense

[Eric Wieser]

In that case, one way to learn how to condense them down would be to read the source of src#Nat.xor_comm etc. Of course, it's possible that the proofs in mathlib could be further condensed down!

[Eric Wieser]

(Reinventing the wheel as an exercise is totally fine, but if you ask "how do I make this shorter" and don't explain that you're doing this, the best answer is "use as much as possible that already exists"!)