Commit 2023-01-10 03:28 021406f0

View on Github →

chore: remove nondeterminism in abel (#1394) As reported on Zulip. The solution is to use the RingM monad in Abel as well, so we move this to its own file and rename it to AtomM. Also fixes two other bugs in abel.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic/Abel.lean

deleted def Mathlib.Tactic.Abel.Context.iapp

deleted def Mathlib.Tactic.Abel.Context.intToExpr

deleted def Mathlib.Tactic.Abel.Context.mkTerm

modified def Mathlib.Tactic.Abel.NormalExpr.term'

modified def Mathlib.Tactic.Abel.NormalExpr.zero'

added def Mathlib.Tactic.Abel.addG

deleted def Mathlib.Tactic.Abel.add_g

modified def Mathlib.Tactic.Abel.evalAtom

modified def Mathlib.Tactic.Abel.evalNeg

modified def Mathlib.Tactic.Abel.evalSMul'

modified def Mathlib.Tactic.Abel.evalSMul

added def Mathlib.Tactic.Abel.iapp

added def Mathlib.Tactic.Abel.intToExpr

modified def Mathlib.Tactic.Abel.mkContext

added def Mathlib.Tactic.Abel.mkTerm

modified theorem Mathlib.Tactic.Abel.term_atom

added theorem Mathlib.Tactic.Abel.term_atom_pf

added theorem Mathlib.Tactic.Abel.term_atom_pfg

modified theorem Mathlib.Tactic.Abel.term_atomg

Modified Mathlib/Tactic/Polyrith.lean

Modified Mathlib/Tactic/Ring/Basic.lean

deleted structure Mathlib.Tactic.Ring.Context

deleted def Mathlib.Tactic.Ring.RingM.run

deleted structure Mathlib.Tactic.Ring.State

deleted def Mathlib.Tactic.Ring.addAtom

modified def Mathlib.Tactic.Ring.evalAtom

modified def Mathlib.Tactic.Ring.evalNSMul

modified def Mathlib.Tactic.Ring.proveEq

Modified Mathlib/Tactic/Ring/RingNF.lean

modified def Mathlib.Tactic.RingNF.ringNFLocalDecl

modified def Mathlib.Tactic.RingNF.ringNFTarget

Created Mathlib/Util/AtomM.lean

added structure Mathlib.Tactic.AtomM.Context

added structure Mathlib.Tactic.AtomM.State

added def Mathlib.Tactic.AtomM.addAtom

added def Mathlib.Tactic.AtomM.run

Modified test/abel.lean