Lean4
/-- A cleanup routine, which simplifies normalized polynomials to a more human-friendly format. -/
def cleanup (cfg : RingNF.Config) (r : Simp.Result) : MetaM Simp.Result := do
match cfg.mode with
| .raw =>
pure r
| .SOP =>
do
let thms : SimpTheorems := { }
let thms ←
[``add_zero, ``add_assoc_rev, ``_root_.mul_one, ``mul_assoc_rev, ``_root_.pow_one, ``mul_neg, ``add_neg].foldlM
(·.addConst ·) thms
let thms ←
[``nat_rawCast_0, ``nat_rawCast_1, ``nat_rawCast_2, ``int_rawCast_neg, ``nnrat_rawCast,
``rat_rawCast_neg].foldlM
(·.addConst · (post := false)) thms
let ctx ←
Simp.mkContext { zetaDelta := cfg.zetaDelta } (simpTheorems := #[thms]) (congrTheorems :=
← getSimpCongrTheorems)
pure <| ← r.mkEqTrans (← Simp.main r.expr ctx (methods := Lean.Meta.Simp.mkDefaultMethodsCore { })).1
