diff --git a/src/Calc/Fcalc_round.v b/src/Calc/Fcalc_round.v index fdc9737cef3cb386651b823caeac5c30093c1662..e84ff6db2f0a96bde4066cbe6f8e2ca25b894488 100644 --- a/src/Calc/Fcalc_round.v +++ b/src/Calc/Fcalc_round.v @@ -58,4 +58,141 @@ rewrite <- H. now apply rounding_generic. Qed. -End Fcalc_round. \ No newline at end of file +Definition round t := + let '(m, e, l) := t in + let k := (fexp (digits beta m + e) - e)%Z in + if Zlt_bool 0 k then + let p := Zpower (radix_val beta) k in + (Zdiv m p, (e + k)%Z, new_location p (Zmod m p) l) + else t. + +Theorem round_correct : + forall x m e l, + (0 <= x)%R -> + inbetween_float beta m e x l -> + (e <= fexp (digits beta m + e))%Z \/ l = loc_Exact -> + let '(m', e', l') := round (m, e, l) in + inbetween_float beta m' e' x l' /\ + (e' = canonic_exponent beta fexp x \/ (l' = loc_Exact /\ format x)). +Proof. +intros x m e l Hx H1 H2. +unfold round. +set (k := (fexp (digits beta m + e) - e)%Z). +set (p := Zpower (radix_val beta) k). +(* *) +assert (Hx': (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R). +apply inbetween_bounds with (2 := H1). +apply F2R_lt_compat. +apply Zlt_succ. +(* *) +assert (Hm: (0 <= m)%Z). +cut (0 < m + 1)%Z. omega. +apply F2R_lt_reg with beta e. +rewrite F2R_0. +apply Rle_lt_trans with (1 := Hx). +apply Hx'. +destruct Hx as [Hx|Hx]. +(* . 0 < x *) +assert (He: (e + k = canonic_exponent beta fexp x)%Z). +(* .. *) +unfold canonic_exponent. +destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm']. +(* ... 0 < m *) +rewrite ln_beta_F2R_bounds with (1 := Hm') (2 := Hx'). +assert (H: m <> Z0). +apply sym_not_eq. +now apply Zlt_not_eq. +rewrite ln_beta_F2R with (1 := H). +rewrite <- digits_ln_beta with (1 := H). +unfold k. +ring. +destruct H2 as [H2|H2]. +(* ... m = 0 and enough digits *) +rewrite <- Hm' in H2. +destruct (ln_beta beta x) as (ex, Hex). +simpl. +specialize (Hex (Rgt_not_eq _ _ Hx)). +unfold k. +ring_simplify. +rewrite <- Hm'. +simpl. +apply sym_eq. +apply (proj2 (prop_exp e)). +exact H2. +apply Zle_trans with e. +eapply bpow_lt_bpow. +apply Rle_lt_trans with (1 := proj1 Hex). +rewrite Rabs_pos_eq. +rewrite <- F2R_bpow. +rewrite <- Hm' in Hx'. +apply Hx'. +now apply Rlt_le. +exact H2. +(* ... m = 0 and exact location *) +rewrite H2 in H1. +inversion_clear H1. +rewrite <- Hm', F2R_0 in H. +rewrite H in Hx. +elim Rlt_irrefl with (1 := Hx). +(* .. *) +generalize (Zlt_cases 0 k). +case (Zlt_bool 0 k) ; intros Hk ; unfold k in Hk. +(* ... shift *) +split. +now apply inbetween_float_new_location. +now left. +split. +exact H1. +destruct H2 as [H2|H2]. +left. +rewrite <- He. +unfold k. +omega. +(* ... no shift *) +right. +split. +exact H2. +rewrite H2 in H1. +inversion_clear H1. +rewrite H. +apply generic_format_canonic_exponent. +rewrite <- H, <- He. +unfold k. +omega. +(* . x = 0 *) +destruct H1 as [H1|l' H1 _]. +(* .. exact location *) +case (Zlt_bool 0 k). +(* ... shift *) +assert (Hm': m = Z0). +apply F2R_eq_0_reg with beta e. +rewrite <- H1. +now apply sym_eq. +rewrite Hm'. +rewrite Zdiv_0_l, Zmod_0_l. +replace (new_location p 0 loc_Exact) with loc_Exact. +split. +constructor. +rewrite F2R_0. +now apply sym_eq. +right. +repeat split. +rewrite <- Hx. +apply generic_format_0. +unfold new_location. +case (Zeven p) ; [ unfold new_location_even | unfold new_location_odd ] ; + ( case Zeq_bool_spec ; [ easy | intros H ; now elim H ] ). +(* ... no shift *) +split. +now constructor. +right. +repeat split. +rewrite <- Hx. +apply generic_format_0. +(* .. inexact location *) +elim Rlt_not_le with (1 := proj1 H1). +rewrite <- Hx. +now apply F2R_ge_0_compat. +Qed. + +End Fcalc_round. diff --git a/src/Calc/Fcalc_round_FLX.v b/src/Calc/Fcalc_round_FLX.v deleted file mode 100644 index 61d40144ff93f48d63a4f21ffb0682997ae1bb92..0000000000000000000000000000000000000000 --- a/src/Calc/Fcalc_round_FLX.v +++ /dev/null @@ -1,114 +0,0 @@ -Require Import Fcore. -Require Import Fcalc_bracket. -Require Import Fcalc_digits. - -Section Fcalc_round_FLX. - -Variable beta : radix. -Notation bpow e := (bpow beta e). -Variable prec : Z. -Variable Hprec : (1 < prec)%Z. -Notation format := (generic_format beta (FLX_exp prec)). - -Definition round_FLX t := - let '(m, e, l) := t in - let k := (digits beta m - prec)%Z in - if Zlt_bool 0 k then - let p := Zpower (radix_val beta) k in - (Zdiv m p, (e + k)%Z, new_location p (Zmod m p) l) - else t. - -Theorem round_FLX_correct : - forall x m e l, - (0 <= x)%R -> - inbetween_float beta m e x l -> - (prec <= digits beta m)%Z \/ l = loc_Exact -> - let '(m', e', l') := round_FLX (m, e, l) in - inbetween_float beta m' e' x l' /\ - (e' = canonic_exponent beta (FLX_exp prec) x \/ (l' = loc_Exact /\ format x)). -Proof. -intros x m e l Hx H1 H2. -unfold round_FLX. -set (k := (digits beta m - prec)%Z). -set (p := Zpower (radix_val beta) k). -(* *) -assert (Hx': (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R). -apply inbetween_bounds with (2 := H1). -apply F2R_lt_compat. -apply Zlt_succ. -(* *) -assert (Hm: (0 <= m)%Z). -cut (0 < m + 1)%Z. omega. -apply F2R_lt_reg with beta e. -rewrite F2R_0. -apply Rle_lt_trans with (1 := Hx). -apply Hx'. -(* *) -assert (He: (m <> 0 -> e + k = canonic_exponent beta (FLX_exp prec) x)%Z). -intros H. -unfold canonic_exponent, FLX_exp. -rewrite ln_beta_F2R_bounds with (2 := Hx'). -rewrite ln_beta_F2R with (1 := H). -rewrite <- digits_ln_beta with (1 := H). -unfold k. -ring. -omega. -(* *) -assert (He': (prec <= digits beta m -> e + k = canonic_exponent beta (FLX_exp prec) x)%Z). -intros Hp. -apply He. -destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm']. -apply sym_not_eq. -now apply Zlt_not_eq. -rewrite <- Hm' in Hp. -simpl in Hp. -omega. -clear Hm. -generalize (Zlt_cases 0 k). -case (Zlt_bool 0 k) ; intros Hk ; unfold k in Hk. -(* shift *) -split. -now apply inbetween_float_new_location. -clear H2. -left. -apply He'. -omega. -(* no shift *) -split. -exact H1. -assert (H3: prec = digits beta m \/ ((digits beta m <= prec)%Z /\ l = loc_Exact)). -destruct H2 as [H2|H2]. -left. -omega. -right. -split. -omega. -easy. -clear H2. -destruct H3 as [H2|(H2,H3)]. -(* . matching prec *) -left. -rewrite <- He'. -unfold k. -rewrite H2. -ring. -rewrite H2. -apply Zle_refl. -(* . exact location *) -right. -split. -exact H3. -rewrite H3 in H1. -inversion_clear H1. -rewrite H. -destruct (Z_eq_dec m 0) as [Hm|Hm]. -rewrite Hm, F2R_0. -apply generic_format_0. -apply generic_format_canonic_exponent. -rewrite <- H, <- He. -unfold k. -omega. -exact Hm. -Qed. - -End Fcalc_round_FLX. diff --git a/src/Makefile.am b/src/Makefile.am index 4d3c8268acaf4609c308f28a19111e143eeca3db..6f23ccf381c0bea679f90c335b9cb230f1045a16 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -17,7 +17,6 @@ FILES = \ Calc/Fcalc_ops.v \ Calc/Fcalc_round.v \ Calc/Fcalc_round_FIX.v \ - Calc/Fcalc_round_FLX.v \ Calc/Fcalc_sqrt.v \ Prop/Fprop_nearest.v