From dce9ff8da2710aa81fbcf6d1498de35ea9ad06f4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 13 Feb 2017 10:28:35 +0100 Subject: Update Flocq to version 2.5.2 This version of Flocq is compatible with Coq 8.6 --- flocq/Appli/Fappli_IEEE.v | 7 +- flocq/Calc/Fcalc_round.v | 3 +- flocq/Core/Fcore_Raux.v | 2 +- flocq/Core/Fcore_digits.v | 3 +- flocq/Core/Fcore_generic_fmt.v | 187 ++++++++++++++++------------------------- flocq/Core/Fcore_rnd.v | 14 ++- flocq/Core/Fcore_ulp.v | 5 +- flocq/Flocq_version.v | 2 +- 8 files changed, 91 insertions(+), 132 deletions(-) (limited to 'flocq') diff --git a/flocq/Appli/Fappli_IEEE.v b/flocq/Appli/Fappli_IEEE.v index a4accfa5..6400304b 100644 --- a/flocq/Appli/Fappli_IEEE.v +++ b/flocq/Appli/Fappli_IEEE.v @@ -1,4 +1,3 @@ -Unset Bracketing Last Introduction Pattern. (** This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/ @@ -416,8 +415,7 @@ Theorem is_finite_Bopp : forall opp_nan x, is_finite (Bopp opp_nan x) = is_finite x. Proof. -intros opp_nan [| | |] ; try easy. -intros s pl. +intros opp_nan [| |s pl|] ; try easy. simpl. now case opp_nan. Qed. @@ -446,8 +444,7 @@ Theorem is_finite_Babs : forall abs_nan x, is_finite (Babs abs_nan x) = is_finite x. Proof. - intros abs_nan [| | |] ; try easy. - intros s pl. + intros abs_nan [| |s pl|] ; try easy. simpl. now case abs_nan. Qed. diff --git a/flocq/Calc/Fcalc_round.v b/flocq/Calc/Fcalc_round.v index 19652d08..86422247 100644 --- a/flocq/Calc/Fcalc_round.v +++ b/flocq/Calc/Fcalc_round.v @@ -646,8 +646,9 @@ case Zlt_bool_spec ; intros Hk. (* *) unfold truncate_aux. rewrite Fx at 1. -unshelve refine (let H := _ in conj _ H). +assert (H: (e + k)%Z = canonic_exp beta fexp x). unfold k. ring. +refine (conj _ H). rewrite <- H. apply F2R_eq_compat. replace (scaled_mantissa beta fexp x) with (Z2R (Zfloor (scaled_mantissa beta fexp x))). diff --git a/flocq/Core/Fcore_Raux.v b/flocq/Core/Fcore_Raux.v index d728e0ba..939002cf 100644 --- a/flocq/Core/Fcore_Raux.v +++ b/flocq/Core/Fcore_Raux.v @@ -1673,7 +1673,7 @@ Qed. (** Another well-used function for having the logarithm of a real number x to the base #β# *) Record ln_beta_prop x := { ln_beta_val :> Z ; - _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R + _ : (x <> 0)%R -> (bpow (ln_beta_val - 1)%Z <= Rabs x < bpow ln_beta_val)%R }. Definition ln_beta : diff --git a/flocq/Core/Fcore_digits.v b/flocq/Core/Fcore_digits.v index 7d1d490a..53743035 100644 --- a/flocq/Core/Fcore_digits.v +++ b/flocq/Core/Fcore_digits.v @@ -853,7 +853,8 @@ Proof. intros n Zn. rewrite <- (Zdigits_abs n). assert (Hn: (0 < Zabs n)%Z). -destruct n ; now easy. +destruct n ; [|easy|easy]. +now elim Zn. destruct (Zabs n) as [|p|p] ; try easy ; clear. simpl. generalize 1%Z (radix_val beta) (refl_equal Lt : (0 < 1)%Z). diff --git a/flocq/Core/Fcore_generic_fmt.v b/flocq/Core/Fcore_generic_fmt.v index bac65b9d..21e51890 100644 --- a/flocq/Core/Fcore_generic_fmt.v +++ b/flocq/Core/Fcore_generic_fmt.v @@ -136,9 +136,9 @@ Proof. intros e He. apply generic_format_bpow. destruct (Zle_lt_or_eq _ _ He). -now apply valid_exp. +now apply valid_exp_. rewrite <- H. -apply valid_exp_. +apply valid_exp. rewrite H. apply Zle_refl. Qed. @@ -604,107 +604,6 @@ Qed. Definition round x := F2R (Float beta (rnd (scaled_mantissa x)) (canonic_exp x)). -Theorem round_le_pos : - forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R. -Proof. -intros x y Hx Hxy. -unfold round, scaled_mantissa, canonic_exp. -destruct (ln_beta beta x) as (ex, Hex). simpl. -destruct (ln_beta beta y) as (ey, Hey). simpl. -specialize (Hex (Rgt_not_eq _ _ Hx)). -specialize (Hey (Rgt_not_eq _ _ (Rlt_le_trans _ _ _ Hx Hxy))). -rewrite Rabs_pos_eq in Hex. -2: now apply Rlt_le. -rewrite Rabs_pos_eq in Hey. -2: apply Rle_trans with (2:=Hxy); now apply Rlt_le. -assert (He: (ex <= ey)%Z). -cut (ex - 1 < ey)%Z. omega. -apply (lt_bpow beta). -apply Rle_lt_trans with (1 := proj1 Hex). -apply Rle_lt_trans with (1 := Hxy). -apply Hey. -destruct (Zle_or_lt ey (fexp ey)) as [Hy1|Hy1]. -rewrite (proj2 (proj2 (valid_exp ey) Hy1) ex). -apply F2R_le_compat. -apply Zrnd_le. -apply Rmult_le_compat_r. -apply bpow_ge_0. -exact Hxy. -now apply Zle_trans with ey. -destruct (Zle_lt_or_eq _ _ He) as [He'|He']. -destruct (Zle_or_lt ey (fexp ex)) as [Hx2|Hx2]. -rewrite (proj2 (proj2 (valid_exp ex) (Zle_trans _ _ _ He Hx2)) ey Hx2). -apply F2R_le_compat. -apply Zrnd_le. -apply Rmult_le_compat_r. -apply bpow_ge_0. -exact Hxy. -apply Rle_trans with (F2R (Float beta (rnd (bpow (ey - 1) * bpow (- fexp ey))) (fexp ey))). -rewrite <- bpow_plus. -rewrite <- (Z2R_Zpower beta (ey - 1 + -fexp ey)). 2: omega. -rewrite Zrnd_Z2R. -destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1]. -apply Rle_trans with (F2R (Float beta 1 (fexp ex))). -apply F2R_le_compat. -rewrite <- (Zrnd_Z2R 1). -apply Zrnd_le. -apply Rlt_le. -exact (proj2 (mantissa_small_pos _ _ Hex Hx1)). -unfold F2R. simpl. -rewrite Z2R_Zpower. 2: omega. -rewrite <- bpow_plus, Rmult_1_l. -apply bpow_le. -omega. -apply Rle_trans with (F2R (Float beta (rnd (bpow ex * bpow (- fexp ex))) (fexp ex))). -apply F2R_le_compat. -apply Zrnd_le. -apply Rmult_le_compat_r. -apply bpow_ge_0. -apply Rlt_le. -apply Hex. -rewrite <- bpow_plus. -rewrite <- Z2R_Zpower. 2: omega. -rewrite Zrnd_Z2R. -unfold F2R. simpl. -rewrite 2!Z2R_Zpower ; try omega. -rewrite <- 2!bpow_plus. -apply bpow_le. -omega. -apply F2R_le_compat. -apply Zrnd_le. -apply Rmult_le_compat_r. -apply bpow_ge_0. -apply Hey. -rewrite He'. -apply F2R_le_compat. -apply Zrnd_le. -apply Rmult_le_compat_r. -apply bpow_ge_0. -exact Hxy. -Qed. - -Theorem round_generic : - forall x, - generic_format x -> - round x = x. -Proof. -intros x Hx. -unfold round. -rewrite scaled_mantissa_generic with (1 := Hx). -rewrite Zrnd_Z2R. -now apply sym_eq. -Qed. - -Theorem round_0 : - round 0 = R0. -Proof. -unfold round, scaled_mantissa. -rewrite Rmult_0_l. -fold (Z2R 0). -rewrite Zrnd_Z2R. -apply F2R_0. -Qed. - Theorem round_bounded_large_pos : forall x ex, (fexp ex < ex)%Z -> @@ -792,6 +691,74 @@ refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))). now apply mantissa_small_pos. Qed. +Theorem round_le_pos : + forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R. +Proof. +intros x y Hx Hxy. +destruct (ln_beta beta x) as [ex Hex]. +destruct (ln_beta beta y) as [ey Hey]. +specialize (Hex (Rgt_not_eq _ _ Hx)). +specialize (Hey (Rgt_not_eq _ _ (Rlt_le_trans _ _ _ Hx Hxy))). +rewrite Rabs_pos_eq in Hex. +2: now apply Rlt_le. +rewrite Rabs_pos_eq in Hey. +2: apply Rle_trans with (2:=Hxy); now apply Rlt_le. +assert (He: (ex <= ey)%Z). + apply bpow_lt_bpow with beta. + apply Rle_lt_trans with (1 := proj1 Hex). + now apply Rle_lt_trans with y. +assert (Heq: fexp ex = fexp ey -> (round x <= round y)%R). + intros H. + unfold round, scaled_mantissa, canonic_exp. + rewrite ln_beta_unique_pos with (1 := Hex). + rewrite ln_beta_unique_pos with (1 := Hey). + rewrite H. + apply F2R_le_compat. + apply Zrnd_le. + apply Rmult_le_compat_r with (2 := Hxy). + apply bpow_ge_0. +destruct (Zle_or_lt ey (fexp ey)) as [Hy1|Hy1]. + apply Heq. + apply valid_exp with (1 := Hy1). + now apply Zle_trans with ey. +destruct (Zle_lt_or_eq _ _ He) as [He'|He']. +2: now apply Heq, f_equal. +apply Rle_trans with (bpow (ey - 1)). +2: now apply round_bounded_large_pos. +destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1]. + destruct (round_bounded_small_pos _ _ Hx1 Hex) as [-> | ->]. + apply bpow_ge_0. + apply bpow_le. + apply valid_exp, proj2 in Hx1. + specialize (Hx1 ey). + omega. +apply Rle_trans with (bpow ex). +now apply round_bounded_large_pos. +apply bpow_le. +now apply Z.lt_le_pred. +Qed. + +Theorem round_generic : + forall x, + generic_format x -> + round x = x. +Proof. +intros x Hx. +unfold round. +rewrite scaled_mantissa_generic with (1 := Hx). +rewrite Zrnd_Z2R. +now apply sym_eq. +Qed. + +Theorem round_0 : + round 0 = R0. +Proof. +unfold round, scaled_mantissa. +rewrite Rmult_0_l. +fold (Z2R 0). +rewrite Zrnd_Z2R. +apply F2R_0. +Qed. Theorem exp_small_round_0_pos : forall x ex, @@ -807,9 +774,6 @@ apply bpow_gt_0. apply (round_bounded_large_pos); assumption. Qed. - - - Theorem generic_format_round_pos : forall x, (0 < x)%R -> @@ -832,14 +796,11 @@ destruct (Rle_or_lt (bpow ex) (round x)) as [Hr|Hr]. rewrite <- (Rle_antisym _ _ Hr Hr2). apply generic_format_bpow. now apply valid_exp. -assert (Hr' := conj Hr1 Hr). -unfold generic_format, scaled_mantissa. -rewrite (canonic_exp_fexp_pos _ _ Hr'). -unfold round, scaled_mantissa. +apply generic_format_F2R. +intros _. +rewrite (canonic_exp_fexp_pos (F2R _) _ (conj Hr1 Hr)). rewrite (canonic_exp_fexp_pos _ _ Hex). -unfold F2R at 3. simpl. -rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r. -now rewrite Ztrunc_Z2R. +now apply Zeq_le. Qed. End Fcore_generic_round_pos. diff --git a/flocq/Core/Fcore_rnd.v b/flocq/Core/Fcore_rnd.v index 171c27fc..e5091684 100644 --- a/flocq/Core/Fcore_rnd.v +++ b/flocq/Core/Fcore_rnd.v @@ -275,15 +275,13 @@ Theorem Only_DN_or_UP : F f -> (fd <= f <= fu)%R -> f = fd \/ f = fu. Proof. -intros F x fd fu f Hd Hu Hf ([Hdf|Hdf], Hfu). -2 : now left. -destruct Hfu. -2 : now right. -destruct (Rle_or_lt x f). -elim Rlt_not_le with (1 := H). +intros F x fd fu f Hd Hu Hf [Hdf Hfu]. +destruct (Rle_or_lt x f) ; [right|left]. +apply Rle_antisym with (1 := Hfu). now apply Hu. -elim Rlt_not_le with (1 := Hdf). -apply Hd ; auto with real. +apply Rlt_le in H. +apply Rle_antisym with (2 := Hdf). +now apply Hd. Qed. Theorem Rnd_ZR_abs : diff --git a/flocq/Core/Fcore_ulp.v b/flocq/Core/Fcore_ulp.v index 1c27de31..28d2bc35 100644 --- a/flocq/Core/Fcore_ulp.v +++ b/flocq/Core/Fcore_ulp.v @@ -35,6 +35,7 @@ Variable fexp : Z -> Z. (** Definition and basic properties about the minimal exponent, when it exists *) Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z. +Proof. intros. destruct (Z_le_dec x y). now left. @@ -158,8 +159,7 @@ rewrite ulp_neq_0. unfold F2R; simpl. apply Rmult_le_compat_r. apply bpow_ge_0. -replace 1%R with (Z2R (Zsucc 0)) by reflexivity. -apply Z2R_le. +apply (Z2R_le (Zsucc 0)). apply Zlt_le_succ. apply F2R_gt_0_reg with beta (canonic_exp beta fexp x). now rewrite <- Fx. @@ -206,6 +206,7 @@ Qed. Theorem ulp_bpow : forall e, ulp (bpow e) = bpow (fexp (e + 1)). +Proof. intros e. rewrite ulp_neq_0. apply f_equal. diff --git a/flocq/Flocq_version.v b/flocq/Flocq_version.v index c391f590..b01a08f9 100644 --- a/flocq/Flocq_version.v +++ b/flocq/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 "2.5.0"%string N0 N0. + parse "2.5.2"%string N0 N0. -- cgit