Skip to content

GitLab

Commit c383f2fb authored by Nikita Zyuzin's avatar Nikita Zyuzin
Browse files
Options

Complete interval validation for FMA proofs

parent e2380c77
Hide whitespace changes
Inline Side-by-side
Showing with 55 additions and 16 deletions
hol4/IntervalValidationScript.sml
View file @ c383f2fb
......@@ -491,15 +491,15 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
\\ simp[Once usedVars_def])
\\ qpat_x_assum `! absenv P fVars dVars E Gamma. _ ==> ?vR. eval_exp E (toRMap Gamma) (toREval f3) _ _ /\ _ /\ _` kall_tac
\\ fs []
\\ rw_thm_asm `validIntervalbounds (Fma f f' f'') absenv P V` validIntervalbounds_def
\\ rw_thm_asm `validIntervalbounds (Fma f1 f2 f3) absenv P V` validIntervalbounds_def
\\ Cases_on `absenv (Fma f1 f2 f3)` \\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
\\ qmatch_assum_rename_tac `absenv (Fma f1 f2 f3) = (iv_b,err_b)`
\\ qmatch_assum_rename_tac `absenv f1 = (iv_f,err_f)`
\\ qmatch_assum_rename_tac `absenv f2 = (iv_f',err_f')`
\\ qmatch_assum_rename_tac `absenv f3 = (iv_f'',err_f'')`
\\ qmatch_assum_rename_tac `absenv f1 = (iv_f1,err_f1)`
\\ qmatch_assum_rename_tac `absenv f2 = (iv_f2,err_f2)`
\\ qmatch_assum_rename_tac `absenv f3 = (iv_f3,err_f3)`
\\ qexists_tac `evalFma v1 v2 v3`
\\ fs[evalFma_def, evalBinop_def, isSupersetInterval_def, absIntvUpd_def, IVlo_def, IVhi_def, multInterval_def, addInterval_def]
\\ qspecl_then [`iv_f'`, `iv_f''`, `v2`, `v3`]
\\ qspecl_then [`iv_f2`, `iv_f3`, `v2`, `v3`]
assume_tac
(REWRITE_RULE
[validIntervalAdd_def,
......@@ -508,30 +508,38 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
contained_def,
IVhi_def,
IVlo_def] interval_multiplication_valid)
\\ qspecl_then [`iv_f`, `multInterval iv_f' iv_f''`, `v1`, `v2 * v3`]
\\ qspecl_then [`iv_f1`, `multInterval iv_f2 iv_f3`, `v1`, `v2 * v3`]
assume_tac
(REWRITE_RULE
[validIntervalAdd_def,
addInterval_def,
multInterval_def,
absIntvUpd_def,
contained_def,
IVhi_def, IVlo_def] interval_addition_valid)
\\ fs[multInterval_def, absIntvUpd_def, IVlo_def, IVhi_def] \\ res_tac
\\ rpt conj_tac
>- (match_mp_tac Fma_dist'
\\ qexistsl_tac [`M0`, `M0`, `M0`, `v1`, `v2`, `v3`, `0:real`]
\\ fs [mTypeToQ_def, perturb_def, evalFma_def, evalBinop_def, join3_def, join_def])
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `min4 (FST iv_f + FST (multInterval iv_f' iv_f''))
(FST iv_f + SND (multInterval iv_f' iv_f''))
(SND iv_f + FST (multInterval iv_f' iv_f''))
(SND iv_f + SND (multInterval iv_f' iv_f''))`
\\ metis_tac[])
\\ asm_exists_tac
\\ conj_tac \\ fs[])
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `max4 (FST iv_f + FST iv_f')
(FST iv_f + SND iv_f')
(SND iv_f + FST iv_f')
(SND iv_f + SND iv_f')`
\\metis_tac []))
\\ qexists_tac `max4
(FST iv_f1 +
min4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
(SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))
(FST iv_f1 +
max4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
(SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))
(SND iv_f1 +
min4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
(SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))
(SND iv_f1 +
max4 (FST iv_f2 * FST iv_f3) (FST iv_f2 * SND iv_f3)
(SND iv_f2 * FST iv_f3) (SND iv_f2 * SND iv_f3))`
\\conj_tac \\ fs[]))
(* Downcast case *)
>- (`?v. eval_exp E (toRMap Gamma) (toREval f) v M0 /\
FST(FST(absenv f)) <= v /\ v <= SND (FST(absenv f))`
......@@ -590,6 +598,7 @@ val swap_Gamma_eval_exp = store_thm (
>- (qexists_tac `v1` \\ fs[])
>- (qexistsl_tac [`v1`, `delta`] \\ fs[])
>- (qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta`] \\ fs[])
>- (qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta`] \\ fs[])
>- (qexistsl_tac [`m1'`, `v1`, `delta`] \\ fs[]));
val swap_Gamma_bstep = store_thm (
......@@ -785,6 +794,36 @@ val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []))
>- (rename1 `Fma f1 f2 f3`
\\ qpat_x_assum `validIntervalbounds _ _ _ _`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
\\ Cases_on `absenv (Fma f1 f2 f3)` \\ rename1 `absenv (Fma f1 f2 f3) = (iv,err)`
\\ fs[]
\\ `valid (FST (absenv f1))`
by (first_x_assum match_mp_tac
\\ qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ `valid (FST (absenv f2))`
by (first_x_assum match_mp_tac
\\ qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ `valid (FST (absenv f3))`
by (first_x_assum match_mp_tac
\\ qexists_tac `P` \\ qexists_tac `dVars`
\\ fs[])
\\ Cases_on `absenv f1` \\ Cases_on `absenv f2` \\ Cases_on `absenv f3`
\\ rename1 `absenv f1 = (iv_f1, err_f1)`
\\ rename1 `absenv f2 = (iv_f2, err_f2)`
\\ rename1 `absenv f3 = (iv_f3, err_f3)`
\\ fs[]
\\ `valid (addInterval iv_f1 (multInterval iv_f2 iv_f3))`
by (match_mp_tac iv_add_preserves_valid \\ fs[]
\\ match_mp_tac iv_mult_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac \\ fs [])
>- (qpat_x_assum `validIntervalbounds _ _ _ _`
(fn thm => ASSUME_TAC (ONCE_REWRITE_RULE[validIntervalbounds_def] thm))
\\ Cases_on `absenv (Downcast m f)` \\ Cases_on `absenv f` \\ fs[]
......
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