Lean4
/-- Postprocessing for the scalar goals constructed in the `match_scalars` and `module` tactics.
These goals feature a proliferation of `algebraMap` operations (because the scalars start in `ℕ` and
get successively bumped up by `algebraMap`s as new semirings are encountered), so we reinterpret the
most commonly occurring `algebraMap`s (those out of `ℕ`, `ℤ` and `ℚ`) into their standard forms
(`ℕ`, `ℤ` and `ℚ` casts) and then try to disperse the casts using the various `push_cast` lemmas. -/
def postprocess (mvarId : MVarId) : MetaM MVarId := do
-- collect the available `push_cast` lemmas
let mut thms : SimpTheorems := ← NormCast.pushCastExt.getTheorems
for thm in algebraMapThms do
let ⟨levelParams, _, proof⟩ ← abstractMVars (mkConst thm)
thms ← thms.add (.stx (← mkFreshId) Syntax.missing) levelParams proof
let ctx ← Simp.mkContext { failIfUnchanged := false } (simpTheorems := #[thms])
let (some r, _) ← simpTarget mvarId ctx (simprocs := #[]) |
throwError"internal error in match_scalars tactic: postprocessing should not close goals"
return r
