Commit 000ccc7c authored by Heiko Becker's avatar Heiko Becker
Browse files

Finish IntervalArithmetic and start proving Errorbounds

parent 354c9cfb
needs "Infra/Abbrevs.hl";;
needs "Expressions.hl";;
let const_abs_err_bounded =
prove (
`!(n:real) (nR:real) (nF:real) (cenv:num->real).
eval_exp (&0) cenv (Const n) nR /\
eval_exp machineEpsilon cenv (Const n) nF ==>
abs (nR - nF) <= abs (n * machineEpsilon)`,
intros "!n nR nF cenv; eval_real eval_float"
THEN (USE_THEN "eval_real"
(fun th -> LABEL_TAC "eval_const_simps"
(MP (SPECL [`&0:real`;`cenv:num->real`; `n:real`; `nR:real`]const_inv) th)))
THEN destruct "eval_const_simps" "@delta. nR_perturb abs_leq_0"
THEN ASM_SIMP_TAC[]
THEN (USE_THEN "abs_leq_0"
(fun th -> REWRITE_TAC [MP (SPECL [`n:real`; `delta:real`] perturb_0_val) th]))
THEN (USE_THEN "eval_float"
(fun th -> LABEL_TAC "eval_const_float"
(MP (SPECL [`machineEpsilon:real`;`cenv:num->real`; `n:real`; `nF:real`]const_inv) th)))
THEN destruct "eval_const_float" "@delta2. nF_eq abs_leq_meps"
THEN ASM_SIMP_TAC[perturb]
THEN REWRITE_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
THEN mp REAL_LE_LMUL THEN split THEN TRY auto
THEN SIMP_TAC [REAL_ABS_POS]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `machineEpsilon:real` THEN split THEN TRY auto
THEN SIMP_TAC[REAL_ABS_LE]);;
let param_abs_err_bounded =
prove (
`!(v:num) (nR:real) (nF:real) (cenv:num->real).
eval_exp (&0) cenv (Param v) nR /\
eval_exp machineEpsilon cenv (Param v) nF ==>
abs (nR - nF) <= abs ((cenv v) * machineEpsilon)`,
intros "!v nR nF cenv; eval_real eval_float"
THEN (USE_THEN "eval_real"
(fun th -> LABEL_TAC "eval_const_simps"
(MP (SPECL [`&0:real`;`cenv:num->real`; `v:num`; `nR:real`] param_inv) th)))
THEN destruct "eval_const_simps" "@delta. nR_perturb abs_leq_0"
THEN ASM_SIMP_TAC[]
THEN (USE_THEN "abs_leq_0"
(fun th -> REWRITE_TAC [MP (SPECL [`n:real`; `delta:real`] perturb_0_val) th]))
THEN (USE_THEN "eval_float"
(fun th -> LABEL_TAC "eval_const_float"
(MP (SPECL [`machineEpsilon:real`;`cenv:num->real`; `v:num`; `nF:real`] param_inv) th)))
THEN destruct "eval_const_float" "@delta2. nF_eq abs_leq_meps"
THEN ASM_SIMP_TAC[perturb]
THEN REWRITE_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
THEN mp REAL_LE_LMUL THEN split THEN TRY auto
THEN SIMP_TAC [REAL_ABS_POS]
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `machineEpsilon:real` THEN split THEN TRY auto
THEN SIMP_TAC[REAL_ABS_LE]);;
......@@ -14,3 +14,13 @@ let REAL_MUL_LE_COMPAT_NEG_L =
THEN ONCE_REWRITE_TAC [REAL_NEG_NEG]
THEN ASM_SIMP_TAC[];
ASM_SIMP_TAC[] ]);;
let REAL_ABS_ERR_SIMPL =
prove (
`!(a:real) (b:real).
abs (a - (a * (&1 + b))) = abs (a * b)`,
intros "!a b"
THEN REWRITE_TAC [REAL_ADD_LDISTRIB; REAL_MUL_RID; REAL_ADD_SUB2; REAL_ABS_NEG]
THEN auto);;
search [`abs (-- (a:real))`];;
......@@ -301,7 +301,6 @@ e (EXISTS_TAC `SND (I2:real#real) * a:real` THEN split THENL [ mp REAL_LE_RMUL T
let interval_mult_valid = top_thm();;
let intv_div_err = define
`intv_div_err (I1:interval) (e1:err) (I2:interval) (e2:err)=
intv_mult_err I1 e1 ((&1) / IVlo (I2), (&1) / IVhi (I2)) e2`;;
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