Skip to content

GitLab

F
FloVer
Commit 3d6185b5 authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

Add fixed-point precision to HOL4, fix minor bug in configure script

parent 2dd19d8d
Hide whitespace changes
Inline Side-by-side
Showing with 782 additions and 664 deletions
hol4/CertificateCheckerScript.sml
View file @ 3d6185b5
......@@ -44,7 +44,7 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
CertificateChecker e A P defVars ==>
?iv err vR vF m.
FloverMapTree_find e A = SOME (iv,err) /\
eval_exp E1 (toRMap defVars) (toREval e) vR M0 /\
eval_exp E1 (toRMap defVars) (toREval e) vR REAL /\
eval_exp E2 defVars e vF m /\
(!vF m.
eval_exp E2 defVars e vF m ==>
......@@ -99,7 +99,7 @@ val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_so
CertificateCheckerCmd f A P defVars ==>
?iv err vR vF m.
FloverMapTree_find (getRetExp f) A = SOME (iv, err) /\
bstep (toREvalCmd f) E1 (toRMap defVars) vR M0 /\
bstep (toREvalCmd f) E1 (toRMap defVars) vR REAL /\
bstep f E2 defVars vF m /\
(!vF m. bstep f E2 defVars vF m ==> abs (vR - vF) <= err)``,
simp [CertificateCheckerCmd_def]
......
hol4/CommandsScript.sml
View file @ 3d6185b5
......@@ -20,7 +20,7 @@ val _ = Datatype `
val toREvalCmd_def = Define `
toREvalCmd (f:real cmd) : real cmd =
case f of
| Let m x e g => Let M0 x (toREval e) (toREvalCmd g)
| Let m x e g => Let REAL x (toREval e) (toREvalCmd g)
| Ret e => Ret (toREval e)`;
(**
......
hol4/EnvironmentsScript.sml
View file @ 3d6185b5
......@@ -12,7 +12,7 @@ val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
approxEnv E1 defVars A fVars dVars E2 /\
(defVars x = SOME m) /\
(abs (v1 - v2) <= abs v1 * (mTypeToR m)) /\
(abs (v1 - v2) <= computeError v1 m) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (insert x () fVars) dVars (updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult)
......@@ -58,7 +58,7 @@ val approxEnv_fVar_bounded = store_thm (
E2 x = SOME v2 /\
x IN (domain fVars) /\
Gamma x = SOME m ==>
abs (v - v2) <= (abs v) * (mTypeToR m)``,
abs (v - v2) <= computeError v m``,
rpt strip_tac
\\ qspec_then
`\E1 Gamma absenv fVars dVars E2.
......@@ -67,7 +67,7 @@ val approxEnv_fVar_bounded = store_thm (
E2 x = SOME v2 /\
x IN (domain fVars) /\
Gamma x = SOME m ==>
abs (v - v2) <= (abs v) * (mTypeToR m)`
abs (v - v2) <= computeError v m`
(fn thm => irule (SIMP_RULE std_ss [] thm))
approxEnv_ind
\\ rpt strip_tac
......
hol4/ErrorBoundsScript.sml
View file @ 3d6185b5
......@@ -13,263 +13,370 @@ val _ = new_theory "ErrorBounds";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val triangle_trans = store_thm (
"triangle_trans",
``!a b c.
abs (a + b) <= abs a + abs b /\
abs a + abs b <= c ==>
abs (a + b) <= c``,
rpt strip_tac
\\ REAL_ASM_ARITH_TAC);
val triangle_tac =
irule triangle_trans \\ fs[REAL_ABS_TRIANGLE];
val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
``!(n:real) (nR:real) (nF:real) (E1 E2:env) (m:mType) (defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (Const M0 n) nR M0 /\
eval_exp E1 (toRMap defVars) (Const REAL n) nR REAL /\
eval_exp E2 defVars (Const m n) nF m ==>
abs (nR - nF) <= abs n * (mTypeToR m)``,
abs (nR - nF) <= computeError n m``,
rpt strip_tac
\\ fs[eval_exp_cases]
\\ `perturb n delta = n` by (irule delta_0_deterministic \\ fs[mTypeToR_def])
\\ simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL]
\\ irule REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC);
\\ Cases_on `m` \\ fs[perturb_def, Rabs_err_simpl, REAL_ABS_MUL, computeError_def]
>- (irule REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC)
>- (irule REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC)
>- (irule REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC)
\\ REAL_ASM_ARITH_TAC);
val float_add_tac =
(`e1R + e2R + -((e1F + e2F) * (1 + deltaF)) =
(e1R + - e1F) + ((e2R + - e2F) + - (e1F + e2F) * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp []
\\ triangle_tac
\\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
\\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub]
\\ once_rewrite_tac [REAL_ADD_ASSOC]
\\ triangle_tac
\\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub]
\\ once_rewrite_tac [REAL_ABS_MUL]
\\ simp[computeError_def]
\\ match_mp_tac REAL_LE_MUL2
\\ fs [REAL_ABS_POS, ABS_NEG]);
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) (E1 E2:env) (m m1 m2:mType) (defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real)
(err1:real) (err2:real) (vR:real) (vF:real) (E1 E2:env) (m m1 m2:mType)
(defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (toREval e1) e1R REAL /\
eval_exp E2 defVars e1 e1F m1 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\
eval_exp E2 defVars e2 e2F m2 /\
eval_exp E1 (toRMap defVars) (toREval (Binop Plus e1 e2)) vR M0 /\
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Plus (Var 1) (Var 2)) vF m /\
eval_exp E1 (toRMap defVars) (toREval (Binop Plus e1 e2)) vR REAL /\
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Plus (Var 1) (Var 2)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= err1 + err2 + (abs (e1F + e2F) * (mTypeToR m))``,
rpt strip_tac
\\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Plus e1 e2)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm))
\\ fs []
abs (vR - vF) <= err1 + err2 + (computeError (e1F + e2F) m)``,
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_exp E1 _ (Binop Plus _ _) _ _` eval_exp_cases
\\ rename1 `vR = perturb (evalBinop Plus v1R v2R) deltaR`
\\ rename1 `vR = perturb (evalBinop Plus v1R v2R) (join m1R m2R) deltaR`
\\ inversion `eval_exp _ _ (Binop Plus (Var 1) (Var 2)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Plus v1F v2F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0 \\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalBinop Plus v1R v2R) deltaR = evalBinop Plus v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalBinop Plus v1R v2R` by simp[]
\\ rename1 `vF = perturb (evalBinop Plus v1F v2F) (join m1F m2F) deltaF`
\\ `(m1R = REAL) /\ (m2R = REAL)`
by (conj_tac \\ irule toRMap_eval_REAL \\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `REAL = _` (fn thm => fs [GSYM thm]))
\\ rveq \\ fs[perturb_def]
\\ `v1R = e1R` by metis_tac [meps_0_deterministic]
\\ `v2R = e2R` by metis_tac [meps_0_deterministic]
\\ rveq \\ fs[evalBinop_def, perturb_def]
\\ rveq
\\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ fs [updDefVars_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]);
\\ Cases_on `join m1 m2` \\ fs[perturb_def, evalBinop_def]
>- (`e1R + e2R + -(e1F + e2F) = (e1R + - e1F) + ((e2R + - e2F))`
by REAL_ASM_ARITH_TAC
\\ simp[computeError_def]
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs (e1R + - e1F) + abs (e2R + - e2F)`
\\ fs[REAL_ABS_TRIANGLE]
\\ REAL_ASM_ARITH_TAC)
>- (float_add_tac)
>- (float_add_tac)
>- (float_add_tac)
\\ simp[computeError_def]
\\ `e1R + e2R + - (e1F + e2F + deltaF) = (e1R + - e1F) + (e2R + - e2F + - deltaF)`
by (REAL_ASM_ARITH_TAC)
\\ simp[]
\\ triangle_tac
\\ rewrite_tac [GSYM REAL_ADD_ASSOC]
\\ irule REAL_LE_ADD2 \\ fs[real_sub]
\\ rewrite_tac [REAL_ADD_ASSOC]
\\ triangle_tac
\\ irule REAL_LE_ADD2 \\ fs[real_sub]
\\ REAL_ASM_ARITH_TAC);
val float_sub_tac =
(`e1R + -e2R + -((e1F + -e2F) * (1 + deltaF)) =
(e1R + - e1F) + ((- e2R + e2F) + - (e1F + - e2F) * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp []
\\ triangle_tac
\\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
\\ match_mp_tac REAL_LE_ADD2 \\ fs[GSYM real_sub]
\\ once_rewrite_tac [REAL_ADD_ASSOC]
\\ triangle_tac
\\ match_mp_tac REAL_LE_ADD2 \\ conj_tac
>- REAL_ASM_ARITH_TAC
\\ once_rewrite_tac [REAL_ABS_MUL, ABS_NEG]
\\ 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) (E1 E2:env) (m m1 m2:mType) (defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\
eval_exp E1 (toRMap defVars) (toREval e1) e1R REAL /\
eval_exp E2 defVars e1 e1F m1 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\
eval_exp E2 defVars e2 e2F m2 /\
eval_exp E1 (toRMap defVars) (toREval (Binop Sub e1 e2)) vR M0 /\
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Sub (Var 1) (Var 2)) vF m /\
eval_exp E1 (toRMap defVars) (toREval (Binop Sub e1 e2)) vR REAL /\
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Sub (Var 1) (Var 2)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= err1 + err2 + (abs (e1F - e2F) * (mTypeToR m))``,
abs (vR - vF) <= err1 + err2 + computeError (e1F - e2F) m``,
rpt strip_tac
\\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Sub e1 e2)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm))
\\ fs []
\\ fs[toREval_def]
\\ inversion `eval_exp E1 _ (Binop Sub _ _) _ _` eval_exp_cases
\\ rename1 `vR = perturb (evalBinop Sub v1R v2R) deltaR`
\\ rename1 `vR = perturb (evalBinop Sub v1R v2R) (join m1R m2R) deltaR`
\\ inversion `eval_exp _ _ (Binop Sub (Var 1) (Var 2)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Sub v1F v2F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalBinop Sub v1R v2R) deltaR = evalBinop Sub v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalBinop Sub v1R v2R` by simp[]
\\ rename1 `vF = perturb (evalBinop Sub v1F v2F) (join m1F m2F) deltaF`
\\ `(m1R = REAL) /\ (m2R = REAL)`
by (conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[])
\\ rveq
\\ `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 (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases)
\\ rveq
\\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _`
eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ fs [updDefVars_def] \\ rveq
\\ Cases_on `join m1 m2`
\\ fs[perturb_def, join_def, evalBinop_def, computeError_def]
\\ 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
>- (`e1R - e2R + - (e1F - e2F) = e1R + - e1F + (- e2R + e2F)`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs (e1R + - e1F) + abs (-e2R + e2F)`
\\ fs[REAL_ABS_TRIANGLE]
\\ REAL_ASM_ARITH_TAC)
>- (float_sub_tac)
>- (float_sub_tac)
>- (float_sub_tac)
\\ `e1R + - e2R + - (e1F + - e2F + deltaF) = (e1R + - e1F) + (- e2R + e2F + - deltaF)`
by (REAL_ASM_ARITH_TAC)
\\ simp[]
\\ triangle_tac
\\ rewrite_tac [GSYM REAL_ADD_ASSOC]
\\ irule REAL_LE_ADD2 \\ fs[real_sub]
\\ rewrite_tac [REAL_ADD_ASSOC]
\\ triangle_tac
\\ irule REAL_LE_ADD2 \\ fs[real_sub]
\\ REAL_ASM_ARITH_TAC);
val float_mul_tac =
(`e1R * e2R + -(e1F * e2F * (1 + deltaF)) =
(e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs (e1R * e2R + - (e1F * e2F)) + abs(- (e1F * e2F * deltaF))`
\\ 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]));
>- (REAL_ASM_ARITH_TAC)
\\ irule REAL_LE_ADD2 \\ fs[ABS_NEG, computeError_def]
\\ 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] \\ fs[]);
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) (E1 E2 :env) (m m1 m2:mType) (defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\
eval_exp E1 (toRMap defVars) (toREval e1) e1R REAL /\
eval_exp E2 defVars e1 e1F m1 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\
eval_exp E2 defVars e2 e2F m2 /\
eval_exp E1 (toRMap defVars) (toREval (Binop Mult e1 e2)) vR M0 /\
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Mult (Var 1) (Var 2)) vF m /\
eval_exp E1 (toRMap defVars) (toREval (Binop Mult e1 e2)) vR REAL /\
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Mult (Var 1) (Var 2)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + (abs (e1F * e2F) * (mTypeToR m))``,
abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + computeError (e1F * e2F) m``,
rpt strip_tac
\\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Mult e1 e2)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm))
\\ fs []
\\ fs[toREval_def]
\\ inversion `eval_exp E1 _ (Binop Mult _ _) _ _` eval_exp_cases
\\ rename1 `vR = perturb (evalBinop Mult v1R v2R) deltaR`
\\ rename1 `vR = perturb (evalBinop Mult v1R v2R) (join m1R m2R) deltaR`
\\ inversion `eval_exp _ _ (Binop Mult (Var 1) (Var 2)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Mult v1F v2F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalBinop Mult v1R v2R) deltaR = evalBinop Mult v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalBinop Mult v1R v2R` by simp[]
\\ rename1 `vF = perturb (evalBinop Mult v1F v2F) (join m1F m2F) deltaF`
\\ `(m1R = REAL) /\ (m2R = REAL)`
by (conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[])
\\ rveq
\\ fs[perturb_def, evalBinop_def]
\\ `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 (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases)
\\ rveq
\\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _`
eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ fs [updDefVars_def] \\ rveq
\\ rewrite_tac [real_sub]
\\ `e1R * e2R + -(e1F * e2F * (1 + deltaF)) = (e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)` by REAL_ASM_ARITH_TAC
\\ Cases_on `join m1 m2` \\ fs[join_def, perturb_def]
>- (rewrite_tac [REAL_LE_ADDR] \\ fs[computeError_def])
>- (float_mul_tac)
>- (float_mul_tac)
>- (float_mul_tac)
\\ `e1R * e2R + - (e1F * e2F + deltaF) =
(e1R * e2R + - (e1F * e2F)) + - deltaF`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ triangle_tac
\\ fs[ABS_NEG, computeError_def]);
val float_div_tac =
(`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
\\ irule REAL_LE_TRANS
\\ qexists_tac `abs (e1R / e2R + - (e1F / e2F)) + abs(- (e1F / e2F * deltaF))`
\\ 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[]));
\\ irule REAL_LE_ADD2 \\ fs[ABS_NEG, computeError_def]
\\ once_rewrite_tac[REAL_ABS_MUL]
\\ match_mp_tac REAL_LE_MUL2 \\ fs[REAL_ABS_POS]);
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) (E1 E2 :env) (m m1 m2:mType) (defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\
eval_exp E1 (toRMap defVars) (toREval e1) e1R REAL /\
eval_exp E2 defVars e1 e1F m1 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\
eval_exp E2 defVars e2 e2F m2 /\
eval_exp E1 (toRMap defVars) (toREval (Binop Div e1 e2)) vR M0 /\
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Div (Var 1) (Var 2)) vF m /\
eval_exp E1 (toRMap defVars) (toREval (Binop Div e1 e2)) vR REAL /\
eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars 2 m2 (updDefVars 1 m1 defVars))
(Binop Div (Var 1) (Var 2)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 ==>
abs (vR - vF) <= abs (e1R / e2R - e1F / e2F) + (abs (e1F / e2F) * (mTypeToR m))``,
rpt strip_tac
\\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Div e1 e2)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm))
\\ fs []
abs (vR - vF) <= abs (e1R / e2R - e1F / e2F) + computeError (e1F / e2F) m``,
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_exp E1 _ (Binop Div _ _) _ _` eval_exp_cases
\\ rename1 `vR = perturb (evalBinop Div v1R v2R) deltaR`
\\ rename1 `vR = perturb (evalBinop Div v1R v2R) (join m1R m2R) deltaR`
\\ inversion `eval_exp _ _ (Binop Div (Var 1) (Var 2)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalBinop Div v1F v2F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0)` by (conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalBinop Div v1R v2R) deltaR = evalBinop Div v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalBinop Div v1R v2R` by simp[]
\\ rename1 `vF = perturb (evalBinop Div v1F v2F) (join m1F m2F) deltaF`
\\ `(m1R = REAL) /\ (m2R = REAL)`
by (conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[])
\\ rveq
\\ fs[perturb_def, evalBinop_def]
\\ `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 (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases)
\\ rveq
\\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _`
eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ fs [updDefVars_def] \\ rveq
\\ rewrite_tac [real_sub]
\\ `e1R / e2R + -(e1F / e2F * (1 + deltaF)) = (e1R / e2R + - (e1F / e2F)) + - (e1F / e2F * deltaF)` by REAL_ASM_ARITH_TAC
\\ Cases_on `join m1 m2` \\ fs[join_def, perturb_def]
>- (rewrite_tac [REAL_LE_ADDR] \\ fs[computeError_def])
>- (float_div_tac)
>- (float_div_tac)
>- (float_div_tac)
\\ `e1R / e2R + - (e1F / e2F + deltaF) =
(e1R / e2R + - (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]));
\\ triangle_tac
\\ fs[ABS_NEG, computeError_def]);
val float_fma_tac =
( `e1R + e2R * e3R + -((e1F + e2F * e3F) * (1 + deltaF)) =
(e1R + e2R * e3R + -(e1F + e2F * e3F)) + (- (e1F + e2F * e3F) * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ triangle_tac
\\ irule REAL_LE_ADD2
\\ TRY (REAL_ASM_ARITH_TAC)
\\ once_rewrite_tac[REAL_ABS_MUL]
\\ irule REAL_LE_MUL2 \\ fs[REAL_ABS_POS]
\\ once_rewrite_tac[GSYM REAL_NEG_LMUL, REAL_ABS_MUL]
\\ once_rewrite_tac[ABS_NEG] \\ fs[]);
val fma_abs_err_bounded = store_thm ("fma_abs_err_bounded",
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (e3:real exp) (e3R:real) (e3F:real) (err1:real) (err2:real) (err3:real)
``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real)
(e3:real exp) (e3R:real) (e3F:real) (err1:real) (err2:real) (err3:real)
(vR:real) (vF:real) (E1 E2 :env) (m m1 m2 m3:mType) (defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (toREval e1) e1R M0 /\
eval_exp E1 (toRMap defVars) (toREval e1) e1R REAL /\
eval_exp E2 defVars e1 e1F m1 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R M0 /\
eval_exp E1 (toRMap defVars) (toREval e2) e2R REAL /\
eval_exp E2 defVars e2 e2F m2 /\
eval_exp E1 (toRMap defVars) (toREval e3) e3R M0 /\
eval_exp E1 (toRMap defVars) (toREval e3) e3R REAL /\
eval_exp E2 defVars e3 e3F m3 /\
eval_exp E1 (toRMap defVars) (toREval (Fma e1 e2 e3)) vR M0 /\
eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) (updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars))) (Fma (Var 1) (Var 2) (Var 3)) vF m /\
eval_exp E1 (toRMap defVars) (toREval (Fma e1 e2 e3)) vR REAL /\
eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv)))
(updDefVars 3 m3 (updDefVars 2 m2 (updDefVars 1 m1 defVars)))
(Fma (Var 1) (Var 2) (Var 3)) vF m /\
abs (e1R - e1F) <= err1 /\
abs (e2R - e2F) <= err2 /\
abs (e3R - e3F) <= err3 ==>
abs (vR - vF) <= abs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) + abs (e1F + e2F * e3F) * (mTypeToR m)``,
rpt strip_tac
\\ qpat_x_assum `eval_exp E1 _ (toREval (Fma e1 e2 e3)) _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [toREval_def] thm))
\\ fs []
abs (vR - vF) <=
abs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) +
computeError (e1F + e2F * e3F) m``,
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_exp E1 _ (Fma _ _ _) _ _` eval_exp_cases
\\ rename1 `vR = perturb (evalFma v1R v2R v3R) deltaR`
\\ rename1 `vR = perturb (evalFma v1R v2R v3R) (join3 m1R m2R m3R) deltaR`
\\ inversion `eval_exp _ _ (Fma (Var 1) (Var 2) (Var 3)) _ _` eval_exp_cases
\\ rename1 `vF = perturb (evalFma v1F v2F v3F) deltaF`
\\ `(m1' = M0) /\ (m2' = M0) /\ (m3' = M0)` by (rpt conj_tac \\ irule toRMap_eval_M0\\ asm_exists_tac \\ fs[]) \\ fs []
\\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
\\ `perturb (evalFma v1R v2R v3R) deltaR = evalFma v1R v2R v3R` by (match_mp_tac delta_M0_deterministic \\ fs[])
\\ `vR = evalFma v1R v2R v3R` by simp[]
\\ rename1 `vF = perturb (evalFma v1F v2F v3F) (join3 m1F m2F m3F) deltaF`
\\ `(m1R = REAL) /\ (m2R = REAL) /\ (m3R = REAL)`
by (rpt conj_tac \\ irule toRMap_eval_REAL\\ asm_exists_tac \\ fs[])
\\ rveq
\\ fs[evalFma_def, evalBinop_def]
\\ `v1R = e1R` by metis_tac[meps_0_deterministic]
\\ `v2R = e2R` by metis_tac[meps_0_deterministic]
\\ `v3R = e3R` by metis_tac[meps_0_deterministic]
\\ fs[evalFma_def, evalBinop_def, perturb_def]
\\ rpt (inversion `eval_exp (updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) _ _ _ _` eval_exp_cases)
\\ rveq
\\ rpt (inversion `eval_exp
(updEnv 3 e3F (updEnv 2 e2F (updEnv 1 e1F emptyEnv))) _ _ _ _`
eval_exp_cases)
\\ fs [updEnv_def] \\ rveq
\\ fs [updDefVars_def] \\ rveq
\\ rewrite_tac [real_sub]
\\ `e1R + e2R * e3R + -((e1F + e2F * e3F) * (1 + deltaF)) = (e1R + e2R * e3R + -(e1F + e2F * e3F)) + (- (e1F + e2F * e3F) * deltaF)` by REAL_ASM_ARITH_TAC
\\ Cases_on `join3 m1 m2 m3`
\\ fs[computeError_def, join3_def, join_def, perturb_def]
\\ rewrite_tac[real_sub]
>- (`e1R + e2R * e3R + - (e1F + e2F * e3F) =
e1R + - e1F + (e2R * e3R + - (e2F * e3F))`
by REAL_ASM_ARITH_TAC
\\ simp[])
>- (float_fma_tac)
>- (float_fma_tac)
>- (float_fma_tac)
\\ `e1R + e2R * e3R + -(e1F + e2F * e3F + deltaF) =
(e1R + e2R * e3R + - (e1F + e2F * e3F)) + - deltaF`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ qspecl_then [`abs (e1R + e2R * e3R + -(e1F + e2F * e3F)) + abs (-(e1F + e2F * e3F) * 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[]));
\\ triangle_tac
\\ irule REAL_LE_ADD2
\\ REAL_ASM_ARITH_TAC);
val round_abs_err_bounded = store_thm ("round_abs_err_bounded",
``!(e:real exp) (nR:real) (nF1:real) (nF:real) (E1:env) (E2:env) (err:real) (machineEpsilon:mType) (m:mType) (defVars: num -> mType option).
eval_exp E1 (toRMap defVars) (toREval e) nR M0 /\