Lean4
/-- Given `x` in a commutative group-with-zero, construct a new expression in the standard form
*** / *** (all denominators at the end) which is equal to `x`. -/
def reduceExpr (disch : ∀ {u : Level} (type : Q(Sort u)), MetaM Q($type)) (x : Expr) : AtomM Simp.Result := do
-- for `field_simp` to work with the recursive infrastructure in `AtomM.recurse`, we need to fail
-- on things `field_simp` would treat as atoms
guard x.isApp
let ⟨f, _⟩ := x.getAppFnArgs
guard <|
f ∈
[``HMul.hMul, ``HDiv.hDiv, ``Inv.inv, ``HPow.hPow, ``HAdd.hAdd, ``HSub.hSub, ``Neg.neg]
-- infer `u` and `K : Q(Type u)` such that `x : Q($K)`
let ⟨u, K, _⟩ ← inferTypeQ' x
let iK : Q(CommGroupWithZero $K) ←
synthInstanceQ
q(CommGroupWithZero $K)
-- run the core normalization function `normalizePretty` on `x`
trace[Tactic.field_simp]"putting {x} in \"field_simp\"-normal-form"
let ⟨e, pf⟩ ← reduceExprQ disch iK x
return { expr := e, proof? := some pf }
