Commit 7ad77387 authored by Heiko Becker's avatar Heiko Becker

Prove positive bound for inversion and add error bound validator'

parent 7d6b6460
......@@ -188,5 +188,82 @@ conj_tac
once_rewrite_tac[REAL_ABS_MUL] \\
ho_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).
0 < elo - err /\ 0 < elo /\
abs (nR - nF) <= err /\
elo <= nR /\
nR <= ehi /\
elo - err <= nF /\
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] \\ ho_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)))));
DB.match [] `` -1 * (b:real)``
val _ = export_theory();
......@@ -8,8 +8,11 @@
**)
open preamble
open simpLib realTheory realLib RealArith
open abbrevsTheory expressionsTheory RealSimpsTheory
open abbrevsTheory expressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
open IntervalValidationTheory
val _ = new_theory "ErrorValidation";
val validErrorbound_def = Define `
validErrorbound e (absenv:analysisResult) =
......@@ -26,20 +29,43 @@ let (intv, err) = absenv e in
let (ive2, err2) = absenv f2 in
let errIve1 = widenInterval ive1 err1 in
let errIve2 = widenInterval ive2 err2 in
let upperBoundE1 = maxAbs ive1 in
let upperBoundE2 = maxAbs ive2 in
let upperBoundE1 = maxAbsFun ive1 in
let upperBoundE2 = maxAbsFun ive2 in
let theVal =
case op of
| Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * machineEpsilon) <= err
| Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * machineEpsilon) <= err
| Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * machineEpsilon) <= err
| Plus => err1 + err2 + (maxAbsFun (addInterval errIve1 errIve2) * machineEpsilon) <= err
| Sub => err1 + err2 + (maxAbsFun (subtractInterval errIve1 errIve2) * machineEpsilon) <= err
| Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbsFun (multInterval errIve1 errIve2) * machineEpsilon) <= err
| Div =>
let upperBoundInvE2 = maxAbs (invertInterval ive2) in
let upperBoundInvE2 = maxAbsFun (invertInterval ive2) in
let nodiv0_fl = (IVhi errIve2 < 0 \/ 0 < IVlo errIve2) in
if nodiv0_fl
then let minAbsIve2 = minAbs (errIve2) in
then let minAbsIve2 = minAbsFun (errIve2) in
let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in
(upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * machineEpsilon) <= err
(upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbsFun (divideInterval errIve1 errIve2) * machineEpsilon) <= err
else F
in rec /\ errPos /\ theVal`;
val err_always_positive = store_thm ("err_always_positive",
``!(e:real exp) (absenv:analysisResult) (iv:interval) (err:real).
(validErrorbound (e:real exp) (absenv:analysisResult)) /\ ((iv,err) = absenv e) ==>
0 <= err``,
once_rewrite_tac [validErrorbound_def] \\ rpt strip_tac \\
Cases_on `e` \\
qpat_assum `(iv,err) = absenv e` (fn thm => fs [GSYM thm]) \\
Cases_on `absenv e0` \\ Cases_on `absenv e'` \\ fs[]);
(**
val validErrorboundCorrectConstant = store_thm ("validErrorboundCorrectConstant",
``!(cenv:env) (absenv:analysisResult) (n:real) (nR:real) (nF:real) (e:real) (nlo:real) (nhi:real) (P:precond).
eval_exp 0 cenv P (Const n) nR /\
eval_exp machineEpsilon cenv P (Const n) nF /\
validErrorbound (Const n) absenv /\
validIntervalbounds (Const n) absenv P /\
(absenv (Const n) = ((nlo,nhi),e)) ==>
(abs (nR - nF)) <= e`,
``,
)
**)
val _ = export_theory();
......@@ -87,11 +87,11 @@ multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2`;
val divideInterval_def = Define `
divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)`;
val RmaxAbsFun_def = Define `
RmaxAbsFun iv = max (abs (FST iv)) (abs (SND iv))`;
val maxAbsFun_def = Define `
maxAbsFun iv = max (abs (FST iv)) (abs (SND iv))`;
val RminAbsFun_def = Define `
RminAbsFun iv = min (abs (FST iv)) (abs (SND iv))`;
val minAbsFun_def = Define `
minAbsFun iv = min (abs (FST iv)) (abs (SND iv))`;
val iv_ss = [IVlo_def, IVhi_def, valid_def, contained_def, isSupersetInterval_def,
pointInterval_def, validIntervalAdd_def,
......@@ -103,7 +103,7 @@ val iv_ss = [IVlo_def, IVhi_def, valid_def, contained_def, isSupersetInterval_de
invertInterval_def,
addInterval_def, subtractInterval_def,
multInterval_def, divideInterval_def,
RmaxAbsFun_def, RminAbsFun_def
maxAbsFun_def, minAbsFun_def
];
val contained_implies_valid = store_thm ("contained_implies_valid",
......@@ -403,11 +403,11 @@ fs[]);
(** Properties of the maxAbs function **)
val contained_leq_maxAbs = store_thm ("contained_leq_maxAbs",
``!a iv. contained a iv ==> abs a <= RmaxAbsFun iv``,
``!a iv. contained a iv ==> abs a <= maxAbsFun iv``,
rpt strip_tac\\ fs iv_ss \\ match_mp_tac maxAbs \\ fs []);
val contained_leq_maxAbs_neg_val = store_thm ("contained_leq_maxAbs_neg_val",
``!a iv. contained a iv ==> - a <= RmaxAbsFun iv``,
``!a iv. contained a iv ==> - a <= maxAbsFun iv``,
rpt strip_tac\\ fs iv_ss \\
`abs a <= max (abs (FST iv)) (abs (SND iv))` by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\
REAL_ASM_ARITH_TAC);
......
......@@ -10,6 +10,8 @@ open simpLib realTheory realLib RealArith
open abbrevsTheory expressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory IntervalArithTheory
val _ = new_theory "IntervalValidation";
val freeVars_def = Define `
(freeVars (Const n) = []) /\
(freeVars (Var v) = []) /\
......@@ -269,3 +271,5 @@ gen_tac \\ Induct_on `f` \\ once_rewrite_tac [eval_exp_cases] \\ rpt gen_tac \\
>- (qexists_tac `max4 (FST iv_f * (inv (SND iv_f')))
(FST iv_f * (inv (FST iv_f'))) (SND iv_f * (inv (SND iv_f'))) (SND iv_f * (inv (FST iv_f')))` \\
metis_tac []))));
val _ = export_theory();
......@@ -11,6 +11,10 @@ rpt strip_tac \\
`inv x < inv y <=> y < x` by MATCH_MP_TAC REAL_INV_LT_ANTIMONO \\ fs []\\
EQ_TAC \\ fs [REAL_LE_LT] \\ STRIP_TAC \\ fs [REAL_INV_INJ]);
val REAL_INV_LE_ANTIMONO_IMPR = store_thm ("REAL_INV_LE_ANTIMONO_IMPR",
``! x y. 0 < x /\ 0 < y /\ y <= x ==> inv x <= inv y``,
rpt strip_tac \\ fs[REAL_INV_LE_ANTIMONO]);
val REAL_MUL_LE_COMPAT_NEG_L = store_thm( "REAL_MUL_LE_COMPAT_NEG_L",
``!(a:real) b c. a <= &0 /\ b <= c ==> a * c <= a * b``,
rpt strip_tac \\
......
......@@ -54,7 +54,7 @@ and elim_exist thm =
fun inversion pattern cases_thm =
qpat_x_assum pattern
(fn thm => elim_exist (ONCE_REWRITE_RULE [cases_thm] thm) \\ try (qpat_x_assum `A /\ B` elim_conj));
(fn thm => elim_exist (ONCE_REWRITE_RULE [cases_thm] thm));
(* -- *)
val _ = set_trace"Goalstack.print_goal_at_top"0 handle HOL_ERR _ => set_trace"goalstack print goal at top"0
......
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