leanprover-community
Approximation tactic
I don't know anything about the implementation of norm_num, but in my ideal world, these lemmas would entirely be handled by norm_num.
Originally posted by @Smaug123 in https://github.com/leanprover-community/mathlib/issues/8002#issuecomment-1158021087
There are a few lemmas in the Bertrand's postulate proof that bound certain expressions using sqrt, log, exp. It would be nice if ~~norm_num~~ some tactic could handle these.
In particular, if we want to prove a goal of the form e1 < e2, where e1 and e2 are compositions of continuous functions (or are at least continuous at their arguments) applied to rationals, then in principle, we can generate finer and finer approximations of both expressions until eventually we can prove the goal by the triangle inequality.
This is not a job for norm_num, which works from the inside out, evaluating terms to a normal form. What we need here is something like Isabelle's approximation tactic, but it's a fairly complicated tactic to port and has little in common with norm_num.
