Commit 2023-10-18 16:31 813c10ab

View on Github →

chore: remove Nat.bitwise' (#7451) 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.

Estimated changes

Modified Mathlib/Data/Bool/Basic.lean

added theorem Bool.bne_eq_xor

Modified Mathlib/Data/Int/Bitwise.lean

modified theorem Int.bitwise_diff

modified theorem Int.bitwise_xor

modified theorem Int.bodd_add

modified theorem Int.bodd_subNatNat

modified theorem Int.ldiff_bit

modified theorem Int.lxor_bit

modified theorem Int.testBit_ldiff

modified theorem Int.testBit_lxor

Modified Mathlib/Data/Nat/Bitwise.lean

added theorem Nat.binaryRec_of_ne_zero

added theorem Nat.bit_mod_two

added theorem Nat.bit_mod_two_eq_one_iff

added theorem Nat.bit_mod_two_eq_zero_iff

added theorem Nat.bit_ne_zero_iff

deleted theorem Nat.bitwise'_bit'

deleted theorem Nat.bitwise'_comm

deleted theorem Nat.bitwise'_eq_bitwise

deleted theorem Nat.bitwise'_of_ne_zero

deleted theorem Nat.bitwise'_swap

deleted theorem Nat.bitwise'_zero_right

added theorem Nat.bitwise_bit'

added theorem Nat.bitwise_comm

added theorem Nat.bitwise_eq_binaryRec

added theorem Nat.bitwise_swap

deleted theorem Nat.land'_assoc

deleted theorem Nat.land'_comm

deleted theorem Nat.land'_eq_land

deleted theorem Nat.land'_zero

added theorem Nat.land_assoc

added theorem Nat.land_comm

added theorem Nat.land_zero

added theorem Nat.ldiff_bit

deleted theorem Nat.lor'_assoc

deleted theorem Nat.lor'_comm

deleted theorem Nat.lor'_eq_lor

deleted theorem Nat.lor'_zero

added theorem Nat.lor_assoc

added theorem Nat.lor_comm

added theorem Nat.lor_zero

deleted theorem Nat.lt_lxor'_cases

added theorem Nat.lt_xor_cases

deleted theorem Nat.lxor'_assoc

deleted theorem Nat.lxor'_cancel_left

deleted theorem Nat.lxor'_comm

deleted theorem Nat.lxor'_eq_zero

deleted theorem Nat.lxor'_left_inj

deleted theorem Nat.lxor'_left_injective

deleted theorem Nat.lxor'_ne_zero

deleted theorem Nat.lxor'_right_inj

deleted theorem Nat.lxor'_right_injective

deleted theorem Nat.lxor'_self

deleted theorem Nat.lxor'_trichotomy

deleted theorem Nat.lxor'_zero

deleted theorem Nat.lxor_bit

modified theorem Nat.lxor_cancel_right

added theorem Nat.testBit_bitwise

added theorem Nat.testBit_land

added theorem Nat.testBit_ldiff

added theorem Nat.testBit_lor

added theorem Nat.testBit_xor

deleted theorem Nat.xor'_eq_xor

added theorem Nat.xor_assoc

added theorem Nat.xor_bit

added theorem Nat.xor_cancel_left

added theorem Nat.xor_comm

added theorem Nat.xor_eq_zero

added theorem Nat.xor_left_inj

added theorem Nat.xor_left_injective

added theorem Nat.xor_ne_zero

added theorem Nat.xor_right_inj

added theorem Nat.xor_right_injective

added theorem Nat.xor_self

added theorem Nat.xor_trichotomy

added theorem Nat.xor_zero

deleted theorem Nat.zero_land'

added theorem Nat.zero_land

deleted theorem Nat.zero_lor'

added theorem Nat.zero_lor

deleted theorem Nat.zero_lxor'

added theorem Nat.zero_xor

Modified Mathlib/Data/Num/Lemmas.lean

deleted theorem Num.bitwise'_to_nat

added theorem Num.bitwise_to_nat

deleted theorem Num.land'_to_nat

added theorem Num.land_to_nat

deleted theorem Num.ldiff'_to_nat

added theorem Num.ldiff_to_nat

deleted theorem Num.lor'_to_nat

added theorem Num.lor_to_nat

deleted theorem Num.lxor'_to_nat

added theorem Num.lxor_to_nat

Modified Mathlib/Init/Data/Int/Bitwise.lean

deleted def Int.ldiff'

added def Int.ldiff

deleted def Int.lxor'

added def Int.xor

Modified Mathlib/Init/Data/Nat/Bitwise.lean

deleted def Nat.bitwise'

deleted theorem Nat.bitwise'_bit

deleted theorem Nat.bitwise'_bit_aux

deleted theorem Nat.bitwise'_zero

deleted theorem Nat.bitwise'_zero_left

deleted def Nat.land'

deleted theorem Nat.land'_bit

deleted def Nat.ldiff'

deleted theorem Nat.ldiff'_bit

added def Nat.ldiff

deleted def Nat.lor'

deleted theorem Nat.lor'_bit

deleted def Nat.lxor'

deleted theorem Nat.lxor'_bit

deleted theorem Nat.testBit_bitwise'

deleted theorem Nat.testBit_land'

deleted theorem Nat.testBit_ldiff'

deleted theorem Nat.testBit_lor'

deleted theorem Nat.testBit_lxor'

Modified Mathlib/SetTheory/Game/Nim.lean

modified theorem SetTheory.PGame.nim_add_nim_equiv