You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
BoltonBailey
changed the title
Get norm_num to prove things about common functions
Approximation tactic
Jun 17, 2022
I don't know anything about the implementation of
norm_num
, but in my ideal world, these lemmas would entirely be handled bynorm_num
.Originally posted by @Smaug123 in #8002 (comment)
There are a few lemmas in the Bertrand's postulate proof that bound certain expressions using
sqrt
,log
,exp
. It would be nice ifsome tactic could handle these.norm_num
In particular, if we want to prove a goal of the form
e1 < e2
, wheree1
ande2
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.The text was updated successfully, but these errors were encountered: