Commit 60b6db5f authored by Heiko Becker's avatar Heiko Becker
Browse files

Change proof for IEEE connection a bit

parent 986fa90e
......@@ -124,19 +124,21 @@ Theorem eval_gives_sem e E v:
eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e) (B2R 53 1024 v).
Proof.
revert v; induction e;
simpl; intros v1 eval_succeeds no_overflow finite_res.
intros v1 eval_succeeds no_overflow finite_res;
simpl in eval_succeeds.
- econstructor.
unfold toREnv.
rewrite eval_succeeds; auto.
- inversion eval_succeeds.
assert (perturb (B2R 53 1024 v) 0 = B2R 53 1024 v).
- inversion eval_succeeds; subst.
assert (perturb (B2R 53 1024 v1) 0 = B2R 53 1024 v1) as const_def.
+ unfold perturb.
rewrite Rmult_plus_distr_l.
rewrite Rmult_1_r.
rewrite Rmult_0_r.
rewrite Rplus_0_r.
reflexivity.
+ rewrite H0 in *. setoid_rewrite <- H at 2.
+ simpl.
setoid_rewrite <- const_def at 2.
eapply Const_dist.
rewrite Rabs_R0.
eapply mEps_geq_zero.
......@@ -147,10 +149,8 @@ Proof.
try congruence.
specialize (IHe1 b0 (refl_equal (Some b0)) no_overflow);
specialize (IHe2 b1 (refl_equal (Some b1)) no_overflow).
specialize (no_overflow (Binop b e1 e2) E v1).
simpl in no_overflow.
rewrite eval_float_e1, eval_float_e2 in no_overflow.
specialize (no_overflow eval_succeeds).
specialize (no_overflow (Binop b e1 e2) E).
simpl.
pose proof (fexp_correct 53 1024 eq_refl) as fexp_corr.
pose proof (relative_error_N_ex radix2
(Fcore_FLT.FLT_exp (3 -1024 - 53) 53)
......@@ -163,8 +163,13 @@ Proof.
destruct (Z.max_spec_le (k - 53) (-1074)); omega.
+ specialize (relative_error_binop exp_valid (fun x0 : Z => negb (Zeven x0))).
clear exp_valid fexp_corr.
destruct b; inversion eval_succeeds; subst.
* assert (is_finite 53 1024 b0 = true /\ is_finite 53 1024 b1 = true)
destruct b.
* pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1).
unfold b64_plus in *.
unfold Bplus in *.
finite_b0 finite_b1).
assert (is_finite 53 1024 b0 = true /\ is_finite 53 1024 b1 = true)
as [finite_b0 finite_b1]
by (apply b64_plus_preserves_finite; auto).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e1) (B2R 53 1024 b0))
......@@ -174,7 +179,6 @@ Proof.
as eval_e2
by (apply IHe2; auto).
clear IHe1 IHe2.
pose proof (Bplus_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1 finite_b0 finite_b1).
simpl in *.
remember (179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216)%R as cst.
unfold b64_plus in *.
......
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