diff options
Diffstat (limited to 'lib/IEEE754_extra.v')
| -rw-r--r-- | lib/IEEE754_extra.v | 416 |
1 files changed, 416 insertions, 0 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index b0d1944e..35feb29d 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -24,8 +24,206 @@ Require Import Psatz. Require Import Bool. Require Import Eqdep_dec. +Require Import Coq.Logic.FunctionalExtensionality. + Local Open Scope Z_scope. + +Lemma Znearest_lub : + forall choice (n : Z) (x : R), (IZR n <= x)%R -> (n <= Znearest choice x)%Z. +Proof. + intros until x. intro BND. + pose proof (Zfloor_lub n x BND). + pose proof (Znearest_ge_floor choice x). + lia. +Qed. + +Lemma Znearest_glb : + forall choice (n : Z) (x : R), (x <= IZR n)%R -> (Znearest choice x <= n)%Z. +Proof. + intros until x. intro BND. + pose proof (Zceil_glb n x BND). + pose proof (Znearest_le_ceil choice x). + lia. +Qed. + +Lemma Znearest_IZR : + forall choice n, (Znearest choice (IZR n)) = n. +Proof. + intros. + unfold Znearest. + case Rcompare_spec ; intro ORDER. + - apply Zfloor_IZR. + - destruct choice. + + apply Zceil_IZR. + + apply Zfloor_IZR. + - apply Zceil_IZR. +Qed. + +Lemma ZnearestE_IZR: + forall n, (ZnearestE (IZR n)) = n. +Proof. + apply Znearest_IZR. +Qed. + +Lemma Zfloor_opp : + forall x : R, (Zfloor (- x)) = - (Zceil x). +Proof. + unfold Zceil, Zfloor. + intro x. + rewrite Z.opp_involutive. + reflexivity. +Qed. + +Lemma Zceil_opp : + forall x : R, (Zceil (- x)) = - (Zfloor x). +Proof. + unfold Zceil, Zfloor. + intro x. + rewrite Ropp_involutive. + reflexivity. +Qed. + +Lemma ZnearestE_opp + : forall x : R, ZnearestE (- x) = - ZnearestE x. +Proof. + intro. + rewrite Znearest_opp. + f_equal. + f_equal. + apply functional_extensionality. + intro. + rewrite Z.even_opp. + fold (Z.succ x0). + rewrite Z.even_succ. + f_equal. + apply Z.negb_odd. +Qed. + +Lemma Zceil_non_floor: + forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x). +Proof. + intros x BETWEEN. + unfold Z.succ. + apply Zceil_imp. + split. + { rewrite minus_IZR. + rewrite plus_IZR. + lra. + } + rewrite plus_IZR. + pose proof (Zfloor_ub x). + lra. +Qed. + +(** more complicated way of proving +Lemma Zceil_non_ceil: + forall x : R, (x < IZR(Zceil x))%R -> Zceil x = Z.succ(Zfloor x). +Proof. + intros x BETWEEN. + unfold Z.succ. + cut (Zfloor x = (Zceil x) - 1). { intros; lia. } + apply Zfloor_imp. + split. + { rewrite minus_IZR. + pose proof (Zceil_lb x). + lra. + } + rewrite plus_IZR. + rewrite minus_IZR. + lra. +Qed. + +Lemma ZnearestE_opp + : forall x : R, ZnearestE (- x) = - ZnearestE x. +Proof. + intro x. + unfold ZnearestE. + case (Rcompare_spec (x - IZR (Zfloor x)) (/ 2)); intro CMP. + - pose proof (Zfloor_lb x) as LB. + destruct (Rcompare_spec x (IZR (Zfloor x))) as [ ABSURD | EXACT | INEXACT]. + lra. + { set (n := Zfloor x) in *. + rewrite EXACT. + rewrite <- opp_IZR. + rewrite Zfloor_IZR. + rewrite opp_IZR. + rewrite Rcompare_Lt by lra. + reflexivity. + } + rewrite Rcompare_Gt. + { apply Zceil_opp. } + rewrite Zfloor_opp. + rewrite opp_IZR. + rewrite Zceil_non_floor by assumption. + unfold Z.succ. + rewrite plus_IZR. + lra. + - rewrite Rcompare_Eq. + { rewrite Zceil_opp. + rewrite Zfloor_opp. + rewrite Z.even_opp. + rewrite Zceil_non_floor by lra. + rewrite Z.even_succ. + rewrite Z.negb_odd. + destruct (Z.even (Zfloor x)); reflexivity. + } + rewrite Zfloor_opp. + rewrite opp_IZR. + ring_simplify. + rewrite Zceil_non_floor by lra. + unfold Z.succ. + rewrite plus_IZR. + lra. + - rewrite Rcompare_Lt. + { apply Zfloor_opp. } + rewrite Zfloor_opp. + rewrite opp_IZR. + rewrite Zceil_non_floor by lra. + unfold Z.succ. + rewrite plus_IZR. + lra. +Qed. + *) + +Lemma Znearest_imp2: + forall choice x, (Rabs (IZR (Znearest choice x) - x) <= /2)%R. +Proof. + intros. + unfold Znearest. + pose proof (Zfloor_lb x) as FL. + pose proof (Zceil_ub x) as CU. + pose proof (Zceil_non_floor x) as NF. + case Rcompare_spec; intro CMP; apply Rabs_le; split; try lra. + - destruct choice; lra. + - destruct choice. 2: lra. + rewrite NF. 2: lra. + unfold Z.succ. rewrite plus_IZR. lra. + - rewrite NF. 2: lra. + unfold Z.succ. rewrite plus_IZR. lra. +Qed. + +Theorem Znearest_le + : forall choice (x y : R), (x <= y)%R -> Znearest choice x <= Znearest choice y. +Proof. + intros. + destruct (Z_le_gt_dec (Znearest choice x) (Znearest choice y)) as [LE | GT]. + assumption. + exfalso. + assert (1 <= IZR (Znearest choice x) - IZR(Znearest choice y))%R as GAP. + { rewrite <- minus_IZR. + apply IZR_le. + lia. + } + pose proof (Znearest_imp2 choice x) as Rx. + pose proof (Znearest_imp2 choice y) as Ry. + apply Rabs_le_inv in Rx. + apply Rabs_le_inv in Ry. + assert (x = y) by lra. + subst y. + lia. +Qed. + Section Extra_ops. (** [prec] is the number of bits of the mantissa including the implicit one. @@ -879,6 +1077,224 @@ Proof. unfold ZofB_range. rewrite D. rewrite Zle_bool_true by lia. rewrite Zle_bool_true by lia. auto. Qed. +(** ZofB_ne : convert float to integer, round to nearest *) + +Definition Zdiv_ne (a b : Z) := + let q := Z.div a b in + let q1 := Z.succ q in + match Z.compare (a-b*q) (b*q1-a) with + | Lt => q + | Gt => q1 + | Eq => (if Z.even q then q else q1) + end. + +Definition ZofB_ne (f: binary_float): option Z := + match f with + | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Z.pow_pos radix2 e)%Z + | B754_finite _ _ s m 0 _ => Some (cond_Zopp s (Zpos m)) + | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zdiv_ne (Zpos m) (Z.pow_pos radix2 e)))%Z + | B754_zero _ _ _ => Some 0%Z + | _ => None + end. + +Ltac field_simplify_den := field_simplify ; [idtac | lra]. +Ltac Rdiv_lt_0_den := apply Rdiv_lt_0_compat ; [idtac | lra]. + +Hint Rewrite <- plus_IZR minus_IZR opp_IZR mult_IZR : l_IZR. +Ltac l_IZR := autorewrite with l_IZR. + +Theorem ZofB_ne_correct: + forall f, + ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None. +Proof. + destruct f as [s|s|s p H|s m e H]; simpl; auto. +- f_equal. symmetry. apply (ZnearestE_IZR 0). +- destruct e; f_equal. + + unfold F2R; cbn. rewrite Rmult_1_r. rewrite ZnearestE_IZR. auto. + + unfold F2R; cbn. rewrite <- mult_IZR. rewrite ZnearestE_IZR. auto. + + unfold F2R; cbn. rewrite IZR_cond_Zopp. rewrite <- cond_Ropp_mult_l. + assert (EQ: forall x, ZnearestE (cond_Ropp s x) = cond_Zopp s (ZnearestE x)). + { intros. destruct s; cbn; auto. apply ZnearestE_opp. } + rewrite EQ. f_equal. + generalize (Zpower_pos_gt_0 2 p (eq_refl _)); intros. + set (p2p := (Z.pow_pos 2 p)) in *. + set (zm := Z.pos m) in *. + assert (p2p > 0) as POS by lia. + assert (0 < IZR p2p)%R as POS2. + { apply IZR_lt. assumption. } + unfold Zdiv_ne, Z.succ in *. + case Z.compare_spec; intro CMP. + * pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE. + destruct (Z_mod_lt zm p2p POS) as [MOD1 MOD2]. + set (q := zm / p2p) in *. + set (r := zm mod p2p) in *. + rewrite inbetween_int_NE with (m := q) (l := loc_Inexact Eq). + { cbn. unfold cond_incr. + destruct Z.even; reflexivity. + } + constructor. + split. + ** assert (0 < IZR zm / IZR p2p - IZR q)%R. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + l_IZR. + apply IZR_lt. + lia. + ** assert (0 < IZR (q + 1) - (IZR zm * / IZR p2p))%R. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + l_IZR. + apply IZR_lt. + lia. + ** apply Rcompare_Eq. + assert ((IZR q + IZR (q + 1))/2 - (IZR zm * / IZR p2p) = 0)%R; [idtac|lra]. + field_simplify_den. + l_IZR. + replace (q * p2p + (q + 1) * p2p - 2 * zm) with 0 by lia. + field. apply IZR_neq. lia. + * symmetry. + apply Znearest_imp with (n := zm / p2p). + apply Rabs_lt. split. + ** pose proof (Z_mult_div_ge zm p2p POS). + assert (0 <= IZR zm * / IZR p2p - IZR (zm / p2p))%R. + 2: lra. + field_simplify_den. + apply Rmult_le_pos. + { l_IZR. + apply IZR_le. + lia. + } + assert (0 < / IZR p2p)%R. + 2: lra. + apply Rinv_0_lt_compat. assumption. + ** assert (0 < 2*(IZR p2p * IZR (zm / p2p) - IZR zm) + (IZR p2p))%R as LT. + { l_IZR. + apply IZR_lt. + lia. } + assert (0 < -(IZR zm * / IZR p2p - IZR (zm / p2p) - / 2))%R as GT. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + lra. + * symmetry. + apply Znearest_imp. + apply Rabs_lt. split. + ** assert (0 < (IZR zm - IZR p2p * IZR (zm / p2p)) - (IZR p2p * (IZR (zm / p2p) + 1) - IZR zm))%R. + { ring_simplify. + l_IZR. + apply IZR_lt. + lia. + } + assert (0 < (/ 2) + IZR zm * / IZR p2p - IZR (zm / p2p + 1))%R. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + rewrite plus_IZR. + lra. + ** assert (0 < IZR (zm / p2p + 1) - (IZR zm * / IZR p2p))%R. + 2: lra. + field_simplify_den. + Rdiv_lt_0_den. + l_IZR. + apply IZR_lt. + pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE. + ring_simplify. + set (q := (zm / p2p)) in *. + pose proof (Z_mod_lt zm p2p POS) as MOD. + lia. +Qed. + +Theorem ZofB_ne_ball: + forall f n, ZofB_ne f = Some n -> (IZR n-1/2 <= B2R _ _ f <= IZR n+1/2)%R. +Proof. + intros. rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; inversion H. + pose proof (Znearest_imp2 (fun x => negb (Z.even x)) (B2R prec emax f)) as ABS. + pose proof (Rabs_le_inv _ _ ABS). + lra. +Qed. + +(* +Theorem ZofB_ne_minus: + forall minus_nan m f p q, + ZofB_ne f = Some p -> 0 <= p < 2*q -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R -> + ZofB_ne (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) = Some (p - q). +Proof. + intros. + assert (Q: -2^prec <= q <= 2^prec). + { split; auto. generalize (Zpower_ge_0 radix2 prec); simpl; lia. } + assert (RANGE: (IZR p -1/2 <= B2R _ _ f <= IZR p + 1/2)%R) by ( apply ZofB_ne_ball; auto ). + rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; try discriminate. + assert (PQ2: (IZR p + 1 <= IZR q * 2)%R). + { l_IZR. apply IZR_le. lia. } + assert (EXACT: round radix2 fexp (round_mode m) (B2R _ _ f - IZR q)%R = (B2R _ _ f - IZR q)%R). + { apply round_generic. apply valid_rnd_round_mode. + apply sterbenz_aux. now apply FLT_exp_valid. apply FLT_exp_monotone. apply generic_format_B2R. + apply integer_representable_n. auto. lra. } + destruct (BofZ_exact q Q) as (A & B & C). + generalize (Bminus_correct _ _ _ Hmax minus_nan m f (BofZ q) FIN B). + rewrite Rlt_bool_true. +- fold emin; fold fexp. intros (D & E & F). + rewrite ZofB_ne_correct. rewrite E. rewrite D. rewrite A. rewrite EXACT. + inversion H. f_equal. + rewrite ! Ztrunc_floor. apply Zfloor_minus. + lra. lra. +- rewrite A. fold emin; fold fexp. rewrite EXACT. + apply Rle_lt_trans with (bpow radix2 prec). + apply Rle_trans with (IZR q). apply Rabs_le. lra. + rewrite <- IZR_Zpower. apply IZR_le; auto. red in prec_gt_0_; lia. + apply bpow_lt. auto. +Qed. + *) + +Definition ZofB_ne_range (f: binary_float) (zmin zmax: Z): option Z := + match ZofB_ne f with + | None => None + | Some z => if Z.leb zmin z && Z.leb z zmax then Some z else None + end. + +Theorem ZofB_ne_range_correct: + forall f min max, + let n := ZnearestE (B2R _ _ f) in + ZofB_ne_range f min max = + if is_finite _ _ f && Z.leb min n && Z.leb n max then Some n else None. +Proof. + intros. unfold ZofB_ne_range. rewrite ZofB_ne_correct. fold n. + destruct (is_finite prec emax f); auto. +Qed. + +Lemma ZofB_ne_range_inversion: + forall f min max n, + ZofB_ne_range f min max = Some n -> + min <= n /\ n <= max /\ ZofB_ne f = Some n. +Proof. + intros. rewrite ZofB_ne_range_correct in H. rewrite ZofB_ne_correct. + destruct (is_finite prec emax f); try discriminate. + set (n1 := ZnearestE (B2R _ _ f)) in *. + destruct (min <=? n1) eqn:MIN; try discriminate. + destruct (n1 <=? max) eqn:MAX; try discriminate. + simpl in H. inversion H. subst n. + split. apply Zle_bool_imp_le; auto. + split. apply Zle_bool_imp_le; auto. + auto. +Qed. + + +(* +Theorem ZofB_ne_range_minus: + forall minus_nan m f p q, + ZofB_ne_range f 0 (2 * q - 1) = Some p -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R -> + ZofB_ne_range (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) (-q) (q - 1) = Some (p - q). +Proof. + intros. destruct (ZofB_ne_range_inversion _ _ _ _ H) as (A & B & C). + set (f' := Bminus prec emax prec_gt_0_ Hmax minus_nan m f (BofZ q)). + assert (D: ZofB_ne f' = Some (p - q)). + { apply ZofB_ne_minus. auto. lia. auto. auto. } + unfold ZofB_range. rewrite D. rewrite Zle_bool_true by lia. rewrite Zle_bool_true by lia. auto. +Qed. + *) + (** ** Algebraic identities *) (** Commutativity of addition and multiplication *) |