Commit 8da916d1 authored by Heiko Becker's avatar Heiko Becker
Browse files

Make all error bound theorems fit the needed style before proving multiplication

parent d102f0e3
......@@ -3,13 +3,16 @@ needs "IntervalValidation.hl";;
needs "ErrorBounds.hl";;
let validErrorbound = define
`(validErrorbound (Const n) (absenv:(real)exp->(real#real)#real) =
`(validErrorbound (Const n) (absenv:analysisResult) =
let (intv, err) = absenv (Const n) in
(maxAbsFun intv * machineEpsilon) <= err) /\
(validErrorbound (Param v) (absenv:(real)exp->(real#real)#real) =
((&0 <= err) /\
(maxAbsFun intv * machineEpsilon) <= err)) /\
(validErrorbound (Param v) (absenv:analysisResult) =
let (intv, err) = absenv (Param v) in
(maxAbsFun intv * machineEpsilon) <= err ) /\
(validErrorbound (Binop b e1 e2) (absenv:(real)exp->(real#real)#real) =
((&0 <= err) /\
(maxAbsFun intv * machineEpsilon) <= err )) /\
(validErrorbound (Var v) (absenv:analysisResult) = F) /\
(validErrorbound (Binop b e1 e2) (absenv:analysisResult) =
let (intv, err) = absenv (Binop b e1 e2) in
let (ive1, err1) = absenv e1 in
let (ive2, err2) = absenv e2 in
......@@ -17,12 +20,58 @@ let validErrorbound = define
let upperBoundE2 = maxAbsFun ive2 in
let e1F = upperBoundE1 + err1 in
let e2F = upperBoundE2 + err2 in
if (b = Plus \/ b = Sub)
then (err1 + err2 + (abs e1F + abs e2F) * machineEpsilon) <= err
else
if b = Mult
then (abs (upperBoundE1 * upperBoundE2 - (e1F * e2F)) + abs (e1F * e2F) * machineEpsilon) <= err
else F)`;;
((&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)))`;;
let err_always_positive = prove (
`!(e:(real)exp) (absenv:analysisResult) (iv:interval) (err:error).
validErrorbound e absenv = T /\
absenv e = (iv,err) ==>
&0 <= err`,
SIMP_TAC[] THEN intros "!e absenv iv err; validbound_e absenv_e"
(* FIXME: Why can't I use SPEC `e:(real)exp` (cases "exp") here? *)
THEN SUBGOAL_TAC "cases_e" `(?a:num. (e:(real)exp) = Var a) \/ (?a:num. e = Param a) \/ (?n:real. e = Const n) \/ (?(b:binop) (e1:(real)exp) (e2:(real)exp). e = Binop b e1 e2)` [MESON_TAC[cases "exp"]]
THEN destruct "cases_e" "e_var | e_param | e_const | e_binop"
THENL [
destruct "e_var" "@v. e_var"
THEN rewrite_asm "e_var" "validbound_e"
THEN rewrite validErrorbound "validbound_e"
THEN falsity "validbound_e";
destruct "e_param" "@v. e_param"
THEN rewrite_asm "e_param" "validbound_e"
THEN rewrite_asm "e_param" "absenv_e"
THEN rewrite validErrorbound "validbound_e"
THEN rewrite_asm "absenv_e" "validbound_e"
THEN simplify "validbound_e"
THEN destruct "validbound_e" "goal _"
THEN auto;
destruct "e_const" "@n. e_const"
THEN rewrite_asm "e_const" "validbound_e"
THEN rewrite_asm "e_const" "absenv_e"
THEN rewrite validErrorbound "validbound_e"
THEN rewrite_asm "absenv_e" "validbound_e"
THEN simplify "validbound_e"
THEN destruct "validbound_e" "goal _"
THEN auto;
destruct "e_binop" "@b. @e1. @e2. e_binop"
THEN rewrite_asm "e_binop" "validbound_e"
THEN rewrite_asm "e_binop" "absenv_e"
THEN rewrite validErrorbound "validbound_e"
THEN rewrite_asm "absenv_e" "validbound_e"
THEN SUBGOAL_TAC "absenv_e1_def" `?(iv1:interval) (err1:error). (absenv:analysisResult) e1 = (iv1,err1)` [MESON_TAC[cases "prod"]]
THEN destruct "absenv_e1_def" "@iv1. @err1. absenv_e1"
THEN rewrite_asm "absenv_e1" "validbound_e"
THEN SUBGOAL_TAC "absenv_e2_def" `?(iv2:interval) (err2:error). (absenv:analysisResult) e2 = (iv2,err2)` [MESON_TAC[cases "prod"]]
THEN destruct "absenv_e2_def" "@iv2. @err2. absenv_e2"
THEN rewrite_asm "absenv_e2" "validbound_e"
THEN simplify "validbound_e"
THEN destruct "validbound_e" "goal _"
THEN auto]);;
let validErrorboundCorrectConstant = prove (
`!(cenv:env_ty) (absenv:analysisResult) (n:real) (nR:real) (nF:real) (e:real) (nlo:real) (nhi:real) (P:precond).
......@@ -65,68 +114,73 @@ let validErrorboundCorrectConstant = prove (
];
auto]]);;
let validErrorboundCorrectParam =
prove (
`!(cenv:env_ty) (absenv:analysisResult) (v:num) (nR:real) (nF:real) (e:real) (P:precond) (plo:real) (phi:real).
envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
eval_exp (&0) cenv (Param v) nR /\
eval_exp machineEpsilon cenv (Param v) nF /\
validErrorbound (Param v) absenv /\
validIntervalbounds (Param v) absenv P /\
absenv (Param v) = ((plo,phi),e) ==>
(abs (nR - nF)) <= e`,
intros "!cenv absenv v nR nF e P plo phi; absenv_approx_p cenv_approx_p eval_real eval_float error_valid intv_valid absenv_param"
THEN rewrite validErrorbound "error_valid"
THEN pose_spec param_inv [`&0:real`; `cenv:env_ty`; `v:num`; `nR:real`] "eval_real" "eval_inv"
THEN destruct "eval_inv" "@d. perturb_nR abs_0"
THEN ASM_SIMP_TAC[perturb_0_val]
THEN pose_spec param_inv [`machineEpsilon:real`; `cenv:env_ty`; `v:num`; `nF:real`] "eval_float" "eval_inv"
THEN destruct "eval_inv" "@d2. perturb_nF abs_leq_meps"
THEN ASM_SIMP_TAC[perturb]
THEN SIMP_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
THEN rewrite envApproximatesPrecond "absenv_approx_p"
THEN rewrite envApproximatesPrecondFun "absenv_approx_p"
THEN rewrite precondValidForExec "cenv_approx_p"
THEN rewrite precondValidForExecFun "cenv_approx_p"
THEN specl "cenv_approx_p" [`v:num`]
THEN specl "absenv_approx_p" [`v:num`]
THEN SUBGOAL_TAC "p_v_def" `?ivlo ivhi. (P:precond) (v:num) = (ivlo,ivhi)` [MESON_TAC [cases "prod"]]
THEN destruct "p_v_def" "@ivlo. @ivhi. p_v_def"
THEN rewrite_asm "p_v_def" "absenv_approx_p"
THEN rewrite_asm "absenv_param" "absenv_approx_p"
THEN rewrite_asm "p_v_def" "cenv_approx_p"
THEN simplify "cenv_approx_p"
THEN REPEAT (simplify "absenv_approx_p")
THEN rewrite_asm "absenv_param" "error_valid"
THEN simplify "error_valid"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `maxAbsFun (plo,phi) * machineEpsilon`
THEN split
THENL [
mp REAL_LE_MUL2 THEN split
THENL [
SIMP_TAC[REAL_ABS_POS];
let validErrorboundCorrectParam = prove (
`!(cenv:env_ty) (absenv:analysisResult) (v:num) (nR:real) (nF:real) (e:real) (P:precond) (plo:real) (phi:real).
(!(n:num). MEM n ((freeVars:(real)exp->(num)list) (Param v)) ==>
isSupersetInterval (P v) (FST (absenv (Param n)))) /\
precondValidForExec P cenv /\
eval_exp (&0) cenv (Param v) nR /\
eval_exp machineEpsilon cenv (Param v) nF /\
validErrorbound (Param v) absenv /\
validIntervalbounds (Param v) absenv P /\
absenv (Param v) = ((plo,phi),e) ==>
(abs (nR - nF)) <= e`,
intros "!cenv absenv v nR nF e P plo phi; absenv_approx_p cenv_approx_p eval_real eval_float error_valid intv_valid absenv_param"
THEN rewrite validErrorbound "error_valid"
THEN pose_spec param_inv [`&0:real`; `cenv:env_ty`; `v:num`; `nR:real`] "eval_real" "eval_inv"
THEN destruct "eval_inv" "@d. perturb_nR abs_0"
THEN ASM_SIMP_TAC[perturb_0_val]
THEN pose_spec param_inv [`machineEpsilon:real`; `cenv:env_ty`; `v:num`; `nF:real`] "eval_float" "eval_inv"
THEN destruct "eval_inv" "@d2. perturb_nF abs_leq_meps"
THEN ASM_SIMP_TAC[perturb]
THEN SIMP_TAC[REAL_ABS_ERR_SIMPL; REAL_ABS_MUL]
THEN rewrite precondValidForExec "cenv_approx_p"
THEN rewrite precondValidForExecFun "cenv_approx_p"
THEN lspecialize "cenv_approx_p" [`v:num`]
THEN lspecialize "absenv_approx_p" [`v:num`]
THEN SUBGOAL_TAC "p_v_def" `?ivlo ivhi. (P:precond) (v:num) = (ivlo,ivhi)` [MESON_TAC [cases "prod"]]
THEN destruct "p_v_def" "@ivlo. @ivhi. p_v_def"
THEN rewrite isSupersetInterval "absenv_approx_p"
THEN rewrite_asm "p_v_def" "absenv_approx_p"
THEN rewrite_asm "absenv_param" "absenv_approx_p"
THEN rewrite_asm "p_v_def" "cenv_approx_p"
THEN simplify "cenv_approx_p"
THEN SUBGOAL_TAC "v_in_fVs" `MEM (v:num) ((freeVars:(real)exp->(num)list) (Param v))` [SIMP_TAC[freeVars; MEM]]
THEN mp_spec "absenv_approx_p" "v_in_fVs"
THEN rewrite IVlo "absenv_approx_p"
THEN rewrite IVhi "absenv_approx_p"
THEN rewrite FST "absenv_approx_p"
THEN rewrite SND "absenv_approx_p"
THEN destruct "absenv_approx_p" "approx_lo approx_hi"
THEN rewrite_asm "absenv_param" "error_valid"
THEN simplify "error_valid"
THEN mp REAL_LE_TRANS
THEN EXISTS_TAC `maxAbsFun (plo,phi) * machineEpsilon`
THEN split
THENL [
mp REAL_LE_MUL2 THEN split
THENL [
SIMP_TAC[REAL_ABS_POS];
split THENL [
SIMP_TAC[maxAbsFun] THEN mp iv_le_maxAbs THEN split THEN mp REAL_LE_TRANS
THENL [
EXISTS_TAC `ivlo:real` THEN split THEN auto;
EXISTS_TAC `ivhi:real` THEN split THEN auto
];
split THENL [
SIMP_TAC[maxAbsFun] THEN mp iv_le_maxAbs THEN split THEN mp REAL_LE_TRANS
THENL [
EXISTS_TAC `ivlo:real` THEN split THEN auto;
EXISTS_TAC `ivhi:real` THEN split THEN auto
];
split THENL [
SIMP_TAC[REAL_ABS_POS];
auto
]
SIMP_TAC[REAL_ABS_POS];
auto
]
];
auto]
);;
]
];
auto]
);;
let validErrorboundCorrectAddition = 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).
envApproximatesPrecond P absenv /\
(!(n:num). MEM n ((freeVars:(real)exp->(num)list) (Binop Plus e1 e2)) ==>
isSupersetInterval (P n) (FST (absenv (Param n)))) /\
precondValidForExec P cenv /\
eval_exp (&0) cenv e1 nR1 /\
eval_exp (&0) cenv e2 nR2 /\
......@@ -142,7 +196,8 @@ let validErrorboundCorrectAddition = prove (
(abs (nR1 - nF1) <= err1) /\
(abs (nR2 - nF2) <= err2) ==>
(abs (nR - nF) <= e)`,
intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1hi e2lo e2hi P;
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;
env_approx_p p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_add err1_bounded err2_bounded"
THEN pose add_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`] "add_bounded"
THEN mp REAL_LE_TRANS
......@@ -158,7 +213,7 @@ let validErrorboundCorrectAddition = prove (
THEN rewrite_asm "absenv_e2" "valid_error"
THEN rewrite validIntervalbounds "valid_intv"
THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
THEN REPEAT (simplify "valid_error")
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 split
......@@ -174,35 +229,26 @@ let validErrorboundCorrectAddition = prove (
THENL [
SIMP_TAC[REAL_ABS_TRIANGLE];
mp REAL_LE_ADD2
THEN SUBGOAL_TAC "fv_e1_superset" `!var. MEM (var:num) ((freeVars:(real)exp->(num)list) (e1:(real)exp)) ==> isSupersetInterval (P var) (FST ((absenv:analysisResult) (Param var)))`
[intros "!var; MEM_var" THEN specialize "env_approx_p" `var:num` THEN ASM_SIMP_TAC[]]
THEN SUBGOAL_TAC "fv_e2_superset" `!var. MEM (var:num) ((freeVars:(real)exp->(num)list) (e2:(real)exp)) ==> isSupersetInterval (P var) (FST ((absenv:analysisResult) (Param var)))`
[intros "!var; MEM_var" THEN specialize "env_approx_p" `var:num` THEN ASM_SIMP_TAC[]]
THEN split
THENL [
pose validIntervalbounds_correct
[`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
"valid_bounds_e1"
THEN SUBGOAL_TAC "e1_bound_prems"
`envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
(validIntervalbounds e1 absenv P <=> T) /\
eval_exp (&0) cenv e1 nR1`
[auto]
THEN mp_spec "valid_bounds_e1" "e1_bound_prems"
THEN mp_ispecl "valid_bounds_e1" ["fv_e1_superset"; "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
;
THEN split THEN auto;
pose validIntervalbounds_correct
[`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
"valid_bounds_e2"
THEN SUBGOAL_TAC "e2_bound_prems"
`envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
(validIntervalbounds e2 absenv P <=> T) /\
eval_exp (&0) cenv e2 nR2`
[auto]
THEN mp_spec "valid_bounds_e2" "e2_bound_prems"
THEN mp_ispecl "valid_bounds_e2" ["fv_e2_superset"; "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"
......@@ -213,14 +259,14 @@ let validErrorboundCorrectAddition = prove (
];
SIMP_TAC[mEps_geq_zero]
];
auto
]
]);;
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).
envApproximatesPrecond P absenv /\
(!(n:num). MEM n (freeVars (Binop Sub e1 e2)) ==>
isSupersetInterval (P n) (FST (absenv (Param n)))) /\
precondValidForExec P cenv /\
eval_exp (&0) cenv e1 nR1 /\
eval_exp (&0) cenv e2 nR2 /\
......@@ -236,7 +282,8 @@ let validErrorboundCorrectAddition = prove (
(abs (nR1 - nF1) <= err1) /\
(abs (nR2 - nF2) <= err2) ==>
(abs (nR - nF) <= e)`,
intros "!cenv absenv e1 e2 nR nR1 nR2 nF nF1 nF2 e err1 err2 alo ahi e1lo e1hi e2lo e2hi P;
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;
env_approx_p p_valid e1_real e2_real eval_real e1_float e2_float eval_float valid_error valid_intv absenv_e1 absenv_e2 absenv_sub err1_bounded err2_bounded"
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
......@@ -252,7 +299,7 @@ let validErrorboundCorrectAddition = prove (
THEN rewrite_asm "absenv_e2" "valid_error"
THEN rewrite validIntervalbounds "valid_intv"
THEN destruct "valid_intv" "valid_e1 valid_e2 valid_bin"
THEN REPEAT (simplify "valid_error")
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 split
......@@ -268,18 +315,16 @@ let validErrorboundCorrectAddition = prove (
THENL [
SIMP_TAC[REAL_LE_REFL];
mp REAL_LE_ADD2
THEN SUBGOAL_TAC "fv_e1_superset" `!var. MEM (var:num) ((freeVars:(real)exp->(num)list) (e1:(real)exp)) ==> isSupersetInterval (P var) (FST ((absenv:analysisResult) (Param var)))`
[intros "!var; MEM_var" THEN specialize "env_approx_p" `var:num` THEN ASM_SIMP_TAC[]]
THEN SUBGOAL_TAC "fv_e2_superset" `!var. MEM (var:num) ((freeVars:(real)exp->(num)list) (e2:(real)exp)) ==> isSupersetInterval (P var) (FST ((absenv:analysisResult) (Param var)))`
[intros "!var; MEM_var" THEN specialize "env_approx_p" `var:num` THEN ASM_SIMP_TAC[]]
THEN split
THENL [
pose validIntervalbounds_correct
[`e1:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR1:real`]
"valid_bounds_e1"
THEN SUBGOAL_TAC "e1_bound_prems"
`envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
(validIntervalbounds e1 absenv P <=> T) /\
eval_exp (&0) cenv e1 nR1`
[auto]
THEN mp_spec "valid_bounds_e1" "e1_bound_prems"
THEN mp_ispecl "valid_bounds_e1" ["fv_e1_superset"; "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"
......@@ -290,13 +335,7 @@ let validErrorboundCorrectAddition = prove (
pose validIntervalbounds_correct
[`e2:(real)exp`;`absenv:analysisResult`;`P:precond`;`cenv:env_ty`;`nR2:real`]
"valid_bounds_e2"
THEN SUBGOAL_TAC "e2_bound_prems"
`envApproximatesPrecond P absenv /\
precondValidForExec P cenv /\
(validIntervalbounds e2 absenv P <=> T) /\
eval_exp (&0) cenv e2 nR2`
[auto]
THEN mp_spec "valid_bounds_e2" "e2_bound_prems"
THEN mp_ispecl "valid_bounds_e2" ["fv_e2_superset"; "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"
......@@ -310,4 +349,6 @@ let validErrorboundCorrectAddition = prove (
auto
]
]);;
let math_hnf_thms = [real_sub; REAL_NEG_ADD; REAL_MUL_RNEG; REAL_MUL_LNEG; REAL_NEG_NEG; GSYM REAL_ADD_ASSOC];;
search [ `(a:real) <= a`];;
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