Commit caa156c7 authored by Heiko Becker's avatar Heiko Becker

Fix error bounds in HOL-Light

parent 6a3720b8
......@@ -124,9 +124,8 @@ let add_abs_err_bounded =
THENL [
REWRITE_TAC[REAL_ABS_POS]; auto]]]]]);;
let sub_abs_err_bounded =
prove (
`!(e1:(real)exp) (e1R:real) (e1F:real) (e2:(real)exp) (e2R:real) (e2F:real)
let sub_abs_err_bounded = prove (
`!(e1:(real)exp) (e1R:real) (e1F:real) (e2:(real)exp) (e2R:real) (e2F:real)
(vR:real) (vF:real) (cenv:num->real) (err1:real) (err2:real).
eval_exp (&0) cenv e1 e1R /\
eval_exp machineEpsilon cenv e1 e1F /\
......@@ -136,9 +135,9 @@ let sub_abs_err_bounded =
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F cenv)) (Binop Sub (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= err1 + err2 + (((abs e1F) + (abs e2F)) * machineEpsilon)`,
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
intros "!e1 e1R e1F e2 e2R e2F vR vF cenv err1 err2; e1_real e1_float e2_real e2_float plus_real plus_float abs_e1 abs_e2"
abs (vR - vF) <= err1 + err2 + (abs (e1F - e2F)) * machineEpsilon`,
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
intros "!e1 e1R e1F e2 e2R e2F vR vF cenv err1 err2; e1_real e1_float e2_real e2_float plus_real plus_float abs_e1 abs_e2"
THEN USE_THEN "plus_real"
(fun th -> LABEL_TAC "plus_real_inv"
(MP (SPECL [`&0:real`;`cenv:num->real`; `Sub:binop`;`e1:(real)exp`; `e2:(real)exp`; `vR:real`] binop_inv) th))
......@@ -207,19 +206,9 @@ let sub_abs_err_bounded =
ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN ONCE_REWRITE_TAC[GSYM real_sub]
THEN ONCE_REWRITE_TAC[SPECL [`e2F:real`; `e2R:real`]REAL_ABS_SUB]
THEN auto;
ASM_REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_MUL]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `(abs (e1F:real) + abs (--(e2F:real))) * abs (delta2:real)`
THEN split
THENL [
mp REAL_LE_RMUL
THEN split
THENL [REWRITE_TAC[REAL_ABS_TRIANGLE]; REWRITE_TAC[REAL_ABS_POS]];
REWRITE_TAC [REAL_ABS_NEG]
THEN mp REAL_LE_LMUL
THEN split
THENL [
REAL_ARITH_TAC; auto]]]]]]);;
ASM_REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_MUL; GSYM real_sub]
THEN mp REAL_LE_LMUL THEN TRY auto
THEN REWRITE_TAC[REAL_ABS_POS]]]]]);;
let mul_abs_err_bounded = prove (
`!(e1:(real)exp) (e1R:real) (e1F:real) (e2:(real)exp) (e2R:real) (e2F:real)
......
......@@ -16,17 +16,20 @@ let validErrorbound = new_recursive_definition exp_REC
let (intv, err) = absenv (Binop b e1 e2) in
let (ive1, err1) = absenv e1 in
let (ive2, err2) = absenv e2 in
let errIve1 = widenInterval ive1 err1 in
let errIve2 = widenInterval ive2 err2 in
let upperBoundE1 = maxAbsFun ive1 in
let upperBoundE2 = maxAbsFun ive2 in
let e1F = upperBoundE1 + err1 in
let e2F = upperBoundE2 + err2 in
(validErrorbound e1 absenv /\ validErrorbound e2 absenv /\ (&0 <= err) /\
(if (b = Plus \/ b = Sub)
then (err1 + err2 + (abs e1F + abs e2F) * machineEpsilon) <= err
else
if b = Mult
then ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + abs (e1F * e2F) * machineEpsilon) <= err
else F)))`;;
(if (b = Plus)
then (err1 + err2 + (maxAbsFun (addInterval errIve1 errIve2)) * machineEpsilon) <= err
else
if (b = Sub)
then (err1 + err2 + (maxAbsFun (subtractInterval errIve1 errIve2)) * machineEpsilon) <= err
else
if b = Mult
then ((upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbsFun (multInterval errIve1 errIve2)) * machineEpsilon) <= err
else F)))`;;
let err_always_positive = prove (
`!(e:(real)exp) (absenv:analysisResult) (iv:interval) (err:error).
......@@ -218,50 +221,51 @@ let validErrorboundCorrectAddition = prove (
THEN rewrite validIntervalbounds "valid_intv"
THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
THEN simplify "valid_error"
THEN destruct "valid_error" "valid_err1 valid_err2 e_pos valid_err"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `err1 + err2 + (abs (maxAbsFun (e1lo,e1hi) + (err1:real)) + abs (maxAbsFun (e2lo,e2hi) + err2)) * machineEpsilon`
THEN EXISTS_TAC `err1 + err2 + (maxAbsFun (addInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2))) * machineEpsilon`
THEN split
THENL [
mp REAL_LE_LADD_IMP
THEN mp REAL_LE_LADD_IMP
THEN mp REAL_LE_RMUL
THEN pose_proof validIntervalbounds_sound "validbounds_e1"
[`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
["p_valid"; "valid_e1"; "e1_real"]
THEN rewrite_asm "absenv_e1" "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN destruct "validbounds_e1" "valid_lo_e1 valid_hi_e1"
THEN pose_proof distance_gives_iv "errIve1"
[`nR1:real`;`nF1:real`;`err1:real`;`e1lo:real`;`e1hi:real`]
["valid_lo_e1"; "valid_hi_e1"; "err1_bounded"]
THEN pose_proof validIntervalbounds_sound "validbounds_e2"
[`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
["p_valid"; "valid_e2"; "e2_real"]
THEN rewrite_asm "absenv_e2" "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN destruct "validbounds_e2" "valid_lo_e2 valid_hi_e2"
THEN pose_proof distance_gives_iv "errIve2"
[`nR2:real`;`nF2:real`;`err2:real`;`e2lo:real`;`e2hi:real`]
["valid_lo_e2"; "valid_hi_e2"; "err2_bounded"]
THEN pose_proof interval_add_valid "add_valid"
[`(widenInterval (e1lo,e1hi) err1)`;`widenInterval (e2lo,e2hi) err2`] []
THEN rewrite validIntervalAdd "add_valid"
THEN spec "add_valid" [`nF1:real`;`nF2:real`]
THEN mp_ispecl "add_valid" ["errIve1"; "errIve2"]
THEN split
THENL [
mp REAL_LE_TRANS
THEN EXISTS_TAC `abs nF1 + abs (nF2:real)`
THEN split
THENL [
SIMP_TAC[REAL_ABS_TRIANGLE];
mp REAL_LE_ADD2
THEN split
THENL [
pose validIntervalbounds_sound
[`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
"valid_bounds_e1"
THEN mp_ispecl "valid_bounds_e1" ["p_valid"; "valid_e1"; "e1_real"]
THEN mp (SPEC `nR1:real` Rabs_error_bounded_maxAbs)
THEN SIMP_TAC[contained; IVlo; IVhi]
THEN rewrite_asm "absenv_e1" "valid_bounds_e1"
THEN rewrite FST "valid_bounds_e1"
THEN rewrite FST "valid_bounds_e1"
THEN split THEN auto;
pose validIntervalbounds_sound
[`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
"valid_bounds_e2"
THEN mp_ispecl "valid_bounds_e2" ["p_valid"; "valid_e2"; "e2_real"]
THEN mp (SPEC `nR2:real` Rabs_error_bounded_maxAbs)
THEN SIMP_TAC[contained; IVlo; IVhi]
THEN rewrite_asm "absenv_e2" "valid_bounds_e2"
THEN rewrite FST "valid_bounds_e2"
THEN rewrite FST "valid_bounds_e2"
THEN split THEN auto
]
];
SUBGOAL_TAC "simp_iv" `?ivlo ivhi. addInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2) = (ivlo, ivhi)` [MESON_TAC [cases "prod"]]
THEN destruct "simp_iv" "@ivlo. @ivhi. simp_iv"
THEN ASM_SIMP_TAC[]
THEN rewrite_asm "simp_iv" "add_valid"
THEN mp contained_leq_maxAbs THEN auto;
SIMP_TAC[mEps_geq_zero]
];
]
;
auto]]);;
let validErrorboundCorrectSubtraction = prove (
`!(cenv:env_ty) (absenv:analysisResult) (e1:(real)exp) (e2:(real)exp) nR nR1
nR2 nF (nF1:real) (nF2:real) (e:error) err1 err2 alo ahi e1lo e1hi e2lo e2hi (P:precond).
......@@ -288,7 +292,7 @@ let validErrorboundCorrectAddition = prove (
["valid_intv"]
THEN pose sub_abs_err_bounded [`e1:(real)exp`; `nR1:real`; `nF1:real`; `e2:(real)exp`; `nR2:real`; `nF2:real`; `nR:real`; `nF:real`; `cenv:env_ty`; `err1:real`; `err2:real`] "sub_bounded"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `(err1:real) + (err2:real) + (abs (nF1:real) + abs (nF2:real)) * machineEpsilon`
THEN EXISTS_TAC `(err1:real) + (err2:real) + (abs ((nF1:real) - nF2:real)) * machineEpsilon`
THEN split
THENL [
mp_asm "sub_bounded" THEN clear["sub_bounded"] THEN auto;
......@@ -302,53 +306,54 @@ let validErrorboundCorrectAddition = prove (
THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
THEN simplify "valid_error"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `err1 + err2 + (abs (maxAbsFun (e1lo,e1hi) + (err1:real)) + abs (maxAbsFun (e2lo,e2hi) + err2)) * machineEpsilon`
THEN EXISTS_TAC `err1 + err2 + (maxAbsFun (subtractInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2))) * machineEpsilon`
THEN split
THENL [
mp REAL_LE_LADD_IMP
THEN mp REAL_LE_LADD_IMP
THEN mp REAL_LE_RMUL
THEN split
THENL [
mp REAL_LE_TRANS
THEN EXISTS_TAC `abs nF1 + abs (nF2:real)`
THEN split
THENL [
SIMP_TAC[REAL_LE_REFL];
mp REAL_LE_ADD2
THEN split
THENL [
pose validIntervalbounds_sound
[`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
"valid_bounds_e1"
THEN mp_ispecl "valid_bounds_e1" ["p_valid"; "valid_e1"; "e1_real"]
THEN mp (SPEC `nR1:real` Rabs_error_bounded_maxAbs)
THEN SIMP_TAC[contained; IVlo; IVhi]
THEN rewrite_asm "absenv_e1" "valid_bounds_e1"
THEN rewrite FST "valid_bounds_e1"
THEN rewrite FST "valid_bounds_e1"
THEN split THEN auto
;
pose validIntervalbounds_sound
[`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
"valid_bounds_e2"
THEN mp_ispecl "valid_bounds_e2" ["p_valid"; "valid_e2"; "e2_real"]
THEN mp (SPEC `nR2:real` Rabs_error_bounded_maxAbs)
THEN SIMP_TAC[contained; IVlo; IVhi]
THEN rewrite_asm "absenv_e2" "valid_bounds_e2"
THEN rewrite FST "valid_bounds_e2"
THEN rewrite FST "valid_bounds_e2"
THEN split THEN auto
]
];
SIMP_TAC[mEps_geq_zero]
];
auto
]
]);;
THEN pose_proof validIntervalbounds_sound "validbounds_e1"
[`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
["p_valid"; "valid_e1"; "e1_real"]
THEN rewrite_asm "absenv_e1" "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN destruct "validbounds_e1" "valid_lo_e1 valid_hi_e1"
THEN pose_proof distance_gives_iv "errIve1"
[`nR1:real`;`nF1:real`;`err1:real`;`e1lo:real`;`e1hi:real`]
["valid_lo_e1"; "valid_hi_e1"; "err1_bounded"]
THEN pose_proof validIntervalbounds_sound "validbounds_e2"
[`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
["p_valid"; "valid_e2"; "e2_real"]
THEN rewrite_asm "absenv_e2" "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN destruct "validbounds_e2" "valid_lo_e2 valid_hi_e2"
THEN pose_proof distance_gives_iv "errIve2"
[`nR2:real`;`nF2:real`;`err2:real`;`e2lo:real`;`e2hi:real`]
["valid_lo_e2"; "valid_hi_e2"; "err2_bounded"]
THEN pose_proof interval_subtraction_valid "sub_valid"
[`(widenInterval (e1lo,e1hi) err1)`;`widenInterval (e2lo,e2hi) err2`] []
THEN rewrite validIntervalSub "sub_valid"
THEN spec "sub_valid" [`nF1:real`;`nF2:real`]
THEN mp_ispecl "sub_valid" ["errIve1"; "errIve2"]
THEN split
THENL [
SUBGOAL_TAC "simp_iv" `?ivlo ivhi. subtractInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2) = (ivlo, ivhi)` [MESON_TAC [cases "prod"]]
THEN destruct "simp_iv" "@ivlo. @ivhi. simp_iv"
THEN ASM_SIMP_TAC[]
THEN rewrite_asm "simp_iv" "sub_valid"
THEN mp contained_leq_maxAbs THEN auto;
SIMP_TAC[mEps_geq_zero]
]
;
destruct "valid_error" "_ _ _ valid_error"
THEN REMOVE_THEN "valid_error"
(fun th -> LABEL_TAC "valid_error" (SIMP_RULE[distinctness "binop"] (CONV_RULE COND_ELIM_CONV th)))
THEN auto]]);;
let validErrorboundCorrectMultiplication = prove (
`!(cenv:env_ty) (absenv:analysisResult) (e1:(real)exp) (e2:(real)exp) nR nR1
let validErrorboundCorrectMultiplication = prove (
`!(cenv:env_ty) (absenv:analysisResult) (e1:(real)exp) (e2:(real)exp) nR nR1
nR2 nF (nF1:real) (nF2:real) (e:error) err1 err2 alo ahi e1lo e1hi e2lo e2hi (P:precond).
precondValidForExec P cenv /\
eval_exp (&0) cenv e1 nR1 /\
......@@ -365,7 +370,7 @@ let validErrorboundCorrectAddition = prove (
(abs (nR1 - nF1) <= err1) /\
(abs (nR2 - nF2) <= err2) ==>
(abs (nR - nF) <= e)`,
SIMP_TAC[freeVars; MEM; MEM_APPEND]
SIMP_TAC[freeVars; MEM; MEM_APPEND]
THEN intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1hi e2lo e2hi P;
p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_mult err1_bounded err2_bounded"
THEN pose_proof ivbounds_approximatesPrecond_sound "env_approx_p"
......@@ -394,16 +399,13 @@ let validErrorboundCorrectAddition = prove (
THEN EXISTS_TAC `(maxAbsFun ((e1lo:real),(e1hi:real)) * (err2:real) +
maxAbsFun ((e2lo:real),(e2hi:real)) * (err1:real) +
(err1:real) * (err2:real)) +
abs
((maxAbsFun ((e1lo:real),(e1hi:real)) + (err1:real)) *
(maxAbsFun ((e2lo:real),(e2hi:real)) + (err2:real))) *
maxAbsFun (multInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2)) *
machineEpsilon`
THEN pose_proof validIntervalbounds_sound "validbounds_e1" [`e1:(real)exp`; `absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `nR1:real`] ["p_valid"; "valid_e1"; "e1_real"]
THEN pose_proof validIntervalbounds_sound "validbounds_e2" [`e2:(real)exp`; `absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `nR2:real`] ["p_valid"; "valid_e2"; "e2_real"]
THEN split
THENL [
clear ["valid_error"]
THEN pose_proof validIntervalbounds_sound "validbounds_e1" [`e1:(real)exp`; `absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `nR1:real`] ["p_valid"; "valid_e1"; "e1_real"]
THEN pose_proof validIntervalbounds_sound "validbounds_e2" [`e2:(real)exp`; `absenv:analysisResult`; `P:precond`; `cenv:env_ty`; `nR2:real`] ["p_valid"; "valid_e2"; "e2_real"]
THEN mp REAL_LE_ADD2
mp REAL_LE_ADD2
THEN split
THENL[
rewrite_asm "absenv_e1" "validbounds_e1"
......@@ -449,8 +451,8 @@ let validErrorboundCorrectAddition = prove (
`maxAbsFun (e1lo:real, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1 <= maxAbsFun (e1lo:real, e1hi) * err2 + maxAbsFun (e2lo, e2hi) * err1 + (err1 * err2)`
[ASM_REAL_ARITH_TAC]
(* Large case distinction for
a) different cases of the value of Rabs (...) and
b) wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *)
a. different cases of the value of Rabs (...) and
b. wether arguments of multiplication in (nf1 * nF2) are < or >= 0 *)
THEN rewrite REAL_ABS_CASES "err1_bounded"
THEN destruct "err1_bounded" "nR1_nF1_geq_0 nR1_nF1_le_err1 | nR1_nF1_lt_0 inv_nR1_nF1_le_err1"
THENL [
......@@ -1050,39 +1052,41 @@ let validErrorboundCorrectAddition = prove (
]
]
;
mp REAL_LE_RMUL THEN split
rewrite_asm "absenv_e1" "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN destruct "validbounds_e1" "valid_lo_e1 valid_hi_e1"
THEN pose_proof distance_gives_iv "errIve1"
[`nR1:real`;`nF1:real`;`err1:real`;`e1lo:real`;`e1hi:real`]
["valid_lo_e1"; "valid_hi_e1"; "err1_bounded"]
THEN rewrite_asm "absenv_e2" "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN destruct "validbounds_e2" "valid_lo_e2 valid_hi_e2"
THEN pose_proof distance_gives_iv "errIve2"
[`nR2:real`;`nF2:real`;`err2:real`;`e2lo:real`;`e2hi:real`]
["valid_lo_e2"; "valid_hi_e2"; "err2_bounded"]
THEN pose_proof interval_mult_valid "mult_valid"
[`(widenInterval (e1lo,e1hi) err1)`;`widenInterval (e2lo,e2hi) err2`] []
THEN spec "mult_valid" [`nF1:real`;`nF2:real`]
THEN mp_ispecl "mult_valid" ["errIve1"; "errIve2"]
THEN mp REAL_LE_RMUL
THEN split
THENL [
REWRITE_TAC [REAL_ABS_MUL]
THEN mp REAL_LE_MUL2
THEN (REPEAT split)
THENL[
SIMP_TAC[REAL_ABS_POS];
rewrite_asm "absenv_e1" "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN rewrite FST "validbounds_e1"
THEN mp (SPEC `nR1:real` Rabs_error_bounded_maxAbs)
THEN split
THEN ASM_SIMP_TAC[contained; IVlo; IVhi; FST; SND];
SIMP_TAC[REAL_ABS_POS];
rewrite_asm "absenv_e2" "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN rewrite FST "validbounds_e2"
THEN mp (SPEC `nR2:real` Rabs_error_bounded_maxAbs)
THEN split
THEN ASM_SIMP_TAC[contained; IVlo; IVhi; FST; SND];
]
;
SUBGOAL_TAC "simp_iv" `?ivlo ivhi. multInterval (widenInterval (e1lo,e1hi) err1) (widenInterval (e2lo,e2hi) err2) = (ivlo, ivhi)` [MESON_TAC [cases "prod"]]
THEN destruct "simp_iv" "@ivlo. @ivhi. simp_iv"
THEN ASM_SIMP_TAC[]
THEN rewrite_asm "simp_iv" "mult_valid"
THEN mp contained_leq_maxAbs THEN auto;
SIMP_TAC[mEps_geq_zero]
]
];
SUBGOAL_TAC "mult_neq_plus" `Mult = Plus \/ Mult = Sub <=> F` [MESON_TAC[distinctness "binop"]]
THEN rewrite_asm "mult_neq_plus" "valid_error"
THEN REMOVE_THEN "valid_error" (fun th -> LABEL_TAC "valid_error" (CONV_RULE COND_ELIM_CONV th))
THEN destruct "valid_error" "asm1 asm2"
THEN mp_asm "asm2"
REMOVE_THEN "valid_error"
(fun th -> LABEL_TAC "valid_error" (SIMP_RULE[distinctness "binop"] (CONV_RULE COND_ELIM_CONV th)))
THEN auto
]
]);;
]
);;
let validErrorbound_sound = prove (
`!(e:(real)exp) (cenv:env_ty) (absenv:analysisResult) (nR:real) (nF:real) (err:real) (P:precond) (elo:real) (ehi:real).
......
......@@ -455,3 +455,17 @@ let Rabs_error_bounded_maxAbs = prove (
THEN TRY auto
THEN SIMP_TAC[REAL_ABS_LE]
);;
let distance_gives_iv = prove (
`!(a:real) (b:real) (e:real) (ivlo:real) (ivhi:real).
ivlo <= a /\ a <= ivhi /\
abs (a - b) <= e ==>
contained b (widenInterval (ivlo,ivhi) e)`,
SIMP_TAC[contained]
THEN intros "!a b e ivlo ivhi; lo_le_a a_le_hi abs_le"
THEN rewrite REAL_ABS_SUB "abs_le"
THEN SUBGOAL_TAC "abs_le_between" `(b:real) - e <= a /\ a <= b + e` [ASM_REAL_ARITH_TAC]
THEN destruct "abs_le_between" "lowerbound upperbound"
THEN split
THEN SIMP_TAC[IVhi; IVlo; mkInterval; widenInterval]
THEN TRY ASM_REAL_ARITH_TAC);;
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