Commit 2022-10-27 04:20 960dc0ee

View on Github →

feat: integer operations in norm_num (#507) Another major rewrite of norm_num, this time to support returning integers as well as nats. Rational numbers are included but stubbed for now pending the rest of the algebraic typeclasses.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GroupPower/Lemmas.lean

added theorem Int.cast_pow

added theorem pow_eq

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

modified def Int.cast

modified theorem Int.cast_negSucc

modified theorem Int.cast_ofNat

modified theorem Int.cast_one

modified theorem Int.cast_zero

Modified Mathlib/Algebra/Ring/Basic.lean

added theorem mul_sub_right_distrib

Created Mathlib/Data/Int/Basic.lean

Created Mathlib/Data/Int/Cast.lean

added theorem Int.cast_mul

Created Mathlib/Data/Int/Cast/Defs.lean

added theorem Int.cast_add

added theorem Int.cast_neg

added theorem Int.cast_sub

added theorem Int.cast_subNatNat

added theorem Nat.cast_sub

Modified Mathlib/Tactic/Convert.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

modified def Mathlib.Meta.NormNum.evalAdd

added def Mathlib.Meta.NormNum.evalIntCast

modified def Mathlib.Meta.NormNum.evalMul

modified def Mathlib.Meta.NormNum.evalNatCast

added def Mathlib.Meta.NormNum.evalNeg

modified def Mathlib.Meta.NormNum.evalOfNat

modified def Mathlib.Meta.NormNum.evalOne

modified def Mathlib.Meta.NormNum.evalPow

added def Mathlib.Meta.NormNum.evalSub

modified def Mathlib.Meta.NormNum.evalZero

deleted def Mathlib.Meta.NormNum.instSemiringNat

added theorem Mathlib.Meta.NormNum.isInt_add

added theorem Mathlib.Meta.NormNum.isInt_cast

added theorem Mathlib.Meta.NormNum.isInt_mul

added theorem Mathlib.Meta.NormNum.isInt_neg

added theorem Mathlib.Meta.NormNum.isInt_pow

added theorem Mathlib.Meta.NormNum.isInt_sub

modified theorem Mathlib.Meta.NormNum.isNat_add

modified theorem Mathlib.Meta.NormNum.isNat_cast

added theorem Mathlib.Meta.NormNum.isNat_int_cast

modified theorem Mathlib.Meta.NormNum.isNat_mul

added theorem Mathlib.Meta.NormNum.isNat_ofNat

modified theorem Mathlib.Meta.NormNum.isNat_one

modified theorem Mathlib.Meta.NormNum.isNat_pow

modified theorem Mathlib.Meta.NormNum.isNat_zero

deleted def Mathlib.Meta.NormNum.withSemiring

Modified Mathlib/Tactic/NormNum/Core.lean

added theorem Mathlib.Meta.NormNum.IsInt.neg_to_eq

added theorem Mathlib.Meta.NormNum.IsInt.nonneg_to_eq

added theorem Mathlib.Meta.NormNum.IsInt.to_isNat

added structure Mathlib.Meta.NormNum.IsInt

added theorem Mathlib.Meta.NormNum.IsNat.raw_refl

added theorem Mathlib.Meta.NormNum.IsNat.to_eq

added theorem Mathlib.Meta.NormNum.IsNat.to_isInt

added structure Mathlib.Meta.NormNum.IsNat

added structure Mathlib.Meta.NormNum.IsRat

added inductive Mathlib.Meta.NormNum.Result'

added def Mathlib.Meta.NormNum.Result.isInt

added def Mathlib.Meta.NormNum.Result.isNat

added def Mathlib.Meta.NormNum.Result.isNegNat

added def Mathlib.Meta.NormNum.Result.isRat

added def Mathlib.Meta.NormNum.Result.toInt

deleted def Mathlib.Meta.NormNum.Result.toIsNat

deleted def Mathlib.Meta.NormNum.Result.toIsNatQ

modified def Mathlib.Meta.NormNum.Result.toSimpResult

added def Mathlib.Meta.NormNum.Result

deleted inductive Mathlib.Meta.NormNum.Result

modified def Mathlib.Meta.NormNum.derive

added def Mathlib.Meta.NormNum.deriveInt

added def Mathlib.Meta.NormNum.deriveNat'

added def Mathlib.Meta.NormNum.deriveNat

deleted def Mathlib.Meta.NormNum.deriveQ

modified def Mathlib.Meta.NormNum.eval

deleted theorem Mathlib.Meta.NormNum.eval_of_isNat

added def Mathlib.Meta.NormNum.inferRing

added def Mathlib.Meta.NormNum.inferSemiring

added def Mathlib.Meta.NormNum.instRingInt

added def Mathlib.Meta.NormNum.instSemiringNat

added def Mathlib.Meta.NormNum.isIntLit

deleted def Mathlib.Meta.NormNum.isNat

added def Mathlib.Meta.NormNum.isNatLit

added def Mathlib.Meta.NormNum.isNormalForm

added def Mathlib.Meta.NormNum.isRatLit

added def Mathlib.Meta.NormNum.mkRawIntLit

Modified lean_packages/manifest.json

Modified test/norm_num.lean