Commit 2022-11-07 21:53 9b2767fe

View on Github →

feat: ring_nf tactic (#552)

depends on #551 (only to avoid conflicts) Implements the ring_nf tactic, and makes ring call both ring1 and ring_nf like in mathlib.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Modified Mathlib/Tactic/Ring.lean

deleted def Lean.LOption.toOption

deleted def Mathlib.Tactic.Ring.Cache.nat

deleted structure Mathlib.Tactic.Ring.Cache

deleted structure Mathlib.Tactic.Ring.Context

deleted def Mathlib.Tactic.Ring.ExBase.evalPos

deleted def Mathlib.Tactic.Ring.ExBase.toProd

deleted inductive Mathlib.Tactic.Ring.ExBase

deleted def Mathlib.Tactic.Ring.ExProd.coeff

deleted def Mathlib.Tactic.Ring.ExProd.evalPos

deleted def Mathlib.Tactic.Ring.ExProd.mkNat

deleted def Mathlib.Tactic.Ring.ExProd.mkNegNat

deleted def Mathlib.Tactic.Ring.ExProd.toSum

deleted inductive Mathlib.Tactic.Ring.ExProd

deleted def Mathlib.Tactic.Ring.ExSum.evalPos

deleted inductive Mathlib.Tactic.Ring.ExSum

deleted structure Mathlib.Tactic.Ring.ExtractCoeff

deleted inductive Mathlib.Tactic.Ring.Overlap

deleted structure Mathlib.Tactic.Ring.Result

deleted def Mathlib.Tactic.Ring.RingM.run

deleted structure Mathlib.Tactic.Ring.State

deleted def Mathlib.Tactic.Ring.addAtom

deleted theorem Mathlib.Tactic.Ring.add_congr

deleted theorem Mathlib.Tactic.Ring.add_mul

deleted theorem Mathlib.Tactic.Ring.add_overlap_pf

deleted theorem Mathlib.Tactic.Ring.add_overlap_pf_zero

deleted theorem Mathlib.Tactic.Ring.add_pf_add_gt

deleted theorem Mathlib.Tactic.Ring.add_pf_add_lt

deleted theorem Mathlib.Tactic.Ring.add_pf_add_overlap

deleted theorem Mathlib.Tactic.Ring.add_pf_add_overlap_zero

deleted theorem Mathlib.Tactic.Ring.add_pf_add_zero

deleted theorem Mathlib.Tactic.Ring.add_pf_zero_add

deleted theorem Mathlib.Tactic.Ring.add_pos_left

deleted theorem Mathlib.Tactic.Ring.add_pos_right

deleted theorem Mathlib.Tactic.Ring.atom_pf

deleted theorem Mathlib.Tactic.Ring.cast_neg

deleted theorem Mathlib.Tactic.Ring.cast_pos

deleted theorem Mathlib.Tactic.Ring.cast_zero

deleted theorem Mathlib.Tactic.Ring.coeff_mul

deleted theorem Mathlib.Tactic.Ring.coeff_one

deleted theorem Mathlib.Tactic.Ring.const_pos

deleted def Mathlib.Tactic.Ring.evalAddOverlap

deleted def Mathlib.Tactic.Ring.evalAtom

deleted def Mathlib.Tactic.Ring.evalCast

deleted def Mathlib.Tactic.Ring.evalMul

deleted def Mathlib.Tactic.Ring.evalMul₁

deleted def Mathlib.Tactic.Ring.evalNSMul

deleted def Mathlib.Tactic.Ring.evalNeg

deleted def Mathlib.Tactic.Ring.evalNegProd

deleted def Mathlib.Tactic.Ring.evalPow

deleted def Mathlib.Tactic.Ring.evalPowAtom

deleted def Mathlib.Tactic.Ring.evalPowProd

deleted def Mathlib.Tactic.Ring.evalPowProdAtom

deleted def Mathlib.Tactic.Ring.evalSub

deleted def Mathlib.Tactic.Ring.extractCoeff

deleted def Mathlib.Tactic.Ring.instCommSemiringNat

deleted theorem Mathlib.Tactic.Ring.mul_add

deleted theorem Mathlib.Tactic.Ring.mul_congr

deleted theorem Mathlib.Tactic.Ring.mul_exp_pos

deleted theorem Mathlib.Tactic.Ring.mul_one

deleted theorem Mathlib.Tactic.Ring.mul_pf_left

deleted theorem Mathlib.Tactic.Ring.mul_pf_right

deleted theorem Mathlib.Tactic.Ring.mul_pow

deleted theorem Mathlib.Tactic.Ring.mul_pp_pf_overlap

deleted theorem Mathlib.Tactic.Ring.mul_zero

deleted theorem Mathlib.Tactic.Ring.nat_cast_add

deleted theorem Mathlib.Tactic.Ring.nat_cast_mul

deleted theorem Mathlib.Tactic.Ring.nat_cast_nat

deleted theorem Mathlib.Tactic.Ring.nat_cast_zero

deleted theorem Mathlib.Tactic.Ring.neg_add

deleted theorem Mathlib.Tactic.Ring.neg_congr

deleted theorem Mathlib.Tactic.Ring.neg_mul

deleted theorem Mathlib.Tactic.Ring.neg_one_mul

deleted theorem Mathlib.Tactic.Ring.neg_zero

deleted theorem Mathlib.Tactic.Ring.nsmul_congr

deleted theorem Mathlib.Tactic.Ring.of_eq

deleted theorem Mathlib.Tactic.Ring.one_mul

deleted theorem Mathlib.Tactic.Ring.one_pow

deleted theorem Mathlib.Tactic.Ring.pow_add

deleted theorem Mathlib.Tactic.Ring.pow_atom

deleted theorem Mathlib.Tactic.Ring.pow_bit0

deleted theorem Mathlib.Tactic.Ring.pow_bit1

deleted theorem Mathlib.Tactic.Ring.pow_congr

deleted theorem Mathlib.Tactic.Ring.pow_nat

deleted theorem Mathlib.Tactic.Ring.pow_one

deleted theorem Mathlib.Tactic.Ring.pow_one_cast

deleted theorem Mathlib.Tactic.Ring.pow_prod_atom

deleted theorem Mathlib.Tactic.Ring.pow_zero

deleted theorem Mathlib.Tactic.Ring.single_pow

deleted theorem Mathlib.Tactic.Ring.smul_eq_cast

deleted theorem Mathlib.Tactic.Ring.smul_nat

deleted theorem Mathlib.Tactic.Ring.sub_congr

deleted theorem Mathlib.Tactic.Ring.sub_pf

deleted def Mathlib.Tactic.Ring.sℕ

deleted theorem Mathlib.Tactic.Ring.zero_mul

deleted theorem Mathlib.Tactic.Ring.zero_pow

Created Mathlib/Tactic/Ring/Basic.lean

added def Lean.LOption.toOption

added def Mathlib.Tactic.Ring.Cache.nat

added 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

added inductive Mathlib.Tactic.Ring.Overlap

added structure Mathlib.Tactic.Ring.Result

added def Mathlib.Tactic.Ring.RingM.run

added structure Mathlib.Tactic.Ring.State

added def Mathlib.Tactic.Ring.addAtom

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.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

added theorem Mathlib.Tactic.Ring.const_pos

added def Mathlib.Tactic.Ring.evalAddOverlap

added def Mathlib.Tactic.Ring.evalAtom

added def Mathlib.Tactic.Ring.evalCast

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

added def Mathlib.Tactic.Ring.instCommSemiringNat

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

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

added def Mathlib.Tactic.Ring.sℕ

added theorem Mathlib.Tactic.Ring.zero_mul

added theorem Mathlib.Tactic.Ring.zero_pow

Created Mathlib/Tactic/Ring/RingNF.lean

added def Mathlib.Tactic.Ring.ExBase.isAtom

added def Mathlib.Tactic.Ring.ExProd.isAtom

added def Mathlib.Tactic.Ring.ExSum.isAtom

added inductive Mathlib.Tactic.Ring.RingMode

added structure Mathlib.Tactic.Ring.RingNF.Config

added theorem Mathlib.Tactic.Ring.add_assoc_rev

added theorem Mathlib.Tactic.Ring.add_neg

added def Mathlib.Tactic.Ring.elabRingNFConv

added theorem Mathlib.Tactic.Ring.int_rawCast_1

added theorem Mathlib.Tactic.Ring.int_rawCast_2

added theorem Mathlib.Tactic.Ring.mul_assoc_rev

added theorem Mathlib.Tactic.Ring.mul_neg

added theorem Mathlib.Tactic.Ring.nat_rawCast_0

added theorem Mathlib.Tactic.Ring.nat_rawCast_1

added theorem Mathlib.Tactic.Ring.nat_rawCast_2

added def Mathlib.Tactic.Ring.ringNFLocalDecl

added def Mathlib.Tactic.Ring.ringNFTarget

Modified test/ring.lean