Skip to content

GitLab

Commit 2310eea4 authored by Heiko Becker's avatar Heiko Becker
Browse files

Division for new semantics

parent 065ad7bf
Hide whitespace changes
Inline Side-by-side
hol4/ErrorValidationScript.sml
View file @ 2310eea4
......@@ -869,16 +869,16 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
``!(E1 E2 ParamEnv:env) (absenv:analysisResult) (e1:real exp) (e2:real exp)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) (P:precond).
``!(E1 E2:env) (absenv:analysisResult) (e1:real exp) (e2:real exp)
(nR nR1 nR2 nF nF1 nF2:real) (e err1 err2:real) (alo ahi e1lo e1hi e2lo e2hi :real) dVars.
eval_exp 0 E1 e1 nR1 /\
eval_exp 0 E1 e2 nR2 /\
eval_exp 0 E1 (Binop Div e1 e2) nR /\
eval_exp machineEpsilon E2 e1 nF1 /\
eval_exp machineEpsilon E2 e2 nF2 /\
eval_exp machineEpsilon
(updEnv 2 nF2 (updEnv 1 nF1 E2))P (Binop Div (Var 1) (Var 2)) nF /\
validErrorbound (Binop Div e1 e2) absenv /\
(updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) (Binop Div (Var 1) (Var 2)) nF /\
validErrorbound (Binop Div e1 e2) absenv dVars /\
(e2hi < 0 \/ 0 < e2lo) /\
FST (FST (absenv e1)) <= nR1 /\
nR1 <= SND (FST (absenv e1)) /\
......@@ -890,81 +890,78 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
abs (nR1 - nF1) <= err1 /\
abs (nR2 - nF2) <= err2 ==>
abs (nR - nF) <= e``,
once_rewrite_tac [validErrorbound_def, GSYM noDivzero_def] \\
rpt (strip_tac) \\
qpat_x_assum `absenv _ = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
qpat_x_assum `absenv e1 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
qpat_x_assum `absenv e2 = _` (fn thm => rule_assum_tac (fn thm2 => REWRITE_RULE [thm] thm2) \\ ASSUME_TAC thm) \\
qpat_x_assum `noDivzero _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [noDivzero_def] thm)) \\
`0 <= err1`
by (match_mp_tac err_always_positive \\
qexists_tac `e1` \\ qexists_tac `absenv` \\ qexists_tac `(e1lo,e1hi)` \\ fs[]) \\
`0 <= err2`
by (match_mp_tac err_always_positive \\
qexists_tac `e2` \\ qexists_tac `absenv` \\ qexists_tac `(e2lo,e2hi)` \\ fs[]) \\
match_mp_tac REAL_LE_TRANS \\
qexists_tac `abs (nR1 / nR2 - nF1 / nF2) + abs (nF1 / nF2) * machineEpsilon` \\
conj_tac
>- (match_mp_tac div_abs_err_bounded \\
qexistsl_tac [`e1`, `e2`, `err1`, `err2`, `E1`, `E2`, `ParamEnv`, `P`] \\
fs [])
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac
`maxAbs (e1lo,e1hi) * (1 / (minAbsFun (widenInterval (e2lo,e2hi) err2) *
minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) +
maxAbs (invertInterval (e2lo,e2hi)) * err1 +
err1 *
(1 /
(minAbsFun (widenInterval (e2lo,e2hi) err2) *
minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) +
maxAbs
(divideInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon` \\
conj_tac
>- (`contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv \\
qexists_tac `nR1` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\
`contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (match_mp_tac distance_gives_iv \\
qexists_tac `nR2` \\ conj_tac \\ simp[contained_def, IVlo_def, IVhi_def]) \\
match_mp_tac REAL_LE_ADD2 \\ conj_tac
>- (rpt (qpat_x_assum `eval_exp _ _ _ _ _ _` kall_tac) \\
`contained (inv nR2) (invertInterval (e2lo, e2hi))`
by (match_mp_tac interval_inversion_valid \\ conj_tac \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`contained (inv nF2) (invertInterval (widenInterval (e2lo, e2hi) err2))`
by (match_mp_tac interval_inversion_valid \\ conj_tac \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`nR1 <= maxAbs (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`inv nR2 <= maxAbs (invertInterval(e2lo, e2hi))`
by (match_mp_tac contained_leq_maxAbs_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`-nR1 <= maxAbs (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`- inv nR2 <= maxAbs (invertInterval (e2lo, e2hi))`
by (match_mp_tac contained_leq_maxAbs_neg_val \\ fs[contained_def, IVlo_def, IVhi_def]) \\
`nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`-nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`inv nR2 * err1 <= maxAbs (invertInterval(e2lo, e2hi)) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`- inv nR2 * err1 <= maxAbs (invertInterval(e2lo, e2hi)) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[]) \\
`- (err1 * err2) <= err1 * err2`
by (fs[REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC) \\
`0 <= maxAbs (e1lo, e1hi) * err2` by REAL_ASM_ARITH_TAC \\
`0 <= maxAbs (invertInterval (e2lo, e2hi)) * err1` by REAL_ASM_ARITH_TAC \\
`maxAbs (e1lo, e1hi) * err2 <= maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1`
by (REAL_ASM_ARITH_TAC) \\
`maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1 <=
rewrite_tac [Once validErrorbound_def, GSYM noDivzero_def]
\\ rpt (strip_tac)
\\ fs[]
\\ `0 <= err1`
by (match_mp_tac err_always_positive
\\ qexistsl_tac [`e1`, `absenv`, `(e1lo,e1hi)`, `dVars`] \\ fs[])
\\ `0 <= err2`
by (match_mp_tac err_always_positive
\\ qexistsl_tac [`e2`, `absenv`, `(e2lo,e2hi)`, `dVars`] \\ fs[])
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `abs (nR1 / nR2 - nF1 / nF2) + abs (nF1 / nF2) * machineEpsilon`
\\ conj_tac
>- (match_mp_tac div_abs_err_bounded
\\ qexistsl_tac [`e1`, `e2`, `err1`, `err2`, `E1`, `E2`]
\\ fs [])
>- (match_mp_tac REAL_LE_TRANS
\\ once_rewrite_tac [CONJ_SYM]
\\ asm_exists_tac
\\ once_rewrite_tac [CONJ_SYM]
\\ conj_tac \\ rw[]
\\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR1` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ `contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (match_mp_tac distance_gives_iv
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
\\ match_mp_tac REAL_LE_ADD2 \\ conj_tac
>- (rpt (qpat_x_assum `eval_exp _ _ _ _ _ _` kall_tac)
\\ `contained (inv nR2) (invertInterval (e2lo, e2hi))`
by (match_mp_tac interval_inversion_valid \\ conj_tac
\\ fs[contained_def, IVlo_def, IVhi_def, noDivzero_def])
\\ `contained (inv nF2) (invertInterval (widenInterval (e2lo, e2hi) err2))`
by (match_mp_tac interval_inversion_valid \\ conj_tac
\\ fs[contained_def, IVlo_def, IVhi_def, noDivzero_def])
\\ `nR1 <= maxAbs (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_val
\\ fs[contained_def, IVlo_def, IVhi_def])
\\ `inv nR2 <= maxAbs (invertInterval(e2lo, e2hi))`
by (match_mp_tac contained_leq_maxAbs_val
\\ fs[contained_def, IVlo_def, IVhi_def])
\\ `-nR1 <= maxAbs (e1lo, e1hi)`
by (match_mp_tac contained_leq_maxAbs_neg_val
\\ fs[contained_def, IVlo_def, IVhi_def])
\\ `- inv nR2 <= maxAbs (invertInterval (e2lo, e2hi))`
by (match_mp_tac contained_leq_maxAbs_neg_val
\\ fs[contained_def, IVlo_def, IVhi_def])
\\ `nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[])
\\ `-nR1 * err2 <= maxAbs (e1lo, e1hi) * err2`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[])
\\ `inv nR2 * err1 <= maxAbs (invertInterval(e2lo, e2hi)) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[])
\\ `- inv nR2 * err1 <= maxAbs (invertInterval(e2lo, e2hi)) * err1`
by (match_mp_tac REAL_LE_RMUL_IMP \\ fs[])
\\ `- (err1 * err2) <= err1 * err2`
by (fs[REAL_NEG_LMUL] \\ match_mp_tac REAL_LE_RMUL_IMP
\\ REAL_ASM_ARITH_TAC)
\\ `0 <= maxAbs (e1lo, e1hi) * err2` by REAL_ASM_ARITH_TAC
\\ `0 <= maxAbs (invertInterval (e2lo, e2hi)) * err1` by REAL_ASM_ARITH_TAC
\\ `maxAbs (e1lo, e1hi) * err2 <= maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1`
by (REAL_ASM_ARITH_TAC)
\\ `maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1 <=
maxAbs (e1lo, e1hi) * err2 + maxAbs (invertInterval (e2lo, e2hi)) * err1 + err1 * err2`
by REAL_ASM_ARITH_TAC \\
by REAL_ASM_ARITH_TAC
(* Case distinction for divisor range
positive or negative in float and real valued execution *)
fs[] \\
rpt (qpat_x_assum `validErrorbound _ _ ` kall_tac) \\
rpt (qpat_x_assum `absenv _ = _` kall_tac) \\
rpt (qpat_x_assum `isSupersetInterval _ _` kall_tac) \\
rpt (qpat_x_assum `maxAbs (e1lo,e1hi) *
\\ rpt (qpat_x_assum `validErrorbound _ _ ` kall_tac)
\\ rpt (qpat_x_assum `absenv _ = _` kall_tac)
\\ rpt (qpat_x_assum `isSupersetInterval _ _` kall_tac)
\\ rpt (qpat_x_assum `maxAbs (e1lo,e1hi) *
(1 /
(minAbsFun (widenInterval (e2lo,e2hi) err2) *
minAbsFun (widenInterval (e2lo,e2hi) err2)) * err2) +
......@@ -976,11 +973,11 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
maxAbs
(divideInterval (widenInterval (e1lo,e1hi) err1)
(widenInterval (e2lo,e2hi) err2)) * machineEpsilon <= e` kall_tac)
\\ fs [IVlo_def, IVhi_def, widenInterval_def, contained_def, noDivzero_def]
(* The range of the divisor lies in the range from -infinity until 0 *)
>- (rule_assum_tac (fn thm => REWRITE_RULE[IVlo_def, IVhi_def, widenInterval_def, contained_def] thm) \\
`abs (inv nR2 - inv nF2) <= err2 * inv ((e2hi + err2) * (e2hi + err2))`
by (match_mp_tac err_prop_inversion_neg \\ qexists_tac `e2lo` \\simp[]) \\
fs [widenInterval_def, IVlo_def, IVhi_def] \\
>- (`abs (inv nR2 - inv nF2) <= err2 * inv ((e2hi + err2) * (e2hi + err2))`
by (match_mp_tac err_prop_inversion_neg \\ qexists_tac `e2lo` \\simp[])
\\ fs [widenInterval_def, IVlo_def, IVhi_def] \\
`minAbsFun (e2lo - err2, e2hi + err2) = - (e2hi + err2)`
by (match_mp_tac minAbs_negative_iv_is_hi \\ REAL_ASM_ARITH_TAC) \\
simp[] \\
......@@ -1970,8 +1967,7 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
by (match_mp_tac interval_division_valid \\
conj_tac \\ fs[]) \\
rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm) \\
simp[]))
>- (fs[])));
fs[widenInterval_def, IVlo_def, IVhi_def,noDivzero_def])));
val validErrorbound_sound = store_thm ("validErrorbound_sound",
``!(e:real exp) (E1 E2 ParamEnv:env) (absenv:analysisResult)
......
hol4/Infra/DaisyTactics.sml
View file @ 2310eea4
......@@ -62,12 +62,17 @@ fun specialize pat_hyp pat_thm =
fun rw_asm pat_asm =
qpat_x_assum pat_asm
(fn asm =>
(once_rewrite_tac [asm]));
(once_rewrite_tac [asm] \\ ASSUME_TAC asm));
fun rw_asm_star pat_asm =
qpat_x_assum pat_asm
(fn asm =>
fs [Once asm] \\ ASSUME_TAC asm);
fun rw_sym_asm pat_asm =
qpat_x_assum pat_asm
(fn asm =>
(once_rewrite_tac [GSYM asm]));
(once_rewrite_tac [GSYM asm] \\ ASSUME_TAC asm));
fun rw_thm_asm pat_asm thm =
qpat_x_assum pat_asm
......
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