Commit a8f0e703 authored by Heiko Becker's avatar Heiko Becker

Fix checker removal also in HOL-Light

parent 1d92ab29
(**
Full Certtificate Checker.
Full Certificate Checker.
This function must be run on the daisy output.
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
......
needs "PreconditionValidation.hl";;
needs "IntervalValidation.hl";;
needs "ErrorValidation.hl";;
let CertificateChecker = define `
CertificateChecker (e:(real)exp) (absenv:analysisResult) (P:precond) =
(validIntervalbounds e absenv P /\ approximatesPrecond e absenv P /\ validErrorbound e absenv)`;;
(validIntervalbounds e absenv P /\ validErrorbound e absenv)`;;
let certificate_checking_is_sound = prove (
`!(e:(real)exp) (absenv:analysisResult) (P:precond) (cenv:env_ty) (vR:real) (vF:real).
......@@ -15,9 +14,9 @@ let certificate_checking_is_sound = prove (
abs (vR - vF) <= (SND (absenv e))`,
SIMP_TAC[CertificateChecker]
THEN intros "!e absenv P cenv vR vF; p_valid eval_real eval_float cert_true"
THEN destruct "cert_true" "validBounds validPrecond validError"
THEN pose_proof approximatesPrecond_sound "approx_precond"
[`e:(real)exp`; `absenv:analysisResult`; `P:precond`] ["validPrecond"]
THEN destruct "cert_true" "validBounds validError"
THEN pose_proof ivbounds_approximatesPrecond_sound "approx_precond"
[`e:(real)exp`; `absenv:analysisResult`; `P:precond`] ["validBounds"]
THEN SUBGOAL_TAC "absenv_e" `?ivlo ivhi err. (absenv:analysisResult) e = ((ivlo,ivhi),err)` [MESON_TAC[cases "prod"]]
THEN destruct "absenv_e" "@ivlo. @ivhi. @err. absenv_e"
THEN mp (validErrorbound_sound)
......
This diff is collapsed.
This diff is collapsed.
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