Commit 4b62ec07 authored by Heiko Becker's avatar Heiko Becker

Remove some unused lemmas

parent 1147fdb5
......@@ -21,26 +21,6 @@ Proof.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Lemma param_abs_err_bounded (P:precond) (n:nat) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult):
eval_exp 0%R E1 P (Param R n) nR ->
eval_exp (Q2R machineEpsilon) E2 P (Param R n) nF ->
(Rabs (nR - nF) <= * (Q2R machineEpsilon))%R.
intros eval_real eval_float.
inversion eval_real; subst.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
unfold perturb; simpl.
exists v; split; try auto.
rewrite H3 in H8; inversion H8.
rewrite Rabs_err_simpl.
repeat rewrite Rabs_mult.
apply Rmult_le_compat_l; [ apply Rabs_pos | auto].
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q):
eval_exp 0%R E1 (toRExp e1) e1R ->
......@@ -275,67 +275,6 @@ Proof.
rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto.
Lemma validErrorboundCorrectParam:
forall E1 E2 absenv (v:nat) nR nF e P plo phi,
eval_exp 0%R E1 P (toRExp (Param Q v)) nR ->
eval_exp (Q2R RationalSimps.machineEpsilon) E2 P (toRExp (Param Q v)) nF ->
validErrorbound (Param Q v) absenv = true ->
(Q2R plo <= nR <= Q2R phi)%R ->
(forall n : nat, NatSet.In n (Expressions.freeVars (Param Q v)) ->
Is_true (isSupersetIntv (P n) (fst (absenv (Param Q n))))) ->
absenv (Param Q v) = ((plo,phi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
intros E1 E2 absenv v nR nF e P plo phi
eval_real eval_float error_valid intv_valid absenv_approx_p absenv_param.
inversion eval_real; subst.
rewrite delta_0_deterministic in *; auto.
unfold validErrorbound in error_valid.
rewrite absenv_param in error_valid.
specialize (absenv_approx_p v).
assert (exists ivlo ivhi, (ivlo,ivhi) = P v) by (destruct (P v) as [ivlo ivhi]; repeat eexists).
destruct H as [ivlo [ivhi P_eq]].
rewrite <- P_eq in absenv_approx_p, H4.
rewrite absenv_param in absenv_approx_p.
unfold freeVars in absenv_approx_p; simpl in absenv_approx_p.
assert (v = v \/ False) by auto.
specialize (absenv_approx_p H).
unfold isSupersetIntv in absenv_approx_p.
apply andb_prop_elim in absenv_approx_p.
destruct absenv_approx_p as [plo_le_ivlo ivhi_le_phi].
apply Is_true_eq_true, Qle_bool_iff in plo_le_ivlo.
apply Is_true_eq_true, Qle_bool_iff in ivhi_le_phi.
simpl in H4; destruct H4.
apply Qle_Rle in plo_le_ivlo; apply Qle_Rle in ivhi_le_phi.
andb_to_prop error_valid.
rename R into error_valid.
apply Qle_bool_iff in error_valid.
apply Qle_Rle in error_valid.
rewrite Q2R_mult in error_valid.
eapply Rle_trans;[ | apply error_valid].
simpl in *.
inversion eval_float; subst.
unfold perturb; simpl.
assert (Q2R plo <= v0)%R as lower_bound_v0 by lra.
assert (v0 <= Q2R phi)%R as upper_bound_v0 by lra.
rewrite Rsub_eq_Ropp_Rplus.
eapply Rle_trans.
apply Rabs_triang.
eapply Rle_trans.
apply Rplus_le_compat.
apply RmaxAbs.
apply lower_bound_v0.
apply upper_bound_v0.
rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
apply Rmult_le_compat_r;try (apply Rabs_pos).
apply mEps_geq_zero.
rewrite <- maxAbs_impl_RmaxAbs.
destruct intv_valid.
eapply RmaxAbs; auto.
Lemma validErrorboundCorrectAddition E1 E2 absenv
(e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars:
......@@ -1536,7 +1475,6 @@ Proof.
{ apply Rmult_le_compat_r; try lra.
repeat (rewrite Q2R_inv; try auto). }
* unfold widenIntv in *; unfold IntervalArith.contained in *; simpl in *.
assert (Q2R e2lo - Q2R err2 <= Q2R e2hi)%R by lra.
......@@ -24,20 +24,6 @@ val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
\\ simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ REAL_ASM_ARITH_TAC);
val param_abs_err_bounded = store_thm ("param_abs_err_bounded",
``!(P:precond) (n:num) (nR:real) (nF:real) (VarEnv1 VarEnv2 :env).
eval_exp 0 VarEnv1 P (Param n) nR /\
eval_exp machineEpsilon VarEnv2 P (Param n) nF ==>
abs (nR - nF) <= abs ( n) * machineEpsilon``,
rpt strip_tac \\
fs[eval_exp_cases] \\
`perturb ( n) delta = ( n)` by metis_tac[delta_0_deterministic] \\
`nR = ( n)` by fs[]\\
simp[perturb_def, Rabs_err_simpl, REAL_ABS_MUL] \\
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).
Subproject commit c3956a13b2f385aeea6019a41423f4782954ee98
open preamble
open machine_ieeeTheory binary_ieeeTheory
open ExpressionsTheory RealSimpsTheory
val dmode_def = Define `dmode = roundTiesToEven`;
val convert_env_def = Define `
convert_env (E:num -> word64 option) =
\n. case E n of
| SOME v => SOME (float_to_real (fp64_to_float v))
| NONE => NONE`;
val eval_exp_float_def = Define `
eval_exp_float (e:real exp) (E:num -> word64 option) =
case e of
| Var n => E n
| Const v => SOME (real_to_fp64 dmode v)
| Binop b e1 e2 =>
(case ((eval_exp_float e1 E), (eval_exp_float e2 E)) of
| SOME v1, SOME v2 =>
(case b of
| Plus => SOME (fp64_add dmode v1 v2)
| Sub => SOME (fp64_sub dmode v1 v2)
| Mult => SOME (fp64_mul dmode v1 v2)
| Div => SOME (fp64_div dmode v1 v2))
|_, _ => NONE)
| _ => NONE`;
val eval_agrees = store_thm ("eval_agrees",
``!(e:real exp) (E:num -> word64 option) (v:word64).
eval_exp_float e E = SOME v ==>
eval_exp machineEpsilon (convert_env E) e (float_to_real (fp64_to_float v))``
Induct_on `e` \\ rpt strip_tac
>- (fs [eval_exp_float_def, convert_env_def]
\\ Cases_on `E n` \\ fs []
\\ match_mp_tac Var_load
\\ fs [])
>- (fs [eval_exp_float_def, convert_env_def, real_to_fp64_def, real_to_float_def, dmode_def]
\\ first_x_assum (fn thm => rw[GSYM thm])
\\ once_rewrite_tac [fp64_to_float_float_to_fp64]
\\ cheat)
/home/hbecker/Git_Repos/HOL/bin/Holmake certificate_Traincar4Theory.sig 0:00.18
/home/hbecker/Git_Repos/HOL/bin/Holmake certificate_Traincar4Theory.sig 10:55:47
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