Lean4
/-- Given `e`, a term with rational division, produces a natural number `n` and a proof of `n*e = e'`,
where `e'` has no division. Assumes "well-behaved" division.
-/
def derive (e : Expr) : MetaM (ℕ × Expr) := do
trace[CancelDenoms]"e = {e}"
let eSimp ← simpOnlyNames (config := Simp.neutralConfig) deriveThms e
trace[CancelDenoms]"e simplified = {eSimp.expr}"
let eSimpNormNum ← Mathlib.Meta.NormNum.deriveSimp (← Simp.mkContext) false eSimp.expr
trace[CancelDenoms]"e norm_num'd = {eSimpNormNum.expr}"
let (n, t) := findCancelFactor eSimpNormNum.expr
let ⟨u, tp, e⟩ ← inferTypeQ' eSimpNormNum.expr
let stp : Q(Field $tp) ← synthInstanceQ q(Field $tp)
try
have n' := (← mkOfNat tp q(inferInstance) <| mkRawNatLit <| n).1
let r ← mkProdPrf tp stp n n' t e
trace[CancelDenoms]"pf : {← inferType r.pf}"
let pf' ←
match eSimp.proof?, eSimpNormNum.proof? with
| some pfSimp, some pfSimp' =>
mkAppM ``derive_trans₂ #[pfSimp, pfSimp', r.pf]
| some pfSimp, none | none, some pfSimp =>
mkAppM ``derive_trans #[pfSimp, r.pf]
| none, none =>
pure r.pf
return (n, pf')
catch E =>
do
throwError "CancelDenoms.derive failed to normalize {e }.\n{E.toMessageData}"
