From d4513f41c54869c9b4ba96ab79d50933a1d5c25a Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 28 Dec 2020 15:53:36 +0100 Subject: Update Flocq to 3.4.0 (#383) --- flocq/Core/Defs.v | 4 + flocq/Core/Digits.v | 93 +++++++--------- flocq/Core/FIX.v | 11 +- flocq/Core/FLT.v | 254 ++++++++++++++++++++++++++++++------------ flocq/Core/FLX.v | 12 +- flocq/Core/FTZ.v | 32 +++--- flocq/Core/Float_prop.v | 12 +- flocq/Core/Generic_fmt.v | 123 ++++++++++++++++++--- flocq/Core/Raux.v | 32 ++++-- flocq/Core/Round_NE.v | 18 +-- flocq/Core/Round_pred.v | 282 +++++++++++++++++++++++++++++++++++++++++++++++ flocq/Core/Ulp.v | 222 ++++++++++++++++++++++++++++++------- flocq/Core/Zaux.v | 29 ++--- 13 files changed, 883 insertions(+), 241 deletions(-) (limited to 'flocq/Core') diff --git a/flocq/Core/Defs.v b/flocq/Core/Defs.v index f5c6f33b..27342df9 100644 --- a/flocq/Core/Defs.v +++ b/flocq/Core/Defs.v @@ -80,4 +80,8 @@ Definition Rnd_NA_pt (F : R -> Prop) (x f : R) := Rnd_N_pt F x f /\ forall f2 : R, Rnd_N_pt F x f2 -> (Rabs f2 <= Rabs f)%R. +Definition Rnd_N0_pt (F : R -> Prop) (x f : R) := + Rnd_N_pt F x f /\ + forall f2 : R, Rnd_N_pt F x f2 -> (Rabs f <= Rabs f2)%R. + End RND. diff --git a/flocq/Core/Digits.v b/flocq/Core/Digits.v index bed2e20a..a18ff8d6 100644 --- a/flocq/Core/Digits.v +++ b/flocq/Core/Digits.v @@ -17,8 +17,13 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *) -Require Import ZArith Zquot. +From Coq Require Import Lia ZArith Zquot. + Require Import Zaux. +Require Import SpecFloatCompat. + +Notation digits2_pos := digits2_pos (only parsing). +Notation Zdigits2 := Zdigits2 (only parsing). (** Number of bits (radix 2) of a positive integer. @@ -41,9 +46,9 @@ intros n d. unfold d. clear. assert (Hp: forall m, (Zpower_nat 2 (S m) = 2 * Zpower_nat 2 m)%Z) by easy. induction n ; simpl digits2_Pnat. rewrite Zpos_xI, 2!Hp. -omega. +lia. rewrite (Zpos_xO n), 2!Hp. -omega. +lia. now split. Qed. @@ -185,13 +190,13 @@ apply Zgt_not_eq. now apply Zpower_gt_0. now apply Zle_minus_le_0. destruct (Zle_or_lt 0 k) as [H0|H0]. -rewrite (Zdigit_lt n) by omega. +rewrite (Zdigit_lt n) by lia. unfold Zdigit. replace k' with (k' - k + k)%Z by ring. rewrite Zpower_plus with (2 := H0). rewrite Zmult_assoc, Z_quot_mult. replace (k' - k)%Z with (k' - k - 1 + 1)%Z by ring. -rewrite Zpower_exp by omega. +rewrite Zpower_exp by lia. rewrite Zmult_assoc. change (Zpower beta 1) with (beta * 1)%Z. rewrite Zmult_1_r. @@ -203,7 +208,7 @@ now apply Zlt_le_weak. rewrite Zdigit_lt with (1 := H0). apply sym_eq. apply Zdigit_lt. -omega. +lia. Qed. Theorem Zdigit_div_pow : @@ -227,7 +232,7 @@ unfold Zdigit. rewrite <- 2!ZOdiv_mod_mult. apply (f_equal (fun x => Z.quot x (beta ^ k))). replace k' with (k + 1 + (k' - (k + 1)))%Z by ring. -rewrite Zpower_exp by omega. +rewrite Zpower_exp by lia. rewrite Zmult_comm. rewrite Zpower_plus by easy. change (Zpower beta 1) with (beta * 1)%Z. @@ -449,7 +454,7 @@ unfold Zscale. case Zle_bool_spec ; intros Hk. now apply Zdigit_mul_pow. apply Zdigit_div_pow with (1 := Hk'). -omega. +lia. Qed. Theorem Zscale_0 : @@ -492,7 +497,7 @@ now rewrite Zpower_plus. now apply Zplus_le_0_compat. case Zle_bool_spec ; intros Hk''. pattern k at 1 ; replace k with (k + k' + -k')%Z by ring. -assert (0 <= -k')%Z by omega. +assert (0 <= -k')%Z by lia. rewrite Zpower_plus by easy. rewrite Zmult_assoc, Z_quot_mult. apply refl_equal. @@ -503,7 +508,7 @@ rewrite Zpower_plus with (2 := Hk). apply Zquot_mult_cancel_r. apply Zgt_not_eq. now apply Zpower_gt_0. -omega. +lia. Qed. Theorem Zscale_scale : @@ -532,7 +537,7 @@ rewrite Zdigit_mod_pow by apply Hk. rewrite Zdigit_scale by apply Hk. unfold Zminus. now rewrite Z.opp_involutive, Zplus_comm. -omega. +lia. Qed. Theorem Zdigit_slice_out : @@ -589,16 +594,16 @@ destruct (Zle_or_lt k2' k) as [Hk''|Hk'']. now apply Zdigit_slice_out. rewrite Zdigit_slice by now split. apply Zdigit_slice_out. -zify ; omega. -rewrite Zdigit_slice by (zify ; omega). +zify ; lia. +rewrite Zdigit_slice by (zify ; lia). rewrite (Zdigit_slice n (k1 + k1')) by now split. rewrite Zdigit_slice. now rewrite Zplus_assoc. -zify ; omega. +zify ; lia. unfold Zslice. rewrite Z.min_r. now rewrite Zle_bool_false. -omega. +lia. Qed. Theorem Zslice_mul_pow : @@ -624,14 +629,14 @@ case Zle_bool_spec ; intros Hk2. apply (f_equal (fun x => Z.rem x (beta ^ k2))). unfold Zscale. case Zle_bool_spec ; intros Hk1'. -replace k1 with Z0 by omega. +replace k1 with Z0 by lia. case Zle_bool_spec ; intros Hk'. -replace k with Z0 by omega. +replace k with Z0 by lia. simpl. now rewrite Z.quot_1_r. rewrite Z.opp_involutive. apply Zmult_1_r. -rewrite Zle_bool_false by omega. +rewrite Zle_bool_false by lia. rewrite 2!Z.opp_involutive, Zplus_comm. rewrite Zpower_plus by assumption. apply Zquot_Zquot. @@ -646,7 +651,7 @@ unfold Zscale. case Zle_bool_spec; intros Hk. now apply Zslice_mul_pow. apply Zslice_div_pow with (2 := Hk1). -omega. +lia. Qed. Theorem Zslice_div_pow_scale : @@ -666,7 +671,7 @@ apply Zdigit_slice_out. now apply Zplus_le_compat_l. rewrite Zdigit_slice by now split. destruct (Zle_or_lt 0 (k1 + k')) as [Hk1'|Hk1']. -rewrite Zdigit_slice by omega. +rewrite Zdigit_slice by lia. rewrite Zdigit_div_pow by assumption. apply f_equal. ring. @@ -685,15 +690,15 @@ rewrite Zdigit_plus. rewrite Zdigit_scale with (1 := Hk). destruct (Zle_or_lt (l1 + l2) k) as [Hk2|Hk2]. rewrite Zdigit_slice_out with (1 := Hk2). -now rewrite 2!Zdigit_slice_out by omega. +now rewrite 2!Zdigit_slice_out by lia. rewrite Zdigit_slice with (1 := conj Hk Hk2). destruct (Zle_or_lt l1 k) as [Hk1|Hk1]. rewrite Zdigit_slice_out with (1 := Hk1). -rewrite Zdigit_slice by omega. +rewrite Zdigit_slice by lia. simpl ; apply f_equal. ring. rewrite Zdigit_slice with (1 := conj Hk Hk1). -rewrite (Zdigit_lt _ (k - l1)) by omega. +rewrite (Zdigit_lt _ (k - l1)) by lia. apply Zplus_0_r. rewrite Zmult_comm. apply Zsame_sign_trans_weak with n. @@ -713,7 +718,7 @@ left. now apply Zdigit_slice_out. right. apply Zdigit_lt. -omega. +lia. Qed. Section digits_aux. @@ -788,7 +793,7 @@ pattern (radix_val beta) at 2 5 ; replace (radix_val beta) with (Zpower beta 1) rewrite <- Zpower_plus. rewrite Zplus_comm. apply IHu. -clear -Hv ; omega. +clear -Hv ; lia. split. now ring_simplify (1 + v - 1)%Z. now rewrite Zplus_assoc. @@ -928,7 +933,7 @@ intros x y Zx Hxy. assert (Hx := Zdigits_correct x). assert (Hy := Zdigits_correct y). apply (Zpower_lt_Zpower beta). -zify ; omega. +zify ; lia. Qed. Theorem lt_Zdigits : @@ -938,7 +943,7 @@ Theorem lt_Zdigits : (x < y)%Z. Proof. intros x y Hy. -cut (y <= x -> Zdigits y <= Zdigits x)%Z. omega. +cut (y <= x -> Zdigits y <= Zdigits x)%Z. lia. now apply Zdigits_le. Qed. @@ -951,7 +956,7 @@ intros e x Hex. destruct (Zdigits_correct x) as [H1 H2]. apply Z.le_trans with (2 := H1). apply Zpower_le. -clear -Hex ; omega. +clear -Hex ; lia. Qed. Theorem Zdigits_le_Zpower : @@ -961,7 +966,7 @@ Theorem Zdigits_le_Zpower : Proof. intros e x. generalize (Zpower_le_Zdigits e x). -omega. +lia. Qed. Theorem Zpower_gt_Zdigits : @@ -982,7 +987,7 @@ Theorem Zdigits_gt_Zpower : Proof. intros e x Hex. generalize (Zpower_gt_Zdigits e x). -omega. +lia. Qed. (** Number of digits of a product. @@ -1010,8 +1015,8 @@ apply Zdigits_correct. apply Zlt_le_succ. rewrite <- (Z.abs_eq y) at 1 by easy. apply Zdigits_correct. -clear -Hx ; omega. -clear -Hy ; omega. +clear -Hx ; lia. +clear -Hy ; lia. change Z0 with (0 + 0 + 0)%Z. apply Zplus_le_compat. now apply Zplus_le_compat. @@ -1031,7 +1036,7 @@ apply Zdigits_le. apply Zabs_pos. rewrite Zabs_Zmult. generalize (Zabs_pos x) (Zabs_pos y). -omega. +lia. apply Zdigits_mult_strong ; apply Zabs_pos. Qed. @@ -1041,7 +1046,7 @@ Theorem Zdigits_mult_ge : (Zdigits x + Zdigits y - 1 <= Zdigits (x * y))%Z. Proof. intros x y Zx Zy. -cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. omega. +cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. lia. apply Zdigits_gt_Zpower. rewrite Zabs_Zmult. rewrite Zpower_exp. @@ -1052,8 +1057,8 @@ apply Zpower_le_Zdigits. apply Zlt_pred. apply Zpower_ge_0. apply Zpower_ge_0. -generalize (Zdigits_gt_0 x). omega. -generalize (Zdigits_gt_0 y). omega. +generalize (Zdigits_gt_0 x). lia. +generalize (Zdigits_gt_0 y). lia. Qed. Theorem Zdigits_div_Zpower : @@ -1073,7 +1078,7 @@ destruct (Zle_lt_or_eq _ _ (proj2 He)) as [He'|He']. replace (Zdigits m - e - 1)%Z with (Zdigits m - 1 - e)%Z by ring. rewrite Z.pow_sub_r. 2: apply Zgt_not_eq, radix_gt_0. - 2: clear -He He' ; omega. + 2: clear -He He' ; lia. apply Z_div_le with (2 := H1). now apply Z.lt_gt, Zpower_gt_0. apply Zmult_lt_reg_r with (Zpower beta e). @@ -1118,13 +1123,6 @@ rewrite <- Zpower_nat_Z. apply digits2_Pnat_correct. Qed. -Fixpoint digits2_pos (n : positive) : positive := - match n with - | xH => xH - | xO p => Pos.succ (digits2_pos p) - | xI p => Pos.succ (digits2_pos p) - end. - Theorem Zpos_digits2_pos : forall m : positive, Zpos (digits2_pos m) = Zdigits radix2 (Zpos m). @@ -1137,13 +1135,6 @@ induction m ; simpl ; try easy ; apply f_equal, IHm. Qed. -Definition Zdigits2 n := - match n with - | Z0 => n - | Zpos p => Zpos (digits2_pos p) - | Zneg p => Zpos (digits2_pos p) - end. - Lemma Zdigits2_Zdigits : forall n, Zdigits2 n = Zdigits radix2 n. Proof. diff --git a/flocq/Core/FIX.v b/flocq/Core/FIX.v index 4e0a25e6..779d94cb 100644 --- a/flocq/Core/FIX.v +++ b/flocq/Core/FIX.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Fixed-point format *) + +From Coq Require Import Lia. Require Import Raux Defs Round_pred Generic_fmt Ulp Round_NE. Section RND_FIX. @@ -86,9 +88,16 @@ intros x; unfold ulp. case Req_bool_spec; intros Zx. case (negligible_exp_spec FIX_exp). intros T; specialize (T (emin-1)%Z); contradict T. -unfold FIX_exp; omega. +unfold FIX_exp; lia. intros n _; reflexivity. reflexivity. Qed. +Global Instance exists_NE_FIX : + Exists_NE beta FIX_exp. +Proof. +unfold Exists_NE, FIX_exp; simpl. +right; split; auto. +Qed. + End RND_FIX. diff --git a/flocq/Core/FLT.v b/flocq/Core/FLT.v index bd48d4b7..7301328d 100644 --- a/flocq/Core/FLT.v +++ b/flocq/Core/FLT.v @@ -46,7 +46,7 @@ intros k. unfold FLT_exp. generalize (prec_gt_0 prec). repeat split ; - intros ; zify ; omega. + intros ; zify ; lia. Qed. Theorem generic_format_FLT : @@ -93,24 +93,28 @@ simpl in ex. specialize (He Hx0). apply Rlt_le_trans with (1 := proj2 He). apply bpow_le. -cut (ex' - prec <= ex)%Z. omega. +cut (ex' - prec <= ex)%Z. lia. unfold ex, FLT_exp. apply Z.le_max_l. apply Z.le_max_r. Qed. - -Theorem FLT_format_bpow : +Theorem generic_format_FLT_bpow : forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e). Proof. intros e He. apply generic_format_bpow; unfold FLT_exp. apply Z.max_case; try assumption. -unfold Prec_gt_0 in prec_gt_0_; omega. +unfold Prec_gt_0 in prec_gt_0_; lia. Qed. - - +Theorem FLT_format_bpow : + forall e, (emin <= e)%Z -> FLT_format (bpow e). +Proof. +intros e He. +apply FLT_format_generic. +now apply generic_format_FLT_bpow. +Qed. Theorem FLT_format_satisfies_any : satisfies_any FLT_format. @@ -136,12 +140,40 @@ apply Zmax_left. destruct (mag beta x) as (ex, He). unfold FLX_exp. simpl. specialize (He Hx0). -cut (emin + prec - 1 < ex)%Z. omega. +cut (emin + prec - 1 < ex)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1 := Hx). apply He. Qed. +(** FLT is a nice format: it has a monotone exponent... *) +Global Instance FLT_exp_monotone : Monotone_exp FLT_exp. +Proof. +intros ex ey. +unfold FLT_exp. +zify ; lia. +Qed. + +(** and it allows a rounding to nearest, ties to even. *) +Global Instance exists_NE_FLT : + (Z.even beta = false \/ (1 < prec)%Z) -> + Exists_NE beta FLT_exp. +Proof. +intros [H|H]. +now left. +right. +intros e. +unfold FLT_exp. +destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ; + rewrite H2 ; clear H2. +generalize (Zmax_spec (e + 1 - prec) emin). +generalize (Zmax_spec (e - prec + 1 - prec) emin). +lia. +generalize (Zmax_spec (e + 1 - prec) emin). +generalize (Zmax_spec (emin + 1 - prec) emin). +lia. +Qed. + (** Links between FLT and FLX *) Theorem generic_format_FLT_FLX : forall x : R, @@ -192,7 +224,7 @@ apply Zmax_right. unfold FIX_exp. destruct (mag beta x) as (ex, Hex). simpl. -cut (ex - 1 < emin + prec)%Z. omega. +cut (ex - 1 < emin + prec)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (2 := Hx). now apply Hex. @@ -222,7 +254,7 @@ apply generic_inclusion_le... intros e He. unfold FIX_exp. apply Z.max_lub. -omega. +lia. apply Z.le_refl. Qed. @@ -238,45 +270,53 @@ destruct (Z.max_spec (n - prec) emin) as [(Hm, Hm')|(Hm, Hm')]. revert Hn prec_gt_0_; unfold FLT_exp, Prec_gt_0; rewrite Hm'; lia. Qed. -Theorem generic_format_FLT_1 (Hemin : (emin <= 0)%Z) : +Theorem generic_format_FLT_1 : + (emin <= 0)%Z -> generic_format beta FLT_exp 1. Proof. -unfold generic_format, scaled_mantissa, cexp, F2R; simpl. -rewrite Rmult_1_l, (mag_unique beta 1 1). -{ unfold FLT_exp. - destruct (Z.max_spec_le (1 - prec) emin) as [(H,Hm)|(H,Hm)]; rewrite Hm; - (rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]); - (rewrite Ztrunc_IZR, IZR_Zpower, <-bpow_plus; - [|unfold Prec_gt_0 in prec_gt_0_; omega]); - now replace (_ + _)%Z with Z0 by ring. } -rewrite Rabs_R1; simpl; split; [now right|]. -rewrite IZR_Zpower_pos; simpl; rewrite Rmult_1_r; apply IZR_lt. -apply (Z.lt_le_trans _ 2); [omega|]; apply Zle_bool_imp_le, beta. +intros Hemin. +now apply (generic_format_FLT_bpow 0). Qed. -Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R -> - ulp beta FLT_exp x = bpow emin. -Proof with auto with typeclass_instances. +Theorem ulp_FLT_0 : + ulp beta FLT_exp 0 = bpow emin. +Proof. +unfold ulp. +rewrite Req_bool_true by easy. +case negligible_exp_spec. +- intros T. + elim Zle_not_lt with (2 := T emin). + apply Z.le_max_r. +- intros n Hn. + apply f_equal. + assert (H: FLT_exp emin = emin). + apply Z.max_r. + generalize (prec_gt_0 prec). + clear ; lia. + rewrite <- H. + apply fexp_negligible_exp_eq. + apply FLT_exp_valid. + exact Hn. + rewrite H. + apply Z.le_refl. +Qed. + +Theorem ulp_FLT_small : + forall x, (Rabs x < bpow (emin + prec))%R -> + ulp beta FLT_exp x = bpow emin. +Proof. intros x Hx. -unfold ulp; case Req_bool_spec; intros Hx2. -(* x = 0 *) -case (negligible_exp_spec FLT_exp). -intros T; specialize (T (emin-1)%Z); contradict T. -apply Zle_not_lt; unfold FLT_exp. -apply Z.le_trans with (2:=Z.le_max_r _ _); omega. -assert (V:FLT_exp emin = emin). -unfold FLT_exp; apply Z.max_r. -unfold Prec_gt_0 in prec_gt_0_; omega. -intros n H2; rewrite <-V. -apply f_equal, fexp_negligible_exp_eq... -omega. -(* x <> 0 *) -apply f_equal; unfold cexp, FLT_exp. +destruct (Req_dec x 0%R) as [Zx|Zx]. +{ rewrite Zx. + apply ulp_FLT_0. } +rewrite ulp_neq_0 by easy. +apply f_equal. apply Z.max_r. -assert (mag beta x-1 < emin+prec)%Z;[idtac|omega]. -destruct (mag beta x) as (e,He); simpl. +destruct (mag beta x) as [e He]. +simpl. +cut (e - 1 < emin + prec)%Z. lia. apply lt_bpow with beta. -apply Rle_lt_trans with (2:=Hx). +apply Rle_lt_trans with (2 := Hx). now apply He. Qed. @@ -295,8 +335,8 @@ apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R. rewrite <- bpow_plus. right; apply f_equal. replace (e - 1 + (1 - prec))%Z with (e - prec)%Z by ring. -apply Z.max_l. -assert (emin+prec-1 < e)%Z; try omega. +apply Z.max_l; simpl. +assert (emin+prec-1 < e)%Z; try lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=Hx). now apply He. @@ -334,7 +374,7 @@ unfold ulp; rewrite Req_bool_false; [|now intro H; apply Nzx, (Rmult_eq_reg_r (bpow e)); [rewrite Rmult_0_l|apply Rgt_not_eq, Rlt_gt, bpow_gt_0]]. rewrite (Req_bool_false _ _ Nzx), <- bpow_plus; f_equal; unfold cexp, FLT_exp. -rewrite (mag_mult_bpow _ _ _ Nzx), !Z.max_l; omega. +rewrite (mag_mult_bpow _ _ _ Nzx), !Z.max_l; lia. Qed. Lemma succ_FLT_exact_shift_pos : @@ -375,32 +415,106 @@ fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool. rewrite ulp_FLT_exact_shift; [ring|lra| |]; rewrite mag_opp; lia. Qed. -(** FLT is a nice format: it has a monotone exponent... *) -Global Instance FLT_exp_monotone : Monotone_exp FLT_exp. -Proof. -intros ex ey. -unfold FLT_exp. -zify ; omega. -Qed. - -(** and it allows a rounding to nearest, ties to even. *) -Hypothesis NE_prop : Z.even beta = false \/ (1 < prec)%Z. - -Global Instance exists_NE_FLT : Exists_NE beta FLT_exp. +Theorem ulp_FLT_pred_pos : + forall x, + generic_format beta FLT_exp x -> + (0 <= x)%R -> + ulp beta FLT_exp (pred beta FLT_exp x) = ulp beta FLT_exp x \/ + (x = bpow (mag beta x - 1) /\ ulp beta FLT_exp (pred beta FLT_exp x) = (ulp beta FLT_exp x / IZR beta)%R). Proof. -destruct NE_prop as [H|H]. -now left. -right. -intros e. -unfold FLT_exp. -destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ; - rewrite H2 ; clear H2. -generalize (Zmax_spec (e + 1 - prec) emin). -generalize (Zmax_spec (e - prec + 1 - prec) emin). -omega. -generalize (Zmax_spec (e + 1 - prec) emin). -generalize (Zmax_spec (emin + 1 - prec) emin). -omega. +intros x Fx [Hx|Hx] ; cycle 1. +{ rewrite <- Hx. + rewrite pred_0. + rewrite ulp_opp. + left. + apply ulp_ulp_0. + apply FLT_exp_valid. + typeclasses eauto. } +assert (Hp: (0 <= pred beta FLT_exp x)%R). +{ apply pred_ge_gt ; try easy. + apply FLT_exp_valid. + apply generic_format_0. } +destruct (Rle_or_lt (bpow (emin + prec)) x) as [Hs|Hs]. +- unfold ulp. + rewrite Req_bool_false ; cycle 1. + { intros Zp. + apply Rle_not_lt with (1 := Hs). + generalize (f_equal (succ beta FLT_exp) Zp). + rewrite succ_pred. + rewrite succ_0, ulp_FLT_0. + intros H. + rewrite H. + apply bpow_lt. + generalize (prec_gt_0 prec). + lia. + apply FLT_exp_valid. + exact Fx. } + rewrite Req_bool_false by now apply Rgt_not_eq. + unfold cexp. + destruct (mag beta x) as [e He]. + simpl. + specialize (He (Rgt_not_eq _ _ Hx)). + rewrite Rabs_pos_eq in He by now apply Rlt_le. + destruct (proj1 He) as [Hb|Hb]. + + left. + apply (f_equal (fun v => bpow (FLT_exp v))). + apply mag_unique. + rewrite Rabs_pos_eq by easy. + split. + * apply pred_ge_gt ; try easy. + apply FLT_exp_valid. + apply generic_format_FLT_bpow. + apply Z.lt_le_pred. + apply lt_bpow with beta. + apply Rle_lt_trans with (2 := proj2 He). + apply Rle_trans with (2 := Hs). + apply bpow_le. + generalize (prec_gt_0 prec). + lia. + * apply pred_lt_le. + now apply Rgt_not_eq. + now apply Rlt_le. + + right. + split. + easy. + replace (FLT_exp _) with (FLT_exp e + -1)%Z. + rewrite bpow_plus. + now rewrite <- (Zmult_1_r beta). + rewrite <- Hb. + unfold FLT_exp at 1 2. + replace (mag_val _ _ (mag _ _)) with (e - 1)%Z. + rewrite <- Hb in Hs. + apply le_bpow in Hs. + zify ; lia. + apply eq_sym, mag_unique. + rewrite Hb. + rewrite Rabs_pos_eq by easy. + split ; cycle 1. + { apply pred_lt_id. + now apply Rgt_not_eq. } + apply pred_ge_gt. + apply FLT_exp_valid. + apply generic_format_FLT_bpow. + cut (emin + 1 < e)%Z. lia. + apply lt_bpow with beta. + apply Rle_lt_trans with (2 := proj2 He). + apply Rle_trans with (2 := Hs). + apply bpow_le. + generalize (prec_gt_0 prec). + lia. + exact Fx. + apply Rlt_le_trans with (2 := proj1 He). + apply bpow_lt. + apply Z.lt_pred_l. +- left. + rewrite (ulp_FLT_small x). + apply ulp_FLT_small. + rewrite Rabs_pos_eq by easy. + apply pred_lt_le. + now apply Rgt_not_eq. + now apply Rlt_le. + rewrite Rabs_pos_eq by now apply Rlt_le. + exact Hs. Qed. End RND_FLT. diff --git a/flocq/Core/FLX.v b/flocq/Core/FLX.v index 803d96ef..78bffba5 100644 --- a/flocq/Core/FLX.v +++ b/flocq/Core/FLX.v @@ -48,7 +48,7 @@ Proof. intros k. unfold FLX_exp. generalize prec_gt_0. -repeat split ; intros ; omega. +repeat split ; intros ; lia. Qed. Theorem FIX_format_FLX : @@ -212,7 +212,7 @@ Proof. case (negligible_exp_spec FLX_exp). intros _; reflexivity. intros n H2; contradict H2. -unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; omega. +unfold FLX_exp; unfold Prec_gt_0 in prec_gt_0_; lia. Qed. Theorem generic_format_FLX_1 : @@ -221,13 +221,13 @@ Proof. unfold generic_format, scaled_mantissa, cexp, F2R; simpl. rewrite Rmult_1_l, (mag_unique beta 1 1). { unfold FLX_exp. - rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]. - rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; omega]. + rewrite <- IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia]. + rewrite Ztrunc_IZR, IZR_Zpower; [|unfold Prec_gt_0 in prec_gt_0_; lia]. rewrite <- bpow_plus. now replace (_ + _)%Z with Z0 by ring. } rewrite Rabs_R1; simpl; split; [now right|]. unfold Z.pow_pos; simpl; rewrite Zmult_1_r; apply IZR_lt. -assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); omega. +assert (H := Zle_bool_imp_le _ _ (radix_prop beta)); lia. Qed. Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R. @@ -356,7 +356,7 @@ destruct NE_prop as [H|H]. now left. right. unfold FLX_exp. -split ; omega. +split ; lia. Qed. End RND_FLX. diff --git a/flocq/Core/FTZ.v b/flocq/Core/FTZ.v index 1a93bcd9..d6bae6ea 100644 --- a/flocq/Core/FTZ.v +++ b/flocq/Core/FTZ.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Floating-point format with abrupt underflow *) + +From Coq Require Import Lia. Require Import Raux Defs Round_pred Generic_fmt. Require Import Float_prop Ulp FLX. @@ -48,22 +50,22 @@ unfold FTZ_exp. generalize (Zlt_cases (k - prec) emin). case (Zlt_bool (k - prec) emin) ; intros H1. split ; intros H2. -omega. +lia. split. generalize (Zlt_cases (emin + prec + 1 - prec) emin). case (Zlt_bool (emin + prec + 1 - prec) emin) ; intros H3. -omega. +lia. generalize (Zlt_cases (emin + prec - 1 + 1 - prec) emin). generalize (prec_gt_0 prec). -case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; omega. +case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; lia. intros l H3. generalize (Zlt_cases (l - prec) emin). -case (Zlt_bool (l - prec) emin) ; omega. +case (Zlt_bool (l - prec) emin) ; lia. split ; intros H2. generalize (Zlt_cases (k + 1 - prec) emin). -case (Zlt_bool (k + 1 - prec) emin) ; omega. +case (Zlt_bool (k + 1 - prec) emin) ; lia. generalize (prec_gt_0 prec). -split ; intros ; omega. +split ; intros ; lia. Qed. Theorem FLXN_format_FTZ : @@ -94,7 +96,7 @@ rewrite Zlt_bool_false. apply Z.le_refl. rewrite Hx1, mag_F2R with (1 := Zxm). cut (prec - 1 < mag beta (IZR xm))%Z. -clear -Hx3 ; omega. +clear -Hx3 ; lia. apply mag_gt_Zpower with (1 := Zxm). apply Hx2. apply generic_format_FLXN. @@ -135,7 +137,7 @@ change (0 < F2R (Float beta (Z.abs (Ztrunc (x * bpow (- (emin + prec - 1))))) (e rewrite F2R_Zabs, <- Hx2. now apply Rabs_pos_lt. apply bpow_le. -omega. +lia. rewrite Hx2. eexists ; repeat split ; simpl. apply le_IZR. @@ -186,7 +188,7 @@ intros e He. unfold FTZ_exp. rewrite Zlt_bool_false. apply Z.le_refl. -omega. +lia. Qed. Theorem ulp_FTZ_0 : @@ -196,12 +198,12 @@ unfold ulp; rewrite Req_bool_true; trivial. case (negligible_exp_spec FTZ_exp). intros T; specialize (T (emin-1)%Z); contradict T. apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_. -rewrite Zlt_bool_true; omega. +rewrite Zlt_bool_true; lia. assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z). -unfold FTZ_exp; rewrite Zlt_bool_true; omega. +unfold FTZ_exp; rewrite Zlt_bool_true; lia. intros n H2; rewrite <-V. apply f_equal, fexp_negligible_exp_eq... -omega. +lia. Qed. @@ -290,12 +292,12 @@ apply Rle_trans with (2 := proj1 He). apply bpow_le. unfold FLX_exp. generalize (prec_gt_0 prec). -clear -He' ; omega. +clear -He' ; lia. apply bpow_ge_0. unfold FLX_exp, FTZ_exp. rewrite Zlt_bool_false. apply refl_equal. -clear -He' ; omega. +clear -He' ; lia. Qed. Theorem round_FTZ_small : @@ -331,7 +333,7 @@ intros He'. elim Rlt_not_le with (1 := Hx). apply Rle_trans with (2 := proj1 He). apply bpow_le. -omega. +lia. apply bpow_ge_0. Qed. diff --git a/flocq/Core/Float_prop.v b/flocq/Core/Float_prop.v index 804dd397..a1f48d04 100644 --- a/flocq/Core/Float_prop.v +++ b/flocq/Core/Float_prop.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *) + +From Coq Require Import Lia. Require Import Raux Defs Digits. Section Float_prop. @@ -360,7 +362,7 @@ unfold F2R. simpl. apply Rmult_le_compat_r. apply bpow_ge_0. apply IZR_le. -omega. +lia. Qed. Theorem F2R_lt_bpow : @@ -379,7 +381,7 @@ rewrite <-IZR_Zpower. 2: now apply Zle_left. now apply IZR_lt. elim Zlt_not_le with (1 := Hm). simpl. -cut (e' - e < 0)%Z. 2: omega. +cut (e' - e < 0)%Z. 2: lia. clear. case (e' - e)%Z ; try easy. intros p _. @@ -413,7 +415,7 @@ now elim (Zle_not_lt _ _ (Zabs_pos m)). (* . *) replace (e - e' + p)%Z with (e - (e' - p))%Z by ring. apply F2R_change_exp. -cut (e' - 1 < e + p)%Z. omega. +cut (e' - 1 < e + p)%Z. lia. apply (lt_bpow beta). apply Rle_lt_trans with (1 := Hf). rewrite <- F2R_Zabs, Zplus_comm, bpow_plus. @@ -472,10 +474,10 @@ assert (Hd := Zdigits_correct beta n). assert (Hd' := Zdigits_gt_0 beta n). apply Zle_antisym ; apply (bpow_lt_bpow beta). apply Rle_lt_trans with (2 := proj2 He). -rewrite <- IZR_Zpower by omega. +rewrite <- IZR_Zpower by lia. now apply IZR_le. apply Rle_lt_trans with (1 := proj1 He). -rewrite <- IZR_Zpower by omega. +rewrite <- IZR_Zpower by lia. now apply IZR_lt. Qed. diff --git a/flocq/Core/Generic_fmt.v b/flocq/Core/Generic_fmt.v index cb37bd91..af1bf3c1 100644 --- a/flocq/Core/Generic_fmt.v +++ b/flocq/Core/Generic_fmt.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * What is a real number belonging to a format, and many properties. *) + +From Coq Require Import Lia. Require Import Raux Defs Round_pred Float_prop. Section Generic. @@ -52,7 +54,7 @@ apply Znot_ge_lt. intros Hl. apply Z.ge_le in Hl. assert (H' := proj2 (proj2 (valid_exp l) Hl) k). -omega. +lia. Qed. Theorem valid_exp_large' : @@ -67,7 +69,7 @@ apply Z.ge_le in H'. assert (Hl := Z.le_trans _ _ _ H H'). apply valid_exp in Hl. assert (H1 := proj2 Hl k H'). -omega. +lia. Qed. Definition cexp x := @@ -425,7 +427,7 @@ rewrite Gx. replace (Ztrunc (scaled_mantissa x)) with Z0. apply F2R_0. cut (Z.abs (Ztrunc (scaled_mantissa x)) < 1)%Z. -clear ; zify ; omega. +clear ; zify ; lia. apply lt_IZR. rewrite abs_IZR. now rewrite <- scaled_mantissa_generic. @@ -522,7 +524,7 @@ specialize (Ex Hxz). apply Rlt_le_trans with (1 := proj2 Ex). apply bpow_le. specialize (Hp ex). -omega. +lia. Qed. Theorem generic_format_bpow_inv' : @@ -544,7 +546,7 @@ apply bpow_gt_0. split. apply bpow_ge_0. apply (bpow_lt _ _ 0). -clear -He ; omega. +clear -He ; lia. Qed. Theorem generic_format_bpow_inv : @@ -555,7 +557,7 @@ Proof. intros e He. apply generic_format_bpow_inv' in He. assert (H := valid_exp_large' (e + 1) e). -omega. +lia. Qed. Section Fcore_generic_round_pos. @@ -587,7 +589,7 @@ rewrite <- (Zrnd_IZR (Zceil x)). apply Zrnd_le. apply Zceil_ub. rewrite Zceil_floor_neq. -omega. +lia. intros H. rewrite <- H in Hx. rewrite Zfloor_IZR, Zrnd_IZR in Hx. @@ -630,7 +632,7 @@ apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: IZR (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)). apply IZR_Zpower. -omega. +lia. rewrite <- Hf. apply IZR_le. apply Zfloor_lub. @@ -657,7 +659,7 @@ apply Rmult_le_compat_r. apply bpow_ge_0. assert (Hf: IZR (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)). apply IZR_Zpower. -omega. +lia. rewrite <- Hf. apply IZR_le. apply Zceil_glb. @@ -738,7 +740,7 @@ destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1]. apply bpow_le. apply valid_exp, proj2 in Hx1. specialize (Hx1 ey). - omega. + lia. apply Rle_trans with (bpow ex). now apply round_bounded_large_pos. apply bpow_le. @@ -1380,7 +1382,7 @@ specialize (He (Rgt_not_eq _ _ Hx)). rewrite Rabs_pos_eq in He. 2: now apply Rlt_le. apply Rle_trans with (bpow (ex - 1)). apply bpow_le. -cut (e < ex)%Z. omega. +cut (e < ex)%Z. lia. apply (lt_bpow beta). now apply Rle_lt_trans with (2 := proj2 He). destruct (Zle_or_lt ex (fexp ex)). @@ -1389,7 +1391,7 @@ rewrite Hr in Hd. elim Rlt_irrefl with (1 := Hd). rewrite Hr. apply bpow_le. -omega. +lia. apply (round_bounded_large_pos rnd x ex H He). Qed. @@ -1526,7 +1528,7 @@ unfold cexp. set (ex := mag beta x). generalize (exp_not_FTZ ex). generalize (proj2 (proj2 (valid_exp _) He) (fexp ex + 1)%Z). -omega. +lia. rewrite <- H. rewrite <- mult_IZR, Ztrunc_IZR. unfold F2R. simpl. @@ -1802,7 +1804,7 @@ Theorem Znearest_imp : Proof. intros x n Hd. cut (Z.abs (Znearest x - n) < 1)%Z. -clear ; zify ; omega. +clear ; zify ; lia. apply lt_IZR. rewrite abs_IZR, minus_IZR. replace (IZR (Znearest x) - IZR n)%R with (- (x - IZR (Znearest x)) + (x - IZR n))%R by ring. @@ -1937,7 +1939,7 @@ replace (- _ + _)%Z with 0%Z by ring; simpl; rewrite Rmult_1_r. apply (Rlt_le_trans _ _ _ (proj2 Hex)). apply Rle_trans with (bpow (fexp (mag beta x) - 1)). - apply bpow_le. - rewrite (mag_unique beta x ex); [omega|]. + rewrite (mag_unique beta x ex); [lia|]. now rewrite Rabs_right. - unfold Zminus; rewrite bpow_plus. rewrite Rmult_comm. @@ -2012,6 +2014,68 @@ Qed. End rndNA. +Notation Znearest0 := (Znearest (fun x => (Zlt_bool x 0))). + +Section rndN0. + +Global Instance valid_rnd_N0 : Valid_rnd Znearest0 := valid_rnd_N _. + +Theorem round_N0_pt : + forall x, + Rnd_N0_pt generic_format x (round Znearest0 x). +Proof. +intros x. +generalize (round_N_pt (fun t => Zlt_bool t 0) x). +set (f := round (Znearest (fun t => Zlt_bool t 0)) x). +intros Rxf. +destruct (Req_dec (x - round Zfloor x) (round Zceil x - x)) as [Hm|Hm]. +(* *) +apply Rnd_N0_pt_N. +apply generic_format_0. +exact Rxf. +destruct (Rle_or_lt 0 x) as [Hx|Hx]. +(* . *) +rewrite Rabs_pos_eq with (1 := Hx). +rewrite Rabs_pos_eq. +unfold f. +rewrite round_N_middle with (1 := Hm). +rewrite Zlt_bool_false. +now apply round_DN_pt. +apply Zfloor_lub. +apply Rmult_le_pos with (1 := Hx). +apply bpow_ge_0. +apply Rnd_N_pt_ge_0 with (2 := Hx) (3 := Rxf). +apply generic_format_0. +(* . *) +rewrite Rabs_left with (1 := Hx). +rewrite Rabs_left1. +apply Ropp_le_contravar. +unfold f. +rewrite round_N_middle with (1 := Hm). +rewrite Zlt_bool_true. +now apply round_UP_pt. +apply lt_IZR. +apply Rle_lt_trans with (scaled_mantissa x). +apply Zfloor_lb. +simpl. +rewrite <- (Rmult_0_l (bpow (- (cexp x))%Z)%R). +apply Rmult_lt_compat_r with (2 := Hx). +apply bpow_gt_0. +apply Rnd_N_pt_le_0 with (3 := Rxf). +apply generic_format_0. +now apply Rlt_le. +(* *) +split. +apply Rxf. +intros g Rxg. +rewrite Rnd_N_pt_unique with (3 := Hm) (4 := Rxf) (5 := Rxg). +apply Rle_refl. +apply round_DN_pt; easy. +apply round_UP_pt; easy. +Qed. + +End rndN0. + Section rndN_opp. Theorem Znearest_opp : @@ -2055,6 +2119,31 @@ rewrite opp_IZR. now rewrite Ropp_mult_distr_l_reverse. Qed. +Lemma round_N0_opp : + forall x, + (round Znearest0 (- x) = - round Znearest0 x)%R. +Proof. +intros x. +rewrite round_N_opp. +apply Ropp_eq_compat. +apply round_ext. +clear x; intro x. +unfold Znearest. +case_eq (Rcompare (x - IZR (Zfloor x)) (/ 2)); intro C; +[|reflexivity|reflexivity]. +apply Rcompare_Eq_inv in C. +assert (H : negb (- (Zfloor x + 1) @@ -1305,9 +1317,9 @@ rewrite Ropp_inv_permute with (1 := Zy'). rewrite <- 2!opp_IZR. rewrite <- Zmod_opp_opp. apply H. -clear -Hy. omega. +clear -Hy. lia. apply H. -clear -Zy Hy. omega. +clear -Zy Hy. lia. (* *) split. pattern (IZR (x / y)) at 1 ; rewrite <- Rplus_0_r. @@ -1454,7 +1466,7 @@ rewrite <- (Rmult_1_r (bpow e1)). rewrite bpow_plus. apply Rmult_lt_compat_l. apply bpow_gt_0. -assert (0 < e2 - e1)%Z by omega. +assert (0 < e2 - e1)%Z by lia. destruct (e2 - e1)%Z ; try discriminate H0. clear. rewrite <- IZR_Zpower by easy. @@ -1756,7 +1768,7 @@ rewrite Rabs_right in Hex; [|now apply Rle_ge; apply Rlt_le]. rewrite Rabs_right in Hey; [|now apply Rle_ge; apply Rlt_le]. apply (Rlt_le_trans _ _ _ Hex). apply Rle_trans with (bpow (ey - 1)); [|exact Hey]. -now apply bpow_le; omega. +now apply bpow_le; lia. Qed. Theorem mag_bpow : @@ -1900,7 +1912,7 @@ apply bpow_le. now apply Zlt_le_weak. apply IZR_le. clear -Zm. -zify ; omega. +zify ; lia. Qed. Lemma mag_mult : @@ -1999,7 +2011,7 @@ assert (Hbeta : (2 <= r)%Z). { destruct r as (beta_val,beta_prop). now apply Zle_bool_imp_le. } intros x y Px Py Hln. -assert (Oxy : (y < x)%R); [apply lt_mag;[assumption|omega]|]. +assert (Oxy : (y < x)%R); [apply lt_mag;[assumption|lia]|]. destruct (mag x) as (ex,Hex). destruct (mag y) as (ey,Hey). simpl in Hln |- *. @@ -2096,7 +2108,7 @@ split. unfold Rsqr ; rewrite <- bpow_plus. apply bpow_le. generalize (Zdiv2_odd_eqn (e + 1)). - destruct Z.odd ; intros ; omega. + destruct Z.odd ; intros ; lia. - rewrite <- (Rabs_pos_eq (bpow _)) by apply bpow_ge_0. apply Rsqr_lt_abs_0. rewrite Rsqr_sqrt by now apply Rlt_le. @@ -2104,7 +2116,7 @@ split. unfold Rsqr ; rewrite <- bpow_plus. apply bpow_le. generalize (Zdiv2_odd_eqn (e + 1)). - destruct Z.odd ; intros ; omega. + destruct Z.odd ; intros ; lia. Qed. Lemma mag_1 : mag 1 = 1%Z :> Z. @@ -2324,7 +2336,7 @@ refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _). refine (H _ _ Py). apply INR_lt in Hy. clear -Hy HyN. - omega. + lia. now apply Rlt_le, Rinv_0_lt_compat. rewrite S_INR, HN. ring_simplify (IZR (up (/ l)) - 1 + 1)%R. @@ -2369,7 +2381,7 @@ rewrite <- (Z.opp_involutive n). rewrite <- (Z.abs_neq n). rewrite <- Zabs2Nat.id_abs. apply K. -omega. +lia. Qed. diff --git a/flocq/Core/Round_NE.v b/flocq/Core/Round_NE.v index 20b60ef5..b7387a62 100644 --- a/flocq/Core/Round_NE.v +++ b/flocq/Core/Round_NE.v @@ -18,6 +18,8 @@ COPYING file for more details. *) (** * Rounding to nearest, ties to even: existence, unicity... *) + +From Coq Require Import Lia. Require Import Raux Defs Round_pred Generic_fmt Float_prop Ulp. Notation ZnearestE := (Znearest (fun x => negb (Z.even x))). @@ -148,7 +150,7 @@ split. apply (round_DN_pt beta fexp x). apply generic_format_bpow. ring_simplify (ex - 1 + 1)%Z. -omega. +lia. apply Hex. apply Rle_lt_trans with (2 := proj2 Hex). apply (round_DN_pt beta fexp x). @@ -209,14 +211,14 @@ rewrite Z.even_add. rewrite eqb_sym. simpl. fold (negb (Z.even (beta ^ (ex - fexp ex)))). rewrite Bool.negb_involutive. -rewrite (Z.even_pow beta (ex - fexp ex)). 2: omega. +rewrite (Z.even_pow beta (ex - fexp ex)) by lia. destruct exists_NE_. rewrite H. apply Zeven_Zpower_odd with (2 := H). now apply Zle_minus_le_0. apply Z.even_pow. specialize (H ex). -omega. +lia. (* - xu < bpow ex *) revert Hud. rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq]. @@ -413,18 +415,18 @@ now rewrite Hs in Hr. destruct (Hs ex) as (H,_). rewrite Z.even_pow. exact Hr. -omega. +lia. assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx. -replace (Zfloor mx) with (Zceil mx + -1)%Z by omega. +replace (Zfloor mx) with (Zceil mx + -1)%Z by lia. rewrite Z.even_add. apply eqb_true. unfold mx. replace (Zceil (scaled_mantissa beta fexp x)) with (Zpower beta (ex - fexp ex)). rewrite Zeven_Zpower_odd with (2 := Hr). easy. -omega. +lia. apply eq_IZR. -rewrite IZR_Zpower. 2: omega. +rewrite IZR_Zpower by lia. apply Rmult_eq_reg_r with (bpow (fexp ex)). unfold Zminus. rewrite bpow_plus. @@ -434,7 +436,7 @@ now apply sym_eq. apply Rgt_not_eq. apply bpow_gt_0. generalize (proj1 (valid_exp ex) He). -omega. +lia. (* .. small pos *) assert (Z.even (Zfloor mx) = true). 2: now rewrite H in Hmx. unfold mx, scaled_mantissa. diff --git a/flocq/Core/Round_pred.v b/flocq/Core/Round_pred.v index 428a4bac..b7b6778f 100644 --- a/flocq/Core/Round_pred.v +++ b/flocq/Core/Round_pred.v @@ -42,6 +42,9 @@ Definition Rnd_NG (F : R -> Prop) (P : R -> R -> Prop) (rnd : R -> R) := Definition Rnd_NA (F : R -> Prop) (rnd : R -> R) := forall x : R, Rnd_NA_pt F x (rnd x). +Definition Rnd_N0 (F : R -> Prop) (rnd : R -> R) := + forall x : R, Rnd_N0_pt F x (rnd x). + Theorem round_val_of_pred : forall rnd : R -> R -> Prop, round_pred rnd -> @@ -1021,6 +1024,251 @@ intros F x f (Hf,_) Hx. now apply Rnd_N_pt_idempotent with F. Qed. +Theorem Rnd_N0_NG_pt : + forall F : R -> Prop, + F 0 -> + forall x f, + Rnd_N0_pt F x f <-> Rnd_NG_pt F (fun x f => Rabs f <= Rabs x) x f. +Proof. +intros F HF x f. +destruct (Rle_or_lt 0 x) as [Hx|Hx]. +(* *) +split ; intros (H1, H2). +(* . *) +assert (Hf := Rnd_N_pt_ge_0 F HF x f Hx H1). +split. +exact H1. +destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3]. +(* . . *) +left. +rewrite Rabs_pos_eq with (1 := Hf). +rewrite Rabs_pos_eq with (1 := Hx). +apply H3. +(* . . *) +right. +intros f2 Hxf2. +specialize (H2 _ Hxf2). +destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4]. +apply Rle_antisym. +apply Rle_trans with x. +apply H4. +apply H3. +rewrite Rabs_pos_eq with (1 := Hf) in H2. +rewrite Rabs_pos_eq in H2. +exact H2. +now apply Rnd_N_pt_ge_0 with F x. +eapply Rnd_UP_pt_unique ; eassumption. +(* . *) +split. +exact H1. +intros f2 Hxf2. +destruct H2 as [H2|H2]. +assert (Hf := Rnd_N_pt_ge_0 F HF x f Hx H1). +assert (Hf2 := Rnd_N_pt_ge_0 F HF x f2 Hx Hxf2). +rewrite 2!Rabs_pos_eq ; trivial. +rewrite 2!Rabs_pos_eq in H2 ; trivial. +destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3]. +apply H3. +apply H1. +apply H2. +apply Rle_trans with (1 := H2). +apply H3. +rewrite (H2 _ Hxf2). +apply Rle_refl. +(* *) +assert (Hx' := Rlt_le _ _ Hx). +clear Hx. rename Hx' into Hx. +split ; intros (H1, H2). +(* . *) +assert (Hf := Rnd_N_pt_le_0 F HF x f Hx H1). +split. +exact H1. +destruct (Rnd_N_pt_DN_or_UP _ _ _ H1) as [H3|H3]. +(* . . *) +right. +intros f2 Hxf2. +specialize (H2 _ Hxf2). +destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H4|H4]. +eapply Rnd_DN_pt_unique ; eassumption. +apply Rle_antisym. +2: apply Rle_trans with x. +2: apply H3. +2: apply H4. +rewrite Rabs_left1 with (1 := Hf) in H2. +rewrite Rabs_left1 in H2. +now apply Ropp_le_cancel. +now apply Rnd_N_pt_le_0 with F x. +(* . . *) +left. +rewrite Rabs_left1 with (1 := Hf). +rewrite Rabs_left1 with (1 := Hx). +apply Ropp_le_contravar. +apply H3. +(* . *) +split. +exact H1. +intros f2 Hxf2. +destruct H2 as [H2|H2]. +assert (Hf := Rnd_N_pt_le_0 F HF x f Hx H1). +assert (Hf2 := Rnd_N_pt_le_0 F HF x f2 Hx Hxf2). +rewrite 2!Rabs_left1 ; trivial. +rewrite 2!Rabs_left1 in H2 ; trivial. +apply Ropp_le_contravar. +apply Ropp_le_cancel in H2. +destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf2) as [H3|H3]. +2: apply H3. +2: apply H1. +2: apply H2. +apply Rle_trans with (2 := H2). +apply H3. +rewrite (H2 _ Hxf2). +apply Rle_refl. +Qed. + +Lemma Rnd_N0_pt_unique_prop : + forall F : R -> Prop, + F 0 -> + Rnd_NG_pt_unique_prop F (fun x f => Rabs f <= Rabs x). +Proof. +intros F HF x d u Hxd1 Hxd2 Hxu1 Hxu2 Hd Hu. +apply Rle_antisym. +apply Rle_trans with x. +apply Hxd1. +apply Hxu1. +destruct (Rle_or_lt 0 x) as [Hx|Hx]. +apply Hxd1. +apply Hxu1. +rewrite Rabs_pos_eq with (1 := Hx) in Hu. +rewrite Rabs_pos_eq in Hu. +exact Hu. +apply Rle_trans with (1:=Hx). +apply Hxu1. +(* *) +apply Hxu1. +apply Hxd1. +rewrite Rabs_left with (1 := Hx) in Hd. +rewrite Rabs_left1 in Hd. +now apply Ropp_le_cancel. +apply Rlt_le, Rle_lt_trans with (2:=Hx). +apply Hxd1. +Qed. + +Theorem Rnd_N0_pt_unique : + forall F : R -> Prop, + F 0 -> + forall x f1 f2 : R, + Rnd_N0_pt F x f1 -> Rnd_N0_pt F x f2 -> + f1 = f2. +Proof. +intros F HF x f1 f2 H1 H2. +apply (Rnd_NG_pt_unique F _ (Rnd_N0_pt_unique_prop F HF) x). +now apply -> Rnd_N0_NG_pt. +now apply -> Rnd_N0_NG_pt. +Qed. + +Theorem Rnd_N0_pt_N : + forall F : R -> Prop, + F 0 -> + forall x f : R, + Rnd_N_pt F x f -> + (Rabs f <= Rabs x)%R -> + Rnd_N0_pt F x f. +Proof. +intros F HF x f Rxf Hxf. +split. +apply Rxf. +intros g Rxg. +destruct (Rabs_eq_Rabs (f - x) (g - x)) as [H|H]. +apply Rle_antisym. +apply Rxf. +apply Rxg. +apply Rxg. +apply Rxf. +(* *) +replace g with f. +apply Rle_refl. +apply Rplus_eq_reg_r with (1 := H). +(* *) +assert (g = 2 * x - f)%R. +replace (2 * x - f)%R with (x - (f - x))%R by ring. +rewrite H. +ring. +destruct (Rle_lt_dec 0 x) as [Hx|Hx]. +(* . *) +revert Hxf. +rewrite Rabs_pos_eq with (1 := Hx). +rewrite 2!Rabs_pos_eq ; try ( apply (Rnd_N_pt_ge_0 F HF x) ; assumption ). +intros Hxf. +rewrite H0. +apply Rplus_le_reg_r with f. +ring_simplify. +apply Rmult_le_compat_l with (2 := Hxf). +now apply IZR_le. +(* . *) +revert Hxf. +apply Rlt_le in Hx. +rewrite Rabs_left1 with (1 := Hx). +rewrite 2!Rabs_left1 ; try ( apply (Rnd_N_pt_le_0 F HF x) ; assumption ). +intros Hxf. +rewrite H0. +apply Ropp_le_contravar. +apply Rplus_le_reg_r with f. +ring_simplify. +apply Rmult_le_compat_l. +now apply IZR_le. +now apply Ropp_le_cancel. +Qed. + +Theorem Rnd_N0_unique : + forall (F : R -> Prop), + F 0 -> + forall rnd1 rnd2 : R -> R, + Rnd_N0 F rnd1 -> Rnd_N0 F rnd2 -> + forall x, rnd1 x = rnd2 x. +Proof. +intros F HF rnd1 rnd2 H1 H2 x. +now apply Rnd_N0_pt_unique with F x. +Qed. + +Theorem Rnd_N0_pt_monotone : + forall F : R -> Prop, + F 0 -> + round_pred_monotone (Rnd_N0_pt F). +Proof. +intros F HF x y f g Hxf Hyg Hxy. +apply (Rnd_NG_pt_monotone F _ (Rnd_N0_pt_unique_prop F HF) x y). +now apply -> Rnd_N0_NG_pt. +now apply -> Rnd_N0_NG_pt. +exact Hxy. +Qed. + +Theorem Rnd_N0_pt_refl : + forall F : R -> Prop, + forall x : R, F x -> + Rnd_N0_pt F x x. +Proof. +intros F x Hx. +split. +now apply Rnd_N_pt_refl. +intros f Hxf. +apply Req_le. +apply f_equal. +now apply sym_eq, Rnd_N_pt_idempotent with (1 := Hxf). +Qed. + +Theorem Rnd_N0_pt_idempotent : + forall F : R -> Prop, + forall x f : R, + Rnd_N0_pt F x f -> F x -> + f = x. +Proof. +intros F x f (Hf,_) Hx. +now apply Rnd_N_pt_idempotent with F. +Qed. + + + + Theorem round_pred_ge_0 : forall P : R -> R -> Prop, round_pred_monotone P -> @@ -1405,4 +1653,38 @@ apply Rnd_NA_pt_monotone. apply Hany. Qed. +Theorem satisfies_any_imp_N0 : + forall F : R -> Prop, + F 0 -> satisfies_any F -> + round_pred (Rnd_N0_pt F). +Proof. +intros F HF0 Hany. +split. +assert (H : round_pred_total (Rnd_NG_pt F (fun a b => (Rabs b <= Rabs a)%R))). +apply satisfies_any_imp_NG. +apply Hany. +intros x d u Hf Hd Hu. +destruct (Rle_lt_dec 0 x) as [Hx|Hx]. +right. +rewrite Rabs_pos_eq with (1 := Hx). +rewrite Rabs_pos_eq. +apply Hd. +apply Hd; try easy. +left. +rewrite Rabs_left with (1 := Hx). +rewrite Rabs_left1. +apply Ropp_le_contravar. +apply Hu. +apply Hu; try easy. +now apply Rlt_le. +intros x. +destruct (H x) as (f, Hf). +exists f. +apply <- Rnd_N0_NG_pt. +apply Hf. +apply HF0. +apply Rnd_N0_pt_monotone. +apply HF0. +Qed. + End RND_prop. diff --git a/flocq/Core/Ulp.v b/flocq/Core/Ulp.v index 4f4a5674..c42b3e65 100644 --- a/flocq/Core/Ulp.v +++ b/flocq/Core/Ulp.v @@ -57,7 +57,7 @@ Proof. unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. now apply negligible_Some. apply negligible_None. -intros n; specialize (Hn n); omega. +intros n; specialize (Hn n); lia. Qed. Lemma negligible_exp_spec': (negligible_exp = None /\ forall n, (fexp n < n)%Z) @@ -66,7 +66,7 @@ Proof. unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn]. right; simpl; exists n; now split. left; split; trivial. -intros n; specialize (Hn n); omega. +intros n; specialize (Hn n); lia. Qed. Context { valid_exp : Valid_exp fexp }. @@ -75,8 +75,8 @@ Lemma fexp_negligible_exp_eq: forall n m, (n <= fexp n)%Z -> (m <= fexp m)%Z -> Proof. intros n m Hn Hm. case (Zle_or_lt n m); intros H. -apply valid_exp; omega. -apply sym_eq, valid_exp; omega. +apply valid_exp; lia. +apply sym_eq, valid_exp; lia. Qed. @@ -198,6 +198,17 @@ rewrite V. apply generic_format_0. Qed. +Theorem ulp_canonical : + forall m e, + m <> 0%Z -> + canonical beta fexp (Float beta m e) -> + ulp (F2R (Float beta m e)) = bpow e. +Proof. +intros m e Hm Hc. +rewrite ulp_neq_0 by now apply F2R_neq_0. +apply f_equal. +now apply sym_eq. +Qed. Theorem ulp_bpow : forall e, ulp (bpow e) = bpow (fexp (e + 1)). @@ -216,7 +227,6 @@ apply bpow_ge_0. apply Rgt_not_eq, Rlt_gt, bpow_gt_0. Qed. - Lemma generic_format_ulp_0 : F (ulp 0). Proof. @@ -238,17 +248,17 @@ rewrite Req_bool_true; trivial. case negligible_exp_spec. intros H1 _. apply generic_format_bpow. -specialize (H1 (e+1)%Z); omega. +specialize (H1 (e+1)%Z); lia. intros n H1 H2. apply generic_format_bpow. case (Zle_or_lt (e+1) (fexp (e+1))); intros H4. absurd (e+1 <= e)%Z. -omega. +lia. apply Z.le_trans with (1:=H4). replace (fexp (e+1)) with (fexp n). now apply le_bpow with beta. now apply fexp_negligible_exp_eq. -omega. +lia. Qed. (** The three following properties are equivalent: @@ -300,10 +310,10 @@ case (Zle_or_lt l (fexp l)); intros Hl. rewrite (fexp_negligible_exp_eq n l); trivial; apply Z.le_refl. case (Zle_or_lt (fexp n) (fexp l)); trivial; intros K. absurd (fexp n <= fexp l)%Z. -omega. +lia. apply Z.le_trans with (2:= H _). apply Zeq_le, sym_eq, valid_exp; trivial. -omega. +lia. Qed. Lemma not_FTZ_ulp_ge_ulp_0: @@ -374,8 +384,6 @@ rewrite Hn1 in H; discriminate. now apply bpow_mag_le. Qed. - - (** Definition and properties of pred and succ *) Definition pred_pos x := @@ -432,6 +440,17 @@ unfold pred. now rewrite Ropp_involutive. Qed. +Theorem pred_bpow : + forall e, pred (bpow e) = (bpow e - bpow (fexp e))%R. +Proof. +intros e. +rewrite pred_eq_pos by apply bpow_ge_0. +unfold pred_pos. +rewrite mag_bpow. +replace (e + 1 - 1)%Z with e by ring. +now rewrite Req_bool_true. +Qed. + (** pred and succ are in the format *) (* cannont be x <> ulp 0, due to the counter-example 1-bit FP format fexp: e -> e-1 *) @@ -450,7 +469,7 @@ apply gt_0_F2R with beta (cexp beta fexp x). rewrite <- Fx. apply Rle_lt_trans with (2:=Hx). apply bpow_ge_0. -omega. +lia. case (Zle_lt_or_eq _ _ H); intros Hm. (* *) pattern x at 1 ; rewrite Fx. @@ -533,7 +552,7 @@ rewrite ulp_neq_0. intro H. assert (ex-1 < cexp beta fexp x < ex)%Z. split ; apply (lt_bpow beta) ; rewrite <- H ; easy. -clear -H0. omega. +clear -H0. lia. now apply Rgt_not_eq. apply Ex'. apply Rle_lt_trans with (2 := proj2 Ex'). @@ -555,7 +574,7 @@ apply gt_0_F2R with beta (cexp beta fexp x). rewrite <- Fx. apply Rle_lt_trans with (2:=proj1 Ex'). apply bpow_ge_0. -omega. +lia. now apply Rgt_not_eq. Qed. @@ -579,7 +598,7 @@ rewrite minus_IZR, IZR_Zpower. rewrite Rmult_minus_distr_r, Rmult_1_l. rewrite <- bpow_plus. now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring. -omega. +lia. rewrite H. apply generic_format_F2R. intros _. @@ -592,7 +611,7 @@ split. apply Rplus_le_reg_l with (bpow (fexp (e-1))). ring_simplify. apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. -apply Rplus_le_compat ; apply bpow_le ; omega. +apply Rplus_le_compat ; apply bpow_le ; lia. apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. @@ -614,7 +633,7 @@ apply Ropp_lt_contravar. apply bpow_gt_0. apply Rle_ge; apply Rle_0_minus. apply bpow_le. -omega. +lia. replace f with 0%R. apply generic_format_0. unfold f. @@ -842,7 +861,7 @@ assert (ex - 1 < fexp ex < ex)%Z. split ; apply (lt_bpow beta) ; rewrite <- M by easy. lra. apply Hex. -omega. +lia. rewrite 2!ulp_neq_0 by lra. apply f_equal. unfold cexp ; apply f_equal. @@ -907,7 +926,7 @@ split. apply Rplus_le_reg_l with (bpow (fexp (e-1))). ring_simplify. apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R. -apply Rplus_le_compat; apply bpow_le; omega. +apply Rplus_le_compat; apply bpow_le; lia. apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac]. apply Rle_trans with (bpow 1*bpow (e - 2))%R. apply Rmult_le_compat_r. @@ -930,7 +949,7 @@ apply bpow_gt_0. apply Rle_ge; apply Rle_0_minus. rewrite Hxe. apply bpow_le. -omega. +lia. (* *) contradict Zp. rewrite Hxe, He; ring. @@ -953,12 +972,12 @@ unfold ulp; rewrite Req_bool_true; trivial. case negligible_exp_spec. intros K. specialize (K (e-1)%Z). -contradict K; omega. +contradict K; lia. intros n Hn. rewrite H3; apply f_equal. case (Zle_or_lt n (e-1)); intros H6. -apply valid_exp; omega. -apply sym_eq, valid_exp; omega. +apply valid_exp; lia. +apply sym_eq, valid_exp; lia. Qed. (** The following one is false for x = 0 in FTZ *) @@ -1081,7 +1100,7 @@ exfalso ; lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. -assert(mag beta eps-1 < fexp n)%Z;[idtac|omega]. +assert(mag beta eps-1 < fexp n)%Z;[idtac|lia]. apply lt_bpow with beta. apply Rle_lt_trans with (2:=proj2 H). destruct (mag beta eps) as (e,He). @@ -1105,7 +1124,6 @@ rewrite <- P, round_0; trivial. apply valid_rnd_DN. Qed. - Theorem round_UP_plus_eps_pos : forall x, (0 <= x)%R -> F x -> forall eps, (0 < eps <= ulp x)%R -> @@ -1147,7 +1165,7 @@ lra. intros n Hn H. assert (fexp (mag beta eps) = fexp n). apply valid_exp; try assumption. -assert(mag beta eps-1 < fexp n)%Z;[idtac|omega]. +assert(mag beta eps-1 < fexp n)%Z;[idtac|lia]. apply lt_bpow with beta. apply Rle_lt_trans with (2:=H). destruct (mag beta eps) as (e,He). @@ -1172,7 +1190,6 @@ apply round_generic... apply generic_format_ulp_0. Qed. - Theorem round_UP_pred_plus_eps_pos : forall x, (0 < x)%R -> F x -> forall eps, (0 < eps <= ulp (pred x) )%R -> @@ -1210,7 +1227,6 @@ apply Ropp_lt_contravar. now apply Heps. Qed. - Theorem round_DN_plus_eps: forall x, F x -> forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x) @@ -1248,7 +1264,6 @@ now apply Ropp_0_gt_lt_contravar. now apply generic_format_opp. Qed. - Theorem round_UP_plus_eps : forall x, F x -> forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x) @@ -1334,11 +1349,11 @@ now apply Rgt_not_eq. case (Zle_lt_or_eq _ _ H2); intros Hexy. assert (fexp ex = fexp (ey-1))%Z. apply valid_exp. -omega. +lia. rewrite <- H1. -omega. +lia. absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z. -omega. +lia. split. apply gt_0_F2R with beta (cexp beta fexp x). now rewrite <- Fx. @@ -1380,9 +1395,9 @@ apply sym_eq; apply mag_unique. rewrite H1, Rabs_right. split. apply bpow_le. -omega. +lia. apply bpow_lt. -omega. +lia. apply Rle_ge; apply bpow_ge_0. apply mag_unique. apply Hey. @@ -1527,7 +1542,7 @@ rewrite mag_bpow. replace (fexp n + 1 - 1)%Z with (fexp n) by ring. rewrite Req_bool_true; trivial. apply Rminus_diag_eq, f_equal. -apply sym_eq, valid_exp; omega. +apply sym_eq, valid_exp; lia. Qed. Theorem succ_0 : @@ -1904,7 +1919,7 @@ rewrite ulp_neq_0; trivial. apply f_equal. unfold cexp. apply valid_exp; trivial. -assert (mag beta x -1 < fexp n)%Z;[idtac|omega]. +assert (mag beta x -1 < fexp n)%Z;[idtac|lia]. apply lt_bpow with beta. destruct (mag beta x) as (e,He). simpl. @@ -2252,9 +2267,9 @@ rewrite Hn1; easy. now apply ulp_ge_ulp_0. Qed. - -Lemma ulp_succ_pos : forall x, F x -> (0 < x)%R -> - ulp (succ x) = ulp x \/ succ x = bpow (mag beta x). +Lemma ulp_succ_pos : + forall x, F x -> (0 < x)%R -> + ulp (succ x) = ulp x \/ succ x = bpow (mag beta x). Proof with auto with typeclass_instances. intros x Fx Hx. generalize (Rlt_le _ _ Hx); intros Hx'. @@ -2281,6 +2296,39 @@ apply ulp_ge_0. now apply sym_eq, mag_unique_pos. Qed. +Theorem ulp_pred_pos : + forall x, F x -> (0 < pred x)%R -> + ulp (pred x) = ulp x \/ x = bpow (mag beta x - 1). +Proof. +intros x Fx Hx. +assert (Hx': (0 < x)%R). + apply Rlt_le_trans with (1 := Hx). + apply pred_le_id. +assert (Zx : x <> 0%R). + now apply Rgt_not_eq. +rewrite (ulp_neq_0 x) by easy. +unfold cexp. +destruct (mag beta x) as [e He]. +simpl. +assert (bpow (e - 1) <= x < bpow e)%R. + rewrite <- (Rabs_pos_eq x) by now apply Rlt_le. + now apply He. +destruct (proj1 H) as [H1|H1]. +2: now right. +left. +apply pred_ge_gt with (2 := Fx) in H1. +rewrite ulp_neq_0 by now apply Rgt_not_eq. +apply (f_equal (fun e => bpow (fexp e))). +apply mag_unique_pos. +apply (conj H1). +apply Rle_lt_trans with (2 := proj2 H). +apply pred_le_id. +apply generic_format_bpow. +apply Z.lt_le_pred. +replace (_ + 1)%Z with e by ring. +rewrite <- (mag_unique_pos _ _ _ H). +now apply mag_generic_gt. +Qed. Lemma ulp_round_pos : forall { Not_FTZ_ : Exp_not_FTZ fexp}, @@ -2333,7 +2381,6 @@ replace (fexp n) with (fexp e); try assumption. now apply fexp_negligible_exp_eq. Qed. - Theorem ulp_round : forall { Not_FTZ_ : Exp_not_FTZ fexp}, forall rnd { Zrnd : Valid_rnd rnd } x, ulp (round beta fexp rnd x) = ulp x @@ -2373,6 +2420,18 @@ destruct (round_DN_or_UP beta fexp rnd x) as [Hr|Hr]; rewrite Hr. apply succ_ge_id. Qed. +Lemma pred_round_le_id : + forall rnd { Zrnd : Valid_rnd rnd } x, + (pred (round beta fexp rnd x) <= x)%R. +Proof. +intros rnd Vrnd x. +apply (Rle_trans _ (round beta fexp Raux.Zfloor x)). +2: now apply round_DN_pt. +destruct (round_DN_or_UP beta fexp rnd x) as [Hr|Hr]; rewrite Hr. +2: now apply pred_UP_le_DN. +apply pred_le_id. +Qed. + (** Properties of rounding to nearest and ulp *) Theorem round_N_le_midp: forall choice u v, @@ -2432,6 +2491,73 @@ unfold pred. right; field. Qed. +Lemma round_N_ge_ge_midp : forall choice u v, + F u -> + (u <= round beta fexp (Znearest choice) v)%R -> + ((u + pred u) / 2 <= v)%R. +Proof with auto with typeclass_instances. +intros choice u v Hu H2. +assert (K: ((u=0)%R /\ negligible_exp = None) \/ (pred u < u)%R). +case (Req_dec u 0); intros Zu. +case_eq (negligible_exp). +intros n Hn; right. +rewrite Zu, pred_0. +unfold ulp; rewrite Req_bool_true, Hn; try easy. +rewrite <- Ropp_0. +apply Ropp_lt_contravar, bpow_gt_0. +intros _; left; split; easy. +right. +apply pred_lt_id... +(* *) +case K. +intros (K1,K2). +(* . *) +rewrite K1, pred_0. +unfold ulp; rewrite Req_bool_true, K2; try easy. +replace ((0+-0)/2)%R with 0%R by field. +case (Rle_or_lt 0 v); try easy. +intros H3; contradict H2. +rewrite K1; apply Rlt_not_le. +assert (H4: (round beta fexp (Znearest choice) v <= 0)%R). +apply round_le_generic... +apply generic_format_0... +now left. +case H4; try easy. +intros H5. +absurd (v=0)%R; try auto with real. +apply eq_0_round_0_negligible_exp with (Znearest choice)... +(* . *) +intros K1. +case (Rle_or_lt ((u + pred u) / 2) v); try easy. +intros H3. +absurd (u <= round beta fexp (Znearest choice) v)%R; try easy. +apply Rlt_not_le. +apply Rle_lt_trans with (2:=K1). +apply round_N_le_midp... +apply generic_format_pred... +rewrite succ_pred... +apply Rlt_le_trans with (1:=H3). +right; f_equal; ring. +Qed. + + +Lemma round_N_le_le_midp : forall choice u v, + F u -> + (round beta fexp (Znearest choice) v <= u)%R -> + (v <= (u + succ u) / 2)%R. +Proof with auto with typeclass_instances. +intros choice u v Hu H2. +apply Ropp_le_cancel. +apply Rle_trans with (((-u)+pred (-u))/2)%R. +rewrite pred_opp; right; field. +apply round_N_ge_ge_midp with + (choice := fun t:Z => negb (choice (- (t + 1))%Z))... +apply generic_format_opp... +rewrite <- (Ropp_involutive (round _ _ _ _)). +rewrite <- round_N_opp, Ropp_involutive. +apply Ropp_le_contravar; easy. +Qed. + Lemma round_N_eq_DN: forall choice x, let d:=round beta fexp Zfloor x in @@ -2518,4 +2644,18 @@ rewrite round_generic; [now apply succ_le_plus_ulp|now simpl|]. now apply generic_format_plus_ulp, generic_format_round. Qed. + +Lemma round_N_eq_ties: forall c1 c2 x, + (x - round beta fexp Zfloor x <> round beta fexp Zceil x - x)%R -> + (round beta fexp (Znearest c1) x = round beta fexp (Znearest c2) x)%R. +Proof with auto with typeclass_instances. +intros c1 c2 x. +pose (d:=round beta fexp Zfloor x); pose (u:=round beta fexp Zceil x); fold d; fold u; intros H. +case (Rle_or_lt ((d+u)/2) x); intros L. +2:rewrite 2!round_N_eq_DN... +destruct L as [L|L]. +rewrite 2!round_N_eq_UP... +contradict H; rewrite <- L; field. +Qed. + End Fcore_ulp. diff --git a/flocq/Core/Zaux.v b/flocq/Core/Zaux.v index e21d93a4..b40b0c4f 100644 --- a/flocq/Core/Zaux.v +++ b/flocq/Core/Zaux.v @@ -17,8 +17,12 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *) -Require Import ZArith Omega. -Require Import Zquot. +From Coq Require Import ZArith Lia Zquot. + +Require Import SpecFloatCompat. + +Notation cond_Zopp := cond_Zopp (only parsing). +Notation iter_pos := iter_pos (only parsing). Section Zmissing. @@ -262,7 +266,7 @@ apply Z.le_refl. split. easy. apply Zpower_gt_1. -clear -He ; omega. +clear -He ; lia. apply Zle_minus_le_0. now apply Zlt_le_weak. revert H1. @@ -282,7 +286,7 @@ apply Znot_gt_le. intros H. apply Zlt_not_le with (1 := He). apply Zpower_le. -clear -H ; omega. +clear -H ; lia. Qed. Theorem Zpower_gt_id : @@ -302,7 +306,7 @@ clear. apply Zlt_0_minus_lt. replace (r * (Z_of_nat n0 + 1) - (Z_of_nat n0 + 1))%Z with ((r - 1) * (Z_of_nat n0 + 1))%Z by ring. apply Zmult_lt_0_compat. -cut (2 <= r)%Z. omega. +cut (2 <= r)%Z. lia. apply Zle_bool_imp_le. apply r. apply (Zle_lt_succ 0). @@ -420,7 +424,7 @@ apply Z.opp_inj. rewrite <- Zquot_opp_l, Z.opp_0. apply Z.quot_small. generalize (Zabs_non_eq a). -omega. +lia. Qed. Theorem ZOmod_small_abs : @@ -437,7 +441,7 @@ apply Z.opp_inj. rewrite <- Zrem_opp_l. apply Z.rem_small. generalize (Zabs_non_eq a). -omega. +lia. Qed. Theorem ZOdiv_plus : @@ -702,8 +706,6 @@ End Zcompare. Section cond_Zopp. -Definition cond_Zopp (b : bool) m := if b then Z.opp m else m. - Theorem cond_Zopp_negb : forall x y, cond_Zopp (negb x) y = Z.opp (cond_Zopp x y). Proof. @@ -921,16 +923,9 @@ intros x. apply IHp. Qed. -Fixpoint iter_pos (n : positive) (x : A) {struct n} : A := - match n with - | xI n' => iter_pos n' (iter_pos n' (f x)) - | xO n' => iter_pos n' (iter_pos n' x) - | xH => f x - end. - Lemma iter_pos_nat : forall (p : positive) (x : A), - iter_pos p x = iter_nat (Pos.to_nat p) x. + iter_pos f p x = iter_nat (Pos.to_nat p) x. Proof. induction p ; intros x. rewrite Pos2Nat.inj_xI. -- cgit