Commit d217410d authored by Heiko Becker's avatar Heiko Becker
Browse files

Statrt working on IEE connection in Coq

parent 90d8f3e6
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.micromega.Psatz Coq.QArith.Qreals.
Require Import Daisy.Expressions Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
(*Require Import Flocq.Prop.Fprop_relative Flocq.Core.Fcore_defs Flocq.Calc.Fcalc_ops Flocq.Calc.Fcalc_div. *)
Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE Flocq.Core.Fcore_Raux Flocq.Prop.Fprop_relative.
Definition valid_div a b (f:binary_float a b):=
match f with
|B754_finite _ _ _ _ _ _ => true
|_ => false
end.
Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option (binary_float 53 1024)):=
match e with
|Const c => Some c
|Var _ x => E x
|Binop b e1 e2 =>
match eval_exp_float e1 E, eval_exp_float e2 E with
|Some f1, Some f2 =>
match b with
|Plus => Some (b64_plus mode_NE f1 f2)
|Sub => Some (b64_minus mode_NE f1 f2)
|Mult => Some (b64_mult mode_NE f1 f2)
|Div => if (valid_div f2) then Some (b64_div mode_NE f1 f2) else None
end
|_ , _ => None
end
| _ => None
end.
Fixpoint toRExp e :=
match e with
|Const c => Const (B2R 53 1024 c)
|Var _ x => Var R x
|Unop u e => Unop u (toRExp e)
|Binop b e1 e2 => Binop b (toRExp e1) (toRExp e2)
end.
Definition toREnv E :env:= fun x:nat => match E x with
|None => None
|Some c => Some (B2R 53 1024 c)
end.
Lemma b64_plus_preserves_finite f1 f2:
is_finite 53 1024 (b64_plus mode_NE f1 f2) = true ->
is_finite 53 1024 f1 = true /\ is_finite 53 1024 f2 = true.
Proof.
intros finite_add.
case_eq (b64_plus mode_NE f1 f2);
intros res add_res;
unfold b64_plus, Bplus in *;
case_eq f1; intros * f1_eq;
try rewrite f1_eq in *; simpl in *;
case_eq f2; intros * f2_eq;
try rewrite f2_eq in *; simpl in *;
try destruct (eqb b b0);
try congruence; try auto.
Qed.
Lemma b64_minus_preserves_finite f1 f2:
is_finite 53 1024 (b64_minus mode_NE f1 f2) = true ->
is_finite 53 1024 f1 = true /\ is_finite 53 1024 f2 = true.
Proof.
intros finite_minus.
case_eq (b64_minus mode_NE f1 f2);
intros res add_res;
unfold b64_minus, Bminus in *;
case_eq f1; intros * f1_eq;
try rewrite f1_eq in *; simpl in *;
case_eq f2; intros * f2_eq;
try rewrite f2_eq in *; simpl in *;
try destruct (eqb b (negb b0));
try congruence; try auto.
Qed.
Lemma b64_mult_preserves_finite f1 f2:
is_finite 53 1024 (b64_mult mode_NE f1 f2) = true ->
is_finite 53 1024 f1 = true /\ is_finite 53 1024 f2 = true.
Proof.
intros finite_mult.
case_eq (b64_mult mode_NE f1 f2);
intros res mult_res;
unfold b64_mult, Bmult in *;
case_eq f1; intros * f1_eq;
try rewrite f1_eq in *; simpl in *;
case_eq f2; intros * f2_eq;
try rewrite f2_eq in *; simpl in *;
try destruct (eqb b b0);
try congruence; try auto.
Qed.
Lemma b64_div_preserves_finite f1 f2:
is_finite 53 1024 (b64_div mode_NE f1 f2) = true ->
(forall sgn, f2 = B754_infinity 53 1024 sgn -> False) ->
is_finite 53 1024 f1 = true /\ is_finite 53 1024 f2 = true.
Proof.
intros finite_div no_infty.
case_eq (b64_div mode_NE f1 f2);
intros res div_res;
unfold b64_div, Bdiv in *;
case_eq f1; intros * f1_eq;
try rewrite f1_eq in *; simpl in *;
case_eq f2; intros * f2_eq;
try rewrite f2_eq in *; simpl in *;
try congruence; try auto.
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 -> *)
(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) -> *)
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.
- econstructor.
unfold toREnv.
rewrite eval_succeeds; auto.
- inversion eval_succeeds.
assert (perturb (B2R 53 1024 v) 0 = B2R 53 1024 v).
+ 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.
eapply Const_dist.
rewrite Rabs_R0.
eapply mEps_geq_zero.
- inversion eval_succeeds.
- destruct (eval_exp_float e1 E);
destruct (eval_exp_float e2 E);
try congruence.
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.
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.
unfold Fcore_FLT.FLT_exp; simpl.
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.
* 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).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e2) (B2R 53 1024 b1))
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).
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 *).
rewrite H0 in *.
destruct H.
destruct H1.
unfold b64_plus.
rewrite H.
assert (exists delta,(Rabs(delta) <= Q2R machineEpsilon)%R /\
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) =
perturb (B2R 53 1024 b0 + B2R 53 1024 b1) delta).
{ specialize (relative_error_binop (B2R 53 1024 b0 + B2R 53 1024 b1)%R).
destruct relative_error_binop.
- unfold bpow, radix2.
(* This is the proof that we do not handle denormals! *) admit.
- destruct H3.
unfold round_mode; simpl in *.
rewrite H4.
unfold perturb.
exists x.
split; try auto.
eapply Rle_trans; eauto.
unfold machineEpsilon.
unfold Q2R.
unfold Qnum, Qden.
assert (2 ^ 53 = 9007199254740992)%positive by (cbv; auto).
rewrite H5.
lra. }
{ destruct H3 as [delta [delta_valid eval_perturb]].
rewrite eval_perturb.
econstructor; eauto.
intros; congruence. }
* assert (is_finite 53 1024 b0 = true /\ is_finite 53 1024 b1 = true)
as [finite_b0 finite_b1]
by (apply b64_minus_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).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e2) (B2R 53 1024 b1))
as eval_e2
by (apply IHe2; auto).
clear IHe1 IHe2.
pose proof (Bminus_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 *).
rewrite H0 in *.
destruct H.
destruct H1.
unfold b64_minus.
rewrite H.
assert (exists delta,(Rabs(delta) <= Q2R machineEpsilon)%R /\
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) =
perturb (B2R 53 1024 b0 - B2R 53 1024 b1) delta).
{ specialize (relative_error_binop (B2R 53 1024 b0 - B2R 53 1024 b1)%R).
destruct relative_error_binop.
- unfold bpow, radix2.
(* This is the proof that we do not handle denormals! *) admit.
- destruct H3.
unfold round_mode; simpl in *.
rewrite H4.
unfold perturb.
exists x.
split; try auto.
eapply Rle_trans; eauto.
unfold machineEpsilon.
unfold Q2R.
unfold Qnum, Qden.
assert (2 ^ 53 = 9007199254740992)%positive by (cbv; auto).
rewrite H5.
lra. }
{ destruct H3 as [delta [delta_valid eval_perturb]].
rewrite eval_perturb.
econstructor; eauto.
intros; congruence. }
* assert (is_finite 53 1024 b0 = true /\ is_finite 53 1024 b1 = true)
as [finite_b0 finite_b1]
by (apply b64_mult_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).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e2) (B2R 53 1024 b1))
as eval_e2
by (apply IHe2; auto).
clear IHe1 IHe2.
pose proof (Bmult_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 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 *).
rewrite H0 in *.
destruct H.
destruct H1.
(*assert (is_nan 53 1024 (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1) = false).
{ unfold is_nan, is_finite, b64_mult in *.
destruct (Bmult 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 b1); auto. } *)
unfold b64_mult.
rewrite H.
assert (exists delta,(Rabs(delta) <= Q2R machineEpsilon)%R /\
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) =
perturb (B2R 53 1024 b0 * B2R 53 1024 b1) delta).
{ specialize (relative_error_binop (B2R 53 1024 b0 * B2R 53 1024 b1)%R).
destruct relative_error_binop.
- unfold bpow, radix2.
(* This is the proof that we do not handle denormals! *) admit.
- destruct H3.
unfold round_mode; simpl in *.
rewrite H4.
unfold perturb.
exists x.
split; try auto.
eapply Rle_trans; eauto.
unfold machineEpsilon.
unfold Q2R.
unfold Qnum, Qden.
assert (2 ^ 53 = 9007199254740992)%positive by (cbv; auto).
rewrite H5.
lra. }
{ destruct H3 as [delta [delta_valid eval_perturb]].
rewrite eval_perturb.
econstructor; eauto.
intros; congruence. }
* assert (valid_div b1 = true) by (destruct (valid_div b1); congruence).
rewrite H in H0.
inversion H0; subst.
assert (forall sgn, b1 = B754_infinity 53 1024 sgn -> False)
by (intros; unfold valid_div in H; destruct b1; congruence).
assert (is_finite 53 1024 b0 = true /\ is_finite 53 1024 b1 = true)
as [finite_b0 finite_b1]
by (apply b64_div_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).
assert (eval_exp (Q2R machineEpsilon) (toREnv E) (toRExp e2) (B2R 53 1024 b1))
as eval_e2
by (apply IHe2; auto).
clear IHe1 IHe2.
pose proof (Bdiv_correct 53 1024 eq_refl eq_refl binop_nan_pl64 mode_NE b0 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 *).
assert (B2R 53 1024 b1 <> 0%R).
{ hnf. intros. unfold B2R in H4. unfold valid_div in H. destruct b1; simpl in H; try congruence.
unfold Fcore_defs.F2R in H4.
simpl in H4.
pose proof (bpow_gt_0 radix2 e).
rewrite Z2R_cond_Zopp in H4.
unfold cond_Ropp in H4.
destruct b.
- pose proof (Zgt_pos_0 m).
rewrite Z.gt_lt_iff in H6.
apply Z2R_lt in H6.
apply Rmult_integral in H4.
unfold Z2R in *.
destruct H4; try lra.
- pose proof (Zgt_pos_0 m).
rewrite Z.gt_lt_iff in H6.
apply Z2R_lt in H6.
apply Rmult_integral in H4.
unfold Z2R in *; destruct H4; lra. }
rewrite H3 in H2.
destruct H2; try auto.
destruct H5.
unfold b64_div.
rewrite H2.
assert (exists delta,(Rabs(delta) <= Q2R machineEpsilon)%R /\
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) =
perturb (B2R 53 1024 b0 / B2R 53 1024 b1) delta).
{ specialize (relative_error_binop (B2R 53 1024 b0 / B2R 53 1024 b1)%R).
destruct relative_error_binop.
- unfold bpow, radix2.
(* This is the proof that we do not handle denormals! *) admit.
- destruct H7.
unfold round_mode; simpl in *.
rewrite H8.
unfold perturb.
exists x.
split; try auto.
eapply Rle_trans; eauto.
unfold machineEpsilon.
unfold Q2R.
unfold Qnum, Qden.
assert (2 ^ 53 = 9007199254740992)%positive by (cbv; auto).
rewrite H9.
lra. }
{ destruct H7 as [delta [delta_valid eval_perturb]].
rewrite eval_perturb.
econstructor; eauto. }
Admitted.
\ No newline at end of file
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