ErrorBounds ported

coq/ErrorBounds.v

@@ -7,6 +7,7 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.
 Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
 Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs.
 
+(* TODO: absenv not used *)
 Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType) defVars:
   eval_exp E1 (toREvalVars defVars) (Const M0 n) nR M0 ->
   eval_exp E2 defVars (Const m n) nF m ->
@@ -466,5 +467,5 @@ Proof.
     rewrite Rabs_mult.
     apply Rmult_le_compat_l.
     + apply Rabs_pos.
-    + auto. 
+    + auto.
 Qed.

hol4/ErrorBoundsScript.sml

@@ -5,7 +5,7 @@ Bounds are explained in section 5, Deriving Computable Error Bounds
 **)
 open preamble
 open simpLib realTheory realLib RealArith
-open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics MachineTypeTheory
 open ExpressionAbbrevsTheory EnvironmentsTheory
 
 val _ = new_theory "ErrorBounds";
@@ -13,12 +13,12 @@ val _ = new_theory "ErrorBounds";
 val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
 
 val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
-  ``!(n:real) (nR:real) (nF:real) (E1 E2:env).
-      eval_exp 0 E1 (Const n) nR /\
-      eval_exp machineEpsilon E2 (Const n) nF ==>
-      abs (nR - nF) <= abs n * machineEpsilon``,
+  ``!(n:real) (nR:real) (nF:real) (E1 E2:env) (m:mType) (defVars: num -> mType option).
+      eval_exp E1 (toREvalVars defVars) (Const M0 n) nR M0 /\
+      eval_exp E2 defVars (Const m n) nF m ==>
+      abs (nR - nF) <= abs n * (meps m)``,
   rpt strip_tac
-  \\ fs[eval_exp_cases]
+  \\ fs[eval_exp_cases,meps_def,inj_eps_Q_def]
   \\ `perturb n delta = n` by metis_tac[delta_0_deterministic]
   \\ `nR = n` by fs[]
   \\ simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL]
@@ -40,28 +40,33 @@ val param_abs_err_bounded = store_thm ("param_abs_err_bounded",
 
 val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
   ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
-     (vR:real) (vF:real) (E1 E2:env).
-       eval_exp 0 E1 e1 e1R /\
-       eval_exp machineEpsilon E2 e1 e1F /\
-       eval_exp 0 E1 e2 e2R /\
-       eval_exp machineEpsilon E2 e2 e2F /\
-       eval_exp 0 E1 (Binop Plus e1 e2) vR /\
-       eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Plus (Var 1) (Var 2)) vF /\
+     (vR:real) (vF:real) (E1 E2:env) (m m1 m2:mType) (defVars: num -> mType option).
+       eval_exp E1 (toREvalVars defVars) (toREval e1) e1R M0 /\
+       eval_exp E2 defVars e1 e1F m1 /\
+       eval_exp E1 (toREvalVars defVars) (toREval e2) e2R M0 /\
+       eval_exp E2 defVars e2 e2F m2 /\
+       eval_exp E1 (toREvalVars defVars) (toREval (Binop Plus e1 e2)) vR M0 /\
+       eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Plus (Var 1) (Var 2)) vF m /\
        abs (e1R - e1F) <= err1 /\
        abs (e2R - e2F) <= err2 ==>
-       abs (vR - vF) <= err1 + err2 + (abs (e1F + e2F) * machineEpsilon)``,
+       abs (vR - vF) <= err1 + err2 + (abs (e1F + e2F) * (meps m))``,
   rpt strip_tac
-  \\ inversion `eval_exp 0 E1 (Binop Plus e1 e2) vR` eval_exp_cases
+  \\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Plus e1 e2)) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))
+  \\ fs []
+  \\ inversion `eval_exp E1 _ (Binop Plus _ _) _ _` eval_exp_cases
   \\ rename1 `vR = perturb (evalBinop Plus v1R v2R) deltaR`
-  \\ inversion `eval_exp machineEpsilon _ (Binop Plus (Var 1) (Var 2)) vF` eval_exp_cases
+  \\ inversion `eval_exp _ _ (Binop Plus (Var 1) (Var 2)) _ _` eval_exp_cases
   \\ rename1 `vF = perturb (evalBinop Plus v1F v2F) deltaF`
-  \\ `perturb (evalBinop Plus v1R v2R) deltaR = evalBinop Plus v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[])
+  \\ `(m1' = M0) /\ (m2' = M0)` by (match_mp_tac ifJoinIs0 \\ fs[]) \\ fs []
+  \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
+  \\ `perturb (evalBinop Plus v1R v2R) deltaR = evalBinop Plus v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
   \\ `vR = evalBinop Plus v1R v2R` by simp[]
   \\ `v1R = e1R` by metis_tac[meps_0_deterministic]
   \\ `v2R = e2R` by metis_tac[meps_0_deterministic]
   \\ rveq \\ fs[evalBinop_def, perturb_def]
-  \\ rpt (inversion `eval_exp machineEpsilon (updEnv n e E) expr vE` eval_exp_cases)
+  \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases)
   \\ fs [updEnv_def] \\ rveq
+  \\ fs [updDefVars_def] \\ rveq
   \\ once_rewrite_tac[real_sub]
   \\ `e1R + e2R + -((e1F + e2F) * (1 + deltaF)) = (e1R + - e1F) + ((e2R + - e2F) + - (e1F + e2F) * deltaF)` by REAL_ASM_ARITH_TAC
   \\ simp []
@@ -80,28 +85,33 @@ val add_abs_err_bounded = store_thm ("add_abs_err_bounded",
 
 val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded",
   ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
-     (vR:real) (vF:real) (E1 E2:env) (absenv:analysisResult).
-       eval_exp 0 E1 e1 e1R /\
-       eval_exp machineEpsilon E2 e1 e1F /\
-       eval_exp 0 E1 e2 e2R /\
-       eval_exp machineEpsilon E2 e2 e2F /\
-       eval_exp 0 E1 (Binop Sub e1 e2) vR /\
-       eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Sub (Var 1) (Var 2)) vF /\
+     (vR:real) (vF:real) (E1 E2:env) (m m1 m2:mType) (defVars: num -> mType option).
+       eval_exp E1 (toREvalVars defVars) (toREval e1) e1R M0 /\
+       eval_exp E2 defVars e1 e1F m1 /\
+       eval_exp E1 (toREvalVars defVars) (toREval e2) e2R M0 /\
+       eval_exp E2 defVars e2 e2F m2 /\
+       eval_exp E1 (toREvalVars defVars) (toREval (Binop Sub e1 e2)) vR M0 /\
+       eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Sub (Var 1) (Var 2)) vF m /\
        abs (e1R - e1F) <= err1 /\
        abs (e2R - e2F) <= err2 ==>
-       abs (vR - vF) <= err1 + err2 + (abs (e1F - e2F) * machineEpsilon)``,
+       abs (vR - vF) <= err1 + err2 + (abs (e1F - e2F) * (meps m))``,
   rpt strip_tac
-  \\ inversion `eval_exp 0 _ (Binop Subs e1 e2) vR` eval_exp_cases
+  \\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Sub e1 e2)) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))
+  \\ fs []
+  \\ inversion `eval_exp E1 _ (Binop Sub _ _) _ _` eval_exp_cases
   \\ rename1 `vR = perturb (evalBinop Sub v1R v2R) deltaR`
-  \\ inversion `eval_exp machineEpsilon _ (Binop Sub (Var 1) (Var 2)) vF` eval_exp_cases
+  \\ inversion `eval_exp _ _ (Binop Sub (Var 1) (Var 2)) _ _` eval_exp_cases
   \\ rename1 `vF = perturb (evalBinop Sub v1F v2F) deltaF`
-  \\ `perturb (evalBinop Sub v1R v2R) deltaR = evalBinop Sub v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[])
+  \\ `(m1' = M0) /\ (m2' = M0)` by (match_mp_tac ifJoinIs0 \\ fs[]) \\ fs []
+  \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
+  \\ `perturb (evalBinop Sub v1R v2R) deltaR = evalBinop Sub v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
   \\ `vR = evalBinop Sub v1R v2R` by simp[]
   \\ `v1R = e1R` by metis_tac[meps_0_deterministic]
   \\ `v2R = e2R` by metis_tac[meps_0_deterministic]
   \\ fs[evalBinop_def, perturb_def]
-  \\ rpt (inversion `eval_exp machineEpsilon (updEnv n e E) expr vE` eval_exp_cases)
+  \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases)
   \\ fs [updEnv_def] \\ rveq
+  \\ fs [updDefVars_def] \\ rveq
   \\ rewrite_tac[real_sub]
   \\ `e1R + -e2R + -((e1F + -e2F) * (1 + deltaF)) = (e1R + - e1F) + ((- e2R + e2F) + - (e1F + - e2F) * deltaF)`
        by REAL_ASM_ARITH_TAC
@@ -117,35 +127,40 @@ val subtract_abs_err_bounded = store_thm ("subtract_abs_err_bounded",
   \\ match_mp_tac REAL_LE_ADD2
   \\ conj_tac
   >- (`-e2R + e2F = e2F - e2R` by REAL_ASM_ARITH_TAC \\ simp[]
-      \\ once_rewrite_tac [ABS_SUB] \\ fs[])
+       \\ once_rewrite_tac [ABS_SUB] \\ fs[])
   >- (once_rewrite_tac [REAL_ABS_MUL]
-      \\ match_mp_tac REAL_LE_MUL2
-      \\ fs [REAL_ABS_POS, ABS_NEG]));
+       \\ match_mp_tac REAL_LE_MUL2
+       \\ fs [REAL_ABS_POS, ABS_NEG]));
 
 val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded",
   ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
-     (vR:real) (vF:real) (E1 E2 :env) (absenv:analysisResult).
-       eval_exp 0 E1 e1 e1R /\
-       eval_exp machineEpsilon E2 e1 e1F /\
-       eval_exp 0 E1 e2 e2R /\
-       eval_exp machineEpsilon E2 e2 e2F /\
-       eval_exp 0 E1 (Binop Mult e1 e2) vR /\
-       eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (Binop Mult (Var 1) (Var 2)) vF /\
+     (vR:real) (vF:real) (E1 E2 :env) (m m1 m2:mType) (defVars: num -> mType option).
+       eval_exp E1 (toREvalVars defVars) (toREval e1) e1R M0 /\
+       eval_exp E2 defVars e1 e1F m1 /\
+       eval_exp E1 (toREvalVars defVars) (toREval e2) e2R M0 /\
+       eval_exp E2 defVars e2 e2F m2 /\
+       eval_exp E1 (toREvalVars defVars) (toREval (Binop Mult e1 e2)) vR M0 /\
+       eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Mult (Var 1) (Var 2)) vF m /\
        abs (e1R - e1F) <= err1 /\
        abs (e2R - e2F) <= err2 ==>
-       abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + (abs (e1F * e2F) * machineEpsilon)``,
+       abs (vR - vF) <= abs (e1R * e2R - e1F * e2F) + (abs (e1F * e2F) * (meps m))``,
   rpt strip_tac
-  \\ inversion `eval_exp 0 _ (Binop Mult e1 e2) vR` eval_exp_cases
+  \\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Mult e1 e2)) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))
+  \\ fs []
+  \\ inversion `eval_exp E1 _ (Binop Mult _ _) _ _` eval_exp_cases
   \\ rename1 `vR = perturb (evalBinop Mult v1R v2R) deltaR`
-  \\ inversion `eval_exp machineEpsilon _ (Binop Mult (Var 1) (Var 2)) v` eval_exp_cases
+  \\ inversion `eval_exp _ _ (Binop Mult (Var 1) (Var 2)) _ _` eval_exp_cases
   \\ rename1 `vF = perturb (evalBinop Mult v1F v2F) deltaF`
-  \\ `perturb (evalBinop Mult v1R v2R) deltaR = evalBinop Mult v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[])
+  \\ `(m1' = M0) /\ (m2' = M0)` by (match_mp_tac ifJoinIs0 \\ fs[]) \\ fs []
+  \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
+  \\ `perturb (evalBinop Mult v1R v2R) deltaR = evalBinop Mult v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
   \\ `vR = evalBinop Mult v1R v2R` by simp[]
   \\ `v1R = e1R` by metis_tac[meps_0_deterministic]
   \\ `v2R = e2R` by metis_tac[meps_0_deterministic]
   \\ fs[evalBinop_def, perturb_def]
-  \\ rpt (inversion `eval_exp machineEpsilon (updEnv n e E) expr vE` eval_exp_cases)
+  \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases)
   \\ fs [updEnv_def] \\ rveq
+  \\ fs [updDefVars_def] \\ rveq
   \\ rewrite_tac [real_sub]
   \\ `e1R * e2R + -(e1F * e2F * (1 + deltaF)) = (e1R * e2R + - (e1F * e2F)) + - (e1F * e2F * deltaF)` by REAL_ASM_ARITH_TAC
   \\ simp[]
@@ -161,28 +176,33 @@ val mult_abs_err_bounded = store_thm ("mult_abs_err_bounded",
 
 val div_abs_err_bounded = store_thm ("div_abs_err_bounded",
   ``!(e1:real exp) (e1R:real) (e1F:real) (e2:real exp) (e2R:real) (e2F:real) (err1:real) (err2:real)
-     (vR:real) (vF:real) (E1 E2 :env) (absenv:analysisResult).
-       eval_exp 0 E1 e1 e1R /\
-       eval_exp machineEpsilon E2 e1 e1F /\
-       eval_exp 0 E1 e2 e2R /\
-       eval_exp machineEpsilon E2 e2 e2F /\
-       eval_exp 0 E1 (Binop Div e1 e2) vR /\
-       eval_exp machineEpsilon (updEnv 2 e2F (updEnv 1 e1F emptyEnv))(Binop Div (Var 1) (Var 2)) vF /\
+     (vR:real) (vF:real) (E1 E2 :env) (m m1 m2:mType) (defVars: num -> mType option).
+       eval_exp E1 (toREvalVars defVars) (toREval e1) e1R M0 /\
+       eval_exp E2 defVars e1 e1F m1 /\
+       eval_exp E1 (toREvalVars defVars) (toREval e2) e2R M0 /\
+       eval_exp E2 defVars e2 e2F m2 /\
+       eval_exp E1 (toREvalVars defVars) (toREval (Binop Div e1 e2)) vR M0 /\
+       eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (updDefVars 2 m2 (updDefVars 1 m1 defVars)) (Binop Div (Var 1) (Var 2)) vF m /\
        abs (e1R - e1F) <= err1 /\
        abs (e2R - e2F) <= err2 ==>
-       abs (vR - vF) <= abs (e1R / e2R - e1F / e2F) + (abs (e1F / e2F) * machineEpsilon)``,
+       abs (vR - vF) <= abs (e1R / e2R - e1F / e2F) + (abs (e1F / e2F) * (meps m))``,
   rpt strip_tac
-  \\ inversion `eval_exp 0 _ (Binop Div e1 e2) vR` eval_exp_cases
+  \\ qpat_x_assum `eval_exp E1 _ (toREval (Binop Div e1 e2)) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))
+  \\ fs []
+  \\ inversion `eval_exp E1 _ (Binop Div _ _) _ _` eval_exp_cases
   \\ rename1 `vR = perturb (evalBinop Div v1R v2R) deltaR`
-  \\ inversion `eval_exp machineEpsilon _ (Binop Div (Var 1) (Var 2)) v` eval_exp_cases
+  \\ inversion `eval_exp _ _ (Binop Div (Var 1) (Var 2)) _ _` eval_exp_cases
   \\ rename1 `vF = perturb (evalBinop Div v1F v2F) deltaF`
-  \\ `perturb (evalBinop Div v1R v2R) deltaR = evalBinop Div v1R v2R` by (match_mp_tac delta_0_deterministic \\ fs[])
+  \\ `(m1' = M0) /\ (m2' = M0)` by (match_mp_tac ifJoinIs0 \\ fs[]) \\ fs []
+  \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))
+  \\ `perturb (evalBinop Div v1R v2R) deltaR = evalBinop Div v1R v2R` by (match_mp_tac delta_M0_deterministic \\ fs[])
   \\ `vR = evalBinop Div v1R v2R` by simp[]
   \\ `v1R = e1R` by metis_tac[meps_0_deterministic]
   \\ `v2R = e2R` by metis_tac[meps_0_deterministic]
   \\ fs[evalBinop_def, perturb_def]
-  \\ rpt (inversion `eval_exp machineEpsilon (updEnv n e E) expr vE` eval_exp_cases)
+  \\ rpt (inversion `eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) _ _ _ _` eval_exp_cases)
   \\ fs [updEnv_def] \\ rveq
+  \\ fs [updDefVars_def] \\ rveq
   \\ rewrite_tac [real_sub]
   \\ `e1R / e2R + -(e1F / e2F * (1 + deltaF)) = (e1R / e2R + - (e1F / e2F)) + - (e1F / e2F * deltaF)` by REAL_ASM_ARITH_TAC
   \\ simp[]

hol4/ExpressionsScript.sml

@@ -141,12 +141,17 @@ val delta_0_deterministic = store_thm("delta_0_deterministic",
   ``!(v:real) (delta:real). abs delta <= 0 ==> perturb v delta = v``,
   fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
 
+val delta_M0_deterministic = store_thm("delta_M0_deterministic",
+  ``!(v:real) (delta:real). abs delta <= meps M0 ==> perturb v delta = v``,
+  fs [meps_def,inj_eps_Q_def,perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
+
+
 (**
 Evaluation with 0 as machine epsilon is deterministic
 **)
 val ifJoinIs0 = store_thm("ifJoinIs0",
 			  ``!m1 m2. M0 = computeJoin m1 m2 ==> m1 = M0 /\ m2 = M0``,
-			  strip_tac \\ strip_tac \\ strip_tac \\ fs [computeJoin_def] 
+			  strip_tac \\ strip_tac \\ strip_tac \\ fs [computeJoin_def]
 				    \\ Cases_on `isMorePrecise m1 m2` \\ fs [] \\  fs [isMorePrecise_def] \\ rw []);
 
 
@@ -161,10 +166,10 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
 	     >- rw []
 	     >- rw []
 	     >- (res_tac \\ fs [meps_def,inj_eps_Q_def,delta_0_deterministic]))
-      >- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ fs [eval_exp_cases] 
-	     \\ `m1' = M0 /\ m2' = M0` by 
+      >- (rw [] \\ rpt (qpat_x_assum `eval_exp _ _ (toREval _) _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [toREval_def] thm))) \\ fs [] \\ fs [eval_exp_cases]
+	     \\ `m1' = M0 /\ m2' = M0` by
 	     (qpat_x_assum `M0 = computeJoin m1 m2` (fn thm => ASSUME_TAC ifJoinIs0 \\ fs []))
-	     \\ `m1 = M0 /\ m2 = M0` by (qpat_x_assum `M0 = computeJoin m1' m2'` (fn thm => ASSUME_TAC ifJoinIs0 
+	     \\ `m1 = M0 /\ m2 = M0` by (qpat_x_assum `M0 = computeJoin m1' m2'` (fn thm => ASSUME_TAC ifJoinIs0
 												       \\ fs []))
 	     \\ rveq
 	     \\ rpt (qpat_x_assum `M0 = _` (fn thm => fs [GSYM thm]))