From e8c312eecf96ae1703f7ba0b65f107233d340238 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 26 Apr 2022 11:14:06 +0200 Subject: Upgrade to Flocq 4.1. --- extraction/extraction.v | 12 - flocq/Calc/Round.v | 16 + flocq/Core/Digits.v | 11 + flocq/Core/FIX.v | 8 + flocq/Core/Generic_fmt.v | 25 ++ flocq/Core/Raux.v | 73 +++-- flocq/Core/Zaux.v | 6 + flocq/IEEE754/Binary.v | 160 +++++---- flocq/IEEE754/BinarySingleNaN.v | 705 ++++++++++++++++++++++++++++++---------- flocq/Version.v | 2 +- lib/IEEE754_extra.v | 4 +- 11 files changed, 737 insertions(+), 285 deletions(-) diff --git a/extraction/extraction.v b/extraction/extraction.v index 2319be17..621298f8 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -144,18 +144,6 @@ Load extractionMachdep. (* Avoid name clashes *) Extraction Blacklist List String Int. -(* Cutting the dependency to R. *) -Extract Inlined Constant Defs.F2R => "fun _ -> assert false". -Extract Inlined Constant Binary.FF2R => "fun _ -> assert false". -Extract Inlined Constant Binary.B2R => "fun _ -> assert false". -Extract Inlined Constant BinarySingleNaN.round_mode => "fun _ -> assert false". -Extract Inlined Constant BinarySingleNaN.SF2R => "fun _ -> assert false". -Extract Inlined Constant BinarySingleNaN.B2R => "fun _ -> assert false". -Extract Inlined Constant Binary.BSN.round_mode => "fun _ -> assert false". -Extract Inlined Constant Binary.BSN.SF2R => "fun _ -> assert false". -Extract Inlined Constant Binary.BSN.B2R => "fun _ -> assert false". -Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". - (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. diff --git a/flocq/Calc/Round.v b/flocq/Calc/Round.v index 40da2f08..b4693ed7 100644 --- a/flocq/Calc/Round.v +++ b/flocq/Calc/Round.v @@ -114,6 +114,12 @@ Qed. Definition cond_incr (b : bool) m := if b then (m + 1)%Z else m. +Lemma le_cond_incr_le : + forall b m, (m <= cond_incr b m <= m + 1)%Z. +Proof. +unfold cond_incr; intros b; case b; lia. +Qed. + Theorem inbetween_float_round_sign : forall rnd choice, ( forall x m l, inbetween_int m (Rabs x) l -> @@ -590,6 +596,16 @@ now case Rlt_bool. lia. Qed. +Theorem inbetween_float_NA_sign : + forall x m l, + let e := cexp beta fexp x in + inbetween_float beta m e (Rabs x) l -> + round beta fexp ZnearestA x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (cond_incr (round_N true l) m)) e). +Proof. +apply inbetween_float_round_sign with (choice := fun s m l => cond_incr (round_N true l) m). +exact inbetween_int_NA_sign. +Qed. + Definition truncate_aux t k := let '(m, e, l) := t in let p := Zpower beta k in diff --git a/flocq/Core/Digits.v b/flocq/Core/Digits.v index b491b436..7fe51cca 100644 --- a/flocq/Core/Digits.v +++ b/flocq/Core/Digits.v @@ -1115,6 +1115,17 @@ exact Hm. now rewrite <- (Z.abs_eq m) at 1. Qed. +Theorem Zdigits_succ_le : + forall x, (0 <= x)%Z -> + (Zdigits (x + 1) <= Zdigits x + 1)%Z. +Proof. + destruct x as [| p | p]; [intros _; now simpl | intros _ | lia]. + transitivity (Zdigits (Z.pos p * beta ^ 1)); + [apply Zdigits_le; [lia |] | rewrite Zdigits_mult_Zpower; lia]. + apply Ztac.Zlt_le_add_1. rewrite <-Z.mul_1_r at 1. apply Zmult_lt_compat_l; [lia |]. + rewrite Z.pow_1_r. apply radix_gt_1. +Qed. + End Fcore_digits. (** Specialized version for computing the number of bits of an integer *) diff --git a/flocq/Core/FIX.v b/flocq/Core/FIX.v index e365951a..1f4a5676 100644 --- a/flocq/Core/FIX.v +++ b/flocq/Core/FIX.v @@ -102,3 +102,11 @@ right; split; auto. Qed. End RND_FIX. + +Theorem round_FIX_IZR : + forall f x, + round radix2 (FIX_exp 0) f x = IZR (f x). +Proof. + intros f x. unfold round, F2R. simpl. rewrite Rmult_1_r. apply f_equal. + apply f_equal. unfold scaled_mantissa. simpl. apply Rmult_1_r. +Qed. diff --git a/flocq/Core/Generic_fmt.v b/flocq/Core/Generic_fmt.v index b3b71b19..a74c81b9 100644 --- a/flocq/Core/Generic_fmt.v +++ b/flocq/Core/Generic_fmt.v @@ -1580,6 +1580,31 @@ apply Zlt_le_succ. now apply mag_gt_bpow. Qed. +Lemma lt_cexp_pos : + forall x y, + (0 < y)%R -> + (cexp x < cexp y)%Z -> + (x < y)%R. +Proof. +intros x y Zy He. +unfold cexp in He. +apply (lt_mag beta) with (1 := Zy). +generalize (monotone_exp (mag beta y) (mag beta x)). +lia. +Qed. + +Theorem lt_cexp : + forall x y, + (y <> 0)%R -> + (cexp x < cexp y)%Z -> + (Rabs x < Rabs y)%R. +Proof. +intros x y Zy He. +apply lt_cexp_pos. +now apply Rabs_pos_lt. +now rewrite 2!cexp_abs. +Qed. + Variable rnd : R -> Z. Context { valid_rnd : Valid_rnd rnd }. diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v index a418bf19..4b2ce8d7 100644 --- a/flocq/Core/Raux.v +++ b/flocq/Core/Raux.v @@ -66,15 +66,6 @@ Qed. Theorem Rabs_eq_R0 x : (Rabs x = 0 -> x = 0)%R. Proof. split_Rabs; lra. Qed. -Theorem Rplus_eq_reg_r : - forall r r1 r2 : R, - (r1 + r = r2 + r)%R -> (r1 = r2)%R. -Proof. -intros r r1 r2 H. -apply Rplus_eq_reg_l with r. -now rewrite 2!(Rplus_comm r). -Qed. - Theorem Rmult_lt_compat : forall r1 r2 r3 r4, (0 <= r1)%R -> (0 <= r3)%R -> (r1 < r2)%R -> (r3 < r4)%R -> @@ -90,15 +81,6 @@ apply Rle_lt_trans with (r1 * r4)%R. + exact H12. Qed. -Theorem Rmult_minus_distr_r : - forall r r1 r2 : R, - ((r1 - r2) * r = r1 * r - r2 * r)%R. -Proof. -intros r r1 r2. -rewrite <- 3!(Rmult_comm r). -apply Rmult_minus_distr_l. -Qed. - Lemma Rmult_neq_reg_r : forall r1 r2 r3 : R, (r2 * r1 <> r3 * r1)%R -> r2 <> r3. Proof. @@ -115,7 +97,6 @@ intros r1 r2 r3 H H1 H2. now apply H1, Rmult_eq_reg_r with r1. Qed. - Theorem Rmult_min_distr_r : forall r r1 r2 : R, (0 <= r)%R -> @@ -245,18 +226,6 @@ intros x y H. apply (Rle_trans _ (Rabs x)); [apply Rle_abs|apply (Rsqr_le_abs_0 _ _ H)]. Qed. -Theorem Rabs_le : - forall x y, - (-y <= x <= y)%R -> (Rabs x <= y)%R. -Proof. -intros x y (Hyx,Hxy). -unfold Rabs. -case Rcase_abs ; intros Hx. -apply Ropp_le_cancel. -now rewrite Ropp_involutive. -exact Hxy. -Qed. - Theorem Rabs_le_inv : forall x y, (Rabs x <= y)%R -> (-y <= x <= y)%R. @@ -1270,8 +1239,6 @@ apply Rmult_lt_compat_r with (2 := H1). now apply IZR_lt. Qed. -Section Zdiv_Rdiv. - Theorem Zfloor_div : forall x y, y <> Z0 -> @@ -1330,7 +1297,36 @@ apply Rplus_lt_compat_l. apply H. Qed. -End Zdiv_Rdiv. +Theorem Ztrunc_div : + forall x y, y <> 0%Z -> + Ztrunc (IZR x / IZR y) = Z.quot x y. +Proof. + destruct y; [easy | |]; destruct x; intros _. + - rewrite Z.quot_0_l; [| easy]. unfold Rdiv. rewrite Rmult_0_l. + rewrite Ztrunc_floor; [| apply Rle_refl]. now rewrite Zfloor_IZR. + - rewrite Z.quot_div_nonneg; [| easy | easy]. rewrite <-Zfloor_div; [| easy]. + unfold Ztrunc. rewrite Rlt_bool_false; [reflexivity |]. + apply Rle_mult_inv_pos; [now apply IZR_le | now apply IZR_lt]. + - rewrite <-Pos2Z.opp_pos. rewrite Z.quot_opp_l; [| easy]. + rewrite Z.quot_div_nonneg; [| easy | easy]. rewrite <-Zfloor_div; [| easy]. + rewrite Ropp_Ropp_IZR. rewrite Ropp_div. unfold Ztrunc. rewrite Rlt_bool_true. + + unfold Zceil. now rewrite Ropp_involutive. + + apply Ropp_lt_gt_0_contravar. apply Rdiv_lt_0_compat; now apply IZR_lt. + - rewrite Z.quot_0_l; [| easy]. unfold Rdiv. rewrite Rmult_0_l. + rewrite Ztrunc_floor; [| apply Rle_refl]. now rewrite Zfloor_IZR. + - rewrite <-Pos2Z.opp_pos. rewrite Z.quot_opp_r; [| easy]. + rewrite Z.quot_div_nonneg; [| easy | easy]. rewrite <-Zfloor_div; [| easy]. + rewrite Ropp_Ropp_IZR. rewrite Ropp_div_den; [| easy]. unfold Ztrunc. + rewrite Rlt_bool_true. + + unfold Zceil. now rewrite Ropp_involutive. + + apply Ropp_lt_gt_0_contravar. apply Rdiv_lt_0_compat; now apply IZR_lt. + - rewrite <-2Pos2Z.opp_pos. rewrite Z.quot_opp_l; [| easy]. rewrite Z.quot_opp_r; [| easy]. + rewrite Z.quot_div_nonneg; [| easy | easy]. rewrite <-Zfloor_div; [| easy]. + rewrite 2Ropp_Ropp_IZR. rewrite Ropp_div. rewrite Ropp_div_den; [| easy]. + rewrite Z.opp_involutive. rewrite Ropp_involutive. + unfold Ztrunc. rewrite Rlt_bool_false; [reflexivity |]. + apply Rle_mult_inv_pos; [now apply IZR_le | now apply IZR_lt]. +Qed. Section pow. @@ -2211,6 +2207,15 @@ now apply Rabs_left. now apply Rabs_pos_eq. Qed. +Theorem Rlt_bool_cond_Ropp : + forall x sx, (0 < x)%R -> + Rlt_bool (cond_Ropp sx x) 0 = sx. +Proof. + intros x sx Hx. destruct sx; simpl. + - apply Rlt_bool_true. now apply Ropp_lt_gt_0_contravar. + - apply Rlt_bool_false. now left. +Qed. + Theorem cond_Ropp_involutive : forall b x, cond_Ropp b (cond_Ropp b x) = x. diff --git a/flocq/Core/Zaux.v b/flocq/Core/Zaux.v index b14c4e93..57e351dd 100644 --- a/flocq/Core/Zaux.v +++ b/flocq/Core/Zaux.v @@ -773,6 +773,12 @@ End Zcompare. Section cond_Zopp. +Theorem cond_Zopp_0 : + forall sx, cond_Zopp sx 0 = 0%Z. +Proof. +now intros [|]. +Qed. + Theorem cond_Zopp_negb : forall x y, cond_Zopp (negb x) y = Z.opp (cond_Zopp x y). Proof. diff --git a/flocq/IEEE754/Binary.v b/flocq/IEEE754/Binary.v index 335d9b38..5f9f0352 100644 --- a/flocq/IEEE754/Binary.v +++ b/flocq/IEEE754/Binary.v @@ -23,12 +23,10 @@ From Coq Require Import ZArith Reals Psatz SpecFloat. Require Import Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN. -Module BSN := BinarySingleNaN. - -Arguments BSN.B754_zero {prec emax}. -Arguments BSN.B754_infinity {prec emax}. -Arguments BSN.B754_nan {prec emax}. -Arguments BSN.B754_finite {prec emax}. +Arguments BinarySingleNaN.B754_zero {prec emax}. +Arguments BinarySingleNaN.B754_infinity {prec emax}. +Arguments BinarySingleNaN.B754_nan {prec emax}. +Arguments BinarySingleNaN.B754_finite {prec emax}. Section AnyRadix. @@ -191,12 +189,12 @@ Inductive binary_float := | B754_finite (s : bool) (m : positive) (e : Z) : bounded m e = true -> binary_float. -Definition B2BSN (x : binary_float) : BSN.binary_float prec emax := +Definition B2BSN (x : binary_float) : BinarySingleNaN.binary_float prec emax := match x with - | B754_zero s => BSN.B754_zero s - | B754_infinity s => BSN.B754_infinity s - | B754_nan _ _ _ => BSN.B754_nan - | B754_finite s m e H => BSN.B754_finite s m e H + | B754_zero s => BinarySingleNaN.B754_zero s + | B754_infinity s => BinarySingleNaN.B754_infinity s + | B754_nan _ _ _ => BinarySingleNaN.B754_nan + | B754_finite s m e H => BinarySingleNaN.B754_finite s m e H end. Definition FF2B x := @@ -231,7 +229,7 @@ Definition B2SF (x : binary_float) := Lemma B2SF_B2BSN : forall x, - BSN.B2SF (B2BSN x) = B2SF x. + BinarySingleNaN.B2SF (B2BSN x) = B2SF x. Proof. now intros [sx|sx|sx px Px|sx mx ex Bx]. Qed. @@ -244,7 +242,7 @@ now intros [sx|sx|sx px|sx mx ex] Bx. Qed. Lemma B2R_B2BSN : - forall x, BSN.B2R (B2BSN x) = B2R x. + forall x, BinarySingleNaN.B2R (B2BSN x) = B2R x. Proof. intros x. now destruct x. @@ -326,16 +324,7 @@ Theorem canonical_canonical_mantissa : canonical radix2 fexp (Float radix2 (cond_Zopp sx (Zpos mx)) ex). Proof. intros sx mx ex H. -assert (Hx := Zeq_bool_eq _ _ H). clear H. -apply sym_eq. -simpl. -pattern ex at 2 ; rewrite <- Hx. -apply (f_equal fexp). -rewrite mag_F2R_Zdigits. -rewrite <- Zdigits_abs. -rewrite Zpos_digits2_pos. -now case sx. -now case sx. +now apply canonical_canonical_mantissa. Qed. Theorem generic_format_B2R : @@ -345,8 +334,7 @@ Proof. intros [sx|sx|sx plx Hx |sx mx ex Hx] ; try apply generic_format_0. simpl. apply generic_format_canonical. -apply canonical_canonical_mantissa. -now destruct (andb_prop _ _ Hx) as (H, _). +now apply canonical_bounded. Qed. Theorem FLT_format_B2R : @@ -395,7 +383,7 @@ Definition is_finite_strict f := end. Lemma is_finite_strict_B2BSN : - forall x, BSN.is_finite_strict (B2BSN x) = is_finite_strict x. + forall x, BinarySingleNaN.is_finite_strict (B2BSN x) = is_finite_strict x. Proof. intros x. now destruct x. @@ -429,10 +417,8 @@ assert (mx = my /\ ex = ey). refine (_ (canonical_unique _ fexp _ _ _ _ Heq)). rewrite Hs. now case sy ; intro H ; injection H ; split. -apply canonical_canonical_mantissa. -exact (proj1 (andb_prop _ _ Hx)). -apply canonical_canonical_mantissa. -exact (proj1 (andb_prop _ _ Hy)). +now apply canonical_bounded. +now apply canonical_bounded. (* *) revert Hx. rewrite Hs, (proj1 H), (proj2 H). @@ -464,7 +450,7 @@ Definition is_finite f := end. Lemma is_finite_B2BSN : - forall x, BSN.is_finite (B2BSN x) = is_finite x. + forall x, BinarySingleNaN.is_finite (B2BSN x) = is_finite x. Proof. intros x. now destruct x. @@ -512,7 +498,7 @@ Definition is_nan f := Lemma is_nan_B2BSN : forall x, - BSN.is_nan (B2BSN x) = is_nan x. + BinarySingleNaN.is_nan (B2BSN x) = is_nan x. Proof. now intros [s|s|s p H|s m e H]. Qed. @@ -572,12 +558,12 @@ Proof. easy. Qed. -Definition BSN2B (nan : {x : binary_float | is_nan x = true }) (x : BSN.binary_float prec emax) : binary_float := +Definition BSN2B (nan : {x : binary_float | is_nan x = true }) (x : BinarySingleNaN.binary_float prec emax) : binary_float := match x with - | BSN.B754_nan => build_nan nan - | BSN.B754_zero s => B754_zero s - | BSN.B754_infinity s => B754_infinity s - | BSN.B754_finite s m e H => B754_finite s m e H + | BinarySingleNaN.B754_nan => build_nan nan + | BinarySingleNaN.B754_zero s => B754_zero s + | BinarySingleNaN.B754_infinity s => B754_infinity s + | BinarySingleNaN.B754_finite s m e H => B754_finite s m e H end. Lemma B2BSN_BSN2B : @@ -588,37 +574,37 @@ now intros nan [s|s| |s m e H]. Qed. Lemma B2R_BSN2B : - forall nan x, B2R (BSN2B nan x) = BSN.B2R x. + forall nan x, B2R (BSN2B nan x) = BinarySingleNaN.B2R x. Proof. now intros nan [s|s| |s m e H]. Qed. Lemma is_finite_BSN2B : - forall nan x, is_finite (BSN2B nan x) = BSN.is_finite x. + forall nan x, is_finite (BSN2B nan x) = BinarySingleNaN.is_finite x. Proof. now intros nan [s|s| |s m e H]. Qed. Lemma is_nan_BSN2B : - forall nan x, is_nan (BSN2B nan x) = BSN.is_nan x. + forall nan x, is_nan (BSN2B nan x) = BinarySingleNaN.is_nan x. Proof. now intros nan [s|s| |s m e H]. Qed. Lemma Bsign_B2BSN : - forall x, is_nan x = false -> BSN.Bsign (B2BSN x) = Bsign x. + forall x, is_nan x = false -> BinarySingleNaN.Bsign (B2BSN x) = Bsign x. Proof. now intros [s|s| |s m e H]. Qed. Lemma Bsign_BSN2B : - forall nan x, BSN.is_nan x = false -> - Bsign (BSN2B nan x) = BSN.Bsign x. + forall nan x, BinarySingleNaN.is_nan x = false -> + Bsign (BSN2B nan x) = BinarySingleNaN.Bsign x. Proof. now intros nan [s|s| |s m e H]. Qed. -Definition BSN2B' (x : BSN.binary_float prec emax) : BSN.is_nan x = false -> binary_float. +Definition BSN2B' (x : BinarySingleNaN.binary_float prec emax) : BinarySingleNaN.is_nan x = false -> binary_float. Proof. destruct x as [sx|sx| |sx mx ex Bx] ; intros H. exact (B754_zero sx). @@ -636,28 +622,28 @@ Qed. Lemma B2R_BSN2B' : forall x Nx, - B2R (BSN2B' x Nx) = BSN.B2R x. + B2R (BSN2B' x Nx) = BinarySingleNaN.B2R x. Proof. now intros [sx|sx| |sx mx ex Bx] Nx. Qed. Lemma B2FF_BSN2B' : forall x Nx, - B2FF (BSN2B' x Nx) = SF2FF (BSN.B2SF x). + B2FF (BSN2B' x Nx) = SF2FF (BinarySingleNaN.B2SF x). Proof. now intros [sx|sx| |sx mx ex Bx] Nx. Qed. Lemma Bsign_BSN2B' : forall x Nx, - Bsign (BSN2B' x Nx) = BSN.Bsign x. + Bsign (BSN2B' x Nx) = BinarySingleNaN.Bsign x. Proof. now intros [sx|sx| |sx mx ex Bx] Nx. Qed. Lemma is_finite_BSN2B' : forall x Nx, - is_finite (BSN2B' x Nx) = BSN.is_finite x. + is_finite (BSN2B' x Nx) = BinarySingleNaN.is_finite x. Proof. now intros [sx|sx| |sx mx ex Bx] Nx. Qed. @@ -785,7 +771,7 @@ Qed. [Some c] means ordered as per [c]; [None] means unordered. *) Definition Bcompare (f1 f2 : binary_float) : option comparison := - BSN.Bcompare (B2BSN f1) (B2BSN f2). + BinarySingleNaN.Bcompare (B2BSN f1) (B2BSN f2). Theorem Bcompare_correct : forall f1 f2, @@ -794,7 +780,7 @@ Theorem Bcompare_correct : Proof. intros f1 f2 H1 H2. unfold Bcompare. - rewrite BSN.Bcompare_correct. + rewrite BinarySingleNaN.Bcompare_correct. now rewrite 2!B2R_B2BSN. now rewrite is_finite_B2BSN. now rewrite is_finite_B2BSN. @@ -805,7 +791,7 @@ Theorem Bcompare_swap : Bcompare y x = match Bcompare x y with Some c => Some (CompOpp c) | None => None end. Proof. intros. - apply BSN.Bcompare_swap. + apply BinarySingleNaN.Bcompare_swap. Qed. Theorem bounded_le_emax_minus_prec : @@ -814,7 +800,7 @@ Theorem bounded_le_emax_minus_prec : (F2R (Float radix2 (Zpos mx) ex) <= bpow radix2 emax - bpow radix2 (emax - prec))%R. Proof. -now apply BSN.bounded_le_emax_minus_prec. +now apply BinarySingleNaN.bounded_le_emax_minus_prec. Qed. Theorem bounded_lt_emax : @@ -876,14 +862,14 @@ Qed. Notation shr_fexp := (shr_fexp prec emax) (only parsing). -Theorem shr_truncate : +Theorem shr_fexp_truncate : forall m e l, (0 <= m)%Z -> shr_fexp m e l = let '(m', e', l') := truncate radix2 fexp (m, e, l) in (shr_record_of_loc m' l', e'). Proof. intros m e l. -now apply shr_truncate. +now apply shr_fexp_truncate. Qed. (** Rounding modes *) @@ -893,7 +879,7 @@ Definition binary_overflow m s := Lemma eq_binary_overflow_FF2SF : forall x m s, - FF2SF x = BSN.binary_overflow prec emax m s -> + FF2SF x = BinarySingleNaN.binary_overflow prec emax m s -> x = binary_overflow m s. Proof. intros x m s H. @@ -924,7 +910,7 @@ intros mode x mx ex lx Px Bx Ex. generalize (binary_round_aux_correct' prec emax _ _ mode x mx ex lx Px Bx Ex). unfold binary_round_aux. destruct (Rlt_bool (Rabs _) _). -- now destruct BSN.binary_round_aux as [sz|sz| |sz mz ez]. +- now destruct BinarySingleNaN.binary_round_aux as [sz|sz| |sz mz ez]. - intros [_ ->]. split. rewrite valid_binary_SF2FF by apply is_nan_binary_overflow. @@ -948,7 +934,7 @@ intros mode x mx ex lx Bx Ex. generalize (binary_round_aux_correct prec emax _ _ mode x mx ex lx Bx Ex). unfold binary_round_aux. destruct (Rlt_bool (Rabs _) _). -- now destruct BSN.binary_round_aux as [sz|sz| |sz mz ez]. +- now destruct BinarySingleNaN.binary_round_aux as [sz|sz| |sz mz ez]. - intros [_ ->]. split. rewrite valid_binary_SF2FF by apply is_nan_binary_overflow. @@ -973,7 +959,7 @@ Theorem Bmult_correct : Proof. intros mult_nan mode x y. generalize (Bmult_correct prec emax _ _ mode (B2BSN x) (B2BSN y)). -replace (BSN.Bmult _ _ _) with (B2BSN (Bmult mult_nan mode x y)) by apply B2BSN_BSN2B. +replace (BinarySingleNaN.Bmult _ _ _) with (B2BSN (Bmult mult_nan mode x y)) by apply B2BSN_BSN2B. intros H. destruct x as [sx|sx|sx plx Hplx|sx mx ex Hx] ; destruct y as [sy|sy|sy ply Hply|sy my ey Hy] ; @@ -1022,7 +1008,7 @@ generalize (binary_round_correct prec emax _ _ mode sx mx ex). simpl. unfold binary_round. destruct Rlt_bool. -- now destruct BSN.binary_round. +- now destruct BinarySingleNaN.binary_round. - intros [H1 ->]. split. rewrite valid_binary_SF2FF by apply is_nan_binary_overflow. @@ -1049,7 +1035,7 @@ Theorem binary_normalize_correct : Proof. intros mode mx ex szero. generalize (binary_normalize_correct prec emax _ _ mode mx ex szero). -replace (BSN.binary_normalize _ _ _ _ _ _ _ _) with (B2BSN (binary_normalize mode mx ex szero)) by apply B2BSN_BSN2B'. +replace (BinarySingleNaN.binary_normalize _ _ _ _ _ _ _ _) with (B2BSN (binary_normalize mode mx ex szero)) by apply B2BSN_BSN2B'. simpl. destruct Rlt_bool. - now destruct binary_normalize. @@ -1083,7 +1069,7 @@ Proof with auto with typeclass_instances. intros plus_nan mode x y Fx Fy. rewrite <- is_finite_B2BSN in Fx, Fy. generalize (Bplus_correct prec emax _ _ mode _ _ Fx Fy). -replace (BSN.Bplus _ _ _) with (B2BSN (Bplus plus_nan mode x y)) by apply B2BSN_BSN2B. +replace (BinarySingleNaN.Bplus _ _ _) with (B2BSN (Bplus plus_nan mode x y)) by apply B2BSN_BSN2B. rewrite 2!B2R_B2BSN. rewrite (Bsign_B2BSN x) by (clear -Fx ; now destruct x). rewrite (Bsign_B2BSN y) by (clear -Fy ; now destruct y). @@ -1120,7 +1106,7 @@ Proof with auto with typeclass_instances. intros minus_nan mode x y Fx Fy. rewrite <- is_finite_B2BSN in Fx, Fy. generalize (Bminus_correct prec emax _ _ mode _ _ Fx Fy). -replace (BSN.Bminus _ _ _) with (B2BSN (Bminus minus_nan mode x y)) by apply B2BSN_BSN2B. +replace (BinarySingleNaN.Bminus _ _ _) with (B2BSN (Bminus minus_nan mode x y)) by apply B2BSN_BSN2B. rewrite 2!B2R_B2BSN. rewrite (Bsign_B2BSN x) by (clear -Fx ; now destruct x). rewrite (Bsign_B2BSN y) by (clear -Fy ; now destruct y). @@ -1161,7 +1147,7 @@ Proof. intros fma_nan mode x y z Fx Fy Fz. rewrite <- is_finite_B2BSN in Fx, Fy, Fz. generalize (Bfma_correct prec emax _ _ mode _ _ _ Fx Fy Fz). -replace (BSN.Bfma _ _ _ _) with (B2BSN (Bfma fma_nan mode x y z)) by apply B2BSN_BSN2B. +replace (BinarySingleNaN.Bfma _ _ _ _) with (B2BSN (Bfma fma_nan mode x y z)) by apply B2BSN_BSN2B. rewrite 3!B2R_B2BSN. cbv zeta. destruct Rlt_bool. @@ -1190,7 +1176,7 @@ Proof. intros div_nan mode x y Zy. rewrite <- B2R_B2BSN in Zy. generalize (Bdiv_correct prec emax _ _ mode (B2BSN x) _ Zy). -replace (BSN.Bdiv _ _ _) with (B2BSN (Bdiv div_nan mode x y)) by apply B2BSN_BSN2B. +replace (BinarySingleNaN.Bdiv _ _ _) with (B2BSN (Bdiv div_nan mode x y)) by apply B2BSN_BSN2B. unfold Rdiv. destruct y as [sy|sy|sy ply|sy my ey Hy] ; try now elim Zy. destruct x as [sx|sx|sx plx Hx|sx mx ex Hx] ; @@ -1215,12 +1201,42 @@ Theorem Bsqrt_correct : Proof. intros sqrt_nan mode x. generalize (Bsqrt_correct prec emax _ _ mode (B2BSN x)). -replace (BSN.Bsqrt _ _) with (B2BSN (Bsqrt sqrt_nan mode x)) by apply B2BSN_BSN2B. +replace (BinarySingleNaN.Bsqrt _ _) with (B2BSN (Bsqrt sqrt_nan mode x)) by apply B2BSN_BSN2B. intros H. destruct x as [sx|[|]|sx plx Hplx|sx mx ex Hx] ; try easy. now destruct Bsqrt. Qed. +(** NearbyInt and Trunc **) + +Definition Bnearbyint nearbyint_nan m x := + BSN2B (nearbyint_nan x) (Bnearbyint m (B2BSN x)). + +Theorem Bnearbyint_correct : + forall nearbyint_nan md x, + B2R (Bnearbyint nearbyint_nan md x) = round radix2 (FIX_exp 0) (round_mode md) (B2R x) /\ + is_finite (Bnearbyint nearbyint_nan md x) = is_finite x /\ + (is_nan (Bnearbyint nearbyint_nan md x) = false -> Bsign (Bnearbyint nearbyint_nan md x) = Bsign x). +Proof. +intros nearbyint_nan mode x. +generalize (Bnearbyint_correct prec emax _ mode (B2BSN x)). +replace (BinarySingleNaN.Bnearbyint _ _) with (B2BSN (Bnearbyint nearbyint_nan mode x)) by apply B2BSN_BSN2B. +intros H. +destruct x as [sx|[|]|sx plx Hplx|sx mx ex Hx] ; try easy. +now destruct Bnearbyint. +Qed. + +Definition Btrunc x := Btrunc (B2BSN x). + +Theorem Btrunc_correct : + forall x, + IZR (Btrunc x) = round radix2 (FIX_exp 0) Ztrunc (B2R x). +Proof. + intros x. + rewrite <-B2R_B2BSN. + now apply Btrunc_correct. +Qed. + (** A few values *) Definition Bone := @@ -1255,7 +1271,7 @@ Definition Bmax_float := Definition Bnormfr_mantissa x := Bnormfr_mantissa (B2BSN x). -Definition lift x y (Ny : @BSN.is_nan prec emax y = is_nan x) : binary_float. +Definition lift x y (Ny : @BinarySingleNaN.is_nan prec emax y = is_nan x) : binary_float. Proof. destruct (is_nan x). exact x. @@ -1293,7 +1309,7 @@ Theorem Bldexp_correct : Proof. intros mode x e. generalize (Bldexp_correct prec emax _ _ mode (B2BSN x) e). -replace (BSN.Bldexp _ _ _) with (B2BSN (Bldexp mode x e)) by apply B2BSN_lift. +replace (BinarySingleNaN.Bldexp _ _ _) with (B2BSN (Bldexp mode x e)) by apply B2BSN_lift. rewrite B2R_B2BSN. destruct Rlt_bool. - destruct x as [sx|sx|sx px Px|sx mx ex Bx] ; try easy. @@ -1304,7 +1320,7 @@ destruct Rlt_bool. rewrite FF2SF_B2FF, H. destruct x as [sx|sx|sx px Px|sx mx ex Bx] ; simpl in H ; try easy. contradict H. - unfold BSN.binary_overflow. + unfold BinarySingleNaN.binary_overflow. now destruct overflow_to_inf. Qed. @@ -1340,7 +1356,7 @@ generalize (Bfrexp_correct prec emax _ (B2BSN x) Fx). simpl. rewrite <- B2R_B2BSN. rewrite B2BSN_lift. -destruct BSN.Bfrexp as [z e]. +destruct BinarySingleNaN.Bfrexp as [z e]. rewrite B2R_B2BSN. now intros [H1 [H2 H3]]. Qed. @@ -1366,7 +1382,7 @@ Proof. intros x Fx. rewrite <- is_finite_B2BSN in Fx. generalize (Bulp_correct prec emax _ _ _ Fx). -replace (BSN.Bulp (B2BSN x)) with (B2BSN (Bulp x)) by apply B2BSN_lift. +replace (BinarySingleNaN.Bulp (B2BSN x)) with (B2BSN (Bulp x)) by apply B2BSN_lift. rewrite 2!B2R_B2BSN. now destruct Bulp. Qed. @@ -1393,7 +1409,7 @@ Proof. intros x Fx. rewrite <- is_finite_B2BSN in Fx. generalize (Bsucc_correct prec emax _ _ _ Fx). -replace (BSN.Bsucc (B2BSN x)) with (B2BSN (Bsucc x)) by apply B2BSN_lift. +replace (BinarySingleNaN.Bsucc (B2BSN x)) with (B2BSN (Bsucc x)) by apply B2BSN_lift. rewrite 2!B2R_B2BSN. destruct Rlt_bool. - rewrite (Bsign_B2BSN x) by now destruct x. @@ -1422,7 +1438,7 @@ Proof. intros x Fx. rewrite <- is_finite_B2BSN in Fx. generalize (Bpred_correct prec emax _ _ _ Fx). -replace (BSN.Bpred (B2BSN x)) with (B2BSN (Bpred x)) by apply B2BSN_lift. +replace (BinarySingleNaN.Bpred (B2BSN x)) with (B2BSN (Bpred x)) by apply B2BSN_lift. rewrite 2!B2R_B2BSN. destruct Rlt_bool. - rewrite (Bsign_B2BSN x) by now destruct x. diff --git a/flocq/IEEE754/BinarySingleNaN.v b/flocq/IEEE754/BinarySingleNaN.v index 2dd5c3c6..f0259966 100644 --- a/flocq/IEEE754/BinarySingleNaN.v +++ b/flocq/IEEE754/BinarySingleNaN.v @@ -164,6 +164,35 @@ now case sx. now case sx. Qed. +Theorem canonical_bounded : + forall sx mx ex, + bounded mx ex = true -> + canonical radix2 fexp (Float radix2 (cond_Zopp sx (Zpos mx)) ex). +Proof. +intros sx mx ex H. +apply canonical_canonical_mantissa. +now apply andb_prop in H. +Qed. + +Lemma emin_lt_emax : + (emin < emax)%Z. +Proof. +unfold emin. +unfold Prec_gt_0 in prec_gt_0_. +unfold Prec_lt_emax in prec_lt_emax_. +lia. +Qed. + +Lemma fexp_emax : + fexp emax = (emax - prec)%Z. +Proof. +apply Z.max_l. +unfold emin. +unfold Prec_gt_0 in prec_gt_0_. +unfold Prec_lt_emax in prec_lt_emax_. +lia. +Qed. + Theorem generic_format_B2R : forall x, generic_format radix2 fexp (B2R x). @@ -171,8 +200,7 @@ Proof. intros [sx|sx| |sx mx ex Hx] ; try apply generic_format_0. simpl. apply generic_format_canonical. -apply canonical_canonical_mantissa. -now destruct (andb_prop _ _ Hx) as (H, _). +now apply canonical_bounded. Qed. Theorem FLT_format_B2R : @@ -261,10 +289,8 @@ assert (mx = my /\ ex = ey). refine (_ (canonical_unique _ fexp _ _ _ _ Heq)). rewrite Hs. now case sy ; intro H ; injection H ; split. -apply canonical_canonical_mantissa. -exact (proj1 (andb_prop _ _ Hx)). -apply canonical_canonical_mantissa. -exact (proj1 (andb_prop _ _ Hy)). +now apply canonical_bounded. +now apply canonical_bounded. (* *) revert Hx. rewrite Hs, (proj1 H), (proj2 H). @@ -513,47 +539,51 @@ Theorem Bcompare_correct : is_finite f1 = true -> is_finite f2 = true -> Bcompare f1 f2 = Some (Rcompare (B2R f1) (B2R f2)). Proof. - Ltac apply_Rcompare := - match goal with - | [ |- Lt = Rcompare _ _ ] => symmetry; apply Rcompare_Lt - | [ |- Eq = Rcompare _ _ ] => symmetry; apply Rcompare_Eq - | [ |- Gt = Rcompare _ _ ] => symmetry; apply Rcompare_Gt - end. - unfold Bcompare, SFcompare; intros f1 f2 H1 H2. - destruct f1, f2; try easy; apply f_equal; clear H1 H2. - now rewrite Rcompare_Eq. - destruct s0 ; apply_Rcompare. +assert (Hb: forall m1 e1 m2 e2, bounded m1 e1 = true -> bounded m2 e2 = true -> (e1 < e2)%Z -> + (F2R (Float radix2 (Zpos m1) e1) < F2R (Float radix2 (Zpos m2) e2))%R). +{ intros m1 e1 m2 e2 B1 B2 He. + apply (lt_cexp_pos radix2 fexp). + now apply F2R_gt_0. + rewrite <- (canonical_bounded false _ _ B1). + rewrite <- (canonical_bounded false _ _ B2). + easy. } +assert (Hc: forall m1 e1 m2 e2, bounded m1 e1 = true -> bounded m2 e2 = true -> + Rcompare (F2R (Float radix2 (Zpos m1) e1)) (F2R (Float radix2 (Zpos m2) e2)) = + match Z.compare e1 e2 with Eq => Z.compare (Zpos m1) (Zpos m2) | Lt => Lt | Gt => Gt end). +{ intros m1 e1 m2 e2 B1 B2. + case Zcompare_spec ; intros He. + + apply Rcompare_Lt. + now apply Hb. + + now rewrite He, Rcompare_F2R. + + apply Rcompare_Gt. + now apply Hb. } +intros [s1|[|]| |[|] m1 e1 B1] ; try easy ; + intros [s2|[|]| |[|] m2 e2 B2] ; try easy ; + intros _ _ ; apply (f_equal Some), eq_sym. +- now apply Rcompare_Eq. +- apply Rcompare_Gt. now apply F2R_lt_0. +- apply Rcompare_Lt. now apply F2R_gt_0. - destruct s ; apply_Rcompare. +- apply Rcompare_Lt. + now apply F2R_lt_0. +- unfold B2R. + rewrite 2!F2R_cond_Zopp. + rewrite Rcompare_opp. + rewrite Hc by easy. + rewrite (Z.compare_antisym e1), (Z.compare_antisym (Zpos m1)). + now case Z.compare. +- apply Rcompare_Lt. + apply Rlt_trans with 0%R. now apply F2R_lt_0. now apply F2R_gt_0. - simpl. - apply andb_prop in e0; destruct e0; apply (canonical_canonical_mantissa false) in H. - apply andb_prop in e2; destruct e2; apply (canonical_canonical_mantissa false) in H1. - pose proof (Zcompare_spec e e1); unfold canonical, Fexp in H1, H. - assert (forall m1 m2 e1 e2, - let x := (IZR (Zpos m1) * bpow radix2 e1)%R in - let y := (IZR (Zpos m2) * bpow radix2 e2)%R in - (cexp radix2 fexp x < cexp radix2 fexp y)%Z -> (x < y)%R). - { - intros; apply Rnot_le_lt; intro; apply (mag_le radix2) in H5. - apply Zlt_not_le with (1 := H4). - now apply fexp_monotone. - now apply (F2R_gt_0 _ (Float radix2 (Zpos m2) e2)). - } - assert (forall m1 m2 e1 e2, (IZR (- Zpos m1) * bpow radix2 e1 < IZR (Zpos m2) * bpow radix2 e2)%R). - { - intros; apply (Rlt_trans _ 0%R). - now apply (F2R_lt_0 _ (Float radix2 (Zneg m1) e0)). - now apply (F2R_gt_0 _ (Float radix2 (Zpos m2) e2)). - } - unfold F2R, Fnum, Fexp. - destruct s, s0; try (now apply_Rcompare; apply H5); inversion H3; - try (apply_Rcompare; apply H4; rewrite H, H1 in H7; assumption); - try (apply_Rcompare; do 2 rewrite opp_IZR, Ropp_mult_distr_l_reverse; - apply Ropp_lt_contravar; apply H4; rewrite H, H1 in H7; assumption); - rewrite H7, Rcompare_mult_r, Rcompare_IZR by (apply bpow_gt_0); reflexivity. +- apply Rcompare_Gt. + now apply F2R_gt_0. +- apply Rcompare_Gt. + apply Rlt_trans with 0%R. + now apply F2R_lt_0. + now apply F2R_gt_0. +- now apply Hc. Qed. Theorem Bcompare_swap : @@ -584,6 +614,16 @@ intros ->. case Rcompare_spec; intro H; case Req_bool_spec; intro H'; try reflexivity; lra. Qed. +Theorem Beqb_refl : + forall f, Beqb f f = negb (is_nan f). +Proof. +intros f. +generalize (fun H => Beqb_correct f f H H). +destruct f as [s|[|]| |s m e H] ; try easy. +intros ->. 2: easy. +now apply Req_bool_true. +Qed. + Definition Bltb (f1 f2 : binary_float) : bool := SFltb (B2SF f1) (B2SF f2). Theorem Bltb_correct : @@ -618,45 +658,38 @@ Theorem bounded_le_emax_minus_prec : (F2R (Float radix2 (Zpos mx) ex) <= bpow radix2 emax - bpow radix2 (emax - prec))%R. Proof. +clear prec_lt_emax_. intros mx ex Hx. -destruct (andb_prop _ _ Hx) as (H1,H2). -generalize (Zeq_bool_eq _ _ H1). clear H1. intro H1. -generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2. -generalize (mag_F2R_Zdigits radix2 (Zpos mx) ex). -destruct (mag radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). -unfold mag_val. -intros H. -elim Ex; [|now apply Rgt_not_eq, F2R_gt_0]; intros _. -rewrite <-F2R_Zabs; simpl; clear Ex; intros Ex. -generalize (Rmult_lt_compat_r (bpow radix2 (-ex)) _ _ (bpow_gt_0 _ _) Ex). -unfold F2R; simpl; rewrite Rmult_assoc, <-!bpow_plus. -rewrite H; [|intro H'; discriminate H']. -rewrite <-Z.add_assoc, Z.add_opp_diag_r, Z.add_0_r, Rmult_1_r. -rewrite <-(IZR_Zpower _ _ (Zdigits_ge_0 _ _)); clear Ex; intro Ex. -generalize (Zlt_le_succ _ _ (lt_IZR _ _ Ex)); clear Ex; intro Ex. -generalize (IZR_le _ _ Ex). -rewrite succ_IZR; clear Ex; intro Ex. -generalize (Rplus_le_compat_r (-1) _ _ Ex); clear Ex; intro Ex. -ring_simplify in Ex; revert Ex. -rewrite (IZR_Zpower _ _ (Zdigits_ge_0 _ _)); intro Ex. -generalize (Rmult_le_compat_r (bpow radix2 ex) _ _ (bpow_ge_0 _ _) Ex). -intro H'; apply (Rle_trans _ _ _ H'). -rewrite Rmult_minus_distr_r, Rmult_1_l, <-bpow_plus. -revert H1; unfold fexp, FLT_exp; intro H1. -generalize (Z.le_max_l (Z.pos (digits2_pos mx) + ex - prec) emin). - -rewrite H1; intro H1'. -generalize (proj1 (Z.le_sub_le_add_r _ _ _) H1'). -rewrite Zpos_digits2_pos; clear H1'; intro H1'. -apply (Rle_trans _ _ _ (Rplus_le_compat_r _ _ _ (bpow_le _ _ _ H1'))). -replace emax with (emax - prec - ex + (ex + prec))%Z at 1 by ring. -replace (emax - prec)%Z with (emax - prec - ex + ex)%Z at 2 by ring. -do 2 rewrite (bpow_plus _ (emax - prec - ex)). -rewrite <-Rmult_minus_distr_l. -rewrite <-(Rmult_1_l (_ + _)). -apply Rmult_le_compat_r. -{ apply Rle_0_minus, bpow_le; unfold Prec_gt_0 in prec_gt_0_; lia. } -change 1%R with (bpow radix2 0); apply bpow_le; lia. +apply Rle_trans with ((bpow radix2 (Zdigits radix2 (Z.pos mx)) - 1) * bpow radix2 ex)%R. +- apply Rmult_le_compat_r. + apply bpow_ge_0. + rewrite <- IZR_Zpower by apply Zdigits_ge_0. + rewrite <- minus_IZR. + apply IZR_le. + apply Z.lt_le_pred. + rewrite <- (Z.abs_eq (Z.pos mx)) by easy. + apply Zdigits_correct. +- destruct (andb_prop _ _ Hx) as [H1 H2]. + apply Rle_trans with (bpow radix2 (ex + prec) - bpow radix2 ex)%R. + { rewrite Rmult_minus_distr_r, Rmult_1_l, <- bpow_plus. + apply Rplus_le_compat_r. + apply bpow_le. + apply Zeq_bool_eq in H1. + rewrite Zpos_digits2_pos in H1. + unfold fexp, FLT_exp in H1. + clear -H1 ; lia. } + replace emax with (emax - prec - ex + (ex + prec))%Z at 1 by ring. + replace (emax - prec)%Z with (emax - prec - ex + ex)%Z at 2 by ring. + do 2 rewrite (bpow_plus _ (emax - prec - ex)). + rewrite <- Rmult_minus_distr_l. + rewrite <- (Rmult_1_l (_ - _)) at 1. + apply Rmult_le_compat_r. + + apply Rle_0_minus, bpow_le. + unfold Prec_gt_0 in prec_gt_0_. + clear -prec_gt_0_ ; lia. + + apply (bpow_le radix2 0). + apply Zle_minus_le_0. + now apply Zle_bool_imp_le. Qed. Theorem bounded_lt_emax : @@ -686,6 +719,27 @@ unfold fexp, FLT_exp. intros ; lia. Qed. +(* needs prec_lt_emax_, so backward-incompatible +Theorem bounded_le_emax_minus_prec : + forall mx ex, + bounded mx ex = true -> + (F2R (Float radix2 (Zpos mx) ex) + <= bpow radix2 emax - bpow radix2 (emax - prec))%R. +Proof. +intros mx ex Bx. +rewrite <- fexp_emax. +rewrite <- pred_bpow. +apply pred_ge_gt. +- exact fexp_correct. +- apply generic_format_canonical. + now apply (canonical_bounded false). +- apply generic_format_FLT_bpow. + exact prec_gt_0_. + apply Zlt_le_weak, emin_lt_emax. +- now apply bounded_lt_emax. +Qed. +*) + Theorem bounded_ge_emin : forall mx ex, bounded mx ex = true -> @@ -778,9 +832,7 @@ rewrite F2R_Zabs. apply Ex. apply Rgt_not_eq. now apply F2R_gt_0. -unfold emin. -generalize (prec_gt_0 prec) (prec_lt_emax prec emax). -clear ; lia. +apply Z.max_l_iff, fexp_emax. Qed. (** Truncation *) @@ -869,9 +921,117 @@ intros (m, r, s) Hm. now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|]. Qed. -Notation shr_fexp := (shr_fexp prec emax). +Lemma le_shr1_le : + forall mrs, (0 <= shr_m mrs)%Z -> + (0 <= 2 * shr_m (shr_1 mrs) <= shr_m mrs)%Z /\ + (shr_m mrs < 2 * (shr_m (shr_1 mrs) + 1))%Z. +Proof. + destruct mrs as [m r s]. simpl. + destruct m as [| p | p]; [simpl; lia | intros _ | intros; easy]. + destruct p; simpl; [| | lia]. + - rewrite Pos2Z.inj_xO, Pos2Z.inj_xI. lia. + - rewrite Pos2Z.inj_xO. lia. +Qed. + +Lemma le_shr_le : + forall mrs e n, + (0 <= shr_m mrs)%Z -> (0 <= n)%Z -> + (0 <= 2 ^ n * shr_m (fst (shr mrs e n)) <= shr_m mrs)%Z /\ + (shr_m mrs < 2 ^ n * (shr_m (fst (shr mrs e n)) + 1))%Z. +Proof. + intros mrs e n Hmrs. + destruct n as [| n | n ]; + [intros _; simpl; now destruct (shr_m mrs); simpl; lia | intro Hn | lia]. + unfold shr. + rewrite iter_pos_nat. rewrite <-!(positive_nat_Z n). simpl fst. + induction (nat_of_P n) as [| n' IHn']; [simpl; destruct (shr_m mrs); simpl; lia |]. + rewrite !Nat2Z.inj_succ. rewrite Z.pow_succ_r; [| apply Zle_0_nat]. + + rewrite iter_nat_S. rewrite (Z.mul_comm 2%Z _), <-Z.mul_assoc. + destruct IHn' as [[IHn'1 IHn'2] IHn'3]. apply Z.mul_nonneg_cancel_l in IHn'1; [| lia]. + repeat split; + [| transitivity (2 ^ Z.of_nat n' * shr_m (iter_nat shr_1 n' mrs))%Z; [| auto] |]. + - apply Z.mul_nonneg_nonneg; [lia |]. now apply le_shr1_le. + - apply Z.mul_le_mono_nonneg_l; [lia |]. now apply le_shr1_le. + - apply Z.lt_le_trans with + (2 ^ Z.of_nat n' * (shr_m (iter_nat shr_1 n' mrs) + 1))%Z; [assumption |]. + rewrite <-Z.mul_assoc. apply Z.mul_le_mono_nonneg_l; [lia |]. + apply Ztac.Zlt_le_add_1. now apply le_shr1_le. +Qed. + +Lemma shr_limit : + forall mrs e n, + ((0 < shr_m mrs)%Z \/ shr_m mrs = 0%Z /\ (shr_r mrs || shr_s mrs = true)%bool) -> + (shr_m mrs < radix2 ^ (n - 1))%Z -> + fst (shr mrs e n) = {| shr_m := 0%Z; shr_r := false; shr_s := true |}. +Proof. + intros mrs e n Hmrs0. set (n' := (n - 1)%Z). replace n with (n' + 1)%Z; [| lia]. + destruct n' as [| p | p ]. + - simpl. destruct Hmrs0 as [Hmrs0 | Hmrs0]; [lia | intros _]. + destruct mrs as [m r s]. simpl in Hmrs0. destruct Hmrs0 as [Hmrs00 Hmrs01]. + rewrite Hmrs00. simpl. now rewrite Hmrs01. + - intros Hmrs1. rewrite !Z.add_1_r. rewrite <-Pos2Z.inj_succ. simpl shr. + rewrite iter_pos_nat. rewrite Pos2Nat.inj_succ. simpl iter_nat. + rewrite <-(positive_nat_Z p) in Hmrs1. rewrite <-(Pos2Nat.id p) at 2. + revert Hmrs1. revert Hmrs0. revert mrs. + induction (nat_of_P p) as [| n'' IHn'']. + + simpl in *. intros mrs [Hmrs0 | [Hmrs00 Hmrs01]] Hmrs1; [lia |]. + destruct mrs as [m r s]. simpl in Hmrs00, Hmrs01, Hmrs1. rewrite Hmrs00. + simpl. now rewrite Hmrs01. + + intros mrs Hmrs0 Hmrs1. simpl iter_nat. + destruct (le_shr1_le mrs) as [[Hmrs'0 Hmrs'1] Hmrs'2]; [destruct Hmrs0; lia |]. + set (mrs' := shr_1 mrs). apply IHn''. + * case (0 + (0 <= m)%Z -> + shr (shr_record_of_loc m l) e (f (Zdigits2 m + e) - e)%Z = + let '(m', e', l') := truncate radix2 f (m, e, l) in (shr_record_of_loc m' l', e'). +Proof. + intros f m e l Hf Hm. case_eq (truncate radix2 f (m, e, l)). intros (m', e') l'. + unfold shr_fexp. rewrite Zdigits2_Zdigits. case_eq (f (Zdigits radix2 m + e) - e)%Z. + - intros He. unfold truncate. rewrite He. simpl. intros H. now inversion H. + - intros p Hp. assert (He: (e <= f (Zdigits radix2 m + e))%Z); [ clear -Hp; lia |]. + destruct (inbetween_float_ex radix2 m e l) as (x, Hx). + generalize (inbetween_shr x m e l (f (Zdigits radix2 m + e) - e) Hm Hx)%Z. + assert (Hx0 : (0 <= x)%R); + [apply Rle_trans with (F2R (Float radix2 m e)); + [now apply F2R_ge_0 + |exact (proj1 (inbetween_float_bounds _ _ _ _ _ Hx))] + |]. + case_eq (shr (shr_record_of_loc m l) e (f (Zdigits radix2 m + e) - e))%Z. + intros mrs e'' H3 H4 H1. + generalize (truncate_correct radix2 _ x m e l Hx0 Hx (or_introl _ He)). + rewrite H1. intros (H2,_). rewrite <- Hp, H3. + assert (e'' = e'). + { change (snd (mrs, e'') = snd (fst (m',e',l'))). rewrite <- H1, <- H3. + unfold truncate. now rewrite Hp. } + rewrite H in H4 |- *. apply (f_equal (fun v => (v, _))). + destruct (inbetween_float_unique _ _ _ _ _ _ _ H2 H4) as (H5, H6). + rewrite H5, H6. case mrs. now intros m0 [|] [|]. + - intros p Hp. unfold truncate. rewrite Hp. simpl. intros H. now inversion H. +Qed. + +Notation shr_fexp := (shr_fexp prec emax). + +Theorem shr_fexp_truncate : forall m e l, (0 <= m)%Z -> shr_fexp m e l = @@ -948,6 +1108,25 @@ Definition choice_mode m sx mx lx := | mode_NA => cond_incr (round_N true lx) mx end. +Lemma le_choice_mode_le : + forall m sx mx lx, (mx <= choice_mode m sx mx lx <= mx + 1)%Z. +Proof. + unfold choice_mode; intros m sx mx lx; case m; simpl; try lia; apply le_cond_incr_le. +Qed. + +Lemma round_mode_choice_mode : + forall md x m l, + inbetween_int m (Rabs x) l -> + round_mode md x = cond_Zopp (Rlt_bool x 0) (choice_mode md (Rlt_bool x 0) m l). +Proof. + destruct md. + - exact inbetween_int_NE_sign. + - exact inbetween_int_ZR_sign. + - exact inbetween_int_DN_sign. + - exact inbetween_int_UP_sign. + - exact inbetween_int_NA_sign. +Qed. + Global Instance valid_rnd_round_mode : forall m, Valid_rnd (round_mode m). Proof. destruct m ; unfold round_mode ; auto with typeclass_instances. @@ -989,9 +1168,8 @@ rewrite Bool.andb_true_r. apply Zeq_bool_true. rewrite Zpos_digits2_pos. replace (Zdigits radix2 _) with prec. -unfold fexp, FLT_exp, emin. -generalize (prec_gt_0 prec) (prec_lt_emax prec emax). -clear ; zify ; lia. +ring_simplify (prec + (emax - prec))%Z. +apply fexp_emax. change 2%Z with (radix_val radix2). assert (H: (0 < radix2 ^ prec - 1)%Z). apply Zlt_succ_pred. @@ -1076,7 +1254,7 @@ Proof with auto with typeclass_instances. intros m x mx ex lx Px Bx Ex z. unfold binary_round_aux in z. revert z. -rewrite shr_truncate. +rewrite shr_fexp_truncate. refine (_ (round_trunc_sign_any_correct' _ _ (round_mode m) (choice_mode m) _ x mx ex lx Bx (or_introl _ Ex))). rewrite <- cexp_abs in Ex. refine (_ (truncate_correct_partial' _ fexp _ _ _ _ _ Bx Ex)). @@ -1108,7 +1286,7 @@ assert (Br: inbetween_float radix2 m1' e1 (Rabs (round radix2 fexp (round_mode m now apply inbetween_Exact. destruct m1' as [|m1'|m1']. (* . m1' = 0 *) -rewrite shr_truncate. 2: apply Z.le_refl. +rewrite shr_fexp_truncate. 2: apply Z.le_refl. generalize (truncate_0 radix2 fexp e1 loc_Exact). destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2). rewrite shr_m_shr_record_of_loc. @@ -1139,7 +1317,7 @@ refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Br He)). 2: now rewrite Hr ; apply F2R_gt_0. refine (_ (truncate_correct_format radix2 fexp (Zpos m1') e1 _ _ He)). 2: discriminate. -rewrite shr_truncate. 2: easy. +rewrite shr_fexp_truncate. 2: easy. destruct (truncate radix2 fexp (Zpos m1', e1, loc_Exact)) as ((m2, e2), l2). rewrite shr_m_shr_record_of_loc. intros (H3,H4) (H2,_). @@ -1201,7 +1379,7 @@ Proof with auto with typeclass_instances. intros m x mx ex lx Bx Ex z. unfold binary_round_aux in z. revert z. -rewrite shr_truncate. 2: easy. +rewrite shr_fexp_truncate. 2: easy. refine (_ (round_trunc_sign_any_correct _ _ (round_mode m) (choice_mode m) _ x (Zpos mx) ex lx Bx (or_introl _ Ex))). refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Bx Ex)). destruct (truncate radix2 fexp (Zpos mx, ex, lx)) as ((m1, e1), l1). @@ -1232,7 +1410,7 @@ assert (Br: inbetween_float radix2 m1' e1 (Rabs (round radix2 fexp (round_mode m now apply inbetween_Exact. destruct m1' as [|m1'|m1']. (* . m1' = 0 *) -rewrite shr_truncate. 2: apply Z.le_refl. +rewrite shr_fexp_truncate. 2: apply Z.le_refl. generalize (truncate_0 radix2 fexp e1 loc_Exact). destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2). rewrite shr_m_shr_record_of_loc. @@ -1263,7 +1441,7 @@ refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Br He)). 2: now rewrite Hr ; apply F2R_gt_0. refine (_ (truncate_correct_format radix2 fexp (Zpos m1') e1 _ _ He)). 2: discriminate. -rewrite shr_truncate. 2: easy. +rewrite shr_fexp_truncate. 2: easy. destruct (truncate radix2 fexp (Zpos m1', e1, loc_Exact)) as ((m2, e2), l2). rewrite shr_m_shr_record_of_loc. intros (H3,H4) (H2,_). @@ -1571,8 +1749,7 @@ split. now rewrite is_finite_SF2B. rewrite Bsign_SF2B, Rz''. rewrite Rcompare_Gt... -apply F2R_gt_0. -simpl. lia. +now apply F2R_gt_0. intros Hz' (Vz, Rz). rewrite B2SF_SF2B, Rz. apply f_equal. @@ -1590,8 +1767,7 @@ split. now rewrite is_finite_SF2B. rewrite Bsign_SF2B, Rz''. rewrite Rcompare_Lt... -apply F2R_lt_0. -simpl. lia. +now apply F2R_lt_0. intros Hz' (Vz, Rz). rewrite B2SF_SF2B, Rz. apply f_equal. @@ -1674,9 +1850,9 @@ now apply F2R_ge_0. now apply F2R_ge_0. (* .. *) elim Rle_not_lt with (1 := Bz). -generalize (bounded_lt_emax _ _ Hx) (bounded_lt_emax _ _ Hy) (andb_prop _ _ Hx) (andb_prop _ _ Hy). -intros Bx By (Hx',_) (Hy',_). -generalize (canonical_canonical_mantissa sx _ _ Hx') (canonical_canonical_mantissa sy _ _ Hy'). +generalize (bounded_lt_emax _ _ Hx) (bounded_lt_emax _ _ Hy). +intros Bx By. +generalize (canonical_bounded sx _ _ Hx) (canonical_bounded sy _ _ Hy). clear -Bx By Hs prec_gt_0_. intros Cx Cy. destruct sx. @@ -1809,11 +1985,9 @@ eapply canonical_unique in Hp. inversion Hp. clear -H0. destruct sy, sx, m ; easy. -apply canonical_canonical_mantissa. -apply Bool.andb_true_iff in Hy. easy. +now apply canonical_bounded. rewrite <- cond_Zopp_negb. -apply canonical_canonical_mantissa. -apply Bool.andb_true_iff in Hx. easy. +now apply canonical_bounded. intros Vz. rewrite Hp in Hz. assert (Sz := sign_plus_overflow m sx mx ex sy my ey Hx Hy Hz). @@ -2244,8 +2418,7 @@ intros. apply Z.le_max_r. now apply F2R_gt_0. apply generic_format_canonical. -apply (canonical_canonical_mantissa false). -apply (andb_prop _ _ Hx). +now apply (canonical_bounded false). apply round_ge_generic... apply generic_format_0. apply sqrt_ge_0. @@ -2293,6 +2466,226 @@ intros _. now rewrite Bsign_SF2B. Qed. +(** NearbyInt and Trunc **) + +Definition SFnearbyint_binary_aux m sx mx ex := + if (0 <=? ex)%Z then ((Z.pos mx) * 2 ^ ex)%Z else + let mrs := {| shr_m := Z.pos mx; shr_r := false; shr_s := false |} in + let mrs' := if (ex + let (mx''', ex''') := shl_align_fexp n 0 in + S754_finite sx mx''' ex''' + | Z.neg n => S754_nan + | Z0 => S754_zero sx + end. + +Lemma Bnearbyint_correct_aux : + forall md sx mx ex (Hx : bounded mx ex = true), + let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in + let z := SFnearbyint_binary md sx mx ex in + valid_binary z = true /\ + SF2R radix2 z = (round radix2 (FIX_exp 0) (round_mode md) x) /\ + is_finite_SF z = true /\ (is_nan_SF z = false -> sign_SF z = sx). +Proof. + intros md sx mx ex Hmxex. simpl. + set (mrs' := if (ex (0 <= shr_m mrs')%Z). + (* N.B.: The hypothesis (ex < 0)%Z is only here to make the proof simpler. *) + { intros Hex. + rewrite mrs'_simpl. + apply (Z.mul_le_mono_pos_l _ _ (2 ^ (- ex))). + apply (Zpower_gt_0 radix2). + lia. + rewrite Z.mul_0_r. + apply le_shr_le. + easy. + lia. } + repeat split; unfold SFnearbyint_binary, SFnearbyint_binary_aux; + case Zle_bool_spec; intros Hex0; fold mrs'; auto. + + - destruct choice_mode eqn:H0; auto. + unfold shl_align_fexp. destruct shl_align as [mx''' ex'''] eqn:H1; simpl. + unfold bounded, canonical_mantissa in Hmxex. apply andb_prop in Hmxex. + destruct Hmxex as [Hmxex Hex']. + unfold bounded, canonical_mantissa. + assert (A : (fexp (Z.pos (digits2_pos p) + 0) <= 0)%Z). + { rewrite Z.add_0_r in *. rewrite Zpos_digits2_pos in *. + destruct (le_shr_le mrs' ex (- ex)) as [H2 H3]; [now apply mrs'_ge_0 | lia |]. + destruct (le_choice_mode_le md sx (shr_m mrs') (loc_of_shr_record mrs')) as [H4 H5]. + rewrite H0 in H4, H5. + transitivity (fexp (Zdigits radix2 (shr_m mrs' + 1))); + [apply fexp_monotone; apply Zdigits_le; [lia | assumption] | + transitivity (fexp ((Zdigits radix2 (shr_m mrs') + 1))); + [apply fexp_monotone; apply Zdigits_succ_le; now apply mrs'_ge_0 | + transitivity (fexp (Zdigits radix2 ((shr_m {| shr_m := Z.pos mx; shr_r := false; shr_s := false |}) / (2 ^ (- ex))) + 1)); + [apply fexp_monotone; apply Zplus_le_compat_r; apply Zdigits_le; simpl; auto | simpl + ]]]. + - apply Zdiv.Zdiv_le_lower_bound; [lia |]. rewrite Z.mul_comm. rewrite mrs'_simpl. + apply le_shr_le; simpl; lia. + - transitivity (fexp (Zdigits radix2 (Z.pos mx / 2 ^ 1) + 1)). + + apply fexp_monotone. apply Zplus_le_compat_r. apply Zdigits_le. + * apply Z.div_pos; lia. + * apply Z.opp_pos_neg in Hex0. apply Z.div_le_compat_l; [lia |]. + split; [lia |]. apply Z.pow_le_mono_r; lia. + + rewrite Zdigits_div_Zpower; [| lia |]. + * rewrite Z.sub_add. apply Zeq_bool_eq in Hmxex. unfold fexp in *. + rewrite Z.max_lub_iff. split; [| lia]. apply (Zplus_le_reg_l _ _ ex). + rewrite Zplus_0_r. rewrite Z.add_sub_assoc. rewrite Z.add_comm. + rewrite <-Hmxex at 2. apply Z.le_max_l. + * split; [lia |]. replace 1%Z with (Zdigits radix2 (Z.pos 1)); [| easy]. + apply Zdigits_le; lia. } + refine (_ (shl_align_correct' p 0 (fexp (Z.pos (digits2_pos p) + 0)) _)). + + rewrite H1. intros [H2 H3]. rewrite <-H3 in H2. + apply andb_true_intro; split. + * apply Zeq_bool_true. rewrite H3 at 2. rewrite !Zpos_digits2_pos. + rewrite <-!mag_F2R_Zdigits; [| lia | lia]. + now apply (f_equal (fun f => fexp (mag radix2 f))). + * apply Zle_bool_true. rewrite H3. transitivity 0%Z; [assumption|]. + apply Zle_minus_le_0. apply Z.lt_le_incl. apply prec_lt_emax_. + + assumption. + + - symmetry. apply round_generic; auto. + + apply valid_rnd_round_mode. + + apply generic_format_FIX. + exists (Float radix2 (cond_Zopp sx (Z.pos mx) * Z.pow 2 ex) 0); auto. + simpl. rewrite <-(Z.sub_0_r ex) at 2. now apply F2R_change_exp. + + - rewrite round_trunc_sign_any_correct with (choice := choice_mode md) + (m := Z.pos mx) (e := ex) (l := loc_Exact). + + fold (shr_record_of_loc (Z.pos mx) loc_Exact) in mrs'_simpl. rewrite mrs'_simpl. + replace (- ex)%Z with (FIX_exp 0 (Zdigits2 (Z.pos mx) + ex) - ex)%Z; [| auto]. + rewrite !shr_truncate; [ | apply FIX_exp_valid | easy ]. + destruct truncate as (rec, loc) eqn:H0. destruct rec as (z0, z1) eqn:H1. + simpl. rewrite shr_m_shr_record_of_loc. rewrite loc_of_shr_record_of_loc. + replace (Rlt_bool (F2R {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}) 0) with sx. + * destruct choice_mode as [| p0 | p0] eqn:H2. + -- simpl. symmetry. rewrite cond_Zopp_0. apply F2R_0. + -- generalize (shl_align_fexp_correct p0 0). + destruct shl_align_fexp as (p1, z2). simpl. intros [H3 _]. + rewrite !F2R_cond_Zopp. apply f_equal. simpl in H0. + rewrite Zlt_bool_true in H0; [| lia]. + rewrite Z.add_opp_diag_r in H0. injection H0. + intros _ H4 _. now rewrite <-H4. + -- destruct (le_choice_mode_le md sx z0 loc) as [H3 _]. + rewrite H2 in H3. simpl in H0. + rewrite Zlt_bool_true in H0 by lia. + injection H0. intros _ _ H4. + elim (Zle_not_lt 0 z0). + rewrite <- H4. + apply Z_div_pos. + apply Z.lt_gt, (Zpower_gt_0 radix2). lia. + easy. + now apply Z.le_lt_trans with (1 := H3). + * rewrite F2R_cond_Zopp. apply eq_sym, Rlt_bool_cond_Ropp. + now apply F2R_gt_0. + + apply FIX_exp_valid. + + apply valid_rnd_round_mode. + + apply round_mode_choice_mode. + + rewrite <-F2R_abs. simpl. rewrite abs_cond_Zopp. simpl. now apply inbetween_Exact. + + auto. + + - destruct choice_mode eqn:H0; [easy | now destruct shl_align_fexp |]. + apply mrs'_ge_0 in Hex0. + destruct (le_choice_mode_le md sx (shr_m mrs') (loc_of_shr_record mrs')) as [H2 H3]. + rewrite H0 in H2, H3. lia. + + - destruct choice_mode eqn:H0; [easy | now destruct shl_align_fexp | easy]. +Qed. + +Definition Bnearbyint md (x : binary_float) := + match x with + | B754_nan => B754_nan + | B754_zero s => B754_zero s + | B754_infinity s => B754_infinity s + | B754_finite s m e H => + SF2B _ (proj1 (Bnearbyint_correct_aux md s m e H)) + end. + +Theorem Bnearbyint_correct : + forall md x, + B2R (Bnearbyint md x) = round radix2 (FIX_exp 0) (round_mode md) (B2R x) /\ + is_finite (Bnearbyint md x) = is_finite x /\ + (is_nan (Bnearbyint md x) = false -> Bsign (Bnearbyint md x) = Bsign x). +Proof. + intros md. + assert (round_0_ : 0%R = (round radix2 (FIX_exp 0) (round_mode md) 0)). + { symmetry. + apply round_0. + apply valid_rnd_round_mode. } + intros [sx | sx | | sx mx ex Hx]; try easy. + unfold Bnearbyint. destruct Bnearbyint_correct_aux as [H1 [H2 [H3 H4]]]. repeat split. + - rewrite B2R_SF2B. easy. + - rewrite is_finite_SF2B. easy. + - rewrite is_nan_SF2B. rewrite Bsign_SF2B. easy. +Qed. + +Definition Btrunc (x : binary_float) := + match x with + | B754_finite s m e _ => + cond_Zopp s (SFnearbyint_binary_aux mode_ZR s m e) + | _ => 0%Z + end. + +Theorem Btrunc_correct : + forall x, + IZR (Btrunc x) = round radix2 (FIX_exp 0) Ztrunc (B2R x). +Proof. + assert (round_0_to_0 : 0%R = (round radix2 (FIX_exp 0) Ztrunc 0)). + { symmetry. apply round_0. apply valid_rnd_ZR. } + intros [sx | sx | | sx mx ex Hx]; simpl; try assumption. + destruct (Bnearbyint_correct_aux mode_ZR sx mx ex) as [_ [H0 _]]; [easy |]. + simpl round_mode in H0. rewrite <-H0. unfold SFnearbyint_binary, SFnearbyint_binary_aux. + set (mrs' := + (if (ex 0%R). - { unfold xr, F2R; simpl. - rewrite <-(Rmult_0_l (bpow radix2 ex)); intro H. - apply Rmult_eq_reg_r in H; [|apply Rgt_not_eq, bpow_gt_0]. - apply eq_IZR in H; lia. } + { now apply F2R_neq_0. } assert (Hulp := Bulp_correct x' (eq_refl _)). rewrite <- (Bulp'_correct Hp x') in Hulp by easy. assert (Hldexp := Bldexp_correct mode_NE Bone (fexp (mag radix2 xr - 1))). @@ -3095,7 +3476,7 @@ assert (B2R (Bpred_pos' x) = pred_pos radix2 fexp (B2R x) /\ { apply Rlt_bool_true; rewrite round_generic; [|apply valid_rnd_round_mode|apply Fbpowxr]. rewrite Rabs_pos_eq; [|apply bpow_ge_0]; apply bpow_lt. - apply Z.max_lub_lt; [|unfold emin; unfold Prec_gt_0 in prec_gt_0_; lia]. + apply Z.max_lub_lt. 2: apply emin_lt_emax. apply (Zplus_lt_reg_r _ _ (prec + 1)); ring_simplify. rewrite Z.add_1_r; apply Zle_lt_succ, mag_le_bpow. - exact Nzxr. @@ -3277,12 +3658,8 @@ destruct x as [sx|sx| |sx mx ex Bx] ; try easy. easy. rewrite H1. apply eq_sym, F2R_bpow. - rewrite Rabs_pos_eq. - apply bpow_lt. - unfold emin. - generalize (prec_gt_0 prec) (prec_lt_emax prec emax). - lia. - apply bpow_ge_0. + rewrite Rabs_pos_eq by now apply bpow_ge_0. + apply bpow_lt, emin_lt_emax. apply valid_rnd_N. apply generic_format_bpow. unfold fexp. @@ -3337,9 +3714,7 @@ assert (H: rewrite opp_IZR, <-Ropp_mult_distr_l, <-Ropp_0; apply Ropp_le_contravar. now apply Rmult_le_pos; [apply IZR_le|apply bpow_ge_0]. } rewrite Hsucc; apply bpow_lt. - unfold emin. - generalize (prec_gt_0 prec) (prec_lt_emax prec emax). - lia. + apply emin_lt_emax. + fold x. assert (Hulp := Bulp_correct x (eq_refl _)). assert (Hplus := Bplus_correct mode_NE x (Bulp x) (eq_refl _)). @@ -3410,6 +3785,8 @@ Arguments Bmult {prec} {emax} {prec_gt_0_} {prec_lt_emax_}. Arguments Bfma {prec} {emax} {prec_gt_0_} {prec_lt_emax_}. Arguments Bdiv {prec} {emax} {prec_gt_0_} {prec_lt_emax_}. Arguments Bsqrt {prec} {emax} {prec_gt_0_} {prec_lt_emax_}. +Arguments Bnearbyint {prec} {emax} {prec_lt_emax_}. +Arguments Btrunc {prec} {emax}. Arguments Bldexp {prec} {emax} {prec_gt_0_} {prec_lt_emax_}. Arguments Bnormfr_mantissa {prec} {emax}. diff --git a/flocq/Version.v b/flocq/Version.v index 55afdadb..8f1a4eae 100644 --- a/flocq/Version.v +++ b/flocq/Version.v @@ -29,4 +29,4 @@ Definition Flocq_version := Eval vm_compute in parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N | Empty_string => (major * 100 + minor)%N end in - parse "4.0.0"%string N0 N0. + parse "4.1.0"%string N0 N0. diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index f7505c49..8db4d114 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -950,7 +950,7 @@ Proof. destruct (Bmult prec emax _ _ mult_nan mode f (BofZ 2)); reflexivity || discriminate. + destruct H0 as (P & Q). apply B2FF_inj. rewrite P, H. auto. - destruct f as [sf|sf|sf pf Hf|sf mf ef Hf]; try discriminate. - + unfold Bplus. simpl BSN.Bplus. rewrite eqb_true. destruct (BofZ 2) as [| | |s2 m2 e2 H2] eqn:B2; try discriminate; simpl in *. + + unfold Bplus. simpl BinarySingleNaN.Bplus. rewrite eqb_true. destruct (BofZ 2) as [| | |s2 m2 e2 H2] eqn:B2; try discriminate; simpl in *. assert ((0 = 2)%Z) by (apply eq_IZR; auto). discriminate. subst s2. unfold Bmult. simpl. rewrite xorb_false_r. auto. auto. @@ -1121,7 +1121,7 @@ clear H1. destruct SFdiv_core_binary as [[mz ez] lz]. destruct Rlt_bool. destruct H2 as [_ [H _]]. -now destruct BSN.binary_round_aux. +now destruct BinarySingleNaN.binary_round_aux. simpl in H2. rewrite H2. apply is_nan_binary_overflow. -- cgit