Commit 69cda5de authored by Heiko Becker's avatar Heiko Becker
Browse files

Make sqrt bound way more accurate

parent 28fb7c69
......@@ -48,7 +48,7 @@ Definition inferErrorbound_def:
sqrtFinLo= newton ITERCOUNT (IVlo errIve1 * 0.99) (IVlo errIve1 * 0.99);
sqrtFinHi = newton ITERCOUNT (IVhi errIve1 * 1.01) (IVhi errIve1 * 1.01);
sqrtFinIv = (sqrtFinLo, sqrtFinHi);
propError = maxAbs (subtractInterval sqrtRealIv sqrtFinIv);
propError = err1 * sqrtFinHi * inv ((IVlo iv1 - err1) * 2);
mAbs = maxAbs sqrtFinIv
in
SOME (FloverMapTree_insert e (iv_f, propError + computeError mAbs m) recRes);
......
......@@ -63,7 +63,7 @@ Definition validErrorbound_def:
sqrtFinLo= newton ITERCOUNT (IVlo errIve1 * 0.99) (IVlo errIve1 * 0.99);
sqrtFinHi = newton ITERCOUNT (IVhi errIve1 * 1.01) (IVhi errIve1 * 1.01);
sqrtFinIv = (sqrtFinLo, sqrtFinHi);
propError = maxAbs (subtractInterval sqrtRealIv sqrtFinIv);
propError = err1 * sqrtFinHi * inv ((IVlo iv1 - err1) * 2);
mAbs = maxAbs sqrtFinIv
in
if (validate_newton_down sqrtRealLo (IVlo iv1)
......@@ -2281,9 +2281,10 @@ Proof
\\ irule REAL_LE_TRANS
\\ qexists_tac abs (sqrt nR1 - sqrt nF1) + computeError (sqrt nF1) m
\\ conj_tac
>- (drule sqrt_abs_err_bounded \\ rpt $ disch_then drule
\\ disch_then $ qspecl_then [nR, nF, err1, m] mp_tac
\\ gs[toREval_def])
>- (
drule sqrt_abs_err_bounded \\ rpt $ disch_then drule
\\ disch_then $ qspecl_then [nR, nF, err1, m] mp_tac
\\ gs[toREval_def])
\\ contained nF1 (widenInterval (elo, ehi) err1)
by (irule distance_gives_iv \\ find_exists_tac \\ gs[contained_def])
\\ rpt (
......@@ -2312,16 +2313,12 @@ Proof
\\ irule REAL_LE_ADD2 \\ conj_tac
(* Prove propagation error *)
>- (
irule contained_leq_maxAbs
\\ assume_tac $ SIMP_RULE std_ss [validIntervalSub_def] interval_subtraction_valid
\\ pop_assum irule \\ conj_tac \\ gs[contained_def]
\\ conj_tac \\ irule REAL_LE_TRANS
>- (asm_exists_tac \\ gs[] \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
>- (once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ gs[]
\\ irule transcTheory.SQRT_MONO_LE \\ gs[] \\ REAL_ASM_ARITH_TAC)
>- (asm_exists_tac \\ gs[] \\ irule transcTheory.SQRT_MONO_LE \\ real_prove)
\\ once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ gs[]
\\ irule transcTheory.SQRT_MONO_LE \\ gs[] \\ REAL_ASM_ARITH_TAC)
irule sqrt_diff_ub_concrete \\ gs[widenInterval_def]
\\ imp_res_tac err_always_positive \\ gs[PULL_EXISTS]
\\ qexists_tac ehi \\ gs[]
\\ imp_res_tac distance_gives_iv
\\ first_x_assum $ qspec_then (elo, ehi) mp_tac
\\ gs[contained_def, widenInterval_def])
(* New error *)
\\ irule computeError_up
\\ irule contained_leq_maxAbs
......
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment