Lean4
/-- The goal of the simprocs grouped under the `field` attribute is to clear denominators in
(semi-)field (in)equalities, by bringing LHS and RHS each over a common denominator and then
cross-multiplying. For example, the `field` simproc will clear the `x` denominators in the following
equation:
```
example {K : Type*} [Field K] {x : K} (hx0 : x ≠ 0) :
(x + 1 / x) ^ 2 + (x + 1 / x) = 1 := by
simp only [field]
-- new goal: `⊢ (x ^ 2 + 1) * (x ^ 2 + 1 + x) = x ^ 2`
```
The `field` simproc-set's functionality is a variant of the more general `field_simp` tactic, which
not only clears denominators in field (in)equalities but also brings isolated field expressions into
the normal form `n / d` (where neither `n` nor `d` contains any division symbol). (For confluence
reasons, the `field` simprocs also have a slightly different normal form from `field_simp`'s.)
Cancelling and combining denominators will generally require checking "nonzeroness"/"positivity"
side conditions. The `field` simproc-set attempts to discharge these, and will omit such steps if it
cannot discharge the corresponding side conditions. The discharger will try, among other things,
`positivity` and `norm_num`, and will also use any nonzeroness/positivity proofs included explicitly
in the simp call (e.g. `simp [field, hx]`). If your (in)equality is not completely reduced by the
`field` simproc-set, check the denominators of the resulting (in)equality and provide proofs that
they are nonzero/positive to enable further progress.
-/
def proc : Simp.Simproc := fun (t : Expr) ↦ do
let ctx ← Simp.getContext
let disch e : MetaM Expr := Prod.fst <$> (FieldSimp.discharge e).run ctx >>= Option.getM
try
let r ← AtomM.run .reducible <| FieldSimp.reduceProp disch t
return .visit <| ← r.mkEqTrans (← simpOnlyNames [``one_div, ``mul_inv] r.expr)
catch _ =>
return .continue
