Commit 2024-07-15 11:16 32fc2e7d

View on Github →

chore: remove bit0/bit1 and associated lemmas (#14745) This PR replaces bit0 x resp. bit1 x with:

  • 2 * x resp. 2 * x + 1 if possible, or
  • 2 • x resp. 2 • x + 1 if possible, or
  • x + x resp. x + x + 1 as fallback. The versions Num.bit0 and Num.bit1 (as well as the PosNum and ZNum versions) are left alone. All lemmas that mention bit0/bit1 have been adapted. A follow-up PR can remove these lemmas. Deletions:
  • bit0
  • bit1

Estimated changes

deleted theorem CharTwo.bit0_eq_zero
deleted theorem CharTwo.bit1_apply_eq_one
deleted theorem CharTwo.bit1_eq_one
deleted theorem bit0_eq_zero
deleted theorem bit0_ne_zero
deleted theorem zero_eq_bit0
deleted theorem zero_ne_bit0
modified theorem bit0_add
modified theorem bit0_neg
deleted theorem bit0_zero
modified theorem bit1_add'
modified theorem bit1_add
deleted theorem bit1_zero
modified theorem pow_bit0'
modified theorem pow_bit0
modified theorem pow_bit1'
modified theorem pow_bit1
modified theorem two_smul'
deleted theorem zpow_bit0_abs
deleted theorem pow_bit0_nonneg
deleted theorem pow_bit0_pos
deleted theorem pow_bit0_pos_iff
deleted theorem pow_bit1_neg_iff
deleted theorem pow_bit1_nonneg_iff
deleted theorem pow_bit1_nonpos_iff
deleted theorem pow_bit1_pos_iff
deleted theorem strictMono_pow_bit1
modified theorem bit0_mul
modified theorem bit1_mul
modified theorem mul_bit0
modified theorem mul_bit1
modified theorem Polynomial.natDegree_bit0
modified theorem Polynomial.natDegree_bit1
deleted theorem Polynomial.bit0_comp
deleted theorem Polynomial.bit1_comp
modified theorem Commute.bit0_left
modified theorem Commute.bit0_right
modified theorem Commute.bit1_left
modified theorem Commute.bit1_right
modified theorem neg_pow_bit0
modified theorem neg_pow_bit1
deleted theorem bit0_eq_two_mul
deleted theorem two_dvd_bit0
deleted theorem two_dvd_bit1
modified theorem Int.not_even_bit1
deleted theorem Nat.bit0_div_bit0
deleted theorem Nat.bit0_div_two
deleted theorem Nat.bit0_mod_bit0
deleted theorem Nat.bit1_div_bit0
deleted theorem Nat.bit1_div_two
deleted theorem Nat.bit1_mod_bit0
modified theorem Nat.not_even_bit1
deleted theorem even_bit0
deleted theorem odd_bit1
modified theorem odd_iff_exists_bit1
deleted theorem Tropical.bit0
modified theorem Complex.I_pow_bit0
modified theorem Complex.I_pow_bit1
modified theorem Matrix.vecAlt0_vecAppend
modified theorem Matrix.vecAlt1_vecAppend
deleted theorem Int.bit0_ne_bit1
deleted theorem Int.bit0_val
deleted theorem Int.bit1_ne_bit0
deleted theorem Int.bit1_ne_zero
deleted theorem Int.bit1_val
deleted theorem Int.bodd_bit0
deleted theorem Int.bodd_bit1
modified theorem Nat.bit0_bits
deleted theorem Nat.bit0_eq_bit0
modified theorem Nat.bit0_le_bit1_iff
modified theorem Nat.bit0_le_bit
modified theorem Nat.bit0_lt_bit1_iff
modified theorem Nat.bit0_mod_two
deleted theorem Nat.bit0_val
modified theorem Nat.bit1_bits
deleted theorem Nat.bit1_eq_bit1
deleted theorem Nat.bit1_eq_one
modified theorem Nat.bit1_le_bit0_iff
modified theorem Nat.bit1_lt_bit0_iff
modified theorem Nat.bit1_mod_two
deleted theorem Nat.bit1_val
modified def Nat.bit
modified theorem Nat.bit_le_bit1
modified theorem Nat.bit_lt_bit0
deleted theorem Nat.bodd_bit0
deleted theorem Nat.bodd_bit1
modified theorem Nat.div2_bit0
modified theorem Nat.div2_bit1
deleted theorem Nat.one_eq_bit1
modified theorem Nat.pos_of_bit0_pos
modified theorem Nat.bit_false
modified theorem Nat.bit_true
deleted theorem Nat.cast_bit0
deleted theorem Nat.cast_bit1
deleted theorem Nat.fib_bit0
deleted theorem Nat.fib_bit0_succ
deleted theorem Nat.fib_bit1
deleted theorem Nat.fib_bit1_succ
modified theorem Nat.size_bit0
modified theorem Nat.size_bit1
modified theorem Num.bit0_of_bit0
modified theorem Num.bit1_of_bit1
modified theorem Num.bit_to_nat
modified theorem Num.castNum_shiftRight
modified theorem Num.cast_bit0
modified theorem Num.cast_bit1
modified theorem PosNum.bit0_of_bit0
modified theorem PosNum.bit1_of_bit1
modified theorem PosNum.bit_to_nat
modified theorem PosNum.cast_bit0
modified theorem PosNum.cast_bit1
modified theorem PosNum.divMod_to_nat_aux
modified theorem ZNum.bit0_of_bit0
modified theorem ZNum.bit1_of_bit1
modified theorem ZNum.cast_bit0
modified theorem ZNum.cast_bit1
modified theorem ZNum.cast_bitm1
deleted def bit0
deleted def bit1