From 06ad54dec40fbf0bbee97243be5ceab57517eadb Mon Sep 17 00:00:00 2001
From: Heiko Becker <hbecker@mpi-sws.org>
Date: Tue, 12 May 2020 13:38:58 +0200
Subject: [PATCH] Fix bug in FMA evaluation, add some small lemmas
---
hol4/CertificateCheckerScript.sml | 8 +
hol4/CommandsScript.sml | 1 +
hol4/ErrorBoundsScript.sml | 16 +-
hol4/ErrorValidationScript.sml | 154 +++++++++--------
hol4/ExpressionsScript.sml | 2 +-
hol4/FPRangeValidatorScript.sml | 37 ++--
hol4/IEEE_connectionScript.sml | 247 +++++++++++++++++++++------
hol4/IntervalValidationScript.sml | 167 +++++++++---------
hol4/RealIntervalInferenceScript.sml | 2 +-
hol4/TypeValidatorScript.sml | 31 ++++
10 files changed, 428 insertions(+), 237 deletions(-)
diff --git a/hol4/CertificateCheckerScript.sml b/hol4/CertificateCheckerScript.sml
index 70de241d..96783cbe 100644
--- a/hol4/CertificateCheckerScript.sml
+++ b/hol4/CertificateCheckerScript.sml
@@ -150,4 +150,12 @@ Proof
\\ fs[]
QED
+Theorem CertificateCheckerCmd_Gamma_is_getValidMapCmd:
+ CertificateCheckerCmd f A P dVars = SOME Gamma ⇒
+ getValidMapCmd dVars f FloverMapTree_empty = Succes Gamma
+Proof
+ fs[CertificateCheckerCmd_def]
+ \\ rpt (TOP_CASE_TAC \\ fs[])
+QED
+
val _ = export_theory();
diff --git a/hol4/CommandsScript.sml b/hol4/CommandsScript.sml
index c7b2e9e5..b1c23388 100644
--- a/hol4/CommandsScript.sml
+++ b/hol4/CommandsScript.sml
@@ -30,6 +30,7 @@ val toREvalCmd_def = Define `
val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
(!m m' x e s E v res Gamma.
eval_expr E Gamma e v m /\
+ Gamma (Var x) = SOME m ∧
bstep s (updEnv x v E) Gamma res m' ==>
bstep (Let m x e s) E Gamma res m') /\
(!m e E v Gamma.
diff --git a/hol4/ErrorBoundsScript.sml b/hol4/ErrorBoundsScript.sml
index 4d9da554..e129830a 100644
--- a/hol4/ErrorBoundsScript.sml
+++ b/hol4/ErrorBoundsScript.sml
@@ -293,8 +293,8 @@ Proof
QED
val float_fma_tac =
- `e1R + e2R * e3R + -((e1F + e2F * e3F) * (1 + deltaF)) =
- (e1R + e2R * e3R + -(e1F + e2F * e3F)) + (- (e1F + e2F * e3F) * deltaF)`
+ `e1R * e2R + e3R + -((1 + deltaF) * (e1F * e2F + e3F)) =
+ (e1R * e2R + e3R + -(e1F * e2F + e3F)) + (- (e1F * e2F + e3F) * deltaF)`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ triangle_tac
@@ -324,8 +324,8 @@ Theorem fma_abs_err_bounded:
abs (e2R - e2F) <= err2 /\
abs (e3R - e3F) <= err3 ==>
abs (vR - vF) <=
- abs ((e1R - e1F) + (e2R * e3R - e2F * e3F)) +
- computeError (e1F + e2F * e3F) m
+ abs ((e1R * e2R - e1F * e2F) + (e3R - e3F)) +
+ computeError (e1F * e2F + e3F) m
Proof
rpt strip_tac \\ fs[toREval_def]
\\ inversion `eval_expr E1 _ (Fma _ _ _) _ _` eval_expr_cases
@@ -350,15 +350,15 @@ Proof
\\ Cases_on `mF`
\\ fs[computeError_def, perturb_def]
\\ rewrite_tac[real_sub]
- >- (`e1R + e2R * e3R + - (e1F + e2F * e3F) =
- e1R + - e1F + (e2R * e3R + - (e2F * e3F))`
+ >- (`e1R * e2R + e3R + - (e1F * e2F + e3F) =
+ (e1R * e2R + - (e1F * e2F) + (e3R + - e3F))`
by REAL_ASM_ARITH_TAC
\\ simp[])
>- (float_fma_tac)
>- (float_fma_tac)
>- (float_fma_tac)
- \\ `e1R + e2R * e3R + -(e1F + e2F * e3F + deltaF) =
- (e1R + e2R * e3R + - (e1F + e2F * e3F)) + - deltaF`
+ \\ `e1R * e2R + e3R + -(e1F * e2F + e3F + deltaF) =
+ (e1R * e2R + e3R + - (e1F * e2F + e3F)) + - deltaF`
by REAL_ASM_ARITH_TAC
\\ simp[]
\\ triangle_tac
diff --git a/hol4/ErrorValidationScript.sml b/hol4/ErrorValidationScript.sml
index c0ba05f0..5cef7fa1 100644
--- a/hol4/ErrorValidationScript.sml
+++ b/hol4/ErrorValidationScript.sml
@@ -98,10 +98,10 @@ val validErrorbound_def = Define `
upperBoundE1 = maxAbs ive1;
upperBoundE2 = maxAbs ive2;
upperBoundE3 = maxAbs ive3;
- errIntv_prod = multInterval errIve2 errIve3;
- mult_error_bound = (upperBoundE2 * err3 + upperBoundE3 * err2 + err2 * err3);
- mAbs = maxAbs (addInterval errIve1 errIntv_prod) in
- err1 + mult_error_bound + computeError mAbs m <= err
+ errIntv_prod = multInterval errIve1 errIve2;
+ mult_error_bound = (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2);
+ mAbs = maxAbs (addInterval errIntv_prod errIve3 ) in
+ mult_error_bound + err3 + computeError mAbs m <= err
|_, _, _ => F
else F)
| Downcast m1 e1 =>
@@ -2100,35 +2100,36 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
\\ assume_tac (REWRITE_RULE [contained_def] interval_division_valid)
\\ fs[contained_def, widenInterval_def, noDivzero_def]);
-val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
- ``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr) (e3: real expr)
- (nR nR1 nR2 nR3 nF nF1 nF2 nF3:real) (e err1 err2 err3:real)
- (alo ahi e1lo e1hi e2lo e2hi e3lo e3hi :real) dVars m m1 m2 m3 Gamma.
- eval_Real E1 Gamma e1 nR1 /\
- eval_Real E1 Gamma e2 nR2 /\
- eval_Real E1 Gamma e3 nR3 /\
- eval_Real E1 Gamma (Fma e1 e2 e3) nR /\
- eval_Fin E2 Gamma e1 nF1 m1 /\
- eval_Fin E2 Gamma e2 nF2 m2 /\
- eval_Fin E2 Gamma e3 nF3 m3 /\
- eval_expr (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)))
- (updDefVars (Fma (Var 1) (Var 2) (Var 3)) m
- (updDefVars (Var 3) m3
- (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma)))))
- (Fma (Var 1) (Var 2) (Var 3)) nF m /\
- validErrorbound (Fma e1 e2 e3) Gamma A dVars /\
- (e1lo <= nR1 /\ nR1 <= e1hi) /\
- (e2lo <= nR2 /\ nR2 <= e2hi) /\
- (e3lo <= nR3 /\ nR3 <= e3hi) /\
- FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
- FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
- FloverMapTree_find e3 A = SOME ((e3lo, e3hi), err3) /\
- FloverMapTree_find (Fma e1 e2 e3) A = SOME ((alo, ahi), e) /\
- FloverMapTree_find (Fma e1 e2 e3) Gamma = SOME m /\
- abs (nR1 - nF1) <= err1 /\
- abs (nR2 - nF2) <= err2 /\
- abs (nR3 - nF3) <= err3 ==>
- abs (nR - nF) <= e``,
+Theorem validErrorboundCorrectFma:
+ !(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr) (e3: real expr)
+ (nR nR1 nR2 nR3 nF nF1 nF2 nF3:real) (e err1 err2 err3:real)
+ (alo ahi e1lo e1hi e2lo e2hi e3lo e3hi :real) dVars m m1 m2 m3 Gamma.
+ eval_Real E1 Gamma e1 nR1 /\
+ eval_Real E1 Gamma e2 nR2 /\
+ eval_Real E1 Gamma e3 nR3 /\
+ eval_Real E1 Gamma (Fma e1 e2 e3) nR /\
+ eval_Fin E2 Gamma e1 nF1 m1 /\
+ eval_Fin E2 Gamma e2 nF2 m2 /\
+ eval_Fin E2 Gamma e3 nF3 m3 /\
+ eval_expr (updEnv 3 nF3 (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)))
+ (updDefVars (Fma (Var 1) (Var 2) (Var 3)) m
+ (updDefVars (Var 3) m3
+ (updDefVars (Var 2) m2 (updDefVars (Var 1) m1 (toRExpMap Gamma)))))
+ (Fma (Var 1) (Var 2) (Var 3)) nF m /\
+ validErrorbound (Fma e1 e2 e3) Gamma A dVars /\
+ (e1lo <= nR1 /\ nR1 <= e1hi) /\
+ (e2lo <= nR2 /\ nR2 <= e2hi) /\
+ (e3lo <= nR3 /\ nR3 <= e3hi) /\
+ FloverMapTree_find e1 A = SOME ((e1lo, e1hi), err1) /\
+ FloverMapTree_find e2 A = SOME ((e2lo, e2hi), err2) /\
+ FloverMapTree_find e3 A = SOME ((e3lo, e3hi), err3) /\
+ FloverMapTree_find (Fma e1 e2 e3) A = SOME ((alo, ahi), e) /\
+ FloverMapTree_find (Fma e1 e2 e3) Gamma = SOME m /\
+ abs (nR1 - nF1) <= err1 /\
+ abs (nR2 - nF2) <= err2 /\
+ abs (nR3 - nF3) <= err3 ==>
+ abs (nR - nF) <= e
+Proof
fs [toREval_def]
\\ rpt strip_tac \\ simp[Once toREval_def]
\\ Flover_compute ``validErrorbound`` \\ fs [] \\ rveq
@@ -2142,8 +2143,8 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
by (irule err_always_positive
\\ rpt (asm_exists_tac \\ fs[]))
\\ irule REAL_LE_TRANS
- \\ qexists_tac `abs ((nR1 - nF1) + (nR2 * nR3 - nF2 * nF3)) +
- computeError (nF1 + nF2 * nF3) m`
+ \\ qexists_tac `abs ((nR1 * nR2 - nF1 * nF2) + (nR3 - nF3)) +
+ computeError (nF1 * nF2 + nF3) m`
\\ conj_tac
>- (irule fma_abs_err_bounded \\ rpt conj_tac
\\ rpt (find_exists_tac \\ fs[toREval_def]))
@@ -2153,6 +2154,10 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
>- (irule triangle_trans \\ fs[REAL_ABS_TRIANGLE]
\\ irule REAL_LE_ADD2 \\ fs[]
\\ irule multiplicationErrorBounded \\ fs[])
+ \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
+ by (irule distance_gives_iv
+ \\ qexists_tac `nR1` \\ conj_tac
+ \\ simp[contained_def, IVlo_def, IVhi_def])
\\ `contained nF2 (widenInterval (e2lo,e2hi) err2)`
by (irule distance_gives_iv
\\ qexists_tac `nR2` \\ conj_tac
@@ -2161,22 +2166,19 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
by (irule distance_gives_iv
\\ qexists_tac `nR3` \\ conj_tac
\\ simp[contained_def, IVlo_def, IVhi_def])
- \\ `contained (nF2 * nF3)
- (multInterval (widenInterval (e2lo, e2hi) err2)
- (widenInterval (e3lo, e3hi) err3))`
+ \\ `contained (nF1 * nF2)
+ (multInterval (widenInterval (e1lo, e1hi) err1)
+ (widenInterval (e2lo, e2hi) err2))`
by (irule
(ONCE_REWRITE_RULE [validIntervalMult_def] interval_multiplication_valid)
\\ conj_tac \\ simp[])
- \\ `contained nF1 (widenInterval (e1lo,e1hi) err1)`
- by (irule distance_gives_iv
- \\ qexists_tac `nR1` \\ conj_tac
- \\ simp[contained_def])
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
\\ PairCases_on `iv` \\ irule computeError_up
\\ unabbrev_all_tac \\ fs[maxAbs_def]
\\ irule maxAbs
\\ assume_tac (REWRITE_RULE [validIntervalAdd_def, contained_def] interval_addition_valid)
- \\ fs[contained_def, widenInterval_def, IVlo_def, IVhi_def, noDivzero_def]);
+ \\ fs[contained_def, widenInterval_def, IVlo_def, IVhi_def, noDivzero_def]
+QED
val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding",
``!(E1 E2:env) (A:analysisResult) (e:real expr)
@@ -2543,21 +2545,21 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ irule Var_load
\\ fs[updDefVars_def, updEnv_def]));
-val validErrorboundCmd_gives_eval = store_thm (
- "validErrorboundCmd_gives_eval",
- ``!(f:real cmd) (A:analysisResult) (E1 E2:env)
- (outVars fVars dVars:num_set) (vR elo ehi err:real)
- (m:mType) Gamma.
- validTypesCmd f Gamma /\
- approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
- ssa f (union fVars dVars) outVars /\
- ((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\
- bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
- validErrorboundCmd f Gamma A dVars /\
- validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
- FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
- ?vF m.
- bstep f E2 (toRExpMap Gamma) vF m``,
+Theorem validErrorboundCmd_gives_eval:
+ !(f:real cmd) (A:analysisResult) (E1 E2:env)
+ (outVars fVars dVars:num_set) (vR elo ehi err:real)
+ (m:mType) Gamma.
+ validTypesCmd f Gamma /\
+ approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
+ ssa f (union fVars dVars) outVars /\
+ ((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\
+ bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
+ validErrorboundCmd f Gamma A dVars /\
+ validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
+ FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
+ ?vF m.
+ bstep f E2 (toRExpMap Gamma) vF m
+Proof
Induct_on `f` \\ rpt strip_tac
\\ Flover_compute ``validErrorboundCmd``
\\ rveq \\ fs[Once toREvalCmd_def]
@@ -2618,7 +2620,7 @@ val validErrorboundCmd_gives_eval = store_thm (
\\ fs[Once toREvalCmd_def])
\\ qexistsl_tac [`vF_res`, `m_res`]
\\ fs[bstep_cases]
- \\ qexists_tac `vF` \\ rveq \\ fs[])
+ \\ qexists_tac `vF` \\ rveq \\ fs[toRExpMap_def])
>- (fs[getRetExp_def]
\\ inversion `ssa _ _ _` ssa_cases
\\ inversion `bstep _ _ _ _ _` bstep_cases
@@ -2628,21 +2630,23 @@ val validErrorboundCmd_gives_eval = store_thm (
by (irule (REWRITE_RULE [eval_Fin_def] validErrorbound_sound)
\\ fs[validTypesCmd_def, validRangesCmd_def, freeVars_def]
\\ rpt (find_exists_tac \\ fs[]))
- \\ qexistsl_tac [`vF`, `m`] \\ fs[]));
+ \\ qexistsl_tac [`vF`, `m`] \\ fs[])
+QED
-val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
- ``!(f:real cmd) (A:analysisResult) (E1 E2:env)
- (outVars fVars dVars:num_set) (vR vF elo ehi err:real) (m:mType) Gamma.
- validTypesCmd f Gamma /\
- approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
- ssa f (union fVars dVars) outVars /\
- ((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\
- bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
- bstep f E2 (toRExpMap Gamma) vF m /\
- validErrorboundCmd f Gamma A dVars /\
- validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
- FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
- abs (vR - vF) <= err``,
+Theorem validErrorboundCmd_sound:
+ !(f:real cmd) (A:analysisResult) (E1 E2:env)
+ (outVars fVars dVars:num_set) (vR vF elo ehi err:real) (m:mType) Gamma.
+ validTypesCmd f Gamma /\
+ approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 /\
+ ssa f (union fVars dVars) outVars /\
+ ((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars) /\
+ bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
+ bstep f E2 (toRExpMap Gamma) vF m /\
+ validErrorboundCmd f Gamma A dVars /\
+ validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
+ FloverMapTree_find (getRetExp f) A = SOME ((elo,ehi),err) ==>
+ abs (vR - vF) <= err
+Proof
Induct_on `f` \\ rpt strip_tac
\\ Flover_compute ``validErrorboundCmd``
\\ rveq \\ fs[Once toREvalCmd_def]
@@ -2668,7 +2672,6 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
>- (fs[Once toREvalCmd_def])
>- (irule approxEnvUpdBound \\ rpt conj_tac
\\ fs[]
- >- (fs[Once validTypesCmd_def] \\ fs[toRExpMap_def])
>- (Cases_on `lookup n (union fVars dVars)` \\ fs [domain_lookup])
\\ qspecl_then
[`e`, `E1`, `E2`, `A`, `vr`, `err_e`, `FST (iv_e)`,
@@ -2688,6 +2691,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
destruct validErrorbound_sound
\\ fs[freeVars_def, getRetExp_def, Once validTypesCmd_def, Once validRangesCmd_def]
\\ first_x_assum irule \\ fs[]
- \\ find_exists_tac \\ fs[]));
+ \\ find_exists_tac \\ fs[])
+QED
val _ = export_theory();
diff --git a/hol4/ExpressionsScript.sml b/hol4/ExpressionsScript.sml
index fa5d871d..549eeeb5 100644
--- a/hol4/ExpressionsScript.sml
+++ b/hol4/ExpressionsScript.sml
@@ -57,7 +57,7 @@ val _ = Datatype `
Errors are added on the exprression evaluation level later
**)
val evalFma_def = Define `
- evalFma v1 v2 v3 = evalBinop Plus v1 (evalBinop Mult v2 v3)`;
+ evalFma v1 v2 v3 = evalBinop Plus (evalBinop Mult v1 v2) v3`;
val toREval_def = Define `
(toREval (Var n) = Var n) /\
diff --git a/hol4/FPRangeValidatorScript.sml b/hol4/FPRangeValidatorScript.sml
index 6a0614c1..ba69e2d4 100644
--- a/hol4/FPRangeValidatorScript.sml
+++ b/hol4/FPRangeValidatorScript.sml
@@ -167,22 +167,22 @@ val FPRangeValidator_sound = store_thm (
\\ fs[] \\ rveq \\ fs[])
\\ solve_tac);
-val FPRangeValidatorCmd_sound = store_thm (
- "FPRangeValidatorCmd_sound",
- ``!f E1 E2 Gamma v vR m A fVars dVars outVars.
- approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ∧
- ssa f (union fVars dVars) outVars /\
- bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR m /\
- bstep f E2 (toRExpMap Gamma) v m ∧
- validTypesCmd f Gamma /\
- validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
- validErrorboundCmd f Gamma A dVars ∧
- FPRangeValidatorCmd f A Gamma dVars ∧
- domain (freeVars f) DIFF domain dVars ⊆ domain fVars ∧
- (!(v:num). v IN domain dVars ==>
- (?vF m. E2 v = SOME vF /\ FloverMapTree_find (Var v) Gamma = SOME m
- /\ validFloatValue vF m)) ==>
- validFloatValue v m``,
+Theorem FPRangeValidatorCmd_sound:
+ !f E1 E2 Gamma v vR m A fVars dVars outVars.
+ approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ∧
+ ssa f (union fVars dVars) outVars /\
+ bstep (toREvalCmd f) E1 (toRTMap (toRExpMap Gamma)) vR m /\
+ bstep f E2 (toRExpMap Gamma) v m ∧
+ validTypesCmd f Gamma /\
+ validRangesCmd f A E1 (toRTMap (toRExpMap Gamma)) /\
+ validErrorboundCmd f Gamma A dVars ∧
+ FPRangeValidatorCmd f A Gamma dVars ∧
+ domain (freeVars f) DIFF domain dVars ⊆ domain fVars ∧
+ (!(v:num). v IN domain dVars ==>
+ (?vF m. E2 v = SOME vF /\ FloverMapTree_find (Var v) Gamma = SOME m
+ /\ validFloatValue vF m)) ==>
+ validFloatValue v m
+Proof
Induct
\\ simp[Once toREvalCmd_def, Once FPRangeValidatorCmd_def,
Once freeVars_def]
@@ -224,8 +224,6 @@ val FPRangeValidatorCmd_sound = store_thm (
impl_subgoal_tac)
>- (fs[] \\ rpt conj_tac
>- (irule approxEnvUpdBound \\ fs[lookup_NONE_domain]
- \\ conj_tac
- >- (fs[Once validTypesCmd_def, toRExpMap_def])
\\ first_x_assum (qspecl_then [`vF`, `m`] irule)
\\ qexists_tac `m` \\ fs[])
>- (irule ssa_equal_set
@@ -285,6 +283,7 @@ val FPRangeValidatorCmd_sound = store_thm (
\\ rpt (inversion `bstep (Ret _) _ _ _ _` bstep_cases)
\\ drule FPRangeValidator_sound
\\ rpt (disch_then drule)
- \\ fs[Once validTypesCmd_def, Once validRangesCmd_def]);
+ \\ fs[Once validTypesCmd_def, Once validRangesCmd_def]
+QED
val _ = export_theory();
diff --git a/hol4/IEEE_connectionScript.sml b/hol4/IEEE_connectionScript.sml
index 7bca265d..e36395ae 100644
--- a/hol4/IEEE_connectionScript.sml
+++ b/hol4/IEEE_connectionScript.sml
@@ -41,8 +41,9 @@ val eval_expr_float_def = Define `
| Div => SOME (fp64_div dmode v1 v2))
| _, _ => NONE)) /\
(eval_expr_float (Fma e1 e2 e3) E =
- (case (eval_expr_float e1 E), (eval_expr_float e2 E), (eval_expr_float e2 E) of
- | _, _, _ => NONE)) /\
+ (case (eval_expr_float e1 E), (eval_expr_float e2 E), (eval_expr_float e3 E) of
+ | SOME v1, SOME v2, SOME v3 => SOME (fp64_mul_add roundTiesToEven v1 v2 v3)
+ | _, _, _ => NONE)) /\
(eval_expr_float (Downcast m e) E = NONE)`;
val bstep_float_def = Define `
@@ -93,7 +94,7 @@ val eval_expr_valid_def = Define `
in
optionLift e3_res
(\ v3. let v3_real = float_to_real (fp64_to_float v3) in
- F)
+ normal_or_zero (evalFma v1_real v2_real v3_real))
T)
T)
T)) /\
@@ -530,29 +531,30 @@ val typing_cmd_64bit = store_thm (
\\ rpt strip_tac \\ fs[]
\\ res_tac);
-val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
- ``!(e:word64 expr) E1 E2 E2_real Gamma vR A fVars dVars.
- (!x. (toREnv E2) x = E2_real x) /\
- validTypes (toRExp e) Gamma /\
- approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real /\
- validRanges (toRExp e) A E1 (toRTMap (toRExpMap Gamma)) /\
- validErrorbound (toRExp e) Gamma A dVars /\
- FPRangeValidator (toRExp e) A Gamma dVars /\
- eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e) vR M64 /\
- domain (usedVars (toRExp e)) DIFF domain dVars ⊆ domain fVars ∧
- is64BitEval (toRExp e) /\
- is64BitEnv Gamma /\
- noDowncast (toRExp e) /\
- eval_expr_valid e E2 /\
- (∀v.
- v ∈ domain dVars ⇒
- ∃vF m.
- (E2_real v = SOME vF ∧ FloverMapTree_find (Var v) Gamma = SOME m ∧
- validFloatValue vF m)) ==>
- ?v.
- eval_expr_float e E2 = SOME v /\
- eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e)
- (float_to_real (fp64_to_float v)) M64``,
+Theorem eval_expr_gives_IEEE:
+ !(e:word64 expr) E1 E2 E2_real Gamma vR A fVars dVars.
+ (!x. (toREnv E2) x = E2_real x) /\
+ validTypes (toRExp e) Gamma /\
+ approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real /\
+ validRanges (toRExp e) A E1 (toRTMap (toRExpMap Gamma)) /\
+ validErrorbound (toRExp e) Gamma A dVars /\
+ FPRangeValidator (toRExp e) A Gamma dVars /\
+ eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e) vR M64 /\
+ domain (usedVars (toRExp e)) DIFF domain dVars ⊆ domain fVars ∧
+ is64BitEval (toRExp e) /\
+ is64BitEnv Gamma /\
+ noDowncast (toRExp e) /\
+ eval_expr_valid e E2 /\
+ (∀v.
+ v ∈ domain dVars ⇒
+ ∃vF m.
+ (E2_real v = SOME vF ∧ FloverMapTree_find (Var v) Gamma = SOME m ∧
+ validFloatValue vF m)) ==>
+ ?v.
+ eval_expr_float e E2 = SOME v /\
+ eval_expr (toREnv E2) (toRExpMap Gamma) (toRExp e)
+ (float_to_real (fp64_to_float v)) M64
+Proof
Induct_on `e` \\ rewrite_tac[toRExp_def] \\ rpt strip_tac
\\ inversion `eval_expr _ _ _ _ _` eval_expr_cases
\\ once_rewrite_tac [eval_expr_float_def]
@@ -1059,34 +1061,168 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
- \\ fs[optionLift_def]));
+ \\ rename1 ‘eval_expr_float e1 E2 = SOME vF1’
+ \\ rename1 ‘eval_expr_float e2 E2 = SOME vF2’
+ \\ rename1 ‘eval_expr_float e3 E2 = SOME vF3’
+ \\ `validFloatValue
+ (evalFma (float_to_real (fp64_to_float vF1))
+ (float_to_real (fp64_to_float vF2))
+ (float_to_real (fp64_to_float vF3))) M64`
+ by (drule FPRangeValidator_sound
+ \\ disch_then
+ (qspecl_then
+ [`(Fma (toRExp e1) (toRExp e2) (toRExp e3))`,
+ `evalFma (float_to_real (fp64_to_float vF1))
+ (float_to_real (fp64_to_float vF2))
+ (float_to_real (fp64_to_float vF3))`,
+ `M64`] irule)
+ \\ fs[]
+ \\ qexistsl_tac [`e1`, `e2`, ‘e3’] \\ fs[]
+ \\ rpt conj_tac
+ >- (simp[Once validTypes_def] \\ first_x_assum MATCH_ACCEPT_TAC)
+ >- (simp[Once validRanges_def] \\ find_exists_tac \\ fs[]
+ \\ fs[] \\ rveq \\ fs[])
+ \\ irule eval_eq_env
+ \\ find_exists_tac \\ fs[eval_expr_cases]
+ \\ qexistsl_tac [`M64`, `M64`, ‘M64’, `float_to_real (fp64_to_float vF1)`,
+ `float_to_real (fp64_to_float vF2)`,
+ `float_to_real (fp64_to_float vF3)`, `0:real`]
+ \\ fs[perturb_def, evalFma_def, mTypeToR_pos])
+ \\ `validFloatValue (float_to_real (fp64_to_float vF1)) M64`
+ by (drule FPRangeValidator_sound
+ \\ disch_then
+ (qspecl_then
+ [`toRExp e1`, `float_to_real (fp64_to_float vF1)`,
+ `M64`] irule)
+ \\ fs[]
+ \\ qexistsl_tac [`e1`] \\ fs[]
+ \\ rpt conj_tac
+ >- (rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
+ \\ fs[domain_union, DIFF_DEF, SUBSET_DEF, Once usedVars_def])
+ >- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
+ \\ fs[] \\ rveq
+ \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
+ \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
+ >- (Flover_compute ``validErrorbound``)
+ \\ irule eval_eq_env
+ \\ find_exists_tac \\ fs[])
+ \\ `validFloatValue (float_to_real (fp64_to_float vF2)) M64`
+ by (drule FPRangeValidator_sound
+ \\ disch_then
+ (qspecl_then
+ [`toRExp e2`, `float_to_real (fp64_to_float vF2)`,
+ `M64`] irule)
+ \\ fs[]
+ \\ qexists_tac `e2` \\ fs[]
+ \\ rpt conj_tac
+ >- (rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
+ \\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
+ >- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
+ \\ fs[] \\ rveq
+ \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
+ \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
+ >- (Flover_compute ``validErrorbound``)
+ \\ irule eval_eq_env
+ \\ find_exists_tac \\ fs[])
+ \\ `validFloatValue (float_to_real (fp64_to_float vF3)) M64`
+ by (drule FPRangeValidator_sound
+ \\ disch_then
+ (qspecl_then
+ [`toRExp e3`, `float_to_real (fp64_to_float vF3)`,
+ `M64`] irule)
+ \\ fs[]
+ \\ qexists_tac `e3` \\ fs[]
+ \\ rpt conj_tac
+ >- (rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
+ \\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
+ >- (rw_thm_asm `FPRangeValidator _ _ _ _` FPRangeValidator_def
+ \\ fs[] \\ rveq
+ \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) A = _`
+ \\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
+ >- (Flover_compute ``validErrorbound``)
+ \\ irule eval_eq_env
+ \\ find_exists_tac \\ fs[])
+ \\ fs[optionLift_def, normal_or_zero_def]
+ \\ simp[Once eval_expr_cases, PULL_EXISTS]
+ \\ rewrite_tac [CONJ_ASSOC]
+ \\ ntac 3 (once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs[])
+ \\ fs[evalFma_def, evalBinop_def, fp64_mul_add_def, fp64_to_float_float_to_fp64]
+ >- (
+ `normal (evalFma (float_to_real (fp64_to_float vF1))
+ (float_to_real (fp64_to_float vF2))
+ (float_to_real (fp64_to_float vF3))) M64`
+ by (
+ rw_thm_asm `validFloatValue (_ + _) _` validFloatValue_def
+ \\ fs[normal_def, denormal_def, evalFma_def, evalBinop_def]
+ >- (
+ `abs (float_to_real (fp64_to_float vF1) *
+ float_to_real (fp64_to_float vF2) + float_to_real (fp64_to_float vF3)) <
+ abs (float_to_real (fp64_to_float vF1) *
+ float_to_real (fp64_to_float vF2) + float_to_real (fp64_to_float vF3))`
+ suffices_by (fs[])
+ \\ irule REAL_LTE_TRANS
+ \\ asm_exists_tac \\ fs[])
+ \\ qpat_x_assum `_ + _ = 0` (fn thm => fs[thm])
+ \\ fs[maxValue_def, maxExponent_def])
+ \\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
+ `(fp64_to_float vF2):(52,11) float`,
+ `(fp64_to_float vF3):(52,11) float`]
+ impl_subgoal_tac
+ float_mul_add_relative
+ >- (rpt conj_tac
+ \\ fs[validFloatValue_def,
+ normalTranslatedValue_implies_finiteness,
+ denormalTranslatedValue_implies_finiteness,
+ normalValue_implies_normalization,
+ GSYM float_is_zero_to_real, float_is_finite, evalFma_def, evalBinop_def])
+ \\ fs[dmode_def]
+ \\ fs[perturb_def]
+ \\ qexistsl_tac [`e`]
+ \\ pop_assum (rewrite_tac o single)
+ \\ fs[perturb_def, evalBinop_def]
+ \\ fs[mTypeToR_def])
+ (* result = 0 *)
+ >- (IMP_RES_TAC validValue_gives_float_value
+ \\ fs[REAL_LNEG_UNIQ, evalFma_def, evalBinop_def]
+ \\ fs[fp64_add_def, dmode_def, fp64_mul_def, fp64_to_float_float_to_fp64]
+ \\ fs[float_mul_add_def, float_round_with_flags_def]
+ \\ qexistsl_tac [`0:real`]
+ \\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
+ \\ fs[float_is_nan_def, float_is_infinite_def]
+ \\ `2 * abs (0:real) <= ulp (:52 #11)`
+ by (fs[REAL_ABS_0, ulp_def, ULP_def, REAL_OF_NUM_POW]
+ \\ once_rewrite_tac [real_div]
+ \\ irule REAL_LE_MUL \\ fs[]
+ \\ irule REAL_LE_INV \\ fs[])
+ \\ fs[float_to_real_round_zero_is_zero]))
+QED
-val bstep_gives_IEEE = store_thm (
- "bstep_gives_IEEE",
- ``!(f:word64 cmd) E1 E2 E2_real Gamma vR vF A fVars dVars outVars.
- (!x. (toREnv E2) x = E2_real x) /\
- approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real /\
- ssa (toRCmd f) (union fVars dVars) outVars /\
- validTypesCmd (toRCmd f) Gamma /\
- validRangesCmd (toRCmd f) A E1 (toRTMap (toRExpMap Gamma)) /\
- validErrorboundCmd (toRCmd f) Gamma A dVars /\
- FPRangeValidatorCmd (toRCmd f) A Gamma dVars /\
- bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
- bstep (toRCmd f) (toREnv E2) (toRExpMap Gamma) vF M64 /\
- domain (freeVars (toRCmd f)) DIFF domain dVars ⊆ domain fVars ∧
- is64BitBstep (toRCmd f) /\
- is64BitEnv Gamma /\
- noDowncastFun (toRCmd f) /\
- bstep_valid f E2 /\
- (∀v.
- v ∈ domain dVars ⇒
- ∃vF m.
- (E2_real v = SOME vF ∧ FloverMapTree_find (Var v) Gamma = SOME m ∧
- validFloatValue vF m)) ==>
- ?v.
- bstep_float f E2 = SOME v /\
- bstep (toRCmd f) (toREnv E2) (toRExpMap Gamma)
- (float_to_real (fp64_to_float v)) M64``,
+Theorem bstep_gives_IEEE:
+ !(f:word64 cmd) E1 E2 E2_real Gamma vR vF A fVars dVars outVars.
+ (!x. (toREnv E2) x = E2_real x) /\
+ approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real /\
+ ssa (toRCmd f) (union fVars dVars) outVars /\
+ validTypesCmd (toRCmd f) Gamma /\
+ validRangesCmd (toRCmd f) A E1 (toRTMap (toRExpMap Gamma)) /\
+ validErrorboundCmd (toRCmd f) Gamma A dVars /\
+ FPRangeValidatorCmd (toRCmd f) A Gamma dVars /\
+ bstep (toREvalCmd (toRCmd f)) E1 (toRTMap (toRExpMap Gamma)) vR REAL /\
+ bstep (toRCmd f) (toREnv E2) (toRExpMap Gamma) vF M64 /\
+ domain (freeVars (toRCmd f)) DIFF domain dVars ⊆ domain fVars ∧
+ is64BitBstep (toRCmd f) /\
+ is64BitEnv Gamma /\
+ noDowncastFun (toRCmd f) /\
+ bstep_valid f E2 /\
+ (∀v.
+ v ∈ domain dVars ⇒
+ ∃vF m.
+ (E2_real v = SOME vF ∧ FloverMapTree_find (Var v) Gamma = SOME m ∧
+ validFloatValue vF m)) ==>
+ ?v.
+ bstep_float f E2 = SOME v /\
+ bstep (toRCmd f) (toREnv E2) (toRExpMap Gamma)
+ (float_to_real (fp64_to_float v)) M64
+Proof
Induct_on `f`
\\ simp [toRCmd_def, Once toREvalCmd_def, is64BitBstep_def,
noDowncastFun_def, bstep_valid_def]
@@ -1245,7 +1381,7 @@ val bstep_gives_IEEE = store_thm (
\\ irule eval_eq_env
\\ asm_exists_tac \\ fs[]))
\\ fs[]
- \\ irule let_b \\ find_exists_tac
+ \\ irule let_b \\ fs[toRExpMap_def] \\ find_exists_tac
\\ fs[] \\ irule bstep_eq_env
\\ find_exists_tac \\ fs[]
\\ strip_tac \\ fs[toREnv_def, updEnv_def, updFlEnv_def]
@@ -1256,7 +1392,8 @@ val bstep_gives_IEEE = store_thm (
>- (find_exists_tac \\ fs[])
\\ qexistsl_tac [`A`, `E1`, `dVars`, `fVars`]
\\ rpt conj_tac
- \\ fs[freeVars_def, Once FPRangeValidatorCmd_def, validRangesCmd_def]));
+ \\ fs[freeVars_def, Once FPRangeValidatorCmd_def, validRangesCmd_def])
+QED
val found_tac = TRY (last_x_assum irule \\ find_exists_tac \\ fs[] \\ FAIL_TAC "")
\\ first_x_assum irule \\ find_exists_tac \\ fs[];
diff --git a/hol4/IntervalValidationScript.sml b/hol4/IntervalValidationScript.sml
index 6f707a89..f718ca03 100644
--- a/hol4/IntervalValidationScript.sml
+++ b/hol4/IntervalValidationScript.sml
@@ -87,7 +87,7 @@ val validIntervalbounds_def = Define `
case FloverMapTree_find f1 absenv, FloverMapTree_find f2 absenv,
FloverMapTree_find f3 absenv of
| SOME (iv1, _), SOME (iv2, _), SOME (iv3, _) =>
- let new_iv = addInterval iv1 (multInterval iv2 iv3) in
+ let new_iv = addInterval (multInterval iv1 iv2) iv3 in
isSupersetInterval new_iv intv
| _, _, _ => F
else F))
@@ -120,16 +120,17 @@ val real_prove =
\\ rpt (qpat_x_assum `_ ==> ! x. _` kall_tac)
\\ REAL_ASM_ARITH_TAC;
-val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
- ``!(f:real expr) (A:analysisResult) (P:precond) (fVars:num_set)
- (dVars:num_set) E Gamma.
- validIntervalbounds f A P dVars /\ (* The checker succeeded *)
- (* All defined vars have already been analyzed *)
- dVars_range_valid dVars E A /\
- (((domain (usedVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
- fVars_P_sound fVars E P /\
- validTypes f Gamma ==>
- validRanges f A E (toRTMap (toRExpMap Gamma))``,
+Theorem validIntervalbounds_sound:
+ !(f:real expr) (A:analysisResult) (P:precond) (fVars:num_set)
+ (dVars:num_set) E Gamma.
+ validIntervalbounds f A P dVars /\ (* The checker succeeded *)
+ (* All defined vars have already been analyzed *)
+ dVars_range_valid dVars E A /\
+ (((domain (usedVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
+ fVars_P_sound fVars E P /\
+ validTypes f Gamma ==>
+ validRanges f A E (toRTMap (toRExpMap Gamma))
+Proof
Induct_on `f`
\\ once_rewrite_tac [usedVars_def, toREval_def] \\ rpt strip_tac \\ rveq
\\ Flover_compute ``validIntervalbounds`` \\ rveq
@@ -295,7 +296,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
\\ rename1 `FloverMapTree_find f1 A = SOME (iv_f1, err1)`
\\ rename1 `FloverMapTree_find f2 A = SOME (iv_f2, err2)`
\\ rename1 `FloverMapTree_find f3 A = SOME (iv_f3, err3)`
- \\ qspecl_then [`iv_f2`, `iv_f3`, `vR2`, `vR3`]
+ \\ qspecl_then [`iv_f1`, `iv_f2`, `vR1`, `vR2`]
destruct
(REWRITE_RULE
[validIntervalAdd_def,
@@ -303,7 +304,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
absIntvUpd_def,
contained_def] interval_multiplication_valid)
\\ fs[]
- \\ qspecl_then [`iv_f1`, `multInterval iv_f2 iv_f3`, `vR1`, `vR2 * vR3`]
+ \\ qspecl_then [`multInterval iv_f1 iv_f2`, `iv_f3`, `vR1 * vR2`, `vR3`]
destruct
(REWRITE_RULE
[validIntervalAdd_def,
@@ -328,65 +329,73 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
\\ fs[Downcast_dist', toREval_def, isSupersetInterval_def]
\\ `FST iv = FST intv` by (metis_tac [REAL_LE_ANTISYM])
\\ `SND iv = SND intv` by (metis_tac [REAL_LE_ANTISYM])
- \\ fs[]));
+ \\ fs[])
+QED
-val validIntervalboundsCmd_sound = store_thm (
- "validIntervalboundsCmd_sound",
- ``!f A E fVars dVars outVars P Gamma.
- ssa f (union fVars dVars) outVars /\
- dVars_range_valid dVars E A /\
- fVars_P_sound fVars E P /\
- (((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
- validIntervalboundsCmd f A P dVars /\
- validTypesCmd f Gamma ==>
- validRangesCmd f A E (toRTMap (toRExpMap Gamma))``,
+Theorem validIntervalboundsCmd_sound:
+ ∀ f A E fVars dVars outVars P Gamma.
+ ssa f (union fVars dVars) outVars /\
+ dVars_range_valid dVars E A /\
+ fVars_P_sound fVars E P /\
+ (((domain (freeVars f)) DIFF (domain dVars)) SUBSET (domain fVars)) /\
+ validIntervalboundsCmd f A P dVars /\
+ validTypesCmd f Gamma ==>
+ validRangesCmd f A E (toRTMap (toRExpMap Gamma))
+Proof
Induct_on `f`
\\ once_rewrite_tac [toREvalCmd_def, getRetExp_def, validTypesCmd_def]
\\ rpt strip_tac
\\ Flover_compute ``validIntervalboundsCmd``
- >- (inversion `ssa _ _ _` ssa_cases \\ rveq
- \\ drule validIntervalbounds_sound
- \\ rpt (disch_then drule)
- \\ disch_then (qspecl_then [`fVars`, `Gamma`] destruct)
- >- (fs [SUBSET_DEF, domain_union]
- \\ rpt strip_tac \\ res_tac)
- \\ IMP_RES_TAC validRanges_single
- \\ rename1 `FloverMapTree_find e A = SOME (iv_e, err_e)`
- \\ first_x_assum
- (qspecl_then [`A`, `updEnv n vR E`, `fVars`, `insert n () dVars`,
- `outVars`, `P`, `Gamma`]
- destruct)
- >- (fs [domain_insert]
- \\ rpt conj_tac
- >- (irule ssa_equal_set
- \\ qexists_tac `(insert n () (union fVars dVars))`
- \\ fs [domain_union, domain_insert]
- \\ once_rewrite_tac [UNION_COMM]
- \\ fs [INSERT_UNION_EQ, UNION_COMM])
- >- (fs[dVars_range_valid_def]
- \\ rpt strip_tac \\ fs[updEnv_def]
- >- (rveq \\ fs[])
- \\ rename1 `v2 IN domain dVars`
- \\ Cases_on `v2 = n` \\ fs[]
- \\ rveq \\ fs [domain_union])
- >- (fs[fVars_P_sound_def]
- \\ rpt strip_tac \\ fs[updEnv_def]
- \\ rename1 `v2 IN domain fVars`
- \\ Cases_on `v2 = n` \\ rveq \\ fs[domain_union])
- \\ fs [domain_insert, SUBSET_DEF]
- \\ rpt strip_tac
- \\ first_x_assum match_mp_tac
- \\ once_rewrite_tac [freeVars_def, domain_union]
- \\ fs [domain_union])
- \\ simp[Once validRangesCmd_def]
- \\ conj_tac
- >- (rpt strip_tac
- \\ `vR = vR'` by (metis_tac [meps_0_deterministic])
- \\ rveq \\ fs[])
- \\ IMP_RES_TAC validRangesCmd_single
- \\ fs[getRetExp_def]
- \\ find_exists_tac \\ simp[Once toREvalCmd_def]
- \\ irule let_b \\ find_exists_tac \\ fs[])
+ >- (
+ inversion `ssa _ _ _` ssa_cases \\ rveq
+ \\ drule validIntervalbounds_sound
+ \\ rpt (disch_then drule)
+ \\ disch_then (qspecl_then [`fVars`, `Gamma`] destruct)
+ >- (
+ fs [SUBSET_DEF, domain_union]
+ \\ rpt strip_tac \\ res_tac)
+ \\ imp_res_tac validRanges_single
+ \\ rename1 `FloverMapTree_find e A = SOME (iv_e, err_e)`
+ \\ first_x_assum
+ (qspecl_then [`A`, `updEnv n vR E`, `fVars`, `insert n () dVars`,
+ `outVars`, `P`, `Gamma`]
+ destruct)
+ >- (
+ fs [domain_insert]
+ \\ rpt conj_tac
+ >- (
+ irule ssa_equal_set
+ \\ qexists_tac `(insert n () (union fVars dVars))`
+ \\ fs [domain_union, domain_insert]
+ \\ once_rewrite_tac [UNION_COMM]
+ \\ fs [INSERT_UNION_EQ, UNION_COMM])
+ >- (
+ fs[dVars_range_valid_def]
+ \\ rpt strip_tac \\ fs[updEnv_def]
+ >- (rveq \\ fs[])
+ \\ rename1 `v2 IN domain dVars`
+ \\ Cases_on `v2 = n` \\ fs[]
+ \\ rveq \\ fs [domain_union])
+ >- (
+ fs[fVars_P_sound_def]
+ \\ rpt strip_tac \\ fs[updEnv_def]
+ \\ rename1 `v2 IN domain fVars`
+ \\ Cases_on `v2 = n` \\ rveq \\ fs[domain_union])
+ \\ fs [domain_insert, SUBSET_DEF]
+ \\ rpt strip_tac
+ \\ first_x_assum match_mp_tac
+ \\ once_rewrite_tac [freeVars_def, domain_union]
+ \\ fs [domain_union])
+ \\ simp[Once validRangesCmd_def]
+ \\ conj_tac
+ >- (
+ rpt strip_tac
+ \\ `vR = vR'` by (metis_tac [meps_0_deterministic])
+ \\ rveq \\ fs[])
+ \\ imp_res_tac validRangesCmd_single
+ \\ fs[getRetExp_def]
+ \\ find_exists_tac \\ simp[Once toREvalCmd_def]
+ \\ irule let_b \\ fs[toRTMap_def, toRExpMap_def] \\ find_exists_tac \\ fs[])
\\ inversion `ssa _ _ _` ssa_cases
\\ drule validIntervalbounds_sound
\\ rpt (disch_then drule)
@@ -395,17 +404,19 @@ val validIntervalboundsCmd_sound = store_thm (
\\ simp[Once validRangesCmd_def]
\\ IMP_RES_TAC validRanges_single
\\ simp[Once getRetExp_def, Once toREvalCmd_def]
- \\ fs[] \\ find_exists_tac \\ fs[ret_b]);
+ \\ fs[] \\ find_exists_tac \\ fs[ret_b]
+QED
-val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates_iv",
- ``!(f:real expr) (A:analysisResult) (P:precond) (dVars:num_set).
- (!v. v IN domain dVars ==>
- ? iv err. FloverMapTree_find (Var v) A = SOME (iv,err) /\
- valid iv) /\
- validIntervalbounds f A P dVars ==>
- ? iv err.
- FloverMapTree_find f A = SOME (iv, err) /\
- valid iv``,
+Theorem validIntervalbounds_validates_iv:
+ !(f:real expr) (A:analysisResult) (P:precond) (dVars:num_set).
+ (!v. v IN domain dVars ==>
+ ? iv err. FloverMapTree_find (Var v) A = SOME (iv,err) /\
+ valid iv) /\
+ validIntervalbounds f A P dVars ==>
+ ? iv err.
+ FloverMapTree_find f A = SOME (iv, err) /\
+ valid iv
+Proof
Induct_on `f`
\\ rpt strip_tac
\\ Flover_compute ``validIntervalbounds``
@@ -481,7 +492,7 @@ val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates
\\ rename1 `FloverMapTree_find f2 A = SOME (iv_f2, err_f2)`
\\ rename1 `FloverMapTree_find f3 A = SOME (iv_f3, err_f3)`
\\ fs[]
- \\ `valid (addInterval iv_f1 (multInterval iv_f2 iv_f3))`
+ \\ `valid (addInterval (multInterval iv_f1 iv_f2) iv_f3)`
by (irule iv_add_preserves_valid \\ fs[]
\\ irule iv_mult_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
diff --git a/hol4/RealIntervalInferenceScript.sml b/hol4/RealIntervalInferenceScript.sml
index ab9d3520..aea0e78c 100644
--- a/hol4/RealIntervalInferenceScript.sml
+++ b/hol4/RealIntervalInferenceScript.sml
@@ -67,7 +67,7 @@ Definition inferIntervalbounds_def:
iv_e1 <- FloverMapTree_find e1 recRes3;
iv_e2 <- FloverMapTree_find e2 recRes3;
iv_e3 <- FloverMapTree_find e3 recRes3;
- SOME (FloverMapTree_insert e (addInterval iv_e1 (multInterval iv_e2 iv_e3)) recRes3);
+ SOME (FloverMapTree_insert e (addInterval (multInterval iv_e1 iv_e2) iv_e3) recRes3);
od))
End
diff --git a/hol4/TypeValidatorScript.sml b/hol4/TypeValidatorScript.sml
index 67783c06..a42f5903 100644
--- a/hol4/TypeValidatorScript.sml
+++ b/hol4/TypeValidatorScript.sml
@@ -860,4 +860,35 @@ val getValidMapCmd_correct = store_thm (
\\ rpt strip_tac \\ fs[bstep_cases]
\\ first_x_assum irule \\ ntac 2 (find_exists_tac \\ fs[]));
+Theorem validTypes_defined_usedVars:
+ ∀ e Gamma.
+ validTypes e Gamma ⇒
+ ∀ x. x IN domain (usedVars e) ⇒
+ ∃ m. FloverMapTree_find (Var x) Gamma = SOME m
+Proof
+ ho_match_mp_tac (fetch "-" "validTypes_ind")
+ \\ rpt strip_tac
+ \\ qpat_x_assum ‘validTypes _ _’ mp_tac \\ simp[Once validTypes_def]
+ \\ every_case_tac
+ \\ qpat_x_assum ‘_ IN domain (usedVars _)’ mp_tac
+ \\ simp[Once usedVars_def]
+ \\ rpt strip_tac \\ rveq \\ fs[domain_union]
+QED
+
+Theorem validTypesCmd_freevars:
+ ∀ e Gamma.
+ validTypesCmd e Gamma ⇒
+ ∀ x. x IN domain (freeVars e) ⇒
+ ∃ m. FloverMapTree_find (Var x) Gamma = SOME m
+Proof
+ ho_match_mp_tac (fetch "-" "validTypesCmd_ind")
+ \\ rpt strip_tac
+ \\ qpat_x_assum ‘validTypesCmd _ _’ mp_tac \\ simp[Once validTypesCmd_def]
+ \\ every_case_tac
+ \\ qpat_x_assum ‘_ IN domain (freeVars _)’ mp_tac
+ \\ simp[Once freeVars_def, domain_union]
+ \\ rpt strip_tac \\ rveq \\ fs[domain_union]
+ \\ imp_res_tac validTypes_defined_usedVars \\ fs[]
+QED
+
val _ = export_theory();
--
GitLab