diff options
Diffstat (limited to 'flocq/Prop/Round_odd.v')
| -rw-r--r-- | flocq/Prop/Round_odd.v | 1220 |
1 files changed, 1220 insertions, 0 deletions
diff --git a/flocq/Prop/Round_odd.v b/flocq/Prop/Round_odd.v new file mode 100644 index 00000000..df2952cc --- /dev/null +++ b/flocq/Prop/Round_odd.v @@ -0,0 +1,1220 @@ +(** +This file is part of the Flocq formalization of floating-point +arithmetic in Coq: http://flocq.gforge.inria.fr/ + +Copyright (C) 2013-2018 Sylvie Boldo +#<br /># +Copyright (C) 2013-2018 Guillaume Melquiond + +This library is free software; you can redistribute it and/or +modify it under the terms of the GNU Lesser General Public +License as published by the Free Software Foundation; either +version 3 of the License, or (at your option) any later version. + +This library is distributed in the hope that it will be useful, +but WITHOUT ANY WARRANTY; without even the implied warranty of +MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +COPYING file for more details. +*) + +(** * Rounding to odd and its properties, including the equivalence + between rnd_NE and double rounding with rnd_odd and then rnd_NE *) + +Require Import Reals Psatz. +Require Import Core Operations. + +Definition Zrnd_odd x := match Req_EM_T x (IZR (Zfloor x)) with + | left _ => Zfloor x + | right _ => match (Z.even (Zfloor x)) with + | true => Zceil x + | false => Zfloor x + end + end. + + + +Global Instance valid_rnd_odd : Valid_rnd Zrnd_odd. +Proof. +split. +(* . *) +intros x y Hxy. +assert (Zfloor x <= Zrnd_odd y)%Z. +(* .. *) +apply Z.le_trans with (Zfloor y). +now apply Zfloor_le. +unfold Zrnd_odd; destruct (Req_EM_T y (IZR (Zfloor y))). +now apply Z.le_refl. +case (Z.even (Zfloor y)). +apply le_IZR. +apply Rle_trans with y. +apply Zfloor_lb. +apply Zceil_ub. +now apply Z.le_refl. +unfold Zrnd_odd at 1. +(* . *) +destruct (Req_EM_T x (IZR (Zfloor x))) as [Hx|Hx]. +(* .. *) +apply H. +(* .. *) +case_eq (Z.even (Zfloor x)); intros Hx2. +2: apply H. +unfold Zrnd_odd; destruct (Req_EM_T y (IZR (Zfloor y))) as [Hy|Hy]. +apply Zceil_glb. +now rewrite <- Hy. +case_eq (Z.even (Zfloor y)); intros Hy2. +now apply Zceil_le. +apply Zceil_glb. +assert (H0:(Zfloor x <= Zfloor y)%Z) by now apply Zfloor_le. +case (Zle_lt_or_eq _ _ H0); intros H1. +apply Rle_trans with (1:=Zceil_ub _). +rewrite Zceil_floor_neq. +apply IZR_le; omega. +now apply sym_not_eq. +contradict Hy2. +rewrite <- H1, Hx2; discriminate. +(* . *) +intros n; unfold Zrnd_odd. +rewrite Zfloor_IZR, Zceil_IZR. +destruct (Req_EM_T (IZR n) (IZR n)); trivial. +case (Z.even n); trivial. +Qed. + + + +Lemma Zrnd_odd_Zodd: forall x, x <> (IZR (Zfloor x)) -> + (Z.even (Zrnd_odd x)) = false. +Proof. +intros x Hx; unfold Zrnd_odd. +destruct (Req_EM_T x (IZR (Zfloor x))) as [H|H]. +now contradict H. +case_eq (Z.even (Zfloor x)). +(* difficult case *) +intros H'. +rewrite Zceil_floor_neq. +rewrite Z.even_add, H'. +reflexivity. +now apply sym_not_eq. +trivial. +Qed. + + +Lemma Zfloor_plus: forall (n:Z) y, + (Zfloor (IZR n+y) = n + Zfloor y)%Z. +Proof. +intros n y; unfold Zfloor. +unfold Zminus; rewrite Zplus_assoc; f_equal. +apply sym_eq, tech_up. +rewrite plus_IZR. +apply Rplus_lt_compat_l. +apply archimed. +rewrite plus_IZR, Rplus_assoc. +apply Rplus_le_compat_l. +apply Rplus_le_reg_r with (-y)%R. +ring_simplify (y+1+-y)%R. +apply archimed. +Qed. + +Lemma Zceil_plus: forall (n:Z) y, + (Zceil (IZR n+y) = n + Zceil y)%Z. +Proof. +intros n y; unfold Zceil. +rewrite Ropp_plus_distr, <- Ropp_Ropp_IZR. +rewrite Zfloor_plus. +ring. +Qed. + + +Lemma Zeven_abs: forall z, Z.even (Z.abs z) = Z.even z. +Proof. +intros z; case (Zle_or_lt z 0); intros H1. +rewrite Z.abs_neq; try assumption. +apply Z.even_opp. +rewrite Z.abs_eq; auto with zarith. +Qed. + + + + +Lemma Zrnd_odd_plus: forall x y, (x = IZR (Zfloor x)) -> + Z.even (Zfloor x) = true -> + (IZR (Zrnd_odd (x+y)) = x+IZR (Zrnd_odd y))%R. +Proof. +intros x y Hx H. +unfold Zrnd_odd; rewrite Hx, Zfloor_plus. +case (Req_EM_T y (IZR (Zfloor y))); intros Hy. +rewrite Hy; repeat rewrite <- plus_IZR. +repeat rewrite Zfloor_IZR. +case (Req_EM_T _ _); intros K; easy. +case (Req_EM_T _ _); intros K. +contradict Hy. +apply Rplus_eq_reg_l with (IZR (Zfloor x)). +now rewrite K, plus_IZR. +rewrite Z.even_add, H; simpl. +case (Z.even (Zfloor y)). +now rewrite Zceil_plus, plus_IZR. +now rewrite plus_IZR. +Qed. + + +Section Fcore_rnd_odd. + +Variable beta : radix. + +Notation bpow e := (bpow beta e). + +Variable fexp : Z -> Z. + +Context { valid_exp : Valid_exp fexp }. +Context { exists_NE_ : Exists_NE beta fexp }. + +Notation format := (generic_format beta fexp). +Notation canonical := (canonical beta fexp). +Notation cexp := (cexp beta fexp). + + +Definition Rnd_odd_pt (x f : R) := + format f /\ ((f = x)%R \/ + ((Rnd_DN_pt format x f \/ Rnd_UP_pt format x f) /\ + exists g : float beta, f = F2R g /\ canonical g /\ Z.even (Fnum g) = false)). + +Definition Rnd_odd (rnd : R -> R) := + forall x : R, Rnd_odd_pt x (rnd x). + +Theorem Rnd_odd_pt_opp_inv : forall x f : R, + Rnd_odd_pt (-x) (-f) -> Rnd_odd_pt x f. +Proof with auto with typeclass_instances. +intros x f (H1,H2). +split. +replace f with (-(-f))%R by ring. +now apply generic_format_opp. +destruct H2. +left. +replace f with (-(-f))%R by ring. +rewrite H; ring. +right. +destruct H as (H2,(g,(Hg1,(Hg2,Hg3)))). +split. +destruct H2. +right. +replace f with (-(-f))%R by ring. +replace x with (-(-x))%R by ring. +apply Rnd_UP_pt_opp... +apply generic_format_opp. +left. +replace f with (-(-f))%R by ring. +replace x with (-(-x))%R by ring. +apply Rnd_DN_pt_opp... +apply generic_format_opp. +exists (Float beta (-Fnum g) (Fexp g)). +split. +rewrite F2R_Zopp. +replace f with (-(-f))%R by ring. +rewrite Hg1; reflexivity. +split. +now apply canonical_opp. +simpl. +now rewrite Z.even_opp. +Qed. + + +Theorem round_odd_opp : + forall x, + round beta fexp Zrnd_odd (-x) = (- round beta fexp Zrnd_odd x)%R. +Proof. +intros x; unfold round. +rewrite <- F2R_Zopp. +unfold F2R; simpl. +apply f_equal2; apply f_equal. +rewrite scaled_mantissa_opp. +generalize (scaled_mantissa beta fexp x); intros r. +unfold Zrnd_odd. +case (Req_EM_T (- r) (IZR (Zfloor (- r)))). +case (Req_EM_T r (IZR (Zfloor r))). +intros Y1 Y2. +apply eq_IZR. +now rewrite opp_IZR, <- Y1, <-Y2. +intros Y1 Y2. +absurd (r=IZR (Zfloor r)); trivial. +pattern r at 2; replace r with (-(-r))%R by ring. +rewrite Y2, <- opp_IZR. +rewrite Zfloor_IZR. +rewrite opp_IZR, <- Y2. +ring. +case (Req_EM_T r (IZR (Zfloor r))). +intros Y1 Y2. +absurd (-r=IZR (Zfloor (-r)))%R; trivial. +pattern r at 2; rewrite Y1. +rewrite <- opp_IZR, Zfloor_IZR. +now rewrite opp_IZR, <- Y1. +intros Y1 Y2. +unfold Zceil; rewrite Ropp_involutive. +replace (Z.even (Zfloor (- r))) with (negb (Z.even (Zfloor r))). +case (Z.even (Zfloor r)); simpl; ring. +apply trans_eq with (Z.even (Zceil r)). +rewrite Zceil_floor_neq. +rewrite Z.even_add. +destruct (Z.even (Zfloor r)); reflexivity. +now apply sym_not_eq. +rewrite <- (Z.even_opp (Zfloor (- r))). +reflexivity. +apply cexp_opp. +Qed. + + + +Theorem round_odd_pt : + forall x, + Rnd_odd_pt x (round beta fexp Zrnd_odd x). +Proof with auto with typeclass_instances. +cut (forall x : R, (0 < x)%R -> Rnd_odd_pt x (round beta fexp Zrnd_odd x)). +intros H x; case (Rle_or_lt 0 x). +intros H1; destruct H1. +now apply H. +rewrite <- H0. +rewrite round_0... +split. +apply generic_format_0. +now left. +intros Hx; apply Rnd_odd_pt_opp_inv. +rewrite <- round_odd_opp. +apply H. +auto with real. +(* *) +intros x Hxp. +generalize (generic_format_round beta fexp Zrnd_odd x). +set (o:=round beta fexp Zrnd_odd x). +intros Ho. +split. +assumption. +(* *) +case (Req_dec o x); intros Hx. +now left. +right. +assert (o=round beta fexp Zfloor x \/ o=round beta fexp Zceil x). +unfold o, round, F2R;simpl. +case (Zrnd_DN_or_UP Zrnd_odd (scaled_mantissa beta fexp x))... +intros H; rewrite H; now left. +intros H; rewrite H; now right. +split. +destruct H; rewrite H. +left; apply round_DN_pt... +right; apply round_UP_pt... +(* *) +unfold o, Zrnd_odd, round. +case (Req_EM_T (scaled_mantissa beta fexp x) + (IZR (Zfloor (scaled_mantissa beta fexp x)))). +intros T. +absurd (o=x); trivial. +apply round_generic... +unfold generic_format, F2R; simpl. +rewrite <- (scaled_mantissa_mult_bpow beta fexp) at 1. +apply f_equal2; trivial; rewrite T at 1. +apply f_equal, sym_eq, Ztrunc_floor. +apply Rmult_le_pos. +now left. +apply bpow_ge_0. +intros L. +case_eq (Z.even (Zfloor (scaled_mantissa beta fexp x))). +(* . *) +generalize (generic_format_round beta fexp Zceil x). +unfold generic_format. +set (f:=round beta fexp Zceil x). +set (ef := cexp f). +set (mf := Ztrunc (scaled_mantissa beta fexp f)). +exists (Float beta mf ef). +unfold canonical. +rewrite <- H0. +repeat split; try assumption. +apply trans_eq with (negb (Z.even (Zfloor (scaled_mantissa beta fexp x)))). +2: rewrite H1; reflexivity. +apply trans_eq with (negb (Z.even (Fnum + (Float beta (Zfloor (scaled_mantissa beta fexp x)) (cexp x))))). +2: reflexivity. +case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)). +rewrite <- round_0 with beta fexp Zfloor... +apply round_le... +now left. +intros Y. +generalize (DN_UP_parity_generic beta fexp)... +unfold DN_UP_parity_prop. +intros T; apply T with x; clear T. +unfold generic_format. +rewrite <- (scaled_mantissa_mult_bpow beta fexp x) at 1. +unfold F2R; simpl. +apply Rmult_neq_compat_r. +apply Rgt_not_eq, bpow_gt_0. +rewrite Ztrunc_floor. +assumption. +apply Rmult_le_pos. +now left. +apply bpow_ge_0. +unfold canonical. +simpl. +apply sym_eq, cexp_DN... +unfold canonical. +rewrite <- H0; reflexivity. +reflexivity. +apply trans_eq with (round beta fexp Ztrunc (round beta fexp Zceil x)). +reflexivity. +apply round_generic... +intros Y. +replace (Fnum {| Fnum := Zfloor (scaled_mantissa beta fexp x); Fexp := cexp x |}) + with (Fnum (Float beta 0 (fexp (mag beta 0)))). +generalize (DN_UP_parity_generic beta fexp)... +unfold DN_UP_parity_prop. +intros T; apply T with x; clear T. +unfold generic_format. +rewrite <- (scaled_mantissa_mult_bpow beta fexp x) at 1. +unfold F2R; simpl. +apply Rmult_neq_compat_r. +apply Rgt_not_eq, bpow_gt_0. +rewrite Ztrunc_floor. +assumption. +apply Rmult_le_pos. +now left. +apply bpow_ge_0. +apply canonical_0. +unfold canonical. +rewrite <- H0; reflexivity. +rewrite <- Y; unfold F2R; simpl; ring. +apply trans_eq with (round beta fexp Ztrunc (round beta fexp Zceil x)). +reflexivity. +apply round_generic... +simpl. +apply eq_IZR, Rmult_eq_reg_r with (bpow (cexp x)). +unfold round, F2R in Y; simpl in Y; rewrite <- Y. +simpl; ring. +apply Rgt_not_eq, bpow_gt_0. +(* . *) +intros Y. +case (Rle_lt_or_eq_dec 0 (round beta fexp Zfloor x)). +rewrite <- round_0 with beta fexp Zfloor... +apply round_le... +now left. +intros Hrx. +set (ef := cexp x). +set (mf := Zfloor (scaled_mantissa beta fexp x)). +exists (Float beta mf ef). +unfold canonical. +repeat split; try assumption. +simpl. +apply trans_eq with (cexp (round beta fexp Zfloor x )). +apply sym_eq, cexp_DN... +reflexivity. +intros Hrx; contradict Y. +replace (Zfloor (scaled_mantissa beta fexp x)) with 0%Z. +simpl; discriminate. +apply eq_IZR, Rmult_eq_reg_r with (bpow (cexp x)). +unfold round, F2R in Hrx; simpl in Hrx; rewrite <- Hrx. +simpl; ring. +apply Rgt_not_eq, bpow_gt_0. +Qed. + +Theorem Rnd_odd_pt_unique : + forall x f1 f2 : R, + Rnd_odd_pt x f1 -> Rnd_odd_pt x f2 -> + f1 = f2. +Proof. +intros x f1 f2 (Ff1,H1) (Ff2,H2). +(* *) +case (generic_format_EM beta fexp x); intros L. +apply trans_eq with x. +case H1; try easy. +intros (J,_); case J; intros J'. +apply Rnd_DN_pt_idempotent with format; assumption. +apply Rnd_UP_pt_idempotent with format; assumption. +case H2; try easy. +intros (J,_); case J; intros J'; apply sym_eq. +apply Rnd_DN_pt_idempotent with format; assumption. +apply Rnd_UP_pt_idempotent with format; assumption. +(* *) +destruct H1 as [H1|(H1,H1')]. +contradict L; now rewrite <- H1. +destruct H2 as [H2|(H2,H2')]. +contradict L; now rewrite <- H2. +destruct H1 as [H1|H1]; destruct H2 as [H2|H2]. +apply Rnd_DN_pt_unique with format x; assumption. +destruct H1' as (ff,(K1,(K2,K3))). +destruct H2' as (gg,(L1,(L2,L3))). +absurd (true = false); try discriminate. +rewrite <- L3. +apply trans_eq with (negb (Z.even (Fnum ff))). +rewrite K3; easy. +apply sym_eq. +generalize (DN_UP_parity_generic beta fexp). +unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption... +rewrite <- K1; apply Rnd_DN_pt_unique with (generic_format beta fexp) x; try easy... +now apply round_DN_pt... +rewrite <- L1; apply Rnd_UP_pt_unique with (generic_format beta fexp) x; try easy... +now apply round_UP_pt... +(* *) +destruct H1' as (ff,(K1,(K2,K3))). +destruct H2' as (gg,(L1,(L2,L3))). +absurd (true = false); try discriminate. +rewrite <- K3. +apply trans_eq with (negb (Z.even (Fnum gg))). +rewrite L3; easy. +apply sym_eq. +generalize (DN_UP_parity_generic beta fexp). +unfold DN_UP_parity_prop; intros T; apply (T x); clear T; try assumption... +rewrite <- L1; apply Rnd_DN_pt_unique with (generic_format beta fexp) x; try easy... +now apply round_DN_pt... +rewrite <- K1; apply Rnd_UP_pt_unique with (generic_format beta fexp) x; try easy... +now apply round_UP_pt... +apply Rnd_UP_pt_unique with format x; assumption. +Qed. + +Theorem Rnd_odd_pt_monotone : + round_pred_monotone (Rnd_odd_pt). +Proof with auto with typeclass_instances. +intros x y f g H1 H2 Hxy. +apply Rle_trans with (round beta fexp Zrnd_odd x). +right; apply Rnd_odd_pt_unique with x; try assumption. +apply round_odd_pt. +apply Rle_trans with (round beta fexp Zrnd_odd y). +apply round_le... +right; apply Rnd_odd_pt_unique with y; try assumption. +apply round_odd_pt. +Qed. + +End Fcore_rnd_odd. + +Section Odd_prop_aux. + +Variable beta : radix. +Hypothesis Even_beta: Z.even (radix_val beta)=true. + +Notation bpow e := (bpow beta e). + +Variable fexp : Z -> Z. +Variable fexpe : Z -> Z. + +Context { valid_exp : Valid_exp fexp }. +Context { exists_NE_ : Exists_NE beta fexp }. (* for underflow reason *) +Context { valid_expe : Valid_exp fexpe }. +Context { exists_NE_e : Exists_NE beta fexpe }. (* for defining rounding to odd *) + +Hypothesis fexpe_fexp: forall e, (fexpe e <= fexp e -2)%Z. + + +Lemma generic_format_fexpe_fexp: forall x, + generic_format beta fexp x -> generic_format beta fexpe x. +Proof. +intros x Hx. +apply generic_inclusion_mag with fexp; trivial; intros Hx2. +generalize (fexpe_fexp (mag beta x)). +omega. +Qed. + + + +Lemma exists_even_fexp_lt: forall (c:Z->Z), forall (x:R), + (exists f:float beta, F2R f = x /\ (c (mag beta x) < Fexp f)%Z) -> + exists f:float beta, F2R f =x /\ canonical beta c f /\ Z.even (Fnum f) = true. +Proof with auto with typeclass_instances. +intros c x (g,(Hg1,Hg2)). +exists (Float beta + (Fnum g*Z.pow (radix_val beta) (Fexp g - c (mag beta x))) + (c (mag beta x))). +assert (F2R (Float beta + (Fnum g*Z.pow (radix_val beta) (Fexp g - c (mag beta x))) + (c (mag beta x))) = x). +unfold F2R; simpl. +rewrite mult_IZR, IZR_Zpower. +rewrite Rmult_assoc, <- bpow_plus. +rewrite <- Hg1; unfold F2R. +apply f_equal, f_equal. +ring. +omega. +split; trivial. +split. +unfold canonical, cexp. +now rewrite H. +simpl. +rewrite Z.even_mul. +rewrite Z.even_pow. +rewrite Even_beta. +apply Bool.orb_true_intro. +now right. +omega. +Qed. + + +Variable choice:Z->bool. +Variable x:R. + + +Variable d u: float beta. +Hypothesis Hd: Rnd_DN_pt (generic_format beta fexp) x (F2R d). +Hypothesis Cd: canonical beta fexp d. +Hypothesis Hu: Rnd_UP_pt (generic_format beta fexp) x (F2R u). +Hypothesis Cu: canonical beta fexp u. + +Hypothesis xPos: (0 < x)%R. + + +Let m:= ((F2R d+F2R u)/2)%R. + + +Lemma d_eq: F2R d= round beta fexp Zfloor x. +Proof with auto with typeclass_instances. +apply Rnd_DN_pt_unique with (generic_format beta fexp) x... +apply round_DN_pt... +Qed. + + +Lemma u_eq: F2R u= round beta fexp Zceil x. +Proof with auto with typeclass_instances. +apply Rnd_UP_pt_unique with (generic_format beta fexp) x... +apply round_UP_pt... +Qed. + + +Lemma d_ge_0: (0 <= F2R d)%R. +Proof with auto with typeclass_instances. +rewrite d_eq; apply round_ge_generic... +apply generic_format_0. +now left. +Qed. + + + +Lemma mag_d: (0< F2R d)%R -> + (mag beta (F2R d) = mag beta x :>Z). +Proof with auto with typeclass_instances. +intros Y. +rewrite d_eq; apply mag_DN... +now rewrite <- d_eq. +Qed. + + +Lemma Fexp_d: (0 < F2R d)%R -> Fexp d =fexp (mag beta x). +Proof with auto with typeclass_instances. +intros Y. +now rewrite Cd, <- mag_d. +Qed. + + + +Lemma format_bpow_x: (0 < F2R d)%R + -> generic_format beta fexp (bpow (mag beta x)). +Proof with auto with typeclass_instances. +intros Y. +apply generic_format_bpow. +apply valid_exp. +rewrite <- Fexp_d; trivial. +apply Z.lt_le_trans with (mag beta (F2R d))%Z. +rewrite Cd; apply mag_generic_gt... +now apply Rgt_not_eq. +apply Hd. +apply mag_le; trivial. +apply Hd. +Qed. + + +Lemma format_bpow_d: (0 < F2R d)%R -> + generic_format beta fexp (bpow (mag beta (F2R d))). +Proof with auto with typeclass_instances. +intros Y; apply generic_format_bpow. +apply valid_exp. +apply mag_generic_gt... +now apply Rgt_not_eq. +now apply generic_format_canonical. +Qed. + + +Lemma d_le_m: (F2R d <= m)%R. +Proof. +assert (F2R d <= F2R u)%R. + apply Rle_trans with x. + apply Hd. + apply Hu. +unfold m. +lra. +Qed. + +Lemma m_le_u: (m <= F2R u)%R. +Proof. +assert (F2R d <= F2R u)%R. + apply Rle_trans with x. + apply Hd. + apply Hu. +unfold m. +lra. +Qed. + +Lemma mag_m: (0 < F2R d)%R -> (mag beta m =mag beta (F2R d) :>Z). +Proof with auto with typeclass_instances. +intros dPos; apply mag_unique_pos. +split. +apply Rle_trans with (F2R d). +destruct (mag beta (F2R d)) as (e,He). +simpl. +rewrite Rabs_right in He. +apply He. +now apply Rgt_not_eq. +apply Rle_ge; now left. +apply d_le_m. +case m_le_u; intros H. +apply Rlt_le_trans with (1:=H). +rewrite u_eq. +apply round_le_generic... +apply generic_format_bpow. +apply valid_exp. +apply mag_generic_gt... +now apply Rgt_not_eq. +now apply generic_format_canonical. +case (Rle_or_lt x (bpow (mag beta (F2R d)))); trivial; intros Z. +absurd ((bpow (mag beta (F2R d)) <= (F2R d)))%R. +apply Rlt_not_le. +destruct (mag beta (F2R d)) as (e,He). +simpl in *; rewrite Rabs_right in He. +apply He. +now apply Rgt_not_eq. +apply Rle_ge; now left. +apply Rle_trans with (round beta fexp Zfloor x). +2: right; apply sym_eq, d_eq. +apply round_ge_generic... +apply generic_format_bpow. +apply valid_exp. +apply mag_generic_gt... +now apply Rgt_not_eq. +now apply generic_format_canonical. +now left. +replace m with (F2R d). +destruct (mag beta (F2R d)) as (e,He). +simpl in *; rewrite Rabs_right in He. +apply He. +now apply Rgt_not_eq. +apply Rle_ge; now left. +unfold m in H |- *. +lra. +Qed. + + +Lemma mag_m_0: (0 = F2R d)%R + -> (mag beta m =mag beta (F2R u)-1:>Z)%Z. +Proof with auto with typeclass_instances. +intros Y. +apply mag_unique_pos. +unfold m; rewrite <- Y, Rplus_0_l. +rewrite u_eq. +destruct (mag beta x) as (e,He). +rewrite Rabs_pos_eq in He by now apply Rlt_le. +rewrite round_UP_small_pos with (ex:=e). +rewrite mag_bpow. +ring_simplify (fexp e + 1 - 1)%Z. +split. +unfold Zminus; rewrite bpow_plus. +unfold Rdiv; apply Rmult_le_compat_l. +apply bpow_ge_0. +simpl; unfold Z.pow_pos; simpl. +rewrite Zmult_1_r; apply Rinv_le. +exact Rlt_0_2. +apply IZR_le. +specialize (radix_gt_1 beta). +omega. +apply Rlt_le_trans with (bpow (fexp e)*1)%R. +2: right; ring. +unfold Rdiv; apply Rmult_lt_compat_l. +apply bpow_gt_0. +lra. +now apply He, Rgt_not_eq. +apply exp_small_round_0_pos with beta (Zfloor) x... +now apply He, Rgt_not_eq. +now rewrite <- d_eq, Y. +Qed. + + + + + +Lemma u'_eq: (0 < F2R d)%R -> exists f:float beta, F2R f = F2R u /\ (Fexp f = Fexp d)%Z. +Proof with auto with typeclass_instances. +intros Y. +rewrite u_eq; unfold round. +eexists; repeat split. +simpl; now rewrite Fexp_d. +Qed. + + +Lemma m_eq : + (0 < F2R d)%R -> + exists f:float beta, + F2R f = m /\ (Fexp f = fexp (mag beta x) - 1)%Z. +Proof with auto with typeclass_instances. +intros Y. +specialize (Zeven_ex (radix_val beta)); rewrite Even_beta. +intros (b, Hb); rewrite Zplus_0_r in Hb. +destruct u'_eq as (u', (Hu'1,Hu'2)); trivial. +exists (Fmult (Float beta b (-1)) (Fplus d u'))%R. +split. +rewrite F2R_mult, F2R_plus, Hu'1. +unfold m; rewrite Rmult_comm. +unfold Rdiv; apply f_equal. +unfold F2R; simpl; unfold Z.pow_pos; simpl. +rewrite Zmult_1_r, Hb, mult_IZR. +simpl; field. +apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2). +rewrite Rmult_0_r, <- (mult_IZR 2), <-Hb. +apply radix_pos. +apply trans_eq with (-1+Fexp (Fplus d u'))%Z. +unfold Fmult. +destruct (Fplus d u'); reflexivity. +rewrite Zplus_comm; unfold Zminus; apply f_equal2. +2: reflexivity. +rewrite Fexp_Fplus. +rewrite Z.min_l. +now rewrite Fexp_d. +rewrite Hu'2; omega. +Qed. + +Lemma m_eq_0: (0 = F2R d)%R -> exists f:float beta, + F2R f = m /\ (Fexp f = fexp (mag beta (F2R u)) -1)%Z. +Proof with auto with typeclass_instances. +intros Y. +specialize (Zeven_ex (radix_val beta)); rewrite Even_beta. +intros (b, Hb); rewrite Zplus_0_r in Hb. +exists (Fmult (Float beta b (-1)) u)%R. +split. +rewrite F2R_mult; unfold m; rewrite <- Y, Rplus_0_l. +rewrite Rmult_comm. +unfold Rdiv; apply f_equal. +unfold F2R; simpl; unfold Z.pow_pos; simpl. +rewrite Zmult_1_r, Hb, mult_IZR. +simpl; field. +apply Rgt_not_eq, Rmult_lt_reg_l with (1 := Rlt_0_2). +rewrite Rmult_0_r, <- (mult_IZR 2), <-Hb. +apply radix_pos. +apply trans_eq with (-1+Fexp u)%Z. +unfold Fmult. +destruct u; reflexivity. +rewrite Zplus_comm, Cu; unfold Zminus; now apply f_equal2. +Qed. + +Lemma fexp_m_eq_0: (0 = F2R d)%R -> + (fexp (mag beta (F2R u)-1) < fexp (mag beta (F2R u))+1)%Z. +Proof with auto with typeclass_instances. +intros Y. +assert ((fexp (mag beta (F2R u) - 1) <= fexp (mag beta (F2R u))))%Z. +2: omega. +destruct (mag beta x) as (e,He). +rewrite Rabs_right in He. +2: now left. +assert (e <= fexp e)%Z. +apply exp_small_round_0_pos with beta (Zfloor) x... +now apply He, Rgt_not_eq. +now rewrite <- d_eq, Y. +rewrite u_eq, round_UP_small_pos with (ex:=e); trivial. +2: now apply He, Rgt_not_eq. +rewrite mag_bpow. +ring_simplify (fexp e + 1 - 1)%Z. +replace (fexp (fexp e)) with (fexp e). +case exists_NE_; intros V. +contradict V; rewrite Even_beta; discriminate. +rewrite (proj2 (V e)); omega. +apply sym_eq, valid_exp; omega. +Qed. + +Lemma Fm: generic_format beta fexpe m. +Proof. +case (d_ge_0); intros Y. +(* *) +destruct m_eq as (g,(Hg1,Hg2)); trivial. +apply generic_format_F2R' with g. +now apply sym_eq. +intros H; unfold cexp; rewrite Hg2. +rewrite mag_m; trivial. +rewrite <- Fexp_d; trivial. +rewrite Cd. +unfold cexp. +generalize (fexpe_fexp (mag beta (F2R d))). +omega. +(* *) +destruct m_eq_0 as (g,(Hg1,Hg2)); trivial. +apply generic_format_F2R' with g. +assumption. +intros H; unfold cexp; rewrite Hg2. +rewrite mag_m_0; try assumption. +apply Z.le_trans with (1:=fexpe_fexp _). +generalize (fexp_m_eq_0 Y). +omega. +Qed. + + + +Lemma Zm: + exists g : float beta, F2R g = m /\ canonical beta fexpe g /\ Z.even (Fnum g) = true. +Proof with auto with typeclass_instances. +case (d_ge_0); intros Y. +(* *) +destruct m_eq as (g,(Hg1,Hg2)); trivial. +apply exists_even_fexp_lt. +exists g; split; trivial. +rewrite Hg2. +rewrite mag_m; trivial. +rewrite <- Fexp_d; trivial. +rewrite Cd. +unfold cexp. +generalize (fexpe_fexp (mag beta (F2R d))). +omega. +(* *) +destruct m_eq_0 as (g,(Hg1,Hg2)); trivial. +apply exists_even_fexp_lt. +exists g; split; trivial. +rewrite Hg2. +rewrite mag_m_0; trivial. +apply Z.le_lt_trans with (1:=fexpe_fexp _). +generalize (fexp_m_eq_0 Y). +omega. +Qed. + + +Lemma DN_odd_d_aux : + forall z, (F2R d <= z < F2R u)%R -> + Rnd_DN_pt (generic_format beta fexp) z (F2R d). +Proof with auto with typeclass_instances. +intros z Hz1. +replace (F2R d) with (round beta fexp Zfloor z). +apply round_DN_pt... +case (Rnd_DN_UP_pt_split _ _ _ _ Hd Hu (round beta fexp Zfloor z)). +apply generic_format_round... +intros Y; apply Rle_antisym; trivial. +apply round_DN_pt... +apply Hd. +apply Hz1. +intros Y ; elim (Rlt_irrefl z). +apply Rlt_le_trans with (1:=proj2 Hz1), Rle_trans with (1:=Y). +apply round_DN_pt... +Qed. + +Lemma UP_odd_d_aux : + forall z, (F2R d < z <= F2R u)%R -> + Rnd_UP_pt (generic_format beta fexp) z (F2R u). +Proof with auto with typeclass_instances. +intros z Hz1. +replace (F2R u) with (round beta fexp Zceil z). +apply round_UP_pt... +case (Rnd_DN_UP_pt_split _ _ _ _ Hd Hu (round beta fexp Zceil z)). +apply generic_format_round... +intros Y ; elim (Rlt_irrefl z). +apply Rle_lt_trans with (2:=proj1 Hz1), Rle_trans with (2:=Y). +apply round_UP_pt... +intros Y; apply Rle_antisym; trivial. +apply round_UP_pt... +apply Hu. +apply Hz1. +Qed. + + +Lemma round_N_odd_pos : + round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) = + round beta fexp (Znearest choice) x. +Proof with auto with typeclass_instances. +set (o:=round beta fexpe Zrnd_odd x). +case (generic_format_EM beta fexp x); intros Hx. +replace o with x; trivial. +unfold o; apply sym_eq, round_generic... +now apply generic_format_fexpe_fexp. +assert (K1:(F2R d <= o)%R). +apply round_ge_generic... +apply generic_format_fexpe_fexp, Hd. +apply Hd. +assert (K2:(o <= F2R u)%R). +apply round_le_generic... +apply generic_format_fexpe_fexp, Hu. +apply Hu. +assert (P:(x <> m -> o=m -> (forall P:Prop, P))). +intros Y1 Y2. +assert (H:(Rnd_odd_pt beta fexpe x o)). +apply round_odd_pt... +destruct H as (_,H); destruct H. +absurd (x=m)%R; try trivial. +now rewrite <- Y2, H. +destruct H as (_,(k,(Hk1,(Hk2,Hk3)))). +destruct Zm as (k',(Hk'1,(Hk'2,Hk'3))). +absurd (true=false). +discriminate. +rewrite <- Hk3, <- Hk'3. +apply f_equal, f_equal. +apply canonical_unique with fexpe... +now rewrite Hk'1, <- Y2. +assert (generic_format beta fexp o -> (forall P:Prop, P)). +intros Y. +assert (H:(Rnd_odd_pt beta fexpe x o)). +apply round_odd_pt... +destruct H as (_,H); destruct H. +absurd (generic_format beta fexp x); trivial. +now rewrite <- H. +destruct H as (_,(k,(Hk1,(Hk2,Hk3)))). +destruct (exists_even_fexp_lt fexpe o) as (k',(Hk'1,(Hk'2,Hk'3))). +eexists; split. +apply sym_eq, Y. +simpl; unfold cexp. +apply Z.le_lt_trans with (1:=fexpe_fexp _). +omega. +absurd (true=false). +discriminate. +rewrite <- Hk3, <- Hk'3. +apply f_equal, f_equal. +apply canonical_unique with fexpe... +now rewrite Hk'1, <- Hk1. +case K1; clear K1; intros K1. +2: apply H; rewrite <- K1; apply Hd. +case K2; clear K2; intros K2. +2: apply H; rewrite K2; apply Hu. +case (Rle_or_lt x m); intros Y;[destruct Y|idtac]. +(* . *) +apply trans_eq with (F2R d). +apply round_N_eq_DN_pt with (F2R u)... +apply DN_odd_d_aux; split; try left; assumption. +apply UP_odd_d_aux; split; try left; assumption. +assert (o <= (F2R d + F2R u) / 2)%R. +apply round_le_generic... +apply Fm. +now left. +destruct H1; trivial. +apply P. +now apply Rlt_not_eq. +trivial. +apply sym_eq, round_N_eq_DN_pt with (F2R u)... +(* . *) +replace o with x. +reflexivity. +apply sym_eq, round_generic... +rewrite H0; apply Fm. +(* . *) +apply trans_eq with (F2R u). +apply round_N_eq_UP_pt with (F2R d)... +apply DN_odd_d_aux; split; try left; assumption. +apply UP_odd_d_aux; split; try left; assumption. +assert ((F2R d + F2R u) / 2 <= o)%R. +apply round_ge_generic... +apply Fm. +now left. +destruct H0; trivial. +apply P. +now apply Rgt_not_eq. +rewrite <- H0; trivial. +apply sym_eq, round_N_eq_UP_pt with (F2R d)... +Qed. + + +End Odd_prop_aux. + +Section Odd_prop. + +Variable beta : radix. +Hypothesis Even_beta: Z.even (radix_val beta)=true. + +Variable fexp : Z -> Z. +Variable fexpe : Z -> Z. +Variable choice:Z->bool. + +Context { valid_exp : Valid_exp fexp }. +Context { exists_NE_ : Exists_NE beta fexp }. (* for underflow reason *) +Context { valid_expe : Valid_exp fexpe }. +Context { exists_NE_e : Exists_NE beta fexpe }. (* for defining rounding to odd *) + +Hypothesis fexpe_fexp: forall e, (fexpe e <= fexp e -2)%Z. + +Theorem round_N_odd : + forall x, + round beta fexp (Znearest choice) (round beta fexpe Zrnd_odd x) = + round beta fexp (Znearest choice) x. +Proof with auto with typeclass_instances. +intros x. +case (total_order_T x 0); intros H; [case H; clear H; intros H | idtac]. +rewrite <- (Ropp_involutive x). +rewrite round_odd_opp. +rewrite 2!round_N_opp. +apply f_equal. +destruct (canonical_generic_format beta fexp (round beta fexp Zfloor (-x))) as (d,(Hd1,Hd2)). +apply generic_format_round... +destruct (canonical_generic_format beta fexp (round beta fexp Zceil (-x))) as (u,(Hu1,Hu2)). +apply generic_format_round... +apply round_N_odd_pos with d u... +rewrite <- Hd1; apply round_DN_pt... +rewrite <- Hu1; apply round_UP_pt... +auto with real. +(* . *) +rewrite H; repeat rewrite round_0... +(* . *) +destruct (canonical_generic_format beta fexp (round beta fexp Zfloor x)) as (d,(Hd1,Hd2)). +apply generic_format_round... +destruct (canonical_generic_format beta fexp (round beta fexp Zceil x)) as (u,(Hu1,Hu2)). +apply generic_format_round... +apply round_N_odd_pos with d u... +rewrite <- Hd1; apply round_DN_pt... +rewrite <- Hu1; apply round_UP_pt... +Qed. + +End Odd_prop. + + +Section Odd_propbis. + +Variable beta : radix. +Hypothesis Even_beta: Z.even (radix_val beta)=true. + +Variable emin prec:Z. +Variable choice:Z->bool. + +Hypothesis prec_gt_1: (1 < prec)%Z. + + +Notation format := (generic_format beta (FLT_exp emin prec)). +Notation round_flt :=(round beta (FLT_exp emin prec) (Znearest choice)). +Notation cexp_flt := (cexp beta (FLT_exp emin prec)). +Notation fexpe k := (FLT_exp (emin-k) (prec+k)). + + + +Lemma Zrnd_odd_plus': forall x y, + (exists n:Z, exists e:Z, (x = IZR n*bpow beta e)%R /\ (1 <= e)%Z) -> + (IZR (Zrnd_odd (x+y)) = x+IZR (Zrnd_odd y))%R. +Proof. +intros x y (n,(e,(H1,H2))). +apply Zrnd_odd_plus. +rewrite H1. +rewrite <- IZR_Zpower. +2: auto with zarith. +now rewrite <- mult_IZR, Zfloor_IZR. +rewrite H1, <- IZR_Zpower. +2: auto with zarith. +rewrite <- mult_IZR, Zfloor_IZR. +rewrite Z.even_mul. +rewrite Z.even_pow. +2: auto with zarith. +rewrite Even_beta. +apply Bool.orb_true_iff; now right. +Qed. + + + +Theorem mag_round_odd: forall (x:R), + (emin < mag beta x)%Z -> + (mag_val beta _ (mag beta (round beta (FLT_exp emin prec) Zrnd_odd x)) + = mag_val beta x (mag beta x))%Z. +Proof with auto with typeclass_instances. +intros x. +assert (T:Prec_gt_0 prec). +unfold Prec_gt_0; auto with zarith. +case (Req_dec x 0); intros Zx. +intros _; rewrite Zx, round_0... +destruct (mag beta x) as (e,He); simpl; intros H. +apply mag_unique; split. +apply abs_round_ge_generic... +apply FLT_format_bpow... +auto with zarith. +now apply He. +assert (V: + (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <= bpow beta e)%R). +apply abs_round_le_generic... +apply FLT_format_bpow... +auto with zarith. +left; now apply He. +case V; try easy; intros K. +assert (H0:Rnd_odd_pt beta (FLT_exp emin prec) x (round beta (FLT_exp emin prec) Zrnd_odd x)). +apply round_odd_pt... +destruct H0 as (_,HH); destruct HH as [H0|(H0,(g,(Hg1,(Hg2,Hg3))))]. +absurd (Rabs x < bpow beta e)%R. +apply Rle_not_lt; right. +now rewrite <- H0,K. +now apply He. +pose (gg:=Float beta (Zpower beta (e-FLT_exp emin prec (e+1))) (FLT_exp emin prec (e+1))). +assert (Y1: F2R gg = bpow beta e). +unfold F2R; simpl. +rewrite IZR_Zpower. +rewrite <- bpow_plus. +f_equal; ring. +assert (FLT_exp emin prec (e+1) <= e)%Z; [idtac|auto with zarith]. +unfold FLT_exp. +apply Z.max_case_strong; auto with zarith. +assert (Y2: canonical beta (FLT_exp emin prec) gg). +unfold canonical; rewrite Y1; unfold gg; simpl. +unfold cexp; now rewrite mag_bpow. +assert (Y3: Fnum gg = Z.abs (Fnum g)). +apply trans_eq with (Fnum (Fabs g)). +2: destruct g; unfold Fabs; now simpl. +f_equal. +apply canonical_unique with (FLT_exp emin prec); try assumption. +destruct g; unfold Fabs; apply canonical_abs; easy. +now rewrite Y1, F2R_abs, <- Hg1,K. +assert (Y4: Z.even (Fnum gg) = true). +unfold gg; simpl. +rewrite Z.even_pow; try assumption. +assert (FLT_exp emin prec (e+1) < e)%Z; [idtac|auto with zarith]. +unfold FLT_exp. +apply Z.max_case_strong; auto with zarith. +absurd (true = false). +discriminate. +rewrite <- Hg3. +rewrite <- Zeven_abs. +now rewrite <- Y3. +Qed. + +Theorem fexp_round_odd: forall (x:R), + (cexp_flt (round beta (FLT_exp emin prec) Zrnd_odd x) + = cexp_flt x)%Z. +Proof with auto with typeclass_instances. +intros x. +assert (G0:Valid_exp (FLT_exp emin prec)). +apply FLT_exp_valid; unfold Prec_gt_0; auto with zarith. +case (Req_dec x 0); intros Zx. +rewrite Zx, round_0... +case (Zle_or_lt (mag beta x) emin). +unfold cexp; destruct (mag beta x) as (e,He); simpl. +intros H; unfold FLT_exp at 4. +rewrite Z.max_r. +2: auto with zarith. +apply Z.max_r. +assert (G: Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) = bpow beta emin). +assert (G1: (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <= bpow beta emin)%R). +apply abs_round_le_generic... +apply generic_format_bpow'... +unfold FLT_exp; rewrite Z.max_r; auto with zarith. +left; apply Rlt_le_trans with (bpow beta e). +now apply He. +now apply bpow_le. +assert (G2: (0 <= Rabs (round beta (FLT_exp emin prec) Zrnd_odd x))%R). +apply Rabs_pos. +assert (G3: (Rabs (round beta (FLT_exp emin prec) Zrnd_odd x) <> 0)%R). +assert (H0:Rnd_odd_pt beta (FLT_exp emin prec) x + (round beta (FLT_exp emin prec) Zrnd_odd x)). +apply round_odd_pt... +destruct H0 as (_,H0); destruct H0 as [H0|(_,(g,(Hg1,(Hg2,Hg3))))]. +apply Rgt_not_eq; rewrite H0. +apply Rlt_le_trans with (bpow beta (e-1)). +apply bpow_gt_0. +now apply He. +rewrite Hg1; intros K. +contradict Hg3. +replace (Fnum g) with 0%Z. +easy. +case (Z.eq_dec (Fnum g) Z0); intros W; try easy. +contradict K. +apply Rabs_no_R0. +now apply F2R_neq_0. +apply Rle_antisym; try assumption. +apply Rle_trans with (succ beta (FLT_exp emin prec) 0). +right; rewrite succ_0. +rewrite ulp_FLT_small; try easy. +unfold Prec_gt_0; auto with zarith. +rewrite Rabs_R0; apply bpow_gt_0. +apply succ_le_lt... +apply generic_format_0. +apply generic_format_abs; apply generic_format_round... +case G2; [easy|intros; now contradict G3]. +rewrite <- mag_abs. +rewrite G, mag_bpow; auto with zarith. +intros H; unfold cexp. +now rewrite mag_round_odd. +Qed. + + + + +End Odd_propbis. + + |