Lean4
/-- Interpret the sum of two expressions in `abel`'s normal form.
-/
partial def evalAdd : NormalExpr → NormalExpr → M (NormalExpr × Expr)
| zero _, e₂ => do
let p ← mkAppM ``zero_add #[e₂]
return (e₂, p)
| e₁, zero _ => do
let p ← mkAppM ``add_zero #[e₁]
return (e₁, p)
| he₁@(nterm e₁ n₁ x₁ a₁), he₂@(nterm e₂ n₂ x₂ a₂) => do
if x₁.1 = x₂.1 then
let n' ← Mathlib.Meta.NormNum.eval (← mkAppM ``HAdd.hAdd #[n₁.1, n₂.1])
let (a', h₂) ← evalAdd a₁ a₂
let k := n₁.2 + n₂.2
let p₁ ← iapp ``term_add_term #[n₁.1, x₁.2, a₁, n₂.1, a₂, n'.expr, a', ← n'.getProof, h₂]
if k = 0 then
do
let p ← mkEqTrans p₁ (← iapp ``zero_term #[x₁.2, a'])
return (a', p)
else
return (← term' (n'.expr, k) x₁ a', p₁)
else if x₁.1 < x₂.1 then
do
let (a', h) ← evalAdd a₁ he₂
return (← term' n₁ x₁ a', ← iapp ``term_add_const #[n₁.1, x₁.2, a₁, e₂, a', h])
else
do
let (a', h) ← evalAdd he₁ a₂
return (← term' n₂ x₂ a', ← iapp ``const_add_term #[e₁, n₂.1, x₂.2, a₂, a', h])
