Lean4
/-- Evaluate an expression into its `abel` normal form, by recursing into subexpressions. -/
partial def eval (e : Expr) : M (NormalExpr × Expr) := do
trace[abel.detail]"running eval on {e}"
trace[abel.detail]"getAppFnArgs: {e.getAppFnArgs}"
match e.getAppFnArgs with
| (``HAdd.hAdd, #[_, _, _, _, e₁, e₂]) =>
do
let (e₁', p₁) ← eval e₁
let (e₂', p₂) ← eval e₂
let (e', p') ← evalAdd e₁' e₂'
return (e', ← iapp ``subst_into_add #[e₁, e₂, e₁', e₂', e', p₁, p₂, p'])
| (``HSub.hSub, #[_, _, _, _, e₁, e₂]) =>
do
let e₂' ← mkAppM ``Neg.neg #[e₂]
let e ← mkAppM ``HAdd.hAdd #[e₁, e₂']
let (e', p) ← eval e
let p' ← (← read).mkApp ``unfold_sub ``SubtractionMonoid #[e₁, e₂, e', p]
return (e', p')
| (``Neg.neg, #[_, _, e]) =>
do
let (e₁, p₁) ← eval e
let (e₂, p₂) ← evalNeg e₁
return (e₂, ← iapp `Mathlib.Tactic.Abel.subst_into_neg #[e, e₁, e₂, p₁, p₂])
| (``AddMonoid.nsmul, #[_, _, e₁, e₂]) =>
do
let n ←
if (← read).isGroup then
mkAppM ``Int.ofNat #[e₁]
else
pure e₁
let (e', p) ← eval <| ← iapp ``smul #[n, e₂]
return (e', ← iapp ``unfold_smul #[e₁, e₂, e', p])
| (``SubNegMonoid.zsmul, #[_, _, e₁, e₂]) =>
do
if ¬(← read).isGroup then
failure
let (e', p) ← eval <| ← iapp ``smul #[e₁, e₂]
return (e', (← read).app ``unfold_zsmul (← read).inst #[e₁, e₂, e', p])
| (``SMul.smul, #[.const ``Int _, _, _, e₁, e₂]) =>
evalSMul' eval true e e₁ e₂
| (``SMul.smul, #[.const ``Nat _, _, _, e₁, e₂]) =>
evalSMul' eval false e e₁ e₂
| (``HSMul.hSMul, #[.const ``Int _, _, _, _, e₁, e₂]) =>
evalSMul' eval true e e₁ e₂
| (``HSMul.hSMul, #[.const ``Nat _, _, _, _, e₁, e₂]) =>
evalSMul' eval false e e₁ e₂
| (``smul, #[_, _, e₁, e₂]) =>
evalSMul' eval false e e₁ e₂
| (``smulg, #[_, _, e₁, e₂]) =>
evalSMul' eval true e e₁ e₂
| (``OfNat.ofNat, #[_, .lit (.natVal 0), _]) | (``Zero.zero, #[_, _]) =>
if ← isDefEq e (← read).α0 then
pure (← zero', ← mkEqRefl (← read).α0)
else
evalAtom e
| _ =>
evalAtom e
