Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-16 08:33 5fd4afc4

View on Github →

refactor(tactic/norm_cast): simplified attributes and numeral support (#2407) This is @pnmadelaine's work, I'm just updating it to work with current mathlib. New and improved version of norm_cast as described in the paper "normalizing casts and coercions": https://arxiv.org/abs/2001.10594 The main new user-facing feature are the simplified attributes. There is now only the @[norm_cast] attribute which subsumes the previous norm_cast, elim_cast, squash_cast, and move_cast attributes. There is a new set_option trace.norm_cast true option to enable debugging output.

Estimated changes

modified theorem nat.cast_eq_zero
modified theorem nat.cast_inj
modified theorem nat.cast_ne_zero
modified theorem rat.cast_fpow
modified theorem int.cast_pow
modified theorem int.coe_nat_pow
modified theorem nat.cast_pow
modified theorem submodule.coe_add
modified theorem submodule.coe_mk
modified theorem submodule.coe_neg
modified theorem submodule.coe_smul
modified theorem submodule.coe_sub
modified theorem submodule.coe_zero
added theorem coe_add_monoid_hom'
modified theorem coe_add_monoid_hom
added theorem coe_monoid_hom'
modified theorem coe_monoid_hom
modified theorem nnreal.coe_rpow
modified theorem convex_cone.mem_coe
modified theorem int.norm_cast_rat
modified theorem int.norm_cast_real
modified theorem rat.norm_cast_real
modified theorem complex.abs_cast_nat
modified theorem complex.int_cast_im
modified theorem complex.int_cast_re
modified theorem complex.nat_cast_im
modified theorem complex.nat_cast_re
modified theorem complex.of_real_add
modified theorem complex.of_real_bit0
modified theorem complex.of_real_bit1
modified theorem complex.of_real_div
modified theorem complex.of_real_fpow
modified theorem complex.of_real_im
modified theorem complex.of_real_inj
modified theorem complex.of_real_int_cast
modified theorem complex.of_real_inv
modified theorem complex.of_real_mul
modified theorem complex.of_real_nat_cast
modified theorem complex.of_real_neg
modified theorem complex.of_real_one
modified theorem complex.of_real_pow
modified theorem complex.of_real_rat_cast
modified theorem complex.of_real_re
modified theorem complex.of_real_sub
modified theorem complex.of_real_zero
modified theorem complex.rat_cast_im
modified theorem complex.rat_cast_re
modified theorem ring_equiv.coe_add_equiv
modified theorem ring_equiv.coe_mul_equiv
modified theorem fin.coe_last
modified theorem fin.coe_mk
modified theorem finset.coe_nonempty
modified theorem finset.piecewise_coe
modified theorem int.bodd_coe
modified theorem int.cast_abs
modified theorem int.cast_add
modified theorem int.cast_bit0
modified theorem int.cast_bit1
modified theorem int.cast_coe_nat
modified theorem int.cast_id
modified theorem int.cast_inj
modified theorem int.cast_le
modified theorem int.cast_lt
modified theorem int.cast_max
modified theorem int.cast_min
modified theorem int.cast_mul
modified theorem int.cast_neg
modified theorem int.cast_neg_of_nat
modified theorem int.cast_neg_succ_of_nat
modified theorem int.cast_one
modified theorem int.cast_sub
modified theorem int.cast_sub_nat_nat
modified theorem int.cast_zero
modified theorem int.coe_nat_abs
modified theorem int.coe_nat_bit0
modified theorem int.coe_nat_bit1
modified theorem int.coe_nat_div
modified theorem int.coe_nat_dvd
modified theorem int.coe_nat_inj'
modified theorem int.coe_nat_le
modified theorem int.coe_nat_lt
modified theorem nat.abs_cast
modified theorem nat.cast_add
modified theorem nat.cast_bit0
modified theorem nat.cast_bit1
modified theorem nat.cast_id
modified theorem nat.cast_ite
modified theorem nat.cast_le
modified theorem nat.cast_lt
modified theorem nat.cast_max
modified theorem nat.cast_min
modified theorem nat.cast_mul
modified theorem nat.cast_one
modified theorem nat.cast_pred
modified theorem nat.cast_sub
modified theorem nat.cast_succ
modified theorem nat.cast_zero
modified theorem enat.coe_add
modified theorem enat.coe_get
modified theorem enat.coe_le_coe
modified theorem enat.coe_lt_coe
modified theorem enat.coe_one
modified theorem enat.coe_zero
modified theorem enat.get_coe
deleted def int.of_snum
deleted def nzsnum.bit0
deleted def nzsnum.bit1
deleted def nzsnum.drec'
deleted def nzsnum.head
deleted def nzsnum.not
deleted def nzsnum.sign
deleted def nzsnum.tail
deleted inductive nzsnum
deleted def snum.bit0
deleted def snum.bit1
deleted def snum.bit
deleted theorem snum.bit_one
deleted theorem snum.bit_zero
deleted def snum.bits
deleted def snum.cadd
deleted def snum.czadd
deleted def snum.drec'
deleted def snum.head
deleted def snum.not
deleted def snum.pred
deleted def snum.rec'
deleted def snum.sign
deleted def snum.succ
deleted def snum.tail
deleted def snum.test_bit
deleted inductive snum
added def nzsnum.bit0
added def nzsnum.bit1
added def nzsnum.drec'
added def nzsnum.head
added def nzsnum.not
added def nzsnum.sign
added def nzsnum.tail
added inductive nzsnum
added def snum.bit0
added def snum.bit1
added def snum.bit
added theorem snum.bit_one
added theorem snum.bit_zero
added def snum.bits
added def snum.cadd
added def snum.czadd
added def snum.drec'
added def snum.head
added def snum.not
added def snum.pred
added def snum.rec'
added def snum.sign
added def snum.succ
added def snum.tail
added def snum.test_bit
added inductive snum
added def int.of_snum
modified theorem num.add_of_nat
modified theorem num.cast_add
modified theorem num.cast_bit0
modified theorem num.cast_bit1
modified theorem num.cast_mul
modified theorem num.cast_one
modified theorem num.cast_to_int
modified theorem num.cast_to_nat
modified theorem num.cast_to_znum
modified theorem num.cast_zero
modified theorem num.div_to_nat
modified theorem num.land_to_nat
modified theorem num.ldiff_to_nat
modified theorem num.lor_to_nat
modified theorem num.lxor_to_nat
modified theorem num.mod_to_nat
modified theorem num.of_nat_inj
modified theorem num.of_to_nat
modified theorem num.shiftl_to_nat
modified theorem num.shiftr_to_nat
modified theorem num.sub_to_nat
modified theorem num.to_nat_inj
modified theorem num.to_nat_to_int
modified theorem pos_num.cast_bit0
modified theorem pos_num.cast_bit1
modified theorem pos_num.cast_one
modified theorem pos_num.cast_to_int
modified theorem pos_num.cast_to_nat
modified theorem pos_num.to_nat_inj
modified theorem pos_num.to_nat_to_int
modified theorem znum.cast_add
modified theorem znum.cast_bit0
modified theorem znum.cast_bit1
modified theorem znum.cast_one
modified theorem znum.cast_to_int
modified theorem znum.cast_zero
modified theorem znum.cast_zneg
modified theorem znum.div_to_int
modified theorem znum.dvd_to_int
modified theorem znum.mod_to_int
modified theorem znum.mul_to_int
modified theorem znum.neg_of_int
modified theorem znum.of_int_cast
modified theorem znum.of_nat_cast
modified theorem znum.of_to_int
modified theorem padic_int.cast_pow
modified theorem padic_int.coe_add
modified theorem padic_int.coe_coe
modified theorem padic_int.coe_mul
modified theorem padic_int.coe_neg
modified theorem padic_int.coe_one
modified theorem padic_int.coe_sub
modified theorem padic_int.coe_zero
modified theorem padic.coe_add
modified theorem padic.coe_div
modified theorem padic.coe_inj
modified theorem padic.coe_mul
modified theorem padic.coe_neg
modified theorem padic.coe_one
modified theorem padic.coe_sub
modified theorem padic.coe_zero
modified theorem rat.coe_int_denom
modified theorem rat.coe_int_num
modified theorem rat.coe_nat_denom
modified theorem rat.coe_nat_num
modified theorem rat.cast_abs
modified theorem rat.cast_add
modified theorem rat.cast_add_of_ne_zero
modified theorem rat.cast_bit0
modified theorem rat.cast_bit1
modified theorem rat.cast_coe_int
modified theorem rat.cast_coe_nat
modified theorem rat.cast_div
modified theorem rat.cast_div_of_ne_zero
modified theorem rat.cast_id
modified theorem rat.cast_inj
modified theorem rat.cast_inv
modified theorem rat.cast_inv_of_ne_zero
modified theorem rat.cast_le
modified theorem rat.cast_lt
modified theorem rat.cast_max
modified theorem rat.cast_min
modified theorem rat.cast_mk
modified theorem rat.cast_mk_of_ne_zero
modified theorem rat.cast_mul
modified theorem rat.cast_mul_of_ne_zero
modified theorem rat.cast_neg
modified theorem rat.cast_nonneg
modified theorem rat.cast_one
modified theorem rat.cast_pow
modified theorem rat.cast_sub
modified theorem rat.cast_sub_of_ne_zero
modified theorem rat.cast_zero
modified theorem ennreal.coe_add
modified theorem ennreal.coe_bit0
modified theorem ennreal.coe_bit1
modified theorem ennreal.coe_div
modified theorem ennreal.coe_eq_coe
modified theorem ennreal.coe_eq_one
modified theorem ennreal.coe_eq_zero
modified theorem ennreal.coe_finset_prod
modified theorem ennreal.coe_finset_sum
modified theorem ennreal.coe_inv
modified theorem ennreal.coe_inv_two
modified theorem ennreal.coe_le_coe
modified theorem ennreal.coe_le_one_iff
modified theorem ennreal.coe_lt_coe
modified theorem ennreal.coe_lt_one_iff
modified theorem ennreal.coe_max
modified theorem ennreal.coe_min
modified theorem ennreal.coe_mul
modified theorem ennreal.coe_nat
modified theorem ennreal.coe_nat_le_coe_nat
modified theorem ennreal.coe_nat_lt_coe_nat
modified theorem ennreal.coe_nonneg
modified theorem ennreal.coe_one
modified theorem ennreal.coe_pos
modified theorem ennreal.coe_pow
modified theorem ennreal.coe_sub
modified theorem ennreal.coe_zero
modified theorem ennreal.one_eq_coe
modified theorem ennreal.one_le_coe_iff
modified theorem ennreal.one_lt_coe_iff
modified theorem ennreal.to_nnreal_coe
modified theorem ennreal.zero_eq_coe
modified theorem nnreal.coe_list_prod
modified theorem nnreal.coe_list_sum
modified theorem nnreal.coe_max
modified theorem nnreal.coe_min
modified theorem nnreal.coe_multiset_prod
modified theorem nnreal.coe_multiset_sum
modified theorem nnreal.coe_ne_zero
modified theorem nnreal.coe_pow
modified theorem nnreal.coe_prod
modified theorem nnreal.coe_sum
modified theorem nnreal.smul_coe
modified theorem linear_equiv.coe_prod
modified theorem measure_theory.l1.coe_add
modified theorem measure_theory.l1.coe_neg
modified theorem measure_theory.l1.coe_smul
modified theorem measure_theory.l1.coe_sub
modified theorem measure_theory.l1.coe_zero
modified theorem mv_polynomial.coe_C
modified theorem mv_polynomial.coe_X
modified theorem mv_polynomial.coe_add
modified theorem mv_polynomial.coe_monomial
modified theorem mv_polynomial.coe_mul
modified theorem mv_polynomial.coe_one
modified theorem mv_polynomial.coe_zero
modified theorem mv_polynomial.coeff_coe
modified theorem polynomial.coe_C
modified theorem polynomial.coe_X
modified theorem polynomial.coe_add
modified theorem polynomial.coe_monomial
modified theorem polynomial.coe_mul
modified theorem polynomial.coe_one
modified theorem polynomial.coe_zero
modified theorem polynomial.coeff_coe
modified theorem cardinal.nat_cast_inj
modified theorem cardinal.nat_cast_le
modified theorem cardinal.nat_cast_lt
modified theorem cardinal.nat_cast_pow
modified theorem cardinal.nat_succ
deleted theorem ge_from_le
deleted theorem gt_from_lt
modified theorem ite_cast
deleted theorem ne_from_not_eq
added inductive norm_cast.label
modified theorem ennreal.tendsto_coe
modified theorem nnreal.coe_tsum
modified theorem nnreal.has_sum_coe
modified theorem nnreal.summable_coe
modified theorem int.dist_cast_rat
modified theorem int.dist_cast_real
modified theorem rat.dist_cast
added theorem hidden.coe_inj
added theorem hidden.coe_one
added theorem hidden.mul_coe
added def hidden.with_zero
added theorem coe_bit0
added theorem coe_bit1
added theorem coe_f1
added def f1
added def f2
added structure hom
added theorem hom_plus.coe_fn
added structure hom_plus