Lean4
/-- Normalize a term `orig` of the form `smul e₁ e₂` or `smulg e₁ e₂`.
Normalized terms use `smul` for monoids and `smulg` for groups,
so there are actually four cases to handle:
* Using `smul` in a monoid just simplifies the pieces using `subst_into_smul`
* Using `smulg` in a group just simplifies the pieces using `subst_into_smulg`
* Using `smul a b` in a group requires converting `a` from a nat to an int and
then simplifying `smulg ↑a b` using `subst_into_smul_upcast`
* Using `smulg` in a monoid is impossible (or at least out of scope),
because you need a group argument to write a `smulg` term -/
def evalSMul' (eval : Expr → M (NormalExpr × Expr)) (is_smulg : Bool) (orig e₁ e₂ : Expr) : M (NormalExpr × Expr) := do
trace[abel]"Calling NormNum on {e₁}"
let ⟨e₁', p₁, _⟩ ←
try
Meta.NormNum.eval e₁
catch _ =>
pure { expr := e₁ }
let p₁ ← p₁.getDM (mkEqRefl e₁')
match e₁'.int? with
| some n =>
do
let c ← read
let (e₂', p₂) ← eval e₂
if c.isGroup = is_smulg then
do
let (e', p) ← evalSMul (e₁', n) e₂'
return (e', ← iapp ``subst_into_smul #[e₁, e₂, e₁', e₂', e', p₁, p₂, p])
else
do
if ¬c.isGroup then
throwError"Doesn't make sense to us `smulg` in a monoid. "
let zl ← Expr.ofInt q(ℤ) n
let p₁' ← mkEqRefl zl
let (e', p) ← evalSMul (zl, n) e₂'
return (e', c.app ``subst_into_smul_upcast c.inst #[e₁, e₂, e₁', zl, e₂', e', p₁, p₁', p₂, p])
| none =>
evalAtom orig
