Commit 2020-09-10 14:56 38d1715b

View on Github →

chore(*): update to Lean 3.20.0c, account for nat.pow removal from core (#3985) Outline:

  • nat.pow has been removed from the core library. We now use the instance monoid.pow to provide has_pow ℕ ℕ.
  • To accomodate this, algebra.group_power has been split into a directory. algebra.group_power.basic contains the definitions of monoid.pow and nsmul and whatever lemmas can be stated with very few imports. It is imported in data.nat.basic. The rest of algebra.group_power has moved to algebra.group_power.lemmas.
  • The new has_pow ℕ ℕ now satisfies a different definitional equality: a^(n+1) = a * a^n (rather than a^(n+1) = a^n * a). As a temporary measure, the lemma nat.pow_succ provides the old equality but I plan to deprecate it in favor of the more general pow_succ'. The lemma nat.pow_eq_pow is gone--the two sides are now the same in all respects so it can be deleted wherever it was used.
  • The lemmas from core that mention nat.pow have been moved into data.nat.lemmas and their proofs adjusted as needed to take into account the new definition.
  • The module data.bitvec from core has moved to data.bitvec.core in mathlib. Future plans:
  • Remove nat. lemmas redundant with general group_power ones, like nat.pow_add. This will be easier after further shuffling of modules.

Estimated changes

added theorem add_nsmul
added theorem commute.pow_left
added theorem commute.pow_pow
added theorem commute.pow_pow_self
added theorem commute.pow_right
added theorem commute.pow_self
added theorem commute.self_pow
added def gpow
added def gsmul
added def monoid.pow
added def nsmul
added theorem nsmul_add_comm'
added theorem pow_add
added theorem pow_mul_comm'
added theorem pow_succ'
added theorem pow_succ
added theorem pow_two
added theorem pow_zero
added theorem semiconj_by.pow_right
added theorem succ_nsmul'
added theorem succ_nsmul
added theorem two_nsmul
added theorem zero_nsmul
deleted theorem add_nsmul
deleted theorem commute.pow_left
deleted theorem commute.pow_pow
deleted theorem commute.pow_pow_self
deleted theorem commute.pow_right
deleted theorem commute.pow_self
deleted theorem commute.self_pow
deleted def gpow
deleted def gsmul
deleted def monoid.pow
deleted theorem nat.pow_eq_pow
deleted def nsmul
deleted theorem nsmul_add_comm'
deleted theorem pow_add
deleted theorem pow_mul_comm'
deleted theorem pow_succ'
deleted theorem pow_succ
deleted theorem pow_two
deleted theorem pow_zero
deleted theorem semiconj_by.pow_right
deleted theorem succ_nsmul'
deleted theorem succ_nsmul
deleted theorem two_nsmul
deleted theorem zero_nsmul
added def bitvec.adc
added def bitvec.add_lsb
added def bitvec.and
added def bitvec.append
added def bitvec.fill_shr
added def bitvec.not
added theorem bitvec.of_nat_succ
added def bitvec.or
added def bitvec.sbb
added def bitvec.sborrow
added def bitvec.sge
added def bitvec.sgt
added def bitvec.shl
added def bitvec.sle
added def bitvec.slt
added def bitvec.sshr
added theorem bitvec.to_nat_append
added theorem bitvec.to_nat_of_nat
added def bitvec.uborrow
added def bitvec.uge
added def bitvec.ugt
added def bitvec.ule
added def bitvec.ult
added def bitvec.ushr
added def bitvec.xor
added def bitvec
added theorem nat.mod_pow_succ
modified theorem nat.one_pow
added theorem nat.one_shiftl
added theorem nat.pos_pow_of_pos
added theorem nat.pow_one
modified theorem nat.pow_right_injective
modified theorem nat.pow_right_strict_mono
added theorem nat.pow_succ
modified theorem nat.pow_two
added theorem nat.pow_zero
added theorem nat.shiftl_eq_mul_pow
added theorem nat.shiftr_eq_div_pow
added theorem nat.zero_pow
added theorem nat.zero_shiftl
added theorem nat.zero_shiftr