Commit 0a383995 authored by Heiko Becker's avatar Heiko Becker
Browse files

Port environment simulation relation and abstract bounds

parent d47a36de
open preamble
open simpLib realTheory realLib RealArith
open AbbrevsTheory ExpressionAbbrevsTheory CommandsTheory
open simpLib realTheory realLib RealArith sptreeTheory
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory
val _ = new_theory "Environments";
val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(!(E:env) (A:analysisResult). approxEnv E A E) /\
(!(E1:env) (E2:env) (A:analysisResult) v1 v2 x.
approxEnv E1 A E2 /\
(abs (v1 - v2) <= SND (A (Var x))) ==>
approxEnv (updEnv x v1 E1) A (updEnv x v2 E2))`;
(!(A:analysisResult).
approxEnv emptyEnv A LN LN emptyEnv) /\
(!(E1:env) (E2:env) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 A fVars dVars E2 /\
(abs (v1 - v2) <= abs v1 * machineEpsilon) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) A (Insert x fVars) dVars (updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 A fVars dVars E2 /\
(abs (v1 - v2) <= SND (A (Var x))) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) A fVars (Insert x dVars) (updEnv x v2 E2))`;
val _ = export_theory ();;
......@@ -5,190 +5,193 @@ Bounds are explained in section 5, Deriving Computable Error Bounds
**)
open preamble
open simpLib realTheory realLib RealArith
open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
open ExpressionAbbrevsTheory EnvironmentsTheory
val _ = new_theory "ErrorBounds";
val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
``!(P:precond) (n:real) (nR:real) (nF:real) (VarEnv1 VarEnv2 ParamEnv:env).
eval_exp 0 VarEnv1 ParamEnv P (Const n) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Const n) nF ==>
``!(n:real) (nR:real) (nF:real) (E1 E2:env).
eval_exp 0 E1 (Const n) nR /\
eval_exp machineEpsilon E2 (Const n) nF ==>
abs (nR - nF) <= abs n * machineEpsilon``,
rpt strip_tac \\
fs[eval_exp_cases] \\
`perturb n delta = n` by metis_tac[delta_0_deterministic] \\
`nR = n` by fs[]\\
simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL] \\
match_mp_tac REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC);
rpt strip_tac
\\ fs[eval_exp_cases]
\\ `perturb n delta = n` by metis_tac[delta_0_deterministic]
\\ `nR = n` by fs[]
\\ simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC);
(*
val param_abs_err_bounded = store_thm ("param_abs_err_bounded",
``!(P:precond) (n:num) (nR:real) (nF:real) (VarEnv1 VarEnv2 ParamEnv:env).
eval_exp 0 VarEnv1 ParamEnv P (Param n) nR /\
eval_exp machineEpsilon VarEnv2 ParamEnv P (Param n) nF ==>
abs (nR - nF) <= abs (ParamEnv n) * machineEpsilon``,
``!(P:precond) (n:num) (nR:real) (nF:real) (VarEnv1 VarEnv2 :env).
eval_exp 0 VarEnv1 P (Param n) nR /\
eval_exp machineEpsilon VarEnv2 P (Param n) nF ==>
abs (nR - nF) <= abs ( n) * machineEpsilon``,
rpt strip_tac \\
fs[eval_exp_cases] \\
`perturb (ParamEnv n) delta = (ParamEnv n)` by metis_tac[delta_0_deterministic] \\
`nR = (ParamEnv n)` by fs[]\\
`perturb ( n) delta = ( n)` by metis_tac[delta_0_deterministic] \\
`nR = ( n)` by fs[]\\
simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL] \\
match_mp_tac REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC);
*)
val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond).
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 e2F /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Plus e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Plus (Var 1) (Var 2)) vF /\
(vR:real) (vF:real) (E1 E2:env).
eval_exp 0 E1 e1 e1R /\
eval_exp machineEpsilon E2 e1 e1F /\
eval_exp 0 E1 e2 e2R /\
eval_exp machineEpsilon E2 e2 e2F /\
eval_exp 0 E1 (Binop Plus e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Plus (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= err1 + err2 + (abs (e1F + e2F) * machineEpsilon)``,
rpt strip_tac \\
inversion `eval_exp 0 VarEnv1 ParamEnv P (Binop Plus e1 e2) vR` eval_exp_cases \\
rename1 `vR = perturb (evalBinop Plus v1R v2R) deltaR` \\
inversion `eval_exp machineEpsilon _ _ P (Binop Plus (Var 1) (Var 2)) vF` eval_exp_cases \\
rename1 `vF = perturb (evalBinop Plus v1F v2F) deltaF` \\
`perturb (evalBinop Plus v1R v2R) deltaR = evalBinop Plus v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[]) \\
`vR = evalBinop Plus v1R v2R` by simp[] \\
`v1R = e1R` by metis_tac[meps_0_deterministic] \\
`v2R = e2R` by metis_tac[meps_0_deterministic] \\
fs[evalBinop_def, perturb_def] \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) _ P expr vE` eval_exp_cases) \\
fs [updEnv_def]\\
once_rewrite_tac[real_sub] \\
`e1R + e2R + -((e1F + e2F) * (1 + deltaF)) = (e1R + - e1F) + ((e2R + - e2F) + - (e1F + e2F) * deltaF)` by REAL_ASM_ARITH_TAC \\
simp [] \\
rpt strip_tac
\\ inversion `eval_exp 0 E1 (Binop Plus e1 e2) vR` eval_exp_cases
\\ rename1 `vR = perturb (evalBinop Plus v1R v2R) deltaR`
\\ inversion `eval_exp machineEpsilon _ (Binop Plus (Var 1) (Var 2)) vF` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Plus v1F v2F) deltaF`
\\ `perturb (evalBinop Plus v1R v2R) deltaR = evalBinop Plus v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[])
\\ `vR = evalBinop Plus v1R v2R` by simp[]
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ rveq \\ fs[evalBinop_def, perturb_def]
\\ rpt (inversion `eval_exp machineEpsilon (updEnv n e E) expr vE` eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ once_rewrite_tac[real_sub]
\\ `e1R + e2R + -((e1F + e2F) * (1 + deltaF)) = (e1R + - e1F) + ((e2R + - e2F) + - (e1F + e2F) * deltaF)` by REAL_ASM_ARITH_TAC
\\ simp []
(** Currently the best way I could find to get around skolem variables, as used in Coq **)
qspecl_then [`abs (e1R + - e1F) + abs ((e2R + - e2F) + - (e1F + e2F) * deltaF)`] match_mp_tac real_le_trans2 \\
fs [REAL_ABS_TRIANGLE] \\
once_rewrite_tac [GSYM REAL_ADD_ASSOC] \\
match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub] \\
once_rewrite_tac [REAL_ADD_ASSOC] \\
qspecl_then [`abs (e2R + - e2F) + abs (-(e1F + e2F) * deltaF)`] match_mp_tac real_le_trans2 \\
fs [REAL_ABS_TRIANGLE] \\
match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub] \\
once_rewrite_tac [REAL_ABS_MUL] \\
match_mp_tac REAL_LE_MUL2 \\
fs [REAL_ABS_POS, ABS_NEG]);
\\ qspecl_then [`abs (e1R + - e1F) + abs ((e2R + - e2F) + - (e1F + e2F) * deltaF)`] match_mp_tac real_le_trans2
\\ fs [REAL_ABS_TRIANGLE]
\\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
\\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub]
\\ once_rewrite_tac [REAL_ADD_ASSOC]
\\ qspecl_then [`abs (e2R + - e2F) + abs (-(e1F + e2F) * deltaF)`] match_mp_tac real_le_trans2
\\ fs [REAL_ABS_TRIANGLE]
\\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub]
\\ once_rewrite_tac [REAL_ABS_MUL]
\\ match_mp_tac REAL_LE_MUL2
\\ fs [REAL_ABS_POS, ABS_NEG]);
val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) (absenv:analysisResult).
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 e2F /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Sub e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Sub (Var 1) (Var 2)) vF /\
(vR:real) (vF:real) (E1 E2:env) (absenv:analysisResult).
eval_exp 0 E1 e1 e1R /\
eval_exp machineEpsilon E2 e1 e1F /\
eval_exp 0 E1 e2 e2R /\
eval_exp machineEpsilon E2 e2 e2F /\
eval_exp 0 E1 (Binop Sub e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Sub (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= err1 + err2 + (abs (e1F - e2F) * machineEpsilon)``,
rpt strip_tac \\
inversion `eval_exp 0 _ _ P (Binop Subs e1 e2) vR` eval_exp_cases \\
rename1 `vR = perturb (evalBinop Sub v1R v2R) deltaR` \\
inversion `eval_exp machineEpsilon _ _ P (Binop Sub (Var 1) (Var 2)) vF` eval_exp_cases \\
rename1 `vF = perturb (evalBinop Sub v1F v2F) deltaF` \\
`perturb (evalBinop Sub v1R v2R) deltaR = evalBinop Sub v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[]) \\
`vR = evalBinop Sub v1R v2R` by simp[] \\
`v1R = e1R` by metis_tac[meps_0_deterministic] \\
`v2R = e2R` by metis_tac[meps_0_deterministic] \\
fs[evalBinop_def, perturb_def] \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) _ P expr vE` eval_exp_cases) \\
fs [updEnv_def]\\
rewrite_tac[real_sub] \\
`e1R + -e2R + -((e1F + -e2F) * (1 + deltaF)) = (e1R + - e1F) + ((- e2R + e2F) + - (e1F + - e2F) * deltaF)` by REAL_ASM_ARITH_TAC \\
simp [] \\
rpt strip_tac
\\ inversion `eval_exp 0 _ (Binop Subs e1 e2) vR` eval_exp_cases
\\ rename1 `vR = perturb (evalBinop Sub v1R v2R) deltaR`
\\ inversion `eval_exp machineEpsilon _ (Binop Sub (Var 1) (Var 2)) vF` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Sub v1F v2F) deltaF`
\\ `perturb (evalBinop Sub v1R v2R) deltaR = evalBinop Sub v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[])
\\ `vR = evalBinop Sub v1R v2R` by simp[]
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ fs[evalBinop_def, perturb_def]
\\ rpt (inversion `eval_exp machineEpsilon (updEnv n e E) expr vE` eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ rewrite_tac[real_sub]
\\ `e1R + -e2R + -((e1F + -e2F) * (1 + deltaF)) = (e1R + - e1F) + ((- e2R + e2F) + - (e1F + - e2F) * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp []
(** Currently the best way I could find to get around skolem variables, as used in Coq **)
qspecl_then [`abs (e1R + - e1F) + abs ((- e2R + e2F) + - (e1F + - e2F) * deltaF)`] match_mp_tac real_le_trans2 \\
fs [REAL_ABS_TRIANGLE] \\
once_rewrite_tac [GSYM REAL_ADD_ASSOC] \\
match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub] \\
once_rewrite_tac [REAL_ADD_ASSOC] \\
qspecl_then [`abs (- e2R + e2F) + abs (-(e1F - e2F) * deltaF)`] match_mp_tac real_le_trans2 \\
fs [REAL_ABS_TRIANGLE] \\
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (`-e2R + e2F = e2F - e2R` by REAL_ASM_ARITH_TAC \\ simp[] \\
once_rewrite_tac [ABS_SUB] \\ fs[])
>- (once_rewrite_tac [REAL_ABS_MUL] \\
match_mp_tac REAL_LE_MUL2 \\
fs [REAL_ABS_POS, ABS_NEG]));
\\ qspecl_then [`abs (e1R + - e1F) + abs ((- e2R + e2F) + - (e1F + - e2F) * deltaF)`] match_mp_tac real_le_trans2
\\ fs [REAL_ABS_TRIANGLE]
\\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
\\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub]
\\ once_rewrite_tac [REAL_ADD_ASSOC]
\\ qspecl_then [`abs (- e2R + e2F) + abs (-(e1F - e2F) * deltaF)`] match_mp_tac real_le_trans2
\\ fs [REAL_ABS_TRIANGLE]
\\ match_mp_tac REAL_LE_ADD2
\\ conj_tac
>- (`-e2R + e2F = e2F - e2R` by REAL_ASM_ARITH_TAC \\ simp[]
\\ once_rewrite_tac [ABS_SUB] \\ fs[])
>- (once_rewrite_tac [REAL_ABS_MUL]
\\ match_mp_tac REAL_LE_MUL2
\\ fs [REAL_ABS_POS, ABS_NEG]));
val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond).
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 e2F /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Mult e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Mult (Var 1) (Var 2)) vF /\
(vR:real) (vF:real) (E1 E2 :env) (absenv:analysisResult).
eval_exp 0 E1 e1 e1R /\
eval_exp machineEpsilon E2 e1 e1F /\
eval_exp 0 E1 e2 e2R /\
eval_exp machineEpsilon E2 e2 e2F /\
eval_exp 0 E1 (Binop Mult e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Mult (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + (abs (e1F * e2F) * machineEpsilon)``,
rpt strip_tac \\
inversion `eval_exp 0 _ _ P (Binop Mult e1 e2) vR` eval_exp_cases \\
rename1 `vR = perturb (evalBinop Mult v1R v2R) deltaR`\\
inversion `eval_exp machineEpsilon _ _ P (Binop Mult (Var 1) (Var 2)) v` eval_exp_cases \\
rename1 `vF = perturb (evalBinop Mult v1F v2F) deltaF` \\
`perturb (evalBinop Mult v1R v2R) deltaR = evalBinop Mult v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[]) \\
`vR = evalBinop Mult v1R v2R` by simp[] \\
`v1R = e1R` by metis_tac[meps_0_deterministic] \\
`v2R = e2R` by metis_tac[meps_0_deterministic] \\
fs[evalBinop_def, perturb_def] \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) _ P expr vE` eval_exp_cases) \\
fs [updEnv_def] \\
rewrite_tac [real_sub] \\
`e1R * e2R + -(e1F * e2F * (1 + deltaF)) = (e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)` by REAL_ASM_ARITH_TAC \\
simp[] \\
qspecl_then [`abs (e1R * e2R + -(e1F * e2F)) + abs (- e1F * e2F * deltaF)`] match_mp_tac real_le_trans2 \\
conj_tac
rpt strip_tac
\\ inversion `eval_exp 0 _ (Binop Mult e1 e2) vR` eval_exp_cases
\\ rename1 `vR = perturb (evalBinop Mult v1R v2R) deltaR`
\\ inversion `eval_exp machineEpsilon _ (Binop Mult (Var 1) (Var 2)) v` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Mult v1F v2F) deltaF`
\\ `perturb (evalBinop Mult v1R v2R) deltaR = evalBinop Mult v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[])
\\ `vR = evalBinop Mult v1R v2R` by simp[]
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ fs[evalBinop_def, perturb_def]
\\ rpt (inversion `eval_exp machineEpsilon (updEnv n e E) expr vE` eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ rewrite_tac [real_sub]
\\ `e1R * e2R + -(e1F * e2F * (1 + deltaF)) = (e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)` by REAL_ASM_ARITH_TAC
\\ simp[]
\\ qspecl_then [`abs (e1R * e2R + -(e1F * e2F)) + abs (- e1F * e2F * deltaF)`] match_mp_tac real_le_trans2
\\ conj_tac
>- (REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_ADD2 \\
conj_tac \\ TRY (REAL_ASM_ARITH_TAC) \\
once_rewrite_tac[REAL_ABS_MUL] \\
match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS] \\
once_rewrite_tac[GSYM REAL_NEG_LMUL, REAL_ABS_MUL] \\
once_rewrite_tac[ABS_NEG] \\ fs[]));
>- (match_mp_tac REAL_LE_ADD2
\\ conj_tac \\ TRY (REAL_ASM_ARITH_TAC)
\\ once_rewrite_tac[REAL_ABS_MUL]
\\ match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS]
\\ once_rewrite_tac[GSYM REAL_NEG_LMUL, REAL_ABS_MUL]
\\ once_rewrite_tac[ABS_NEG] \\ fs[]));
val div_abs_err_bounded = store_thm ("div_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
(vR:real) (vF:real) (VarEnv1 VarEnv2 ParamEnv:env) (P:precond) (absenv:analysisResult).
eval_exp 0 VarEnv1 ParamEnv P e1 e1R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e1 e1F /\
eval_exp 0 VarEnv1 ParamEnv P e2 e2R /\
eval_exp machineEpsilon VarEnv2 ParamEnv P e2 e2F /\
eval_exp 0 VarEnv1 ParamEnv P (Binop Div e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F VarEnv2)) ParamEnv P (Binop Div (Var 1) (Var 2)) vF /\
(vR:real) (vF:real) (E1 E2 :env) (absenv:analysisResult).
eval_exp 0 E1 e1 e1R /\
eval_exp machineEpsilon E2 e1 e1F /\
eval_exp 0 E1 e2 e2R /\
eval_exp machineEpsilon E2 e2 e2F /\
eval_exp 0 E1 (Binop Div e1 e2) vR /\
eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F emptyEnv))(Binop Div (Var 1) (Var 2)) vF /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= abs (e1R / e2R - e1F / e2F) + (abs (e1F / e2F) * machineEpsilon)``,
rpt strip_tac \\
inversion `eval_exp 0 _ _ P (Binop Div e1 e2) vR` eval_exp_cases \\
rename1 `vR = perturb (evalBinop Div v1R v2R) deltaR`\\
inversion `eval_exp machineEpsilon _ _ P (Binop Div (Var 1) (Var 2)) v` eval_exp_cases \\
rename1 `vF = perturb (evalBinop Div v1F v2F) deltaF` \\
`perturb (evalBinop Div v1R v2R) deltaR = evalBinop Div v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[]) \\
`vR = evalBinop Div v1R v2R` by simp[] \\
`v1R = e1R` by metis_tac[meps_0_deterministic] \\
`v2R = e2R` by metis_tac[meps_0_deterministic] \\
fs[evalBinop_def, perturb_def] \\
rpt (inversion `eval_exp machineEpsilon (updEnv n e E) _ P expr vE` eval_exp_cases) \\
fs [updEnv_def] \\
rewrite_tac [real_sub] \\
`e1R / e2R + -(e1F / e2F * (1 + deltaF)) = (e1R / e2R + - (e1F / e2F)) + - (e1F / e2F * deltaF)` by REAL_ASM_ARITH_TAC \\
simp[] \\
qspecl_then [`abs (e1R / e2R + -(e1F / e2F)) + abs (- (e1F / e2F * deltaF))`] match_mp_tac real_le_trans2 \\
conj_tac
rpt strip_tac
\\ inversion `eval_exp 0 _ (Binop Div e1 e2) vR` eval_exp_cases
\\ rename1 `vR = perturb (evalBinop Div v1R v2R) deltaR`
\\ inversion `eval_exp machineEpsilon _ (Binop Div (Var 1) (Var 2)) v` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Div v1F v2F) deltaF`
\\ `perturb (evalBinop Div v1R v2R) deltaR = evalBinop Div v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[])
\\ `vR = evalBinop Div v1R v2R` by simp[]
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ fs[evalBinop_def, perturb_def]
\\ rpt (inversion `eval_exp machineEpsilon (updEnv n e E) expr vE` eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ rewrite_tac [real_sub]
\\ `e1R / e2R + -(e1F / e2F * (1 + deltaF)) = (e1R / e2R + - (e1F / e2F)) + - (e1F / e2F * deltaF)` by REAL_ASM_ARITH_TAC
\\ simp[]
\\ qspecl_then [`abs (e1R / e2R + -(e1F / e2F)) + abs (- (e1F / e2F * deltaF))`] match_mp_tac real_le_trans2
\\ conj_tac
>- (REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_ADD2 \\
conj_tac \\ TRY (REAL_ASM_ARITH_TAC) \\
once_rewrite_tac [ABS_NEG] \\
once_rewrite_tac[REAL_ABS_MUL] \\
match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS]));
>- (match_mp_tac REAL_LE_ADD2
\\ conj_tac \\ TRY (REAL_ASM_ARITH_TAC)
\\ once_rewrite_tac [ABS_NEG]
\\ once_rewrite_tac[REAL_ABS_MUL]
\\ match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS]));
val err_prop_inversion_pos = store_thm ("err_prop_inversion_pos",
``!(nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
......@@ -200,72 +203,72 @@ val err_prop_inversion_pos = store_thm ("err_prop_inversion_pos",
nF <= ehi + err /\
0 <= err ==>
abs (inv nR - inv nF) <= err * inv ((elo - err) * (elo - err))``,
rpt strip_tac \\
`! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)` by REAL_ASM_ARITH_TAC \\
qpat_x_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR - nF` ] DISJ_CASES_TAC thm)
>- (fs [] \\
`nF <= nR` by REAL_ASM_ARITH_TAC \\
`0 < nF` by REAL_ASM_ARITH_TAC \\
`0 < nR` by REAL_ASM_ARITH_TAC \\
`inv nR <= inv nF` by fs [GSYM REAL_INV_LE_ANTIMONO] \\
`inv nR - inv nF <= 0` by REAL_ASM_ARITH_TAC \\
`0 <= - (inv nR - inv nF) ` by REAL_ASM_ARITH_TAC \\
`abs (- (inv nR - inv nF)) = - (inv nR - inv nF)` by fs [ABS_REFL] \\
`abs (inv nR - inv nF) = - (inv nR - inv nF)` by fs[ABS_NEG] \\
simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD] \\
rpt (qpat_x_assum `abs v = v'` kall_tac) \\
`- (1 / nR) = 1 / - nR` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC) \\
simp[] \\
qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP \\
simp[GSYM REAL_INV_1OVER] \\
`0 < nR - err /\ nR - err <= nF` by REAL_ASM_ARITH_TAC \\
qpat_abbrev_tac `nRerr = nR - err` \\
fs [REAL_INV_LE_ANTIMONO])
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC \\ fs [REAL_ADD_RAT] \\
`nR - err + - nR = - err` by REAL_ASM_ARITH_TAC \\
qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL \\
`nR <> 0` by REAL_ASM_ARITH_TAC \\
`nR * (nR - err) <> 0` by fs[REAL_ENTIRE] \\
fs [GSYM REAL_NEG_INV, GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[] \\
rpt (qpat_x_assum `T` kall_tac) \\
`0 < elo + - err` by REAL_ASM_ARITH_TAC \\
`0 < (elo + - err) * (elo + - err)` by fs[REAL_LT_MUL] \\
match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
rpt strip_tac
\\ `! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)` by (REAL_ASM_ARITH_TAC)
\\ qpat_x_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR - nF` ] DISJ_CASES_TAC thm)
>- (fs []
\\ `nF <= nR` by REAL_ASM_ARITH_TAC
\\ `0 < nF` by REAL_ASM_ARITH_TAC
\\ `0 < nR` by REAL_ASM_ARITH_TAC
\\ `inv nR <= inv nF` by fs [GSYM REAL_INV_LE_ANTIMONO]
\\ `inv nR - inv nF <= 0` by REAL_ASM_ARITH_TAC
\\ `0 <= - (inv nR - inv nF) ` by REAL_ASM_ARITH_TAC
\\ `abs (- (inv nR - inv nF)) = - (inv nR - inv nF)` by fs [ABS_REFL]
\\ `abs (inv nR - inv nF) = - (inv nR - inv nF)` by fs[ABS_NEG]
\\ simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs v = v'` kall_tac)
\\ `- (1 / nR) = 1 / - nR` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ simp[]
\\ qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
\\ simp[GSYM REAL_INV_1OVER]
\\ `0 < nR - err /\ nR - err <= nF` by REAL_ASM_ARITH_TAC
\\ qpat_abbrev_tac `nRerr = nR - err`
\\ fs [REAL_INV_LE_ANTIMONO])
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC \\ fs [REAL_ADD_RAT]
\\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
\\ `nR <> 0` by REAL_ASM_ARITH_TAC
\\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
\\ fs [GSYM REAL_NEG_INV, GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
\\ rpt (qpat_x_assum `T` kall_tac)
\\ `0 < elo + - err` by REAL_ASM_ARITH_TAC
\\ `0 < (elo + - err) * (elo + - err)` by fs[REAL_LT_MUL]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))))
>- (fs[] \\
`nR <= nF` by REAL_ASM_ARITH_TAC \\
`0 < nF` by REAL_ASM_ARITH_TAC \\
`0 < nR` by REAL_ASM_ARITH_TAC \\
`inv nF <= inv nR` by fs [GSYM REAL_INV_LE_ANTIMONO] \\
`0 <= inv nR - inv nF` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `inv nF <= inv nR` kall_tac \\
`abs (inv nR - inv nF) = inv nR - inv nF` by fs[ABS_REFL] \\ qpat_x_assum `0 <= inv a - b` kall_tac \\
simp [REAL_INV_1OVER, real_sub, REAL_NEG_ADD] \\
rpt (qpat_x_assum `abs x = y` kall_tac) \\
qspec_then `1 / nR + - (1 / (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP \\
simp [GSYM REAL_INV_1OVER, GSYM REAL_NEG_INV, REAL_LE_NEG] \\
`0 < nR + err /\ nF <= nR + err` by REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\
conj_tac \\ REAL_ASM_ARITH_TAC)
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC \\
`- (1 / (nR + err)) = 1 / - (nR + err)` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC) \\
`- (nR + err) <> 0` by REAL_ASM_ARITH_TAC \\
`nR <> 0` by REAL_ASM_ARITH_TAC \\
fs [REAL_ADD_RAT] \\
`- (nR + err) + nR = - err` by REAL_ASM_ARITH_TAC \\
qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL \\
simp [REAL_NEG_RMUL, REAL_NEG_INV] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[] \\
match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC)))));
>- (fs[]
\\ `nR <= nF` by REAL_ASM_ARITH_TAC
\\ `0 < nF` by REAL_ASM_ARITH_TAC
\\ `0 < nR` by REAL_ASM_ARITH_TAC
\\ `inv nF <= inv nR` by fs [GSYM REAL_INV_LE_ANTIMONO]
\\ `0 <= inv nR - inv nF` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `inv nF <= inv nR` kall_tac
\\ `abs (inv nR - inv nF) = inv nR - inv nF` by fs[ABS_REFL] \\ qpat_x_assum `0 <= inv a - b` kall_tac
\\ simp [REAL_INV_1OVER, real_sub, REAL_NEG_ADD]
\\ rpt (qpat_x_assum `abs x = y` kall_tac)
\\ qspec_then `1 / nR + - (1 / (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP
\\ simp [GSYM REAL_INV_1OVER, GSYM REAL_NEG_INV, REAL_LE_NEG]
\\ `0 < nR + err /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR
\\ conj_tac \\ REAL_ASM_ARITH_TAC)
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ `- (1 / (nR + err)) = 1 / - (nR + err)` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC)
\\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
\\ `nR <> 0` by REAL_ASM_ARITH_TAC
\\ fs [REAL_ADD_RAT]
\\ `- (nR + err) + nR = - err` by REAL_ASM_ARITH_TAC
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
\\ simp [REAL_NEG_RMUL, REAL_NEG_INV]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC)))));
val err_prop_inversion_neg = store_thm ("err_prop_inversion_neg",
``!(nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
......@@ -277,108 +280,108 @@ val err_prop_inversion_neg = store_thm ("err_prop_inversion_neg",
nF <= ehi + err /\
0 <= err ==>
abs (inv nR - inv nF) <= err * inv ((ehi + err) * (ehi + err))``,
rpt strip_tac \\
`! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)` by REAL_ASM_ARITH_TAC \\
qpat_x_assum `!x. (A /\ B) \/ C` (fn thm => qspecl_then [`nR - nF` ] DISJ_CASES_TAC thm)
>- (fs [] \\
`nF <= nR` by REAL_ASM_ARITH_TAC \\
`0 < -nF /\ nF <> 0` by REAL_ASM_ARITH_TAC \\
`0 < -nR /\ nR <> 0` by REAL_ASM_ARITH_TAC \\
`inv (- nF) <= inv (- nR)`
by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac \\
REAL_ASM_ARITH_TAC) \\
`inv (- nF) - inv (- nR) <= 0` by REAL_ASM_ARITH_TAC \\
`0 <= - (inv (- nF) - inv (-nR)) ` by REAL_ASM_ARITH_TAC \\
`abs (- (inv (- nF) - inv (- nR))) = - (inv (- nF) - inv (- nR))` by fs [ABS_REFL] \\
`abs (inv (- nF) - inv (- nR)) = - (inv (- nF) - inv (- nR))` by fs [ABS_NEG] \\
`inv (- nF) - inv (- nR) = inv nR - inv nF` by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC) \\
`abs (inv nR - inv nF) = - (inv nR - inv nF)` by fs[] \\
simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD] \\
rpt (qpat_x_assum `abs v = v'` kall_tac) \\
`- (1 / nR) = 1 / - nR` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC) \\
simp[] \\
qspec_then `1 / -nR + 1 / (nR - err)` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP \\
simp[GSYM REAL_INV_1OVER] \\
`nR - err <= nF` by REAL_ASM_ARITH_TAC \\
`- nF <= - (nR - err)` by REAL_ASM_ARITH_TAC \\