Commit 986fa90e authored by Heiko Becker's avatar Heiko Becker
Browse files

Start working on HOL4 IEEE proofs and refine coq proof

parent 5fb8ccfc
......@@ -110,21 +110,21 @@ Qed.
Theorem eval_gives_sem e E v:
eval_exp_float e E = Some v ->
(* (forall e E v,
eval_exp_float e E = Some v -> *)
(forall e E v,
eval_exp_float e E = Some v ->
(Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 v)))
(bpow radix2 1024) = false) ->
(* -> False) -> *)
(bpow radix2 1024) = false)
-> False) ->
is_finite 53 1024 v = true ->
eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e) (B2R 53 1024 v).
Proof.
revert v; induction e;
simpl; intros v1 eval_succeeds no_oveflow finite_res.
simpl; intros v1 eval_succeeds no_overflow finite_res.
- econstructor.
unfold toREnv.
rewrite eval_succeeds; auto.
......@@ -141,14 +141,21 @@ Proof.
rewrite Rabs_R0.
eapply mEps_geq_zero.
- inversion eval_succeeds.
- destruct (eval_exp_float e1 E);
destruct (eval_exp_float e2 E);
try congruence.
- case_eq (eval_exp_float e1 E); intros * eval_float_e1;
case_eq (eval_exp_float e2 E); intros * eval_float_e2;
rewrite eval_float_e1, eval_float_e2 in *;
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).
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)
(-1022)%Z 53%Z)
as relative_error_binop.
as relative_error_binop.
assert (forall k : Z, (-1022 < k)%Z -> (53 <= k - Fcore_FLT.FLT_exp (3 - 1024 - 53) 53 k)%Z)
as exp_valid.
+ intros k k_pos.
......@@ -156,12 +163,10 @@ 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; clear eval_succeeds.
destruct b; inversion eval_succeeds; subst.
* 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).
specialize (IHe1 b0).
specialize (IHe2 b1).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e1) (B2R 53 1024 b0))
as eval_e1
by (apply IHe1; auto).
......@@ -170,14 +175,16 @@ Proof.
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).
assert (Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2
(Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
(round_mode mode_NE)
(B2R 53 1024 b0 + B2R 53 1024 b1)))
(bpow radix2 1024) = true)
by admit (* TODO: Overflow assumption *).
simpl in *.
remember (179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216)%R as cst.
unfold b64_plus in *.
destruct (
Rlt_bool
(Rabs
(Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (-1074) 53)
(Fcore_generic_fmt.Znearest (fun x : Z => negb (Zeven x))) (B2R 53 1024 b0 + B2R 53 1024 b1))) cst).
Focus 2.
exfalso; apply no_overflow; auto. ; try congruence; auto).
rewrite H0 in *.
destruct H.
destruct H1.
......
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)
>- (cheat)
>- (cheat));
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