From 21e92c6aeacdd7e5b5b5970016bf34206fee8c2f Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Tue, 23 Jul 2013 14:37:50 +0200 Subject: [PATCH] Add support for NaN payload. --- src/Appli/Fappli_IEEE.v | 233 +++++++++++++++++++++-------------- src/Appli/Fappli_IEEE_bits.v | 64 ++++++---- 2 files changed, 183 insertions(+), 114 deletions(-) diff --git a/src/Appli/Fappli_IEEE.v b/src/Appli/Fappli_IEEE.v index bb747e3..2156184 100644 --- a/src/Appli/Fappli_IEEE.v +++ b/src/Appli/Fappli_IEEE.v @@ -33,7 +33,7 @@ Section AnyRadix. Inductive full_float := | F754_zero : bool -> full_float | F754_infinity : bool -> full_float - | F754_nan : full_float + | F754_nan : bool -> positive -> full_float | F754_finite : bool -> positive -> Z -> full_float. Definition FF2R beta x := @@ -67,16 +67,20 @@ Definition bounded m e := Definition valid_binary x := match x with | F754_finite _ m e => bounded m e + | F754_nan _ pl => (Z_of_nat' (S (digits2_Pnat pl)) true end. (** Basic type used for representing binary FP numbers. Note that there is exactly one such object per FP datum. NaNs do not have any payload. They cannot be distinguished. *) + +Definition nan_pl := {pl | (Z_of_nat' (S (digits2_Pnat pl)) binary_float | B754_infinity : bool -> binary_float - | B754_nan : binary_float + | B754_nan : bool -> nan_pl -> binary_float | B754_finite : bool -> forall (m : positive) (e : Z), bounded m e = true -> binary_float. @@ -85,7 +89,7 @@ Definition FF2B x := | F754_finite s m e => B754_finite s m e | F754_infinity s => fun _ => B754_infinity s | F754_zero s => fun _ => B754_zero s - | F754_nan => fun _ => B754_nan + | F754_nan b pl => fun H => B754_nan b (exist _ pl H) end. Definition B2FF x := @@ -93,7 +97,7 @@ Definition B2FF x := | B754_finite s m e _ => F754_finite s m e | B754_infinity s => F754_infinity s | B754_zero s => F754_zero s - | B754_nan => F754_nan + | B754_nan b (exist pl _) => F754_nan b pl end. Definition radix2 := Build_radix 2 (refl_equal true). @@ -108,30 +112,30 @@ Theorem FF2R_B2FF : forall x, FF2R radix2 (B2FF x) = B2R x. Proof. -now intros [sx|sx| |sx mx ex Hx]. +now intros [sx|sx|sx [plx Hplx]|sx mx ex Hx]. Qed. Theorem B2FF_FF2B : forall x Hx, B2FF (FF2B x Hx) = x. Proof. -now intros [sx|sx| |sx mx ex] Hx. +now intros [sx|sx|sx plx|sx mx ex] Hx. Qed. Theorem valid_binary_B2FF : forall x, valid_binary (B2FF x) = true. Proof. -now intros [sx|sx| |sx mx ex Hx]. +now intros [sx|sx|sx [plx Hplx]|sx mx ex Hx]. Qed. Theorem FF2B_B2FF : forall x H, FF2B (B2FF x) H = x. Proof. -intros [sx|sx| |sx mx ex Hx] H ; try easy. -apply f_equal. -apply eqbool_irrelevance. +intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] H ; try easy. +simpl. apply f_equal, f_equal, eqbool_irrelevance. +apply f_equal, eqbool_irrelevance. Qed. Theorem FF2B_B2FF_valid : @@ -146,7 +150,7 @@ Theorem B2R_FF2B : forall x Hx, B2R (FF2B x Hx) = FF2R radix2 x. Proof. -now intros [sx|sx| |sx mx ex] Hx. +now intros [sx|sx|sx plx|sx mx ex] Hx. Qed. Theorem match_FF2B : @@ -154,17 +158,17 @@ Theorem match_FF2B : match FF2B x Hx return T with | B754_zero sx => fz sx | B754_infinity sx => fi sx - | B754_nan => fn + | B754_nan b (exist p _) => fn b p | B754_finite sx mx ex _ => ff sx mx ex end = match x with | F754_zero sx => fz sx | F754_infinity sx => fi sx - | F754_nan => fn + | F754_nan b p => fn b p | F754_finite sx mx ex => ff sx mx ex end. Proof. -now intros T fz fi fn ff [sx|sx| |sx mx ex] Hx. +now intros T fz fi fn ff [sx|sx|sx plx|sx mx ex] Hx. Qed. Theorem canonic_canonic_mantissa : @@ -189,7 +193,7 @@ Theorem generic_format_B2R : forall x, generic_format radix2 fexp (B2R x). Proof. -intros [sx|sx| |sx mx ex Hx] ; try apply generic_format_0. +intros [sx|sx|sx plx|sx mx ex Hx] ; try apply generic_format_0. simpl. apply generic_format_canonic. apply canonic_canonic_mantissa. @@ -210,7 +214,7 @@ Theorem B2FF_inj : B2FF x = B2FF y -> x = y. Proof. -intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy. +intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] [sy|sy|sy [ply Hply]|sy my ey Hy] ; try easy. (* *) intros H. now inversion H. @@ -221,11 +225,18 @@ now inversion H. intros H. inversion H. clear H. +revert Hplx. +rewrite H2. +intros Hx. +apply f_equal, f_equal, eqbool_irrelevance. +(* *) +intros H. +inversion H. +clear H. revert Hx. rewrite H2, H3. intros Hx. -apply f_equal. -apply eqbool_irrelevance. +apply f_equal, eqbool_irrelevance. Qed. Definition is_finite_strict f := @@ -299,37 +310,71 @@ Theorem is_finite_FF_B2FF : forall x, is_finite_FF (B2FF x) = is_finite x. Proof. +now intros [| |? []|]. +Qed. + +Definition is_nan f := + match f with + | B754_nan _ _ => true + | _ => false + end. + +Definition is_nan_FF f := + match f with + | F754_nan _ _ => true + | _ => false + end. + +Theorem is_nan_FF2B : + forall x Hx, + is_nan (FF2B x Hx) = is_nan_FF x. +Proof. now intros [| | |]. Qed. -Definition Bopp x := +Theorem is_nan_FF_B2FF : + forall x, + is_nan_FF (B2FF x) = is_nan x. +Proof. +now intros [| |? []|]. +Qed. + +Definition Bopp opp_nan x := match x with - | B754_nan => x + | B754_nan sx plx => + let '(sres, plres) := opp_nan sx plx in B754_nan sres plres | B754_infinity sx => B754_infinity (negb sx) | B754_finite sx mx ex Hx => B754_finite (negb sx) mx ex Hx | B754_zero sx => B754_zero (negb sx) end. Theorem Bopp_involutive : - forall x, Bopp (Bopp x) = x. + forall opp_nan x, + is_nan x = false -> + Bopp opp_nan (Bopp opp_nan x) = x. Proof. -now intros [sx|sx| |sx mx ex Hx] ; simpl ; try rewrite Bool.negb_involutive. +now intros opp_nan [sx|sx|sx plx|sx mx ex Hx] ; simpl ; try rewrite Bool.negb_involutive. Qed. Theorem B2R_Bopp : - forall x, - B2R (Bopp x) = (- B2R x)%R. + forall opp_nan x, + B2R (Bopp opp_nan x) = (- B2R x)%R. Proof. -intros [sx|sx| |sx mx ex Hx] ; apply sym_eq ; try apply Ropp_0. +intros opp_nan [sx|sx|sx plx|sx mx ex Hx]; apply sym_eq ; try apply Ropp_0. +simpl. destruct opp_nan. apply Ropp_0. simpl. rewrite <- F2R_opp. now case sx. Qed. -Theorem is_finite_Bopp: forall x, - is_finite (Bopp x) = is_finite x. +Theorem is_finite_Bopp : + forall opp_nan x, + is_finite (Bopp opp_nan x) = is_finite x. Proof. -now intros [| | |]. +intros opp_nan [| | |] ; try easy. +intros s pl. +simpl. +now case opp_nan. Qed. Theorem bounded_lt_emax : @@ -367,7 +412,7 @@ Theorem abs_B2R_lt_emax : forall x, (Rabs (B2R x) < bpow radix2 emax)%R. Proof. -intros [sx|sx| |sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ). +intros [sx|sx|sx plx|sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ). rewrite <- F2R_Zabs, abs_cond_Zopp. now apply bounded_lt_emax. Qed. @@ -644,7 +689,7 @@ Definition binary_round_aux mode sx mx ex lx := match shr_m mrs'' with | Z0 => F754_zero sx | Zpos m => if Zle_bool e'' (emax - prec) then F754_finite sx m e'' else binary_overflow mode sx - | _ => F754_nan (* dummy *) + | _ => F754_nan false xH (* dummy *) end. Theorem binary_round_aux_correct : @@ -826,7 +871,7 @@ Qed. Definition Bsign x := match x with - | B754_nan => false + | B754_nan s _ => s | B754_zero s => s | B754_infinity s => s | B754_finite s _ _ _ => s @@ -834,7 +879,7 @@ Definition Bsign x := Definition sign_FF x := match x with - | F754_nan => false + | F754_nan s _ => s | F754_zero s => s | F754_infinity s => s | F754_finite s _ _ => s @@ -844,7 +889,7 @@ Theorem Bsign_FF2B : forall x H, Bsign (FF2B x H) = sign_FF x. Proof. -now intros [sx|sx| |sx mx ex] H. +now intros [sx|sx|sx plx|sx mx ex] H. Qed. (** Multiplication *) @@ -902,15 +947,15 @@ apply Rlt_bool_false. now apply F2R_ge_0_compat. Qed. -Definition Bmult m x y := +Definition Bmult mult_nan m x y := + let f pl := B754_nan (fst pl) (snd pl) in match x, y with - | B754_nan, _ => x - | _, B754_nan => y + | B754_nan _ _, _ | _, B754_nan _ _ => f (mult_nan x y) | B754_infinity sx, B754_infinity sy => B754_infinity (xorb sx sy) | B754_infinity sx, B754_finite sy _ _ _ => B754_infinity (xorb sx sy) | B754_finite sx _ _ _, B754_infinity sy => B754_infinity (xorb sx sy) - | B754_infinity _, B754_zero _ => B754_nan - | B754_zero _, B754_infinity _ => B754_nan + | B754_infinity _, B754_zero _ => f (mult_nan x y) + | B754_zero _, B754_infinity _ => f (mult_nan x y) | B754_finite sx _ _ _, B754_zero sy => B754_zero (xorb sx sy) | B754_zero sx, B754_finite sy _ _ _ => B754_zero (xorb sx sy) | B754_zero sx, B754_zero sy => B754_zero (xorb sx sy) @@ -919,14 +964,14 @@ Definition Bmult m x y := end. Theorem Bmult_correct : - forall m x y, + forall mult_nan m x y, if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x * B2R y))) (bpow radix2 emax) then - B2R (Bmult m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y) /\ - is_finite (Bmult m x y) = andb (is_finite x) (is_finite y) + B2R (Bmult mult_nan m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y) /\ + is_finite (Bmult mult_nan m x y) = andb (is_finite x) (is_finite y) else - B2FF (Bmult m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)). + B2FF (Bmult mult_nan m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)). Proof. -intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; +intros mult_nan m [sx|sx|sx plx|sx mx ex Hx] [sy|sy|sy ply|sy my ey Hy] ; try ( rewrite ?Rmult_0_r, ?Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ split ; apply refl_equal | apply bpow_gt_0 | auto with typeclass_instances ] ). simpl. case Bmult_correct_aux. @@ -940,15 +985,15 @@ intros H2. now rewrite B2FF_FF2B. Qed. -Definition Bmult_FF m x y := +Definition Bmult_FF mult_nan m x y := + let f pl := F754_nan (fst pl) (snd pl) in match x, y with - | F754_nan, _ => x - | _, F754_nan => y + | F754_nan _ _, _ | _, F754_nan _ _ => f (mult_nan x y) | F754_infinity sx, F754_infinity sy => F754_infinity (xorb sx sy) | F754_infinity sx, F754_finite sy _ _ => F754_infinity (xorb sx sy) | F754_finite sx _ _, F754_infinity sy => F754_infinity (xorb sx sy) - | F754_infinity _, F754_zero _ => F754_nan - | F754_zero _, F754_infinity _ => F754_nan + | F754_infinity _, F754_zero _ => f (mult_nan x y) + | F754_zero _, F754_infinity _ => f (mult_nan x y) | F754_finite sx _ _, F754_zero sy => F754_zero (xorb sx sy) | F754_zero sx, F754_finite sy _ _ => F754_zero (xorb sx sy) | F754_zero sx, F754_zero sy => F754_zero (xorb sx sy) @@ -957,14 +1002,20 @@ Definition Bmult_FF m x y := end. Theorem B2FF_Bmult : + forall mult_nan mult_nan_ff, forall m x y, - B2FF (Bmult m x y) = Bmult_FF m (B2FF x) (B2FF y). + mult_nan_ff (B2FF x) (B2FF y) = (let '(sr, exist plr _) := mult_nan x y in (sr, plr)) -> + B2FF (Bmult mult_nan m x y) = Bmult_FF mult_nan_ff m (B2FF x) (B2FF y). Proof. -intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy. +intros mult_nan mult_nan_ff m x y Hmult_nan. +unfold Bmult_FF. rewrite Hmult_nan. +destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Hx], y as [sy|sy|sy [ply Hply]|sy my ey Hy] ; + simpl; try match goal with |- context [mult_nan ?x ?y] => + destruct (mult_nan x y) as [? []] end; + try easy. apply B2FF_FF2B. Qed. - Definition shl_align mx ex ex' := match (ex' - ex)%Z with | Zneg d => (shift_pos d mx, ex') @@ -1129,12 +1180,12 @@ now apply F2R_lt_0_compat. Qed. (** Addition *) -Definition Bplus m x y := +Definition Bplus plus_nan m x y := + let f pl := B754_nan (fst pl) (snd pl) in match x, y with - | B754_nan, _ => x - | _, B754_nan => y + | B754_nan _ _, _ | _, B754_nan _ _ => f (plus_nan x y) | B754_infinity sx, B754_infinity sy => - if Bool.eqb sx sy then x else B754_nan + if Bool.eqb sx sy then x else f (plus_nan x y) | B754_infinity _, _ => x | _, B754_infinity _ => y | B754_zero sx, B754_zero sy => @@ -1149,16 +1200,16 @@ Definition Bplus m x y := end. Theorem Bplus_correct : - forall m x y, + forall plus_nan m x y, is_finite x = true -> is_finite y = true -> if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x + B2R y))) (bpow radix2 emax) then - B2R (Bplus m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y) /\ - is_finite (Bplus m x y) = true + B2R (Bplus plus_nan m x y) = round radix2 fexp (round_mode m) (B2R x + B2R y) /\ + is_finite (Bplus plus_nan m x y) = true else - (B2FF (Bplus m x y) = binary_overflow m (Bsign x) /\ Bsign x = Bsign y). + (B2FF (Bplus plus_nan m x y) = binary_overflow m (Bsign x) /\ Bsign x = Bsign y). Proof with auto with typeclass_instances. -intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] Fx Fy ; try easy. +intros plus_nan m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] Fx Fy ; try easy. (* *) rewrite Rplus_0_r, round_0, Rabs_R0, Rlt_bool_true... simpl. @@ -1279,26 +1330,25 @@ now apply f_equal. apply Sz. Qed. -Definition Bminus m x y := Bplus m x (Bopp y). +Definition Bminus minus_nan m x y := Bplus minus_nan m x (Bopp pair y). Theorem Bminus_correct : - forall m x y, + forall minus_nan m x y, is_finite x = true -> is_finite y = true -> if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x - B2R y))) (bpow radix2 emax) then - B2R (Bminus m x y) = round radix2 fexp (round_mode m) (B2R x - B2R y) /\ - is_finite (Bminus m x y) = true + B2R (Bminus minus_nan m x y) = round radix2 fexp (round_mode m) (B2R x - B2R y) /\ + is_finite (Bminus minus_nan m x y) = true else - (B2FF (Bminus m x y) = binary_overflow m (Bsign x) /\ Bsign x = negb (Bsign y)). + (B2FF (Bminus minus_nan m x y) = binary_overflow m (Bsign x) /\ Bsign x = negb (Bsign y)). Proof with auto with typeclass_instances. -intros m x y Fx Fy. -replace (negb (Bsign y)) with (Bsign (Bopp y)). +intros m minus_nan x y Fx Fy. +replace (negb (Bsign y)) with (Bsign (Bopp pair y)). unfold Rminus. -rewrite <- B2R_Bopp. +erewrite <- B2R_Bopp. apply Bplus_correct. exact Fx. -now rewrite is_finite_Bopp. -now destruct y as [ | | | ]. +rewrite is_finite_Bopp. auto. now destruct y as [ | | | ]. Qed. (** Division *) @@ -1322,7 +1372,7 @@ Lemma Bdiv_correct_aux : let '(mz, ez, lz) := Fdiv_core_binary (Zpos mx) ex (Zpos my) ey in match mz with | Zpos mz => binary_round_aux m (xorb sx sy) mz ez lz - | _ => F754_nan (* dummy *) + | _ => F754_nan false xH (* dummy *) end in valid_binary z = true /\ if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (x / y))) (bpow radix2 emax) then @@ -1412,35 +1462,35 @@ apply Rinv_0_lt_compat. now apply F2R_gt_0_compat. Qed. -Definition Bdiv m x y := +Definition Bdiv div_nan m x y := + let f pl := B754_nan (fst pl) (snd pl) in match x, y with - | B754_nan, _ => x - | _, B754_nan => y - | B754_infinity sx, B754_infinity sy => B754_nan + | B754_nan _ _, _ | _, B754_nan _ _ => f (div_nan x y) + | B754_infinity sx, B754_infinity sy => f (div_nan x y) | B754_infinity sx, B754_finite sy _ _ _ => B754_infinity (xorb sx sy) | B754_finite sx _ _ _, B754_infinity sy => B754_zero (xorb sx sy) | B754_infinity sx, B754_zero sy => B754_infinity (xorb sx sy) | B754_zero sx, B754_infinity sy => B754_zero (xorb sx sy) | B754_finite sx _ _ _, B754_zero sy => B754_infinity (xorb sx sy) | B754_zero sx, B754_finite sy _ _ _ => B754_zero (xorb sx sy) - | B754_zero sx, B754_zero sy => B754_nan + | B754_zero sx, B754_zero sy => f (div_nan x y) | B754_finite sx mx ex _, B754_finite sy my ey _ => FF2B _ (proj1 (Bdiv_correct_aux m sx mx ex sy my ey)) end. Theorem Bdiv_correct : - forall m x y, + forall div_nan m x y, B2R y <> R0 -> if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x / B2R y))) (bpow radix2 emax) then - B2R (Bdiv m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\ - is_finite (Bdiv m x y) = is_finite x + B2R (Bdiv div_nan m x y) = round radix2 fexp (round_mode m) (B2R x / B2R y) /\ + is_finite (Bdiv div_nan m x y) = is_finite x else - B2FF (Bdiv m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)). + B2FF (Bdiv div_nan m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)). Proof. -intros m x [sy|sy| |sy my ey Hy] Zy ; try now elim Zy. +intros div_nan m x [sy|sy|sy ply|sy my ey Hy] Zy ; try now elim Zy. revert x. unfold Rdiv. -intros [sx|sx| |sx mx ex Hx] ; +intros [sx|sx|sx plx|sx mx ex Hx] ; try ( rewrite Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ split ; apply refl_equal | apply bpow_gt_0 | auto with typeclass_instances ] ). simpl. case Bdiv_correct_aux. @@ -1479,7 +1529,7 @@ Lemma Bsqrt_correct_aux : let '(mz, ez, lz) := Fsqrt_core_binary (Zpos mx) ex in match mz with | Zpos mz => binary_round_aux m false mz ez lz - | _ => F754_nan (* dummy *) + | _ => F754_nan false xH (* dummy *) end in valid_binary z = true /\ FF2R radix2 z = round radix2 fexp (round_mode m) (sqrt x) /\ @@ -1584,23 +1634,24 @@ now case mz. apply sqrt_ge_0. Qed. -Definition Bsqrt m x := +Definition Bsqrt sqrt_nan m x := + let f pl := B754_nan (fst pl) (snd pl) in match x with - | B754_nan => x + | B754_nan sx plx => f (sqrt_nan x) | B754_infinity false => x - | B754_infinity true => B754_nan - | B754_finite true _ _ _ => B754_nan + | B754_infinity true => f (sqrt_nan x) + | B754_finite true _ _ _ => f (sqrt_nan x) | B754_zero _ => x | B754_finite sx mx ex Hx => FF2B _ (proj1 (Bsqrt_correct_aux m mx ex Hx)) end. Theorem Bsqrt_correct : - forall m x, - B2R (Bsqrt m x) = round radix2 fexp (round_mode m) (sqrt (B2R x)) /\ - is_finite (Bsqrt m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end. + forall sqrt_nan m x, + B2R (Bsqrt sqrt_nan m x) = round radix2 fexp (round_mode m) (sqrt (B2R x)) /\ + is_finite (Bsqrt sqrt_nan m x) = match x with B754_zero _ => true | B754_finite false _ _ _ => true | _ => false end. Proof. -intros m [sx|[|]| |sx mx ex Hx] ; try ( now simpl ; rewrite sqrt_0, round_0 ; auto with typeclass_instances ). +intros sqrt_nan m [sx|[|]| |sx mx ex Hx] ; try ( now simpl ; rewrite sqrt_0, round_0 ; auto with typeclass_instances ). simpl. case Bsqrt_correct_aux. intros H1 (H2, H3). diff --git a/src/Appli/Fappli_IEEE_bits.v b/src/Appli/Fappli_IEEE_bits.v index 06ed21e..ed31252 100644 --- a/src/Appli/Fappli_IEEE_bits.v +++ b/src/Appli/Fappli_IEEE_bits.v @@ -172,7 +172,7 @@ Definition bits_of_binary_float (x : binary_float) := match x with | B754_zero sx => join_bits sx 0 0 | B754_infinity sx => join_bits sx 0 (Zpower 2 ew - 1) - | B754_nan => join_bits false (Zpower 2 mw - 1) (Zpower 2 ew - 1) + | B754_nan sx (exist plx _) => join_bits sx (Zpos plx) (Zpower 2 ew - 1) | B754_finite sx mx ex _ => if Zle_bool (Zpower 2 mw) (Zpos mx) then join_bits sx (Zpos mx - Zpower 2 mw) (ex - emin + 1) @@ -184,7 +184,7 @@ Definition split_bits_of_binary_float (x : binary_float) := match x with | B754_zero sx => (sx, 0, 0)%Z | B754_infinity sx => (sx, 0, Zpower 2 ew - 1)%Z - | B754_nan => (false, Zpower 2 mw - 1, Zpower 2 ew - 1)%Z + | B754_nan sx (exist plx _) => (sx, Zpos plx, Zpower 2 ew - 1)%Z | B754_finite sx mx ex _ => if Zle_bool (Zpower 2 mw) (Zpos mx) then (sx, Zpos mx - Zpower 2 mw, ex - emin + 1)%Z @@ -196,8 +196,16 @@ Theorem split_bits_of_binary_float_correct : forall x, split_bits (bits_of_binary_float x) = split_bits_of_binary_float x. Proof. -intros [sx|sx| |sx mx ex Hx] ; +intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] ; try ( simpl ; apply split_join_bits ; split ; try apply Zle_refl ; try apply Zlt_pred ; trivial ; omega ). +simpl. apply split_join_bits; split; try (zify; omega). +destruct (digits2_Pnat_correct plx). +rewrite Zpower_nat_Z in H0. +eapply Zlt_le_trans. apply H0. +change 2%Z with (radix_val radix2). apply Zpower_le. +rewrite Z.ltb_lt in Hplx. +unfold prec in *. zify; omega. +(* *) unfold bits_of_binary_float, split_bits_of_binary_float. assert (Hf: (emin <= ex /\ Zdigits radix2 (Zpos mx) <= prec)%Z). destruct (andb_prop _ _ Hx) as (Hx', _). @@ -246,14 +254,18 @@ Definition binary_float_of_bits_aux x := match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin - | Zneg _ => F754_nan (* dummy *) + | Zneg _ => F754_nan false xH (* dummy *) end else if Zeq_bool ex (Zpower 2 ew - 1) then - if Zeq_bool mx 0 then F754_infinity sx else F754_nan + match mx with + | Z0 => F754_infinity sx + | Zpos plx => F754_nan sx plx + | Zneg _ => F754_nan false xH (* dummy *) + end else match (mx + Zpower 2 mw)%Z with | Zpos px => F754_finite sx px (ex + emin - 1) - | _ => F754_nan (* dummy *) + | _ => F754_nan false xH (* dummy *) end. Lemma binary_float_of_bits_aux_correct : @@ -292,9 +304,20 @@ cut (0 < emax)%Z. clear -H Hew ; omega. apply (Zpower_gt_0 radix2). clear -Hew ; omega. apply bpow_gt_0. +simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega. case Zeq_bool_spec ; intros He2. -now case Zeq_bool. +case_eq (x mod 2 ^ mw)%Z; try easy. +(* nan *) +intros plx Eqplx. apply Z.ltb_lt. +rewrite Z_of_nat_S_digits2_Pnat. +assert (forall a b, a <= b -> a < b+1)%Z by (intros; omega). apply H. clear H. +apply Zdigits_le_Zpower. simpl. +rewrite <- Eqplx. edestruct Z_mod_lt; eauto. +change 2%Z with (radix_val radix2). +apply Z.lt_gt, Zpower_gt_0. omega. +simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega. case_eq (x mod 2^mw + 2^mw)%Z ; try easy. +simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega. (* normal *) intros px Hm. assert (prec = Zdigits radix2 (Zpos px)). @@ -365,6 +388,7 @@ apply Zlt_gt. apply (Zpower_gt_0 radix2). now apply Zlt_le_weak. apply bpow_gt_0. +simpl. intros. rewrite Z.ltb_lt. unfold prec. zify; omega. Qed. Definition binary_float_of_bits x := @@ -380,7 +404,7 @@ unfold binary_float_of_bits. rewrite B2FF_FF2B. unfold binary_float_of_bits_aux. rewrite split_bits_of_binary_float_correct. -destruct x as [sx|sx| |sx mx ex Bx]. +destruct x as [sx|sx|sx [plx Hplx]|sx mx ex Bx]. apply refl_equal. (* *) simpl. @@ -391,12 +415,7 @@ now apply (Zpower_gt_1 radix2). (* *) simpl. rewrite Zeq_bool_false. -rewrite Zeq_bool_true. -rewrite Zeq_bool_false. -apply refl_equal. -cut (1 < 2^mw)%Z. clear ; omega. -now apply (Zpower_gt_1 radix2). -apply refl_equal. +rewrite Zeq_bool_true; auto. cut (1 < 2^ew)%Z. clear ; omega. now apply (Zpower_gt_1 radix2). (* *) @@ -442,7 +461,6 @@ Qed. Theorem bits_of_binary_float_of_bits : forall x, (0 <= x < 2^(mw+ew+1))%Z -> - binary_float_of_bits x <> B754_nan prec emax -> bits_of_binary_float (binary_float_of_bits x) = x. Proof. intros x Hx. @@ -462,28 +480,28 @@ now apply Zlt_gt. case Zeq_bool_spec ; intros He1. (* subnormal *) case_eq mx. -intros Hm Jx _ _. +intros Hm Jx _. now rewrite He1 in Jx. -intros px Hm Jx _ _. +intros px Hm Jx _. rewrite Zle_bool_false. now rewrite <- He1. now rewrite <- Hm. -intros px Hm _ _ _. +intros px Hm _ _. apply False_ind. apply Zle_not_lt with (1 := proj1 Bm). now rewrite Hm. case Zeq_bool_spec ; intros He2. (* infinity/nan *) -case Zeq_bool_spec ; intros Hm. -now rewrite Hm, He2. -intros _ Cx Nx. -now elim Nx. +case_eq mx; intros Hm. +now rewrite He2. +now rewrite He2. +intros. zify; omega. (* normal *) case_eq (mx + 2 ^ mw)%Z. intros Hm. apply False_ind. clear -Bm Hm ; omega. -intros p Hm Jx Cx _. +intros p Hm Jx Cx. rewrite <- Hm. rewrite Zle_bool_true. now ring_simplify (mx + 2^mw - 2^mw)%Z (ex + emin - 1 - emin + 1)%Z. -- GitLab