[Merged by Bors] - chore: remove Nat.bitwise'

[alexkeizer]

Building upon the proof that Nat.bitwise and Nat.bitwise' are equal (from #7410), this PR completely removes bitwise' and changes all uses to bitwise instead.

In particular, land'/lor'/lxor' are replaced with the bitwise-based equivalent operations in core, which have overriden optimized implementations in the compiler.

---

• depends on: [Merged by Bors] - feat: prove equality of Nat.bitwise and Nat.bitwise' #7410

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: prove equality of Nat.bitwise and Nat.bitwise' #7410
  By Dependent Issues (🤖). Happy coding!

[eric-wieser]

Checking for removed aligns:

git diff $(git merge-base origin/master HEAD) | grep -e '[+-]#align' | sort -k1 | sort -s -k2,2

gives

+#align int.ldiff Int.ldiff
-#align int.ldiff Int.ldiff'
+#align int.lxor Int.xor
-#align int.lxor Int.lxor'
+#align nat.bitwise Nat.bitwise
-#align nat.bitwise Nat.bitwise'
+#align nat.bitwise_bit Nat.bitwise_bit
-#align nat.bitwise_bit Nat.bitwise'_bit
-#align nat.bitwise_bit_aux Nat.bitwise'_bit_aux
+#align nat.bitwise_comm Nat.bitwise_comm
-#align nat.bitwise_comm Nat.bitwise'_comm
+#align nat.bitwise_swap Nat.bitwise_swap
-#align nat.bitwise_swap Nat.bitwise'_swap
+#align nat.bitwise_zero Nat.bitwise_zero
-#align nat.bitwise_zero Nat.bitwise'_zero
+#align nat.bitwise_zero_left Nat.bitwise_zero_left
-#align nat.bitwise_zero_left Nat.bitwise'_zero_left
+#align nat.bitwise_zero_right Nat.bitwise_zero_right
+#align nat.land Nat.land
-#align nat.land Nat.land'
+#align nat.land_assoc Nat.land_assoc
-#align nat.land_assoc Nat.land'_assoc
+#align nat.land_bit Nat.land_bit
-#align nat.land_bit Nat.land'_bit
+#align nat.land_comm Nat.land_comm
-#align nat.land_comm Nat.land'_comm
+#align nat.land_zero Nat.land_zero
-#align nat.land_zero Nat.land'_zero
+#align nat.ldiff Nat.ldiff
-#align nat.ldiff Nat.ldiff'
+#align nat.ldiff_bit Nat.ldiff_bit
-#align nat.ldiff_bit Nat.ldiff'_bit
+#align nat.lor Nat.lor
-#align nat.lor Nat.lor'
+#align nat.lor_assoc Nat.lor_assoc
-#align nat.lor_assoc Nat.lor'_assoc
+#align nat.lor_bit Nat.lor_bit
-#align nat.lor_bit Nat.lor'_bit
+#align nat.lor_comm Nat.lor_comm
-#align nat.lor_comm Nat.lor'_comm
+#align nat.lor_zero Nat.lor_zero
-#align nat.lor_zero Nat.lor'_zero
+#align nat.lt_lxor_cases Nat.lt_xor_cases
-#align nat.lt_lxor_cases Nat.lt_lxor'_cases
+#align nat.lxor Nat.xor
-#align nat.lxor Nat.lxor'
+#align nat.lxor_assoc Nat.xor_assoc
-#align nat.lxor_assoc Nat.lxor'_assoc
-#align nat.lxor_bit Nat.lxor'_bit
+#align nat.lxor_cancel_left Nat.xor_cancel_left
-#align nat.lxor_cancel_left Nat.lxor'_cancel_left
+#align nat.lxor_comm Nat.xor_comm
-#align nat.lxor_comm Nat.lxor'_comm
+#align nat.lxor_eq_zero Nat.xor_eq_zero
-#align nat.lxor_eq_zero Nat.lxor'_eq_zero
+#align nat.lxor_left_inj Nat.xor_left_inj
-#align nat.lxor_left_inj Nat.lxor'_left_inj
+#align nat.lxor_left_injective Nat.xor_left_injective
-#align nat.lxor_left_injective Nat.lxor'_left_injective
+#align nat.lxor_ne_zero Nat.xor_ne_zero
-#align nat.lxor_ne_zero Nat.lxor'_ne_zero
+#align nat.lxor_right_inj Nat.xor_right_inj
-#align nat.lxor_right_inj Nat.lxor'_right_inj
+#align nat.lxor_right_injective Nat.xor_right_injective
-#align nat.lxor_right_injective Nat.lxor'_right_injective
+#align nat.lxor_self Nat.xor_self
-#align nat.lxor_self Nat.lxor'_self
+#align nat.lxor_trichotomy Nat.xor_trichotomy
-#align nat.lxor_trichotomy Nat.lxor'_trichotomy
+#align nat.lxor_zero Nat.xor_zero
-#align nat.lxor_zero Nat.lxor'_zero
-#align nat.test_bit_bitwise Nat.testBit_bitwise'
+#align nat.test_bit_land Nat.testBit_land
-#align nat.test_bit_land Nat.testBit_land'
+#align nat.test_bit_ldiff Nat.testBit_ldiff
-#align nat.test_bit_ldiff Nat.testBit_ldiff'
+#align nat.test_bit_lor Nat.testBit_lor
-#align nat.test_bit_lor Nat.testBit_lor'
+#align nat.test_bit_lxor Nat.testBit_xor
-#align nat.test_bit_lxor Nat.testBit_lxor'
+#align nat.xor_bit Nat.xor_bit
+#align nat.zero_land Nat.zero_land
-#align nat.zero_land Nat.zero_land'
+#align nat.zero_lor Nat.zero_lor
-#align nat.zero_lor Nat.zero_lor'
+#align nat.zero_lxor Nat.zero_xor
-#align nat.zero_lxor Nat.zero_lxor'
+#align num.bitwise_to_nat Num.bitwise_to_nat
-#align num.bitwise_to_nat Num.bitwise'_to_nat
+#align num.land_to_nat Num.land_to_nat
-#align num.land_to_nat Num.land'_to_nat
+#align num.ldiff_to_nat Num.ldiff_to_nat
-#align num.ldiff_to_nat Num.ldiff'_to_nat
+#align num.lor_to_nat Num.lor_to_nat
-#align num.lor_to_nat Num.lor'_to_nat
+#align num.lxor_to_nat Num.xor_to_nat
-#align num.lxor_to_nat Num.lxor'_to_nat

There seems to be a few mistakes here, as they should be paired.

[eric-wieser]

@ChrisHughes24, do you want one final look?

[eric-wieser]

I replaced this proof with one using binaryRec', now that we have bitwise_bit proven first.

[ChrisHughes24]

Suggested change

	theorem bitwise_to_nat {f : Num → Num → Num} {g : Bool → Bool → Bool} (p : PosNum → PosNum → Num)
	theorem bitwise_toNat {f : Num → Num → Num} {g : Bool → Bool → Bool} (p : PosNum → PosNum → Num)

I think this is the correct name if it's about Num.toNat or something. And the name usually describes the LHS, so maybe swap the direction of the equality.

[ChrisHughes24]

Suggested change

	theorem lor_to_nat : ∀ m n : Num, ↑(m ||| n) = Nat.lor m n := by
	theorem toNat_lor : ∀ m n : Num, ↑(m ||| n) = Nat.lor m n := by

This is just correcting other people's mistakes I know, but we might as well tidy it up, here and everywhere else.

[eric-wieser]

I think we should do this in a follow-up PR, where we also fix this to

Suggested change

	theorem lor_to_nat : ∀ m n : Num, ↑(m ||| n) = Nat.lor m n := by
	theorem toNat_lor : ∀ m n : Num, ↑(m ||| n) = m ||| n := by

[ChrisHughes24]

okay. I'll let you do the merging, but I approve.

[eric-wieser]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style