Commit 2022-11-15 22:02 28bde4b3

View on Github →

feat: refactoring RingNF, ring1_nf tactic (#601) The ring1_nf tactic acts like ring1 in that it expects the goal to be an equality and does not produce subgoals, but it will recursively simplify inside atoms like ring_nf does in recursive mode.

Estimated changes

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Tactic/Ring/Basic.lean

added def Mathlib.Tactic.Ring.proveEq

Modified Mathlib/Tactic/Ring/RingNF.lean

deleted inductive Mathlib.Tactic.Ring.RingMode

deleted structure Mathlib.Tactic.Ring.RingNF.Config

deleted theorem Mathlib.Tactic.Ring.add_assoc_rev

deleted theorem Mathlib.Tactic.Ring.add_neg

deleted def Mathlib.Tactic.Ring.elabRingNFConv

deleted theorem Mathlib.Tactic.Ring.int_rawCast_1

deleted theorem Mathlib.Tactic.Ring.int_rawCast_2

deleted theorem Mathlib.Tactic.Ring.mul_assoc_rev

deleted theorem Mathlib.Tactic.Ring.mul_neg

deleted theorem Mathlib.Tactic.Ring.nat_rawCast_0

deleted theorem Mathlib.Tactic.Ring.nat_rawCast_1

deleted theorem Mathlib.Tactic.Ring.nat_rawCast_2

deleted def Mathlib.Tactic.Ring.ringNFLocalDecl

deleted def Mathlib.Tactic.Ring.ringNFTarget

added structure Mathlib.Tactic.RingNF.Config

added structure Mathlib.Tactic.RingNF.Context

added inductive Mathlib.Tactic.RingNF.RingMode

added theorem Mathlib.Tactic.RingNF.add_assoc_rev

added theorem Mathlib.Tactic.RingNF.add_neg

added def Mathlib.Tactic.RingNF.elabRingNFConv

added theorem Mathlib.Tactic.RingNF.int_rawCast_1

added theorem Mathlib.Tactic.RingNF.int_rawCast_2

added theorem Mathlib.Tactic.RingNF.mul_assoc_rev

added theorem Mathlib.Tactic.RingNF.mul_neg

added theorem Mathlib.Tactic.RingNF.nat_rawCast_0

added theorem Mathlib.Tactic.RingNF.nat_rawCast_1

added theorem Mathlib.Tactic.RingNF.nat_rawCast_2

added def Mathlib.Tactic.RingNF.rewrite

added def Mathlib.Tactic.RingNF.ringNFLocalDecl

added def Mathlib.Tactic.RingNF.ringNFTarget