Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-14 12:43 22790e06

View on Github →

feat(tactic): new tactics to normalize casts inside expressions (#988)

  • new tactics for normalizing casts
  • update using the norm_cast tactics
  • minor proof update
  • minor changes
  • moved a norm_cast lemma
  • minor changes
  • fix(doc/tactics): make headers uniform
  • nicer proof using discharger
  • fixed numerals handling by adding simp_cast lemmas
  • add documentation
  • fixed unnecessary normalizations in assumption_mod_cast
  • minor proof update
  • minor coding style update
  • documentation update
  • rename flip_equation to expr.flip_eq
  • update proofs to remove boiler plate code about casts
  • revert to old proof
  • fixed imports and moved attributes
  • add test file
  • new attribute system
  • the attribute norm_cast is split into norm_cast and norm_cast_rev
  • update of the equation flipping mechanism
  • update of the numerals handling
  • syntax fix
  • change attributes names
  • test update
  • small update
  • add elim_cast attribute
  • add examples for attributes
  • new examples

Estimated changes

modified theorem nat.cast_inj
modified theorem int.cast_pow
modified theorem int.coe_nat_pow
modified theorem nat.cast_pow
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 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
added theorem int.coe_nat_bit0
added 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_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 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
added theorem padic.coe_add
added theorem padic.coe_div
added theorem padic.coe_inj
added theorem padic.coe_mul
added theorem padic.coe_neg
added theorem padic.coe_one
added theorem padic.coe_sub
added theorem padic.coe_zero
modified theorem padic_norm_e.eq_padic_norm
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_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 rat.coe_int_denom
modified theorem rat.coe_int_num
modified theorem rat.coe_nat_denom
modified theorem rat.coe_nat_num
added theorem nat.find_le
added theorem ge_from_le
added theorem gt_from_lt
added theorem ite_cast
added theorem ne_from_not_eq