From 0f919eb26c68d3882e612a1b3a9df45bee6d3624 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 13 Feb 2019 18:53:17 +0100 Subject: Upgrade embedded version of Flocq to 3.1. Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully). --- flocq/Prop/Fprop_plus_error.v | 538 ------------------------------------------ 1 file changed, 538 deletions(-) delete mode 100644 flocq/Prop/Fprop_plus_error.v (limited to 'flocq/Prop/Fprop_plus_error.v') diff --git a/flocq/Prop/Fprop_plus_error.v b/flocq/Prop/Fprop_plus_error.v deleted file mode 100644 index 9bb5aee8..00000000 --- a/flocq/Prop/Fprop_plus_error.v +++ /dev/null @@ -1,538 +0,0 @@ -(** -This file is part of the Flocq formalization of floating-point -arithmetic in Coq: http://flocq.gforge.inria.fr/ - -Copyright (C) 2010-2013 Sylvie Boldo -#
# -Copyright (C) 2010-2013 Guillaume Melquiond - -This library is free software; you can redistribute it and/or -modify it under the terms of the GNU Lesser General Public -License as published by the Free Software Foundation; either -version 3 of the License, or (at your option) any later version. - -This library is distributed in the hope that it will be useful, -but WITHOUT ANY WARRANTY; without even the implied warranty of -MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -COPYING file for more details. -*) - -(** * Error of the rounded-to-nearest addition is representable. *) - -Require Import Psatz. -Require Import Fcore_Raux. -Require Import Fcore_defs. -Require Import Fcore_float_prop. -Require Import Fcore_generic_fmt. -Require Import Fcore_FIX. -Require Import Fcore_FLX. -Require Import Fcore_FLT. -Require Import Fcore_ulp. -Require Import Fcalc_ops. - - -Section Fprop_plus_error. - -Variable beta : radix. -Notation bpow e := (bpow beta e). - -Variable fexp : Z -> Z. -Context { valid_exp : Valid_exp fexp }. - -Section round_repr_same_exp. - -Variable rnd : R -> Z. -Context { valid_rnd : Valid_rnd rnd }. - -Theorem round_repr_same_exp : - forall m e, - exists m', - round beta fexp rnd (F2R (Float beta m e)) = F2R (Float beta m' e). -Proof with auto with typeclass_instances. -intros m e. -set (e' := canonic_exp beta fexp (F2R (Float beta m e))). -unfold round, scaled_mantissa. fold e'. -destruct (Zle_or_lt e' e) as [He|He]. -exists m. -unfold F2R at 2. simpl. -rewrite Rmult_assoc, <- bpow_plus. -rewrite <- Z2R_Zpower. 2: omega. -rewrite <- Z2R_mult, Zrnd_Z2R... -unfold F2R. simpl. -rewrite Z2R_mult. -rewrite Rmult_assoc. -rewrite Z2R_Zpower. 2: omega. -rewrite <- bpow_plus. -apply (f_equal (fun v => Z2R m * bpow v)%R). -ring. -exists ((rnd (Z2R m * bpow (e - e'))) * Zpower beta (e' - e))%Z. -unfold F2R. simpl. -rewrite Z2R_mult. -rewrite Z2R_Zpower. 2: omega. -rewrite 2!Rmult_assoc. -rewrite <- 2!bpow_plus. -apply (f_equal (fun v => _ * bpow v)%R). -ring. -Qed. - -End round_repr_same_exp. - -Context { monotone_exp : Monotone_exp fexp }. -Notation format := (generic_format beta fexp). - -Variable choice : Z -> bool. - -Lemma plus_error_aux : - forall x y, - (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z -> - format x -> format y -> - format (round beta fexp (Znearest choice) (x + y) - (x + y))%R. -Proof. -intros x y. -set (ex := canonic_exp beta fexp x). -set (ey := canonic_exp beta fexp y). -intros He Hx Hy. -destruct (Req_dec (round beta fexp (Znearest choice) (x + y) - (x + y)) R0) as [H0|H0]. -rewrite H0. -apply generic_format_0. -set (mx := Ztrunc (scaled_mantissa beta fexp x)). -set (my := Ztrunc (scaled_mantissa beta fexp y)). -(* *) -assert (Hxy: (x + y)%R = F2R (Float beta (mx + my * beta ^ (ey - ex)) ex)). -rewrite Hx, Hy. -fold mx my ex ey. -rewrite <- F2R_plus. -unfold Fplus. simpl. -now rewrite Zle_imp_le_bool with (1 := He). -(* *) -rewrite Hxy. -destruct (round_repr_same_exp (Znearest choice) (mx + my * beta ^ (ey - ex)) ex) as (mxy, Hxy'). -rewrite Hxy'. -assert (H: (F2R (Float beta mxy ex) - F2R (Float beta (mx + my * beta ^ (ey - ex)) ex))%R = - F2R (Float beta (mxy - (mx + my * beta ^ (ey - ex))) ex)). -now rewrite <- F2R_minus, Fminus_same_exp. -rewrite H. -apply generic_format_F2R. -intros _. -apply monotone_exp. -rewrite <- H, <- Hxy', <- Hxy. -apply ln_beta_le_abs. -exact H0. -pattern x at 3 ; replace x with (-(y - (x + y)))%R by ring. -rewrite Rabs_Ropp. -now apply (round_N_pt beta _ choice (x + y)). -Qed. - -(** Error of the addition *) -Theorem plus_error : - forall x y, - format x -> format y -> - format (round beta fexp (Znearest choice) (x + y) - (x + y))%R. -Proof. -intros x y Hx Hy. -destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)). -now apply plus_error_aux. -rewrite Rplus_comm. -apply plus_error_aux ; try easy. -now apply Zlt_le_weak. -Qed. - -End Fprop_plus_error. - -Section Fprop_plus_zero. - -Variable beta : radix. -Notation bpow e := (bpow beta e). - -Variable fexp : Z -> Z. -Context { valid_exp : Valid_exp fexp }. -Context { exp_not_FTZ : Exp_not_FTZ fexp }. -Notation format := (generic_format beta fexp). - -Section round_plus_eq_zero_aux. - -Variable rnd : R -> Z. -Context { valid_rnd : Valid_rnd rnd }. - -Lemma round_plus_eq_zero_aux : - forall x y, - (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z -> - format x -> format y -> - (0 <= x + y)%R -> - round beta fexp rnd (x + y) = 0%R -> - (x + y = 0)%R. -Proof with auto with typeclass_instances. -intros x y He Hx Hy Hp Hxy. -destruct (Req_dec (x + y) 0) as [H0|H0]. -exact H0. -destruct (ln_beta beta (x + y)) as (exy, Hexy). -simpl. -specialize (Hexy H0). -destruct (Zle_or_lt exy (fexp exy)) as [He'|He']. -(* . *) -assert (H: (x + y)%R = F2R (Float beta (Ztrunc (x * bpow (- fexp exy)) + - Ztrunc (y * bpow (- fexp exy))) (fexp exy))). -rewrite (subnormal_exponent beta fexp exy x He' Hx) at 1. -rewrite (subnormal_exponent beta fexp exy y He' Hy) at 1. -now rewrite <- F2R_plus, Fplus_same_exp. -rewrite H in Hxy. -rewrite round_generic in Hxy... -now rewrite <- H in Hxy. -apply generic_format_F2R. -intros _. -rewrite <- H. -unfold canonic_exp. -rewrite ln_beta_unique with (1 := Hexy). -apply Zle_refl. -(* . *) -elim Rle_not_lt with (1 := round_le beta _ rnd _ _ (proj1 Hexy)). -rewrite (Rabs_pos_eq _ Hp). -rewrite Hxy. -rewrite round_generic... -apply bpow_gt_0. -apply generic_format_bpow. -apply Zlt_succ_le. -now rewrite (Zsucc_pred exy) in He'. -Qed. - -End round_plus_eq_zero_aux. - -Variable rnd : R -> Z. -Context { valid_rnd : Valid_rnd rnd }. - -(** rnd(x+y)=0 -> x+y = 0 provided this is not a FTZ format *) -Theorem round_plus_eq_zero : - forall x y, - format x -> format y -> - round beta fexp rnd (x + y) = 0%R -> - (x + y = 0)%R. -Proof with auto with typeclass_instances. -intros x y Hx Hy. -destruct (Rle_or_lt 0 (x + y)) as [H1|H1]. -(* . *) -revert H1. -destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)) as [H2|H2]. -now apply round_plus_eq_zero_aux. -rewrite Rplus_comm. -apply round_plus_eq_zero_aux ; try easy. -now apply Zlt_le_weak. -(* . *) -revert H1. -rewrite <- (Ropp_involutive (x + y)), Ropp_plus_distr, <- Ropp_0. -intros H1. -rewrite round_opp. -intros Hxy. -apply f_equal. -cut (round beta fexp (Zrnd_opp rnd) (- x + - y) = 0)%R. -cut (0 <= -x + -y)%R. -destruct (Zle_or_lt (canonic_exp beta fexp (-x)) (canonic_exp beta fexp (-y))) as [H2|H2]. -apply round_plus_eq_zero_aux ; try apply generic_format_opp... -rewrite Rplus_comm. -apply round_plus_eq_zero_aux ; try apply generic_format_opp... -now apply Zlt_le_weak. -apply Rlt_le. -now apply Ropp_lt_cancel. -rewrite <- (Ropp_involutive (round _ _ _ _)). -rewrite Hxy. -apply Ropp_involutive. -Qed. - -End Fprop_plus_zero. - -Section Fprop_plus_FLT. -Variable beta : radix. - -Notation bpow e := (bpow beta e). - -Variable emin prec : Z. -Context { prec_gt_0_ : Prec_gt_0 prec }. - -Theorem FLT_format_plus_small: forall x y, - generic_format beta (FLT_exp emin prec) x -> - generic_format beta (FLT_exp emin prec) y -> - (Rabs (x+y) <= bpow (prec+emin))%R -> - generic_format beta (FLT_exp emin prec) (x+y). -Proof with auto with typeclass_instances. -intros x y Fx Fy H. -apply generic_format_FLT_FIX... -rewrite Zplus_comm; assumption. -apply generic_format_FIX_FLT, FIX_format_generic in Fx. -apply generic_format_FIX_FLT, FIX_format_generic in Fy. -destruct Fx as (nx,(H1x,H2x)). -destruct Fy as (ny,(H1y,H2y)). -apply generic_format_FIX. -exists (Float beta (Fnum nx+Fnum ny)%Z emin). -split;[idtac|reflexivity]. -rewrite H1x,H1y; unfold F2R; simpl. -rewrite H2x, H2y. -rewrite Z2R_plus; ring. -Qed. - -End Fprop_plus_FLT. - -Section Fprop_plus_mult_ulp. - -Variable beta : radix. -Notation bpow e := (bpow beta e). - -Variable fexp : Z -> Z. -Context { valid_exp : Valid_exp fexp }. -Context { monotone_exp : Monotone_exp fexp }. -Variable rnd : R -> Z. -Context { valid_rnd : Valid_rnd rnd }. - -Notation format := (generic_format beta fexp). -Notation cexp := (canonic_exp beta fexp). - -Lemma ex_shift : - forall x e, format x -> (e <= cexp x)%Z -> - exists m, (x = Z2R m * bpow e)%R. -Proof with auto with typeclass_instances. -intros x e Fx He. -exists (Ztrunc (scaled_mantissa beta fexp x)*Zpower beta (cexp x -e))%Z. -rewrite Fx at 1; unfold F2R; simpl. -rewrite Z2R_mult, Rmult_assoc. -f_equal. -rewrite Z2R_Zpower. -2: omega. -rewrite <- bpow_plus; f_equal; ring. -Qed. - -Lemma ln_beta_minus1 : - forall z, z <> 0%R -> - (ln_beta beta z - 1)%Z = ln_beta beta (z / Z2R beta). -Proof. -intros z Hz. -unfold Zminus. -rewrite <- ln_beta_mult_bpow with (1 := Hz). -now rewrite bpow_opp, bpow_1. -Qed. - -Theorem round_plus_mult_ulp : - forall x y, format x -> format y -> (x <> 0)%R -> - exists m, (round beta fexp rnd (x+y) = Z2R m * ulp beta fexp (x/Z2R beta))%R. -Proof with auto with typeclass_instances. -intros x y Fx Fy Zx. -case (Zle_or_lt (ln_beta beta (x/Z2R beta)) (ln_beta beta y)); intros H1. -pose (e:=cexp (x / Z2R beta)). -destruct (ex_shift x e) as (nx, Hnx); try exact Fx. -apply monotone_exp. -rewrite <- (ln_beta_minus1 x Zx); omega. -destruct (ex_shift y e) as (ny, Hny); try assumption. -apply monotone_exp... -destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn). -exists n. -apply trans_eq with (F2R (Float beta n e)). -rewrite <- Hn; f_equal. -rewrite Hnx, Hny; unfold F2R; simpl; rewrite Z2R_plus; ring. -unfold F2R; simpl. -rewrite ulp_neq_0; try easy. -apply Rmult_integral_contrapositive_currified; try assumption. -apply Rinv_neq_0_compat. -apply Rgt_not_eq. -apply radix_pos. -(* *) -destruct (ex_shift (round beta fexp rnd (x + y)) (cexp (x/Z2R beta))) as (n,Hn). -apply generic_format_round... -apply Zle_trans with (cexp (x+y)). -apply monotone_exp. -rewrite <- ln_beta_minus1 by easy. -rewrite <- (ln_beta_abs beta (x+y)). -(* . *) -assert (U: (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R). -assert (V: forall x y, (Rabs y <= Rabs x)%R -> - (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y) = Rabs x - Rabs y)%R). -clear; intros x y. -case (Rle_or_lt 0 y); intros Hy. -case Hy; intros Hy'. -case (Rle_or_lt 0 x); intros Hx. -intros _; rewrite (Rabs_pos_eq y) by easy. -rewrite (Rabs_pos_eq x) by easy. -left; apply Rabs_pos_eq. -now apply Rplus_le_le_0_compat. -rewrite (Rabs_pos_eq y) by easy. -rewrite (Rabs_left x) by easy. -intros H; right; split. -now apply Rgt_not_eq. -rewrite Rabs_left1. -ring. -apply Rplus_le_reg_l with (-x)%R; ring_simplify; assumption. -intros _; left. -now rewrite <- Hy', Rabs_R0, 2!Rplus_0_r. -case (Rle_or_lt 0 x); intros Hx. -rewrite (Rabs_left y) by easy. -rewrite (Rabs_pos_eq x) by easy. -intros H; right; split. -now apply Rlt_not_eq. -rewrite Rabs_pos_eq. -ring. -apply Rplus_le_reg_l with (-y)%R; ring_simplify; assumption. -intros _; left. -rewrite (Rabs_left y) by easy. -rewrite (Rabs_left x) by easy. -rewrite Rabs_left1. -ring. -lra. -apply V; left. -apply ln_beta_lt_pos with beta. -now apply Rabs_pos_lt. -rewrite <- ln_beta_minus1 in H1; try assumption. -rewrite 2!ln_beta_abs; omega. -(* . *) -destruct U as [U|U]. -rewrite U; apply Zle_trans with (ln_beta beta x). -omega. -rewrite <- ln_beta_abs. -apply ln_beta_le. -now apply Rabs_pos_lt. -apply Rplus_le_reg_l with (-Rabs x)%R; ring_simplify. -apply Rabs_pos. -destruct U as (U',U); rewrite U. -rewrite <- ln_beta_abs. -apply ln_beta_minus_lb. -now apply Rabs_pos_lt. -now apply Rabs_pos_lt. -rewrite 2!ln_beta_abs. -assert (ln_beta beta y < ln_beta beta x - 1)%Z. -now rewrite (ln_beta_minus1 x Zx). -omega. -apply canonic_exp_round_ge... -intros K. -apply round_plus_eq_zero in K... -contradict H1; apply Zle_not_lt. -rewrite <- (ln_beta_minus1 x Zx). -replace y with (-x)%R. -rewrite ln_beta_opp; omega. -lra. -exists n. -rewrite ulp_neq_0. -assumption. -apply Rmult_integral_contrapositive_currified; try assumption. -apply Rinv_neq_0_compat. -apply Rgt_not_eq. -apply radix_pos. -Qed. - -Context {exp_not_FTZ : Exp_not_FTZ fexp}. - -Theorem round_plus_ge_ulp : - forall x y, format x -> format y -> - round beta fexp rnd (x+y) = 0%R \/ - (ulp beta fexp (x/Z2R beta) <= Rabs (round beta fexp rnd (x+y)))%R. -Proof with auto with typeclass_instances. -intros x y Fx Fy. -case (Req_dec x 0); intros Zx. -(* *) -rewrite Zx, Rplus_0_l. -rewrite round_generic... -unfold Rdiv; rewrite Rmult_0_l. -rewrite Fy at 2. -unfold F2R; simpl; rewrite Rabs_mult. -rewrite (Rabs_pos_eq (bpow _)) by apply bpow_ge_0. -case (Z.eq_dec (Ztrunc (scaled_mantissa beta fexp y)) 0); intros Hm. -left. -rewrite Fy, Hm; unfold F2R; simpl; ring. -right. -apply Rle_trans with (1*bpow (cexp y))%R. -rewrite Rmult_1_l. -rewrite <- ulp_neq_0. -apply ulp_ge_ulp_0... -intros K; apply Hm. -rewrite K, scaled_mantissa_0. -apply (Ztrunc_Z2R 0). -apply Rmult_le_compat_r. -apply bpow_ge_0. -rewrite <- Z2R_abs. -apply (Z2R_le 1). -apply (Zlt_le_succ 0). -now apply Z.abs_pos. -(* *) -destruct (round_plus_mult_ulp x y Fx Fy Zx) as (m,Hm). -case (Z.eq_dec m 0); intros Zm. -left. -rewrite Hm, Zm; simpl; ring. -right. -rewrite Hm, Rabs_mult. -rewrite (Rabs_pos_eq (ulp _ _ _)) by apply ulp_ge_0. -apply Rle_trans with (1*ulp beta fexp (x/Z2R beta))%R. -right; ring. -apply Rmult_le_compat_r. -apply ulp_ge_0. -rewrite <- Z2R_abs. -apply (Z2R_le 1). -apply (Zlt_le_succ 0). -now apply Z.abs_pos. -Qed. - -End Fprop_plus_mult_ulp. - -Section Fprop_plus_ge_ulp. - -Variable beta : radix. -Notation bpow e := (bpow beta e). - -Variable rnd : R -> Z. -Context { valid_rnd : Valid_rnd rnd }. -Variable emin prec : Z. -Context { prec_gt_0_ : Prec_gt_0 prec }. - -Theorem round_plus_ge_ulp_FLT : forall x y e, - generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y -> - (bpow e <= Rabs x)%R -> - round beta (FLT_exp emin prec) rnd (x+y) = 0%R \/ - (bpow (e - prec) <= Rabs (round beta (FLT_exp emin prec) rnd (x+y)))%R. -Proof with auto with typeclass_instances. -intros x y e Fx Fy He. -assert (Zx: x <> 0%R). - contradict He. - apply Rlt_not_le; rewrite He, Rabs_R0. - apply bpow_gt_0. -case round_plus_ge_ulp with beta (FLT_exp emin prec) rnd x y... -intros H; right. -apply Rle_trans with (2:=H). -rewrite ulp_neq_0. -unfold canonic_exp. -rewrite <- ln_beta_minus1 by easy. -unfold FLT_exp; apply bpow_le. -apply Zle_trans with (2:=Z.le_max_l _ _). -destruct (ln_beta beta x) as (n,Hn); simpl. -assert (e < n)%Z; try omega. -apply lt_bpow with beta. -apply Rle_lt_trans with (1:=He). -now apply Hn. -apply Rmult_integral_contrapositive_currified; try assumption. -apply Rinv_neq_0_compat. -apply Rgt_not_eq. -apply radix_pos. -Qed. - -Theorem round_plus_ge_ulp_FLX : forall x y e, - generic_format beta (FLX_exp prec) x -> generic_format beta (FLX_exp prec) y -> - (bpow e <= Rabs x)%R -> - round beta (FLX_exp prec) rnd (x+y) = 0%R \/ - (bpow (e - prec) <= Rabs (round beta (FLX_exp prec) rnd (x+y)))%R. -Proof with auto with typeclass_instances. -intros x y e Fx Fy He. -assert (Zx: x <> 0%R). - contradict He. - apply Rlt_not_le; rewrite He, Rabs_R0. - apply bpow_gt_0. -case round_plus_ge_ulp with beta (FLX_exp prec) rnd x y... -intros H; right. -apply Rle_trans with (2:=H). -rewrite ulp_neq_0. -unfold canonic_exp. -rewrite <- ln_beta_minus1 by easy. -unfold FLX_exp; apply bpow_le. -destruct (ln_beta beta x) as (n,Hn); simpl. -assert (e < n)%Z; try omega. -apply lt_bpow with beta. -apply Rle_lt_trans with (1:=He). -now apply Hn. -apply Rmult_integral_contrapositive_currified; try assumption. -apply Rinv_neq_0_compat. -apply Rgt_not_eq. -apply radix_pos. -Qed. - -End Fprop_plus_ge_ulp. -- cgit