Commit 2022-11-01 23:28 6f1cc3b7

View on Github →

feat: ring_exp tactic, subtraction in ring (#519) Another complete rewrite. This implements one ring to rule them all: it incorporates both ring_exp and ring behaviors, now under the name ring. (ring_exp had some small (1.4x) performance issues that prevented it from being used by default; I'm hoping that those issues are fixed now, and we can revisit later if it becomes an issue.)

Estimated changes

Modified Mathlib/Algebra/GroupPower/Basic.lean

added theorem succ_nsmul'

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

added theorem nsmul_eq_mul'

added theorem nsmul_eq_mul

Modified Mathlib/Algebra/Ring/Basic.lean

added theorem Commute.add_left

added theorem Commute.add_right

added theorem Commute.zero_left

added theorem Commute.zero_right

added theorem Nat.cast_commute

added theorem mul_neg

added theorem neg_mul

modified theorem neg_mul_eq_neg_mul

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

Modified Mathlib/Tactic/NormNum/Core.lean

added def Int.rawCast

added theorem Mathlib.Meta.NormNum.IsInt.of_raw

added theorem Mathlib.Meta.NormNum.IsInt.to_raw_eq

added theorem Mathlib.Meta.NormNum.IsNat.of_raw

modified theorem Mathlib.Meta.NormNum.IsNat.to_eq

added theorem Mathlib.Meta.NormNum.IsNat.to_raw_eq

added def Mathlib.Meta.NormNum.Result.ofRawInt

added def Mathlib.Meta.NormNum.Result.ofRawNat

added def Mathlib.Meta.NormNum.Result.toRawEq

added def Nat.rawCast

Modified Mathlib/Tactic/Ring.lean

added def Lean.LOption.toOption

added def Mathlib.Tactic.Ring.Cache.nat

modified structure Mathlib.Tactic.Ring.Cache

added structure Mathlib.Tactic.Ring.Context

added def Mathlib.Tactic.Ring.ExBase.evalPos

added def Mathlib.Tactic.Ring.ExBase.toProd

added inductive Mathlib.Tactic.Ring.ExBase

added def Mathlib.Tactic.Ring.ExProd.coeff

added def Mathlib.Tactic.Ring.ExProd.evalPos

added def Mathlib.Tactic.Ring.ExProd.mkNat

added def Mathlib.Tactic.Ring.ExProd.mkNegNat

added def Mathlib.Tactic.Ring.ExProd.toSum

added inductive Mathlib.Tactic.Ring.ExProd

added def Mathlib.Tactic.Ring.ExSum.evalPos

added inductive Mathlib.Tactic.Ring.ExSum

added structure Mathlib.Tactic.Ring.ExtractCoeff

deleted def Mathlib.Tactic.Ring.HornerExpr.e

deleted def Mathlib.Tactic.Ring.HornerExpr.isZero

deleted def Mathlib.Tactic.Ring.HornerExpr.pp

deleted def Mathlib.Tactic.Ring.HornerExpr.reflConv

deleted def Mathlib.Tactic.Ring.HornerExpr.xadd'

deleted inductive Mathlib.Tactic.Ring.HornerExpr

added inductive Mathlib.Tactic.Ring.Overlap

added structure Mathlib.Tactic.Ring.Result

modified def Mathlib.Tactic.Ring.RingM.run

deleted def Mathlib.Tactic.Ring.State.numAtoms

added theorem Mathlib.Tactic.Ring.add_congr

added theorem Mathlib.Tactic.Ring.add_mul

added theorem Mathlib.Tactic.Ring.add_overlap_pf

added theorem Mathlib.Tactic.Ring.add_overlap_pf_zero

added theorem Mathlib.Tactic.Ring.add_pf_add_gt

added theorem Mathlib.Tactic.Ring.add_pf_add_lt

added theorem Mathlib.Tactic.Ring.add_pf_add_overlap

added theorem Mathlib.Tactic.Ring.add_pf_add_overlap_zero

added theorem Mathlib.Tactic.Ring.add_pf_add_zero

added theorem Mathlib.Tactic.Ring.add_pf_zero_add

added theorem Mathlib.Tactic.Ring.add_pos_left

added theorem Mathlib.Tactic.Ring.add_pos_right

added theorem Mathlib.Tactic.Ring.atom_pf

added theorem Mathlib.Tactic.Ring.cast_neg

added theorem Mathlib.Tactic.Ring.cast_pos

added theorem Mathlib.Tactic.Ring.cast_zero

added theorem Mathlib.Tactic.Ring.coeff_mul

added theorem Mathlib.Tactic.Ring.coeff_one

deleted theorem Mathlib.Tactic.Ring.const_add_horner

added theorem Mathlib.Tactic.Ring.const_pos

added def Mathlib.Tactic.Ring.evalAddOverlap

modified def Mathlib.Tactic.Ring.evalAtom

added def Mathlib.Tactic.Ring.evalCast

deleted def Mathlib.Tactic.Ring.evalConstMul

deleted def Mathlib.Tactic.Ring.evalHorner

added def Mathlib.Tactic.Ring.evalMul

added def Mathlib.Tactic.Ring.evalMul₁

added def Mathlib.Tactic.Ring.evalNSMul

added def Mathlib.Tactic.Ring.evalNeg

added def Mathlib.Tactic.Ring.evalNegProd

added def Mathlib.Tactic.Ring.evalPow

added def Mathlib.Tactic.Ring.evalPowAtom

added def Mathlib.Tactic.Ring.evalPowProd

added def Mathlib.Tactic.Ring.evalPowProdAtom

added def Mathlib.Tactic.Ring.evalSub

added def Mathlib.Tactic.Ring.extractCoeff

deleted def Mathlib.Tactic.Ring.horner

deleted theorem Mathlib.Tactic.Ring.horner_add_const

deleted theorem Mathlib.Tactic.Ring.horner_add_horner_eq

deleted theorem Mathlib.Tactic.Ring.horner_add_horner_gt

deleted theorem Mathlib.Tactic.Ring.horner_add_horner_lt

deleted theorem Mathlib.Tactic.Ring.horner_atom

deleted theorem Mathlib.Tactic.Ring.horner_const_mul

deleted theorem Mathlib.Tactic.Ring.horner_horner

deleted theorem Mathlib.Tactic.Ring.horner_mul_const

deleted theorem Mathlib.Tactic.Ring.horner_mul_horner

deleted theorem Mathlib.Tactic.Ring.horner_mul_horner_zero

deleted theorem Mathlib.Tactic.Ring.horner_pow

added def Mathlib.Tactic.Ring.instCommSemiringNat

deleted def Mathlib.Tactic.Ring.mkAppCS

added theorem Mathlib.Tactic.Ring.mul_add

added theorem Mathlib.Tactic.Ring.mul_congr

added theorem Mathlib.Tactic.Ring.mul_exp_pos

added theorem Mathlib.Tactic.Ring.mul_one

added theorem Mathlib.Tactic.Ring.mul_pf_left

added theorem Mathlib.Tactic.Ring.mul_pf_right

added theorem Mathlib.Tactic.Ring.mul_pow

added theorem Mathlib.Tactic.Ring.mul_pp_pf_overlap

added theorem Mathlib.Tactic.Ring.mul_zero

added theorem Mathlib.Tactic.Ring.nat_cast_add

added theorem Mathlib.Tactic.Ring.nat_cast_mul

added theorem Mathlib.Tactic.Ring.nat_cast_nat

added theorem Mathlib.Tactic.Ring.nat_cast_zero

added theorem Mathlib.Tactic.Ring.neg_add

added theorem Mathlib.Tactic.Ring.neg_congr

added theorem Mathlib.Tactic.Ring.neg_mul

added theorem Mathlib.Tactic.Ring.neg_one_mul

added theorem Mathlib.Tactic.Ring.neg_zero

added theorem Mathlib.Tactic.Ring.nsmul_congr

added theorem Mathlib.Tactic.Ring.of_eq

added theorem Mathlib.Tactic.Ring.one_mul

added theorem Mathlib.Tactic.Ring.one_pow

added theorem Mathlib.Tactic.Ring.pow_add

added theorem Mathlib.Tactic.Ring.pow_atom

added theorem Mathlib.Tactic.Ring.pow_bit0

added theorem Mathlib.Tactic.Ring.pow_bit1

added theorem Mathlib.Tactic.Ring.pow_congr

added theorem Mathlib.Tactic.Ring.pow_nat

added theorem Mathlib.Tactic.Ring.pow_one

added theorem Mathlib.Tactic.Ring.pow_one_cast

added theorem Mathlib.Tactic.Ring.pow_prod_atom

deleted theorem Mathlib.Tactic.Ring.pow_succ_eq

added theorem Mathlib.Tactic.Ring.pow_zero

added theorem Mathlib.Tactic.Ring.single_pow

added theorem Mathlib.Tactic.Ring.smul_eq_cast

added theorem Mathlib.Tactic.Ring.smul_nat

added theorem Mathlib.Tactic.Ring.sub_congr

added theorem Mathlib.Tactic.Ring.sub_pf

deleted theorem Mathlib.Tactic.Ring.subst_into_add

deleted theorem Mathlib.Tactic.Ring.subst_into_mul

deleted theorem Mathlib.Tactic.Ring.subst_into_pow

added def Mathlib.Tactic.Ring.sℕ

deleted theorem Mathlib.Tactic.Ring.zero_horner

added theorem Mathlib.Tactic.Ring.zero_mul

added theorem Mathlib.Tactic.Ring.zero_pow

Modified lean_packages/manifest.json

Modified test/ring.lean