Skip to content

GitLab

Commit 2b268a70 authored by Heiko Becker's avatar Heiko Becker
Browse files

Show variable soundness in HOL4

parent 2310eea4
Hide whitespace changes
Inline Side-by-side
hol4/ErrorValidationScript.sml
View file @ 2b268a70
......@@ -59,6 +59,8 @@ val validErrorboundCmd_def = Define `
| Ret e =>
validErrorbound e env dVars`;
val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
val err_always_positive = store_thm ("err_always_positive",
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real) dVars.
(validErrorbound (e:real exp) (absenv:analysisResult) dVars) /\
......@@ -69,31 +71,155 @@ val err_always_positive = store_thm ("err_always_positive",
qpat_assum `(iv,err) = absenv e` (fn thm => fs [GSYM thm]) \\
Cases_on `absenv e0` \\ Cases_on `absenv e'` \\ fs[]);
val validErrorboundCorrectVariable_ind = prove (
``!(E1 E2:env) absenv fVars dVars.
approxEnv E1 absenv fVars dVars E2 ==>
! (v:num) (nR nF err nlo nhi:real) (P:precond).
eval_exp 0 E1 (Var v) nR /\
eval_exp machineEpsilon E2 (Var v) nF /\
validIntervalbounds (Var v) absenv P dVars /\
validErrorbound (Var v) absenv dVars /\
(!v.
v IN domain dVars ==>
?r.
(E1 v = SOME r) /\
FST (FST (absenv (Var v))) <= r /\
r <= SND (FST (absenv (Var v)))) /\
(!v.
v IN domain fVars ==>
?r.
(E1 v = SOME r) /\
FST (P v) <= r /\ r <= SND (P v)) /\
(absenv (Var v) = ((nlo, nhi),err)) ==>
abs (nR - nF) <= err``,
(* rule induction on approximation relation *)
qspec_then
`\E1 absenv fVars dVars E2.
!(v:num) (nR nF err nlo nhi:real) (P:precond).
eval_exp 0 E1 (Var v) nR /\
eval_exp machineEpsilon E2 (Var v) nF /\
validIntervalbounds (Var v) absenv P dVars /\
validErrorbound (Var v) absenv dVars /\
(!v.
v IN domain dVars ==>
?r.
(E1 v = SOME r) /\
FST (FST (absenv (Var v))) <= r /\
r <= SND (FST (absenv (Var v)))) /\
(!v.
v IN domain fVars ==>
?r.
(E1 v = SOME r) /\
FST (P v) <= r /\ r <= SND (P v)) /\
(absenv (Var v) = ((nlo, nhi),err)) ==>
abs (nR - nF) <= err` (fn thm => ASSUME_TAC (SIMP_RULE std_ss [] thm)) approxEnv_ind
\\ first_x_assum match_mp_tac
\\ rpt strip_tac
\\ inversion `eval_exp 0 _ _ _` eval_exp_cases
\\ inversion `eval_exp machineEpsilon _ _ _` eval_exp_cases
>- (fs [emptyEnv_def])
>- (fs[updEnv_def]
\\ Cases_on `v = x` \\ rveq
>- (fs [validErrorbound_def, lookup_union] \\ rveq \\ Cases_on `lookup v fVars` \\ fs[]
\\ first_assum (qspec_then `v` ASSUME_TAC)
\\ match_mp_tac REAL_LE_TRANS
\\ asm_exists_tac
\\ conj_tac \\ fs []
\\ match_mp_tac REAL_LE_TRANS
\\ qexists_tac `maxAbs (nlo, nhi) * machineEpsilon`
\\ conj_tac \\ fs []
\\ match_mp_tac REAL_LE_RMUL_IMP
\\ fs [mEps_geq_zero]
\\ match_mp_tac contained_leq_maxAbs
\\ rewrite_tac [contained_def, IVlo_def, IVhi_def]
\\ qspecl_then [`Var v`, `A`] ASSUME_TAC validIntervalbounds_sound
\\ rw_asm_star `A (Var v) = _`
\\ rw_asm_star `A (Var v) = _`
\\ first_x_assum match_mp_tac
\\ qexistsl_tac [`P`, `Insert v fVars`, `dVars`, `updEnv v nR E1`]
\\ fs [updEnv_def]
\\ conj_tac
>- (fs [usedVars_def, SUBSET_DEF, Insert_def, domain_insert])
>- (match_mp_tac Var_load \\ fs [updEnv_def]))
>- (first_x_assum match_mp_tac
\\ qexistsl_tac [`v`, `nlo`, `nhi`, `P`]
\\ fs []
\\ rpt conj_tac
>- (match_mp_tac Var_load \\ fs [])
>- (match_mp_tac Var_load \\ fs [])
>- (rpt strip_tac
\\ rpt( first_x_assum (qspec_then `v'` ASSUME_TAC))
\\ specialize `v' IN domin dVars ==> _` `v' IN domain dVars`
\\ fs []
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
\\ Cases_on `lookup v' fVars`
\\ fs [domain_lookup])
>- (rveq \\ fs []))
>- (rpt strip_tac
\\ first_x_assum (qspec_then `v'` ASSUME_TAC)
\\ Cases_on `v' = x`
>- (rveq \\ fs[lookup_union]
\\ Cases_on `lookup v' fVars`
\\ fs [domain_lookup])
>- (fs []
\\ first_x_assum match_mp_tac
\\ fs [domain_insert, Insert_def]))))
>- (fs [updEnv_def]
\\ Cases_on `v = x` \\ rveq
>- (fs [validErrorbound_def, lookup_union]
\\ rveq \\ Cases_on `lookup v fVars` \\ fs[])
>- (first_x_assum match_mp_tac
\\ qexistsl_tac [`v`, `nlo`, `nhi`, `P`]
\\ rpt conj_tac
>- (match_mp_tac Var_load \\ fs [])
>- (match_mp_tac Var_load \\ fs [])
>- (fs [validIntervalbounds_def, Insert_def, lookup_insert])
>- (fs [validErrorbound_def, Insert_def, lookup_insert])
>- (rpt strip_tac
\\ specialize `!v. v IN domain (Insert _ _) ==> _` `v'`
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
\\ Cases_on `lookup v' fVars`
\\ fs [domain_lookup])
>- (fs []
\\ first_x_assum match_mp_tac
\\ fs [domain_insert, Insert_def]))
>- (rpt strip_tac
\\ rpt (first_x_assum (qspec_then `v'` ASSUME_TAC))
\\ specialize `v' IN domin fVars ==> _` `v' IN domain fVars`
\\ fs []
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
\\ Cases_on `lookup v' fVars`
\\ fs [domain_lookup])
>- (rveq \\ fs []))
>- (fs []))));
val validErrorboundCorrectVariable = store_thm ("validErrorboundCorrectVariable",
``!(E1 E2:env) absenv (v:num)
(nR nF err nlo nhi:real) (P:precond) VarEnv1 absenv E2.
approxEnv VarEnv1 absenv E2 /\
eval_exp 0 VarEnv1P (Var v) nR /\
``!(E1 E2:env) absenv fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond).
approxEnv E1 absenv fVars dVars E2 /\
eval_exp 0 E1 (Var v) nR /\
eval_exp machineEpsilon E2 (Var v) nF /\
validErrorbound (Var v) absenv /\
validIntervalbounds (Var v) absenv P dVars /\
validErrorbound (Var v) absenv dVars /\
(!v.
v IN domain dVars ==>
?r.
(E1 v = SOME r) /\
FST (FST (absenv (Var v))) <= r /\
r <= SND (FST (absenv (Var v)))) /\
(!v.
v IN domain fVars ==>
?r.
(E1 v = SOME r) /\
FST (P v) <= r /\ r <= SND (P v)) /\
(absenv (Var v) = ((nlo, nhi),err)) ==>
abs (nR - nF) <= err``,
once_rewrite_tac [GSYM AND_IMP_INTRO] \\
gen_tac \\ gen_tac \\ gen_tac \\ gen_tac \\ gen_tac \\ gen_tac \\
gen_tac \\ gen_tac \\
ho_match_mp_tac approxEnv_ind \\
once_rewrite_tac [validErrorbound_def] \\
rpt strip_tac \\
fs[]
>- (inversion `eval_exp 0 _ _ _ _ _` eval_exp_cases \\
inversion `eval_exp machineEpsilon _ _ _ _ _` eval_exp_cases \\
fs[])
>- (inversion `eval_exp 0 _ _ _ _ _` eval_exp_cases \\
inversion `eval_exp machineEpsilon _ _ _ _ _` eval_exp_cases \\
fs[updEnv_def] \\
Cases_on `v = x` \\ fs[] \\
first_x_assum match_mp_tac \\
conj_tac \\ metis_tac [eval_exp_rules]));
rpt strip_tac
\\ drule validErrorboundCorrectVariable_ind
\\ disch_then (fn thm => qspecl_then [`v`, `nR`, `nF`, `err`, `nlo`, `nhi`, `P`] ASSUME_TAC thm)
\\ fs []);
val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant",
``!(E1 E2:env) (absenv:analysisResult) (n nR nF e nlo nhi:real) dVars.
......@@ -866,8 +992,6 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
\\ rule_assum_tac (fn thm => REWRITE_RULE [contained_def, IVlo_def, IVhi_def] thm)
\\ simp[])));
val noDivzero_def = Define `noDivzero (a:real) (b:real) = (a < &0 \/ &0 < b)`;
val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
``!(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.
......@@ -977,90 +1101,90 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
(* The range of the divisor lies in the range from -infinity until 0 *)
>- (`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[] \\
qpat_x_assum `minAbsFun _ = _ ` kall_tac \\
`nF1 <= err1 + nR1` by REAL_ASM_ARITH_TAC \\
`nR1 - err1 <= nF1` by REAL_ASM_ARITH_TAC \\
`(nR2 - nF2 > 0 /\ nR2 - nF2 <= err2) \/ (nR2 - nF2 <= 0 /\ - (nR2 - nF2) <= err2)`
by REAL_ASM_ARITH_TAC
(* Positive case for abs (nR2 - nF2) <= err2 *)
>- (`nF2 < nR2` by REAL_ASM_ARITH_TAC \\
qpat_x_assum `nF2 < nR2` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [GSYM REAL_LT_NEG] thm)) \\
`inv (- nF2) < inv (- nR2)` by (match_mp_tac REAL_LT_INV \\ REAL_ASM_ARITH_TAC) \\
`inv (- nF2) = - (inv nF2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
`inv (- nR2) = - (inv nR2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC) \\
rpt (
qpat_x_assum `inv (- _) = - (inv _)`
(fn thm => rule_assum_tac (fn hyp => REWRITE_RULE [thm] hyp))) \\
`inv nR2 < inv nF2` by REAL_ASM_ARITH_TAC \\
qpat_x_assum `- _ < - _` kall_tac \\
`inv nR2 - inv nF2 < 0` by REAL_ASM_ARITH_TAC \\
`- (nR2⁻¹ − nF2⁻¹) ≤ err2 * ((e2hi + err2) * (e2hi + err2))⁻¹` by REAL_ASM_ARITH_TAC \\
`inv nF2 <= inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2))` by REAL_ASM_ARITH_TAC \\
`inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)) <= inv nF2` by REAL_ASM_ARITH_TAC \\
(* Next do a case distinction for the absolute value *)
`! (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 => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm)
(* Case 1: Absolute value positive *)
>- (fs[real_sub, real_div, REAL_NEG_LMUL] \\
qspecl_then [`-nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* -nF1 < 0 *)
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\
conj_tac
>- (fs[REAL_LE_LADD] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\
conj_tac \\ REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)` \\
qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L\\
conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
by REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => ONCE_REWRITE_TAC [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
match_mp_tac REAL_LE_ADD2 \\
conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_ADD2 \\
conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
conj_tac \\ REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)` \\
conj_tac
>- (fs [REAL_LE_ADD] \\
match_mp_tac REAL_LE_RMUL_IMP \\
conj_tac \\ REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) =
nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
by REAL_ASM_ARITH_TAC \\
simp[REAL_NEG_MUL2] \\
qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => ONCE_REWRITE_TAC [thm]) REAL_MUL_COMM \\
qunabbrev_tac `err_inv` \\
simp [real_sub] \\
match_mp_tac REAL_LE_ADD2 \\
conj_tac
>- (match_mp_tac REAL_LE_ADD2 \\
conj_tac \\ TRY REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_LE_RMUL_IMP \\
conj_tac \\ REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL] \\
match_mp_tac REAL_LE_RMUL_IMP \\
conj_tac \\ REAL_ASM_ARITH_TAC)))))
\\ 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[]
\\ qpat_x_assum `minAbsFun _ = _ ` kall_tac
\\ `nF1 <= err1 + nR1` by REAL_ASM_ARITH_TAC
\\ `nR1 - err1 <= nF1` by REAL_ASM_ARITH_TAC
\\ `(nR2 - nF2 > 0 /\ nR2 - nF2 <= err2) \/ (nR2 - nF2 <= 0 /\ - (nR2 - nF2) <= err2)`
by REAL_ASM_ARITH_TAC
(* Positive case for abs (nR2 - nF2) <= err2 *)
>- (`nF2 < nR2` by REAL_ASM_ARITH_TAC
\\ qpat_x_assum `nF2 < nR2` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [GSYM REAL_LT_NEG] thm))
\\ `inv (- nF2) < inv (- nR2)` by (match_mp_tac REAL_LT_INV \\ REAL_ASM_ARITH_TAC)
\\ `inv (- nF2) = - (inv nF2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ `inv (- nR2) = - (inv nR2)` by (match_mp_tac (GSYM REAL_NEG_INV) \\ REAL_ASM_ARITH_TAC)
\\ rpt (
qpat_x_assum `inv (- _) = - (inv _)`
(fn thm => rule_assum_tac (fn hyp => REWRITE_RULE [thm] hyp)))
\\ `inv nR2 < inv nF2` by REAL_ASM_ARITH_TAC
\\ qpat_x_assum `- _ < - _` kall_tac
\\ `inv nR2 - inv nF2 < 0` by REAL_ASM_ARITH_TAC
\\ `- (nR2⁻¹ − nF2⁻¹) ≤ err2 * ((e2hi + err2) * (e2hi + err2))⁻¹` by REAL_ASM_ARITH_TAC
\\ `inv nF2 <= inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2))` by REAL_ASM_ARITH_TAC
\\ `inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)) <= inv nF2` by REAL_ASM_ARITH_TAC
(* Next do a case distinction for the absolute value *)
\\ `! (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 => qspec_then `(nR1:real / nR2:real) - (nF1:real / nF2:real)` DISJ_CASES_TAC thm)
(* Case 1: Absolute value positive *)
>- (fs[real_sub, real_div, REAL_NEG_LMUL]
\\ qspecl_then [`-nF1`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* -nF1 < 0 *)
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 - err2 * inv ((e2hi + err2) * (e2hi + err2)))`
\\ conj_tac
>- (fs[REAL_LE_LADD]
\\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L
\\ conj_tac \\ REAL_ASM_ARITH_TAC)
>- (qabbrev_tac `err_inv = (err2 * ((e2hi + err2) * (e2hi + err2))⁻¹)`
\\ qspecl_then [`inv nR2 - err_inv`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv)`
\\ conj_tac
>- (fs [REAL_LE_ADD]
\\ once_rewrite_tac [REAL_MUL_COMM]
\\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L
\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
\\ fs [REAL_LE_NEG])
>- (`nR1 * inv nR2 + - (nR1 + err1) * (inv nR2 - err_inv) =
nR1 * err_inv + - (inv nR2) * err1 + err1 * err_inv`
by REAL_ASM_ARITH_TAC
\\ simp[REAL_NEG_MUL2]
\\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => ONCE_REWRITE_TAC [thm]) REAL_MUL_COMM
\\ qunabbrev_tac `err_inv`
\\ match_mp_tac REAL_LE_ADD2
\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
\\ match_mp_tac REAL_LE_ADD2
\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
\\ match_mp_tac REAL_LE_RMUL_IMP
\\ conj_tac \\ REAL_ASM_ARITH_TAC))
>- (match_mp_tac REAL_LE_TRANS
\\ qexists_tac `nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv)`
\\ conj_tac
>- (fs [REAL_LE_ADD]
\\ match_mp_tac REAL_LE_RMUL_IMP
\\ conj_tac \\ REAL_ASM_ARITH_TAC)
>- (`nR1 * inv nR2 + - (nR1 + - err1) * (inv nR2 - err_inv) =
nR1 * err_inv + inv nR2 * err1 - err1 * err_inv`
by REAL_ASM_ARITH_TAC
\\ simp[REAL_NEG_MUL2]
\\ qspecl_then [`inv ((e2hi + err2) * (e2hi + err2))`,`err2`]
(fn thm => ONCE_REWRITE_TAC [thm]) REAL_MUL_COMM
\\ qunabbrev_tac `err_inv`
\\ simp [real_sub]
\\ match_mp_tac REAL_LE_ADD2
\\ conj_tac
>- (match_mp_tac REAL_LE_ADD2
\\ conj_tac \\ TRY REAL_ASM_ARITH_TAC
\\ match_mp_tac REAL_LE_RMUL_IMP
\\ conj_tac \\ REAL_ASM_ARITH_TAC)
>- (simp [REAL_NEG_LMUL]
\\ match_mp_tac REAL_LE_RMUL_IMP
\\ conj_tac \\ REAL_ASM_ARITH_TAC)))))
(* 0 <= - nF1 *)
>- (match_mp_tac REAL_LE_TRANS \\
qexists_tac `nR1 * inv nR2 + - nF1 * (inv nR2 + err2 * inv ((e2hi + err2) * (e2hi + err2)))` \\
......
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