Commit 82d8d10e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Added a typeclass for existence of rounding to nearest even.

parent 6f3b558c
......@@ -41,8 +41,10 @@ Theorem Fsqrt_FLT_ne_correct :
Proof.
intros x.
replace (F2R (Fsqrt_FLT_ne x)) with (round beta (FLT_exp emin prec) rndNE (sqrt (F2R x))).
apply round_NE_pt_FLT.
apply round_NE_pt.
apply FLT_exp_valid.
omega.
apply exists_NE_FLT.
now right.
unfold Fsqrt_FLT_ne.
destruct x as (mx, ex).
......@@ -78,8 +80,10 @@ Qed.
End test.
(*
Definition radix10 : radix.
now refine (Build_radix 10 _).
Defined.
(* Time Eval vm_compute in (Fsqrt radix10 20 (-15) (Float radix10 2 0)). *)
Time Eval vm_compute in (Fsqrt radix10 20 (-15) (Float radix10 2 0)).
*)
......@@ -75,15 +75,6 @@ apply iff_sym.
apply FIX_format_generic.
Qed.
Theorem Rnd_NE_pt_FIX :
round_pred (Rnd_NE_pt beta FIX_exp).
Proof.
apply Rnd_NE_pt_round.
apply FIX_exp_valid.
right.
split ; easy.
Qed.
Global Instance FIX_exp_monotone : Monotone_exp FIX_exp.
Proof.
intros ex ey H.
......
......@@ -274,8 +274,7 @@ Qed.
(** and it allows a rounding to nearest, ties to even. *)
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
Theorem NE_ex_prop_FLT :
NE_ex_prop beta FLT_exp.
Global Instance exists_NE_FLT : Exists_NE beta FLT_exp.
Proof.
destruct NE_prop as [H|H].
now left.
......@@ -292,22 +291,4 @@ generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.
Theorem round_NE_pt_FLT :
forall x,
Rnd_NE_pt beta FLT_exp x (round beta FLT_exp rndNE x).
Proof.
intros x.
apply round_NE_pt.
apply FLT_exp_valid.
apply NE_ex_prop_FLT.
Qed.
Theorem Rnd_NE_pt_FLT :
round_pred (Rnd_NE_pt beta FLT_exp).
Proof.
apply Rnd_NE_pt_round.
apply FLT_exp_valid.
apply NE_ex_prop_FLT.
Qed.
End RND_FLT.
......@@ -245,8 +245,7 @@ Qed.
(** and it allows a rounding to nearest, ties to even. *)
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
Theorem NE_ex_prop_FLX :
NE_ex_prop beta FLX_exp.
Global Instance exists_NE_FLX : Exists_NE beta FLX_exp.
Proof.
destruct NE_prop as [H|H].
now left.
......@@ -255,22 +254,4 @@ unfold FLX_exp.
split ; omega.
Qed.
Theorem round_NE_pt_FLX :
forall x,
Rnd_NE_pt beta FLX_exp x (round beta FLX_exp rndNE x).
Proof.
intros x.
apply round_NE_pt.
apply FLX_exp_valid.
apply NE_ex_prop_FLX.
Qed.
Theorem Rnd_NE_pt_FLX :
round_pred (Rnd_NE_pt beta FLX_exp).
Proof.
apply Rnd_NE_pt_round.
apply FLX_exp_valid.
apply NE_ex_prop_FLX.
Qed.
End RND_FLX.
......@@ -99,10 +99,11 @@ rewrite round_UP_opp, <- opp_F2R.
now apply f_equal.
Qed.
Definition NE_ex_prop := Zeven beta = false \/ forall e,
Class Exists_NE :=
exists_NE : Zeven beta = false \/ forall e,
((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e).
Hypothesis strong_fexp : NE_ex_prop.
Context { exists_NE_ : Exists_NE }.
Theorem DN_UP_parity_generic_pos :
DN_UP_parity_pos_prop.
......@@ -135,7 +136,7 @@ now apply valid_exp.
rewrite Hd3, Hu3.
rewrite Zmult_1_l.
simpl.
destruct strong_fexp as [H|H].
destruct exists_NE_ as [H|H].
apply Zeven_Zpower_odd with (2 := H).
apply Zle_minus_le_0.
now apply valid_exp.
......@@ -211,7 +212,7 @@ rewrite eqb_sym. simpl.
fold (negb (Zeven (beta ^ (ex - fexp ex)))).
rewrite Bool.negb_involutive.
rewrite (Zeven_Zpower beta (ex - fexp ex)). 2: omega.
destruct strong_fexp.
destruct exists_NE_.
rewrite H.
apply Zeven_Zpower_odd with (2 := H).
now apply Zle_minus_le_0.
......@@ -411,7 +412,7 @@ rewrite ln_beta_bpow.
rewrite <- bpow_plus, <- Z2R_Zpower.
rewrite Ztrunc_Z2R.
case_eq (Zeven beta) ; intros Hr.
destruct strong_fexp as [Hs|Hs].
destruct exists_NE_ as [Hs|Hs].
now rewrite Hs in Hr.
destruct (Hs ex) as (H,_).
rewrite Zeven_Zpower.
......
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