Skip to content
Snippets Groups Projects
Commit a273a862 authored by Heiko Becker's avatar Heiko Becker
Browse files

Make checker store actual error bound inferred

parent 5b8bf7ed
No related branches found
No related tags found
No related merge requests found
Pipeline #54795 passed
......@@ -189,10 +189,12 @@ Definition validateZerosLeqErr_def:
(ub + B * e))
in
if ~ (validBounds iv realZeros recordered (FST iv) realZeros (SND iv)) then
Invalid "Zeros not correctly spaced"
(Invalid "Zeros not correctly spaced", 0)
else if ~ (LENGTH realZeros = numZeros) then
Invalid "Did not find sufficient zeros"
else isValid (globalErr eps) "Bounding error too large"
(Invalid "Did not find sufficient zeros", 0)
else if globalErr eps
then (Valid, globalErr)
else (Invalid "Bounding error too large", 0)
End
(* Unused for new structure
......@@ -280,8 +282,8 @@ Proof
QED
Theorem validateZerosLeqErr_EVERY:
err errorp iv zeroList zeros.
validateZerosLeqErr errorp iv zeroList err zeros = Valid
err errorp iv zeroList zeros eps.
validateZerosLeqErr errorp iv zeroList err zeros = (Valid, eps)
let realZeros =
(findN zeros (λ(u,v). poly (diff errorp) u * poly (diff errorp) v 0)
zeroList)
......@@ -293,6 +295,7 @@ Theorem validateZerosLeqErr_EVERY:
Proof
gs[validateZerosLeqErr_def, isValid_def]
>> rpt gen_tac >> rpt (cond_cases_tac >> gs[])
>> disch_then kall_tac
>> qmatch_goalsub_abbrev_tac EVERY all_conds_pred realZeros
>> all_conds_pred =
λ x. (λ (u,v). FST iv u v SND iv) x
......@@ -330,10 +333,10 @@ Proof
QED
Theorem validateZerosLeqErr_sound:
deriv errorp iv zerosList zeros err.
deriv errorp iv zerosList zeros err eps.
deriv = diff errorp
{x | FST iv x x SND iv (poly deriv x = &0)} HAS_SIZE zeros
validateZerosLeqErr errorp iv zerosList err zeros = Valid
validateZerosLeqErr errorp iv zerosList err zeros = (Valid, eps)
x.
FST iv x x SND iv
abs(poly errorp x) err
......@@ -345,6 +348,7 @@ Proof
>> qpat_x_assum validateZerosLeqErr _ _ _ _ _ = _ mp_tac
>> gs[validateZerosLeqErr_def, isValid_def]
>> rpt (cond_cases_tac >> gs[])
>> disch_then kall_tac
>> pop_assum mp_tac
>> qmatch_goalsub_abbrev_tac computed_ub err
>> strip_tac >> irule REAL_LE_TRANS
......
......@@ -163,7 +163,7 @@ struct
Parse.Term validateZerosLeqErr ^poly ^dom ^zeroList ^eps ^numZeros
|> EVAL
val _ = save_thm ("validationThm", validationThm)
val _ = if Term.compare (rhs o concl $ validationThm, Valid) = EQUAL then ()
val _ = if Term.compare (rhs o concl $ validationThm |> pairSyntax.dest_pair |> fst, Valid) = EQUAL then ()
else raise ZeroLibErr "Failed to prove validity of zeros found by Sollya"
val resThm = (MATCH_MP (REWRITE_RULE [GSYM AND_IMP_INTRO] validateZerosLeqErr_sound) (GSYM polyDiff))
|> Q.SPEC (^lb, ^ub) |> SIMP_RULE std_ss []
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment