Commit 4aa79696 by Guillaume Melquiond

### Changed some theorem names.

parent 81b2a74c
 ... @@ -15,17 +15,17 @@ Notation cexp := (canonic_exponent beta (FLX_exp prec)). ... @@ -15,17 +15,17 @@ Notation cexp := (canonic_exponent beta (FLX_exp prec)). Notation ulp := (ulp beta (FLX_exp prec)). Notation ulp := (ulp beta (FLX_exp prec)). Definition MinOrMax x f := Definition MinOrMax x f := ((f = rounding beta (FLX_exp prec) ZrndDN x) ((f = round beta (FLX_exp prec) rndDN x) \/ (f = rounding beta (FLX_exp prec) ZrndUP x)). \/ (f = round beta (FLX_exp prec) rndUP x)). Theorem MinOrMax_opp: forall x f, Theorem MinOrMax_opp: forall x f, MinOrMax x f <-> MinOrMax (-x) (-f). MinOrMax x f <-> MinOrMax (-x) (-f). assert (forall x f, MinOrMax x f -> MinOrMax (- x) (- f)). assert (forall x f, MinOrMax x f -> MinOrMax (- x) (- f)). unfold MinOrMax; intros x f [H|H]. unfold MinOrMax; intros x f [H|H]. right. right. now rewrite H, rounding_UP_opp. now rewrite H, round_UP_opp. left. left. now rewrite H, rounding_DN_opp. now rewrite H, round_DN_opp. intros x f; split; intros H1. intros x f; split; intros H1. now apply H. now apply H. rewrite <- (Ropp_involutive x), <- (Ropp_involutive f). rewrite <- (Ropp_involutive x), <- (Ropp_involutive f). ... @@ -37,11 +37,11 @@ Theorem implies_DN_lt_ulp: ... @@ -37,11 +37,11 @@ Theorem implies_DN_lt_ulp: forall x f, format f -> forall x f, format f -> (0 < f <= x)%R -> (0 < f <= x)%R -> (Rabs (f-x) < ulp f)%R -> (Rabs (f-x) < ulp f)%R -> (f = rounding beta (FLX_exp prec) ZrndDN x)%R. (f = round beta (FLX_exp prec) rndDN x)%R. intros x f Hf Hxf1 Hxf2. intros x f Hf Hxf1 Hxf2. apply sym_eq. apply sym_eq. replace x with (f+-(f-x))%R by ring. replace x with (f+-(f-x))%R by ring. apply rounding_DN_succ; trivial. apply round_DN_succ; trivial. apply Hxf1. apply Hxf1. replace (- (f - x))%R with (Rabs (f-x)). replace (- (f - x))%R with (Rabs (f-x)). split; trivial; apply Rabs_pos. split; trivial; apply Rabs_pos. ... @@ -66,7 +66,7 @@ right; apply sym_eq. ... @@ -66,7 +66,7 @@ right; apply sym_eq. replace f with ((f-ulp f) + (ulp (f-ulp f)))%R. replace f with ((f-ulp f) + (ulp (f-ulp f)))%R. 2: rewrite H; ring. 2: rewrite H; ring. replace x with ((f-ulp f)+-(f-ulp f-x))%R by ring. replace x with ((f-ulp f)+-(f-ulp f-x))%R by ring. apply rounding_UP_succ; trivial. apply round_UP_succ; trivial. apply Hxf1. apply Hxf1. replace (- (f - x))%R with (Rabs (f-x)). replace (- (f - x))%R with (Rabs (f-x)). ... @@ -104,8 +104,8 @@ Hypothesis Ha: format a. ... @@ -104,8 +104,8 @@ Hypothesis Ha: format a. Hypothesis Hx: format x. Hypothesis Hx: format x. Hypothesis Hy: format y. Hypothesis Hy: format y. Notation t := (rounding beta (FLX_exp prec) (ZrndN choice) (a*x)). Notation t := (round beta (FLX_exp prec) (rndN choice) (a*x)). Notation u := (rounding beta (FLX_exp prec) (ZrndN choice) (t+y)). Notation u := (round beta (FLX_exp prec) (rndN choice) (t+y)). ... ...
 ... @@ -161,7 +161,7 @@ apply Rcompare_not_Lt_inv. ... @@ -161,7 +161,7 @@ apply Rcompare_not_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. apply Rcompare_not_Lt. apply Rcompare_not_Lt. change 2%R with (Z2R 2). change 2%R with (Z2R 2). rewrite <- mult_Z2R. rewrite <- Z2R_mult. apply Z2R_le. apply Z2R_le. omega. omega. exact Hstep. exact Hstep. ... @@ -183,7 +183,7 @@ apply Rcompare_Lt_inv. ... @@ -183,7 +183,7 @@ apply Rcompare_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l. apply Rcompare_Lt. apply Rcompare_Lt. change 2%R with (Z2R 2). change 2%R with (Z2R 2). rewrite <- mult_Z2R. rewrite <- Z2R_mult. apply Z2R_lt. apply Z2R_lt. omega. omega. exact Hstep. exact Hstep. ... @@ -228,7 +228,7 @@ Lemma middle_odd : ... @@ -228,7 +228,7 @@ Lemma middle_odd : Proof. Proof. intros k Hk. intros k Hk. rewrite <- Hk. rewrite <- Hk. rewrite 2!plus_Z2R, mult_Z2R. rewrite 2!Z2R_plus, Z2R_mult. simpl. field. simpl. field. Qed. Qed. ... @@ -259,7 +259,7 @@ rewrite Hl. ... @@ -259,7 +259,7 @@ rewrite Hl. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. apply Rcompare_Lt. apply Rcompare_Lt. change 2%R with (Z2R 2). change 2%R with (Z2R 2). rewrite <- mult_Z2R. rewrite <- Z2R_mult. apply Z2R_lt. apply Z2R_lt. rewrite <- Hk. rewrite <- Hk. apply Zlt_succ. apply Zlt_succ. ... @@ -282,7 +282,7 @@ apply Rle_lt_trans with (2 := proj1 Hx'). ... @@ -282,7 +282,7 @@ apply Rle_lt_trans with (2 := proj1 Hx'). apply Rcompare_not_Lt_inv. apply Rcompare_not_Lt_inv. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r. change 2%R with (Z2R 2). change 2%R with (Z2R 2). rewrite <- mult_Z2R. rewrite <- Z2R_mult. apply Rcompare_not_Lt. apply Rcompare_not_Lt. apply Z2R_le. apply Z2R_le. rewrite Hk. rewrite Hk. ... @@ -301,7 +301,7 @@ apply inbetween_step_not_Eq with (1 := Hx). ... @@ -301,7 +301,7 @@ apply inbetween_step_not_Eq with (1 := Hx). omega. omega. apply Rcompare_Eq. apply Rcompare_Eq. inversion_clear Hx as [Hx'|]. inversion_clear Hx as [Hx'|]. rewrite Hx', <- Hk, mult_Z2R. rewrite Hx', <- Hk, Z2R_mult. simpl (Z2R 2). simpl (Z2R 2). field. field. Qed. Qed. ... @@ -524,12 +524,12 @@ now apply Zpower_gt_0. ... @@ -524,12 +524,12 @@ now apply Zpower_gt_0. rewrite 2!Hr. rewrite 2!Hr. rewrite Zmult_plus_distr_l, Zmult_1_l. rewrite Zmult_plus_distr_l, Zmult_1_l. unfold F2R at 2. simpl. unfold F2R at 2. simpl. rewrite plus_Z2R, Rmult_plus_distr_r. rewrite Z2R_plus, Rmult_plus_distr_r. apply new_location_correct. apply new_location_correct. apply bpow_gt_0. apply bpow_gt_0. now apply Zpower_gt_1. now apply Zpower_gt_1. now apply Z_mod_lt. now apply Z_mod_lt. rewrite <- 2!Rmult_plus_distr_r, <- 2!plus_Z2R. rewrite <- 2!Rmult_plus_distr_r, <- 2!Z2R_plus. rewrite Zmult_comm, Zplus_assoc. rewrite Zmult_comm, Zplus_assoc. now rewrite <- Z_div_mod_eq. now rewrite <- Z_div_mod_eq. Qed. Qed. ... @@ -545,16 +545,16 @@ now apply inbetween_float_new_location. ... @@ -545,16 +545,16 @@ now apply inbetween_float_new_location. apply Zmult_1_r. apply Zmult_1_r. Qed. Qed. Theorem inbetween_float_rounding : Theorem inbetween_float_round : forall rnd choice, forall rnd choice, ( forall x m l, inbetween_int m x l -> Zrnd rnd x = choice m l ) -> ( forall x m l, inbetween_int m x l -> Zrnd rnd x = choice m l ) -> forall x m l, forall x m l, let e := canonic_exponent beta fexp x in let e := canonic_exponent beta fexp x in inbetween_float m e x l -> inbetween_float m e x l -> rounding beta fexp rnd x = F2R (Float beta (choice m l) e). round beta fexp rnd x = F2R (Float beta (choice m l) e). Proof. Proof. intros rnd choice Hc x m l e Hl. intros rnd choice Hc x m l e Hl. unfold rounding, F2R. simpl. unfold round, F2R. simpl. apply (f_equal (fun m => (Z2R m * bpow e)%R)). apply (f_equal (fun m => (Z2R m * bpow e)%R)). apply Hc. apply Hc. apply inbetween_mult_reg with (bpow e). apply inbetween_mult_reg with (bpow e). ... @@ -566,9 +566,9 @@ Theorem inbetween_float_DN : ... @@ -566,9 +566,9 @@ Theorem inbetween_float_DN : forall x m l, forall x m l, let e := canonic_exponent beta fexp x in let e := canonic_exponent beta fexp x in inbetween_float m e x l -> inbetween_float m e x l -> rounding beta fexp ZrndDN x = F2R (Float beta m e). round beta fexp rndDN x = F2R (Float beta m e). Proof. Proof. apply inbetween_float_rounding with (choice := fun m l => m). apply inbetween_float_round with (choice := fun m l => m). intros x m l Hl. intros x m l Hl. refine (Zfloor_imp m _ _). refine (Zfloor_imp m _ _). apply inbetween_bounds with (2 := Hl). apply inbetween_bounds with (2 := Hl). ... @@ -588,9 +588,9 @@ Theorem inbetween_float_UP : ... @@ -588,9 +588,9 @@ Theorem inbetween_float_UP : forall x m l, forall x m l, let e := canonic_exponent beta fexp x in let e := canonic_exponent beta fexp x in inbetween_float m e x l -> inbetween_float m e x l -> rounding beta fexp ZrndUP x = F2R (Float beta (cond_incr (round_UP l) m) e). round beta fexp rndUP x = F2R (Float beta (cond_incr (round_UP l) m) e). Proof. Proof. apply inbetween_float_rounding with (choice := fun m l => cond_incr (round_UP l) m). apply inbetween_float_round with (choice := fun m l => cond_incr (round_UP l) m). intros x m l Hl. intros x m l Hl. assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)). assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)). case l ; try (now left) ; now right ; split. case l ; try (now left) ; now right ; split. ... @@ -621,16 +621,16 @@ Theorem inbetween_float_NE : ... @@ -621,16 +621,16 @@ Theorem inbetween_float_NE : forall x m l, forall x m l, let e := canonic_exponent beta fexp x in let e := canonic_exponent beta fexp x in inbetween_float m e x l -> inbetween_float m e x l -> rounding beta fexp ZrndNE x = F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e). round beta fexp rndNE x = F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e). Proof. Proof. apply inbetween_float_rounding with (choice := fun m l => cond_incr (round_NE (Zeven m) l) m). apply inbetween_float_round with (choice := fun m l => cond_incr (round_NE (Zeven m) l) m). intros x m l Hl. intros x m l Hl. inversion_clear Hl as [Hx|l' Hx Hl']. inversion_clear Hl as [Hx|l' Hx Hl']. (* Exact *) (* Exact *) rewrite Hx. rewrite Hx. now rewrite Zrnd_Z2R. now rewrite Zrnd_Z2R. (* not Exact *) (* not Exact *) unfold Zrnd, ZrndNE, ZrndN, Znearest. unfold Zrnd, rndNE, rndN, Znearest. assert (Hm: Zfloor x = m). assert (Hm: Zfloor x = m). apply Zfloor_imp. apply Zfloor_imp. exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)). ... @@ -639,7 +639,7 @@ rewrite Hm. ... @@ -639,7 +639,7 @@ rewrite Hm. replace (Rcompare (x - Z2R m) (/2)) with l'. replace (Rcompare (x - Z2R m) (/2)) with l'. now case l'. now case l'. rewrite <- Hl'. rewrite <- Hl'. rewrite plus_Z2R. rewrite Z2R_plus. rewrite <- (Rcompare_plus_r (- Z2R m) x). rewrite <- (Rcompare_plus_r (- Z2R m) x). apply f_equal. apply f_equal. simpl (Z2R 1). simpl (Z2R 1). ... ...
 ... @@ -100,7 +100,7 @@ intros n Hn. ... @@ -100,7 +100,7 @@ intros n Hn. destruct (ln_beta beta (Z2R n)) as (e, He). destruct (ln_beta beta (Z2R n)) as (e, He). simpl. simpl. specialize (He (Z2R_neq _ _ Hn)). specialize (He (Z2R_neq _ _ Hn)). rewrite <- abs_Z2R in He. rewrite <- Z2R_abs in He. assert (Hn': (0 < Zabs n)%Z). assert (Hn': (0 < Zabs n)%Z). destruct n ; try easy. destruct n ; try easy. now elim Hn. now elim Hn. ... @@ -174,7 +174,7 @@ apply <- bpow_le. ... @@ -174,7 +174,7 @@ apply <- bpow_le. apply Rlt_le. apply Rlt_le. apply Rle_lt_trans with (Rabs (Z2R n)). apply Rle_lt_trans with (Rabs (Z2R n)). simpl. simpl. rewrite <- abs_Z2R. rewrite <- Z2R_abs. apply (Z2R_le 1). apply (Z2R_le 1). apply (Zlt_le_succ 0). apply (Zlt_le_succ 0). revert H. revert H. ... @@ -192,7 +192,7 @@ Theorem digits_shift : ... @@ -192,7 +192,7 @@ Theorem digits_shift : Proof. Proof. intros m e Hm He. intros m e Hm He. rewrite 2!digits_ln_beta. rewrite 2!digits_ln_beta. rewrite mult_Z2R. rewrite Z2R_mult. rewrite Z2R_Zpower with (1 := He). rewrite Z2R_Zpower with (1 := He). change (Z2R m * bpow e)%R with (F2R (Float beta m e)). change (Z2R m * bpow e)%R with (F2R (Float beta m e)). apply ln_beta_F2R. apply ln_beta_F2R. ... @@ -281,11 +281,11 @@ apply Rlt_le_trans with (Z2R (x + 1) * Z2R (y + 1))%R. ... @@ -281,11 +281,11 @@ apply Rlt_le_trans with (Z2R (x + 1) * Z2R (y + 1))%R. apply Rle_lt_trans with (Z2R (x + y + x * y)). apply Rle_lt_trans with (Z2R (x + y + x * y)). rewrite <- (Rabs_pos_eq _ (Rlt_le _ _ Hxy)). rewrite <- (Rabs_pos_eq _ (Rlt_le _ _ Hxy)). apply Hexy. apply Hexy. rewrite <- mult_Z2R. rewrite <- Z2R_mult. apply Z2R_lt. apply Z2R_lt. apply Zplus_lt_reg_r with (- (x + y + x * y + 1))%Z. apply Zplus_lt_reg_r with (- (x + y + x * y + 1))%Z. now ring_simplify. now ring_simplify. rewrite bpow_add. rewrite bpow_plus. apply Rmult_le_compat ; try (apply (Z2R_le 0) ; omega). apply Rmult_le_compat ; try (apply (Z2R_le 0) ; omega). rewrite <- (Rmult_1_r (Z2R (x + 1))). rewrite <- (Rmult_1_r (Z2R (x + 1))). change (F2R (Float beta (x + 1) 0) <= bpow ex)%R. change (F2R (Float beta (x + 1) 0) <= bpow ex)%R. ... ...
 ... @@ -110,8 +110,8 @@ omega. ... @@ -110,8 +110,8 @@ omega. now apply Zlt_le_weak. now apply Zlt_le_weak. (* . the location is correctly computed *) (* . the location is correctly computed *) unfold inbetween_float, F2R. simpl. unfold inbetween_float, F2R. simpl. rewrite bpow_add, plus_Z2R. rewrite bpow_plus, Z2R_plus. rewrite Hq, plus_Z2R, mult_Z2R. rewrite Hq, Z2R_plus, Z2R_mult. replace ((Z2R m2 * Z2R q + Z2R r) * (bpow e' * bpow e2) / (Z2R m2 * bpow e2))%R replace ((Z2R m2 * Z2R q + Z2R r) * (bpow e' * bpow e2) / (Z2R m2 * bpow e2))%R with ((Z2R q + Z2R r / Z2R m2) * bpow e')%R. with ((Z2R q + Z2R r / Z2R m2) * bpow e')%R. apply inbetween_mult_compat. apply inbetween_mult_compat. ... ...
 ... @@ -49,7 +49,7 @@ Theorem Fopp_F2R : ... @@ -49,7 +49,7 @@ Theorem Fopp_F2R : forall f1 : float beta, forall f1 : float beta, (F2R (Fopp f1) = -F2R f1)%R. (F2R (Fopp f1) = -F2R f1)%R. unfold Fopp, F2R; intros (m1,e1). unfold Fopp, F2R; intros (m1,e1). simpl; rewrite opp_Z2R; ring. simpl; rewrite Z2R_opp; ring. Qed. Qed. Definition Fabs (f1: float beta) := Definition Fabs (f1: float beta) := ... @@ -78,7 +78,7 @@ destruct (Falign f1 f2) as ((m1, m2), e). ... @@ -78,7 +78,7 @@ destruct (Falign f1 f2) as ((m1, m2), e). intros (H1, H2). intros (H1, H2). rewrite H1, H2. rewrite H1, H2. unfold F2R. simpl. unfold F2R. simpl. rewrite plus_Z2R. rewrite Z2R_plus. apply Rmult_plus_distr_r. apply Rmult_plus_distr_r. Qed. Qed. ... @@ -115,7 +115,7 @@ Theorem mult_F2R : ... @@ -115,7 +115,7 @@ Theorem mult_F2R : Proof. Proof. intros (m1, e1) (m2, e2). intros (m1, e1) (m2, e2). unfold Fmult, F2R. simpl. unfold Fmult, F2R. simpl. rewrite mult_Z2R, bpow_add. rewrite Z2R_mult, bpow_plus. ring. ring. Qed. Qed. ... ...
 ... @@ -150,20 +150,20 @@ Qed. ... @@ -150,20 +150,20 @@ Qed. Section round_dir. Section round_dir. Variable rnd: Zrounding. Variable rnd: Zround. Variable choice : Z -> location -> Z. Variable choice : Z -> location -> Z. Hypothesis choice_valid : forall m, choice m loc_Exact = m. Hypothesis choice_valid : forall m, choice m loc_Exact = m. Hypothesis inbetween_float_valid : Hypothesis inbetween_float_valid : forall x m l, forall x m l, let e := canonic_exponent beta fexp x in let e := canonic_exponent beta fexp x in inbetween_float beta m e x l -> inbetween_float beta m e x l -> rounding beta fexp rnd x = F2R (Float beta (choice m l) e). round beta fexp rnd x = F2R (Float beta (choice m l) e). Theorem round_any_correct : Theorem round_any_correct : forall x m e l, forall x m e l, inbetween_float beta m e x l -> inbetween_float beta m e x l -> (e = canonic_exponent beta fexp x \/ (l = loc_Exact /\ format x)) -> (e = canonic_exponent beta fexp x \/ (l = loc_Exact /\ format x)) -> rounding beta fexp rnd x = F2R (Float beta (choice m l) e). round beta fexp rnd x = F2R (Float beta (choice m l) e). Proof. Proof. intros x m e l Hin [He|(Hl,Hf)]. intros x m e l Hin [He|(Hl,Hf)]. rewrite He in Hin |- *. rewrite He in Hin |- *. ... @@ -172,7 +172,7 @@ rewrite Hl in Hin. ... @@ -172,7 +172,7 @@ rewrite Hl in Hin. inversion_clear Hin. inversion_clear Hin. rewrite Hl, choice_valid. rewrite Hl, choice_valid. rewrite <- H. rewrite <- H. now apply rounding_generic. now apply round_generic. Qed. Qed. Theorem round_trunc_any_correct : Theorem round_trunc_any_correct : ... @@ -180,7 +180,7 @@ Theorem round_trunc_any_correct : ... @@ -180,7 +180,7 @@ Theorem round_trunc_any_correct : (0 <= x)%R -> (0 <= x)%R -> inbetween_float beta m e x l -> inbetween_float beta m e x l -> (e <= fexp (digits beta m + e))%Z \/ l = loc_Exact -> (e <= fexp (digits beta m + e))%Z \/ l = loc_Exact -> rounding beta fexp rnd x = let '(m', e', l') := truncate (m, e, l) in F2R (Float beta (choice m' l') e'). round beta fexp rnd x = let '(m', e', l') := truncate (m, e, l) in F2R (Float beta (choice m' l') e'). Proof. Proof. intros x m e l Hx Hl He. intros x m e l Hx Hl He. generalize (truncate_correct x m e l Hx Hl He). generalize (truncate_correct x m e l Hx Hl He). ... ...
 ... @@ -223,7 +223,7 @@ replace (digits beta q * 2)%Z with (digits beta q + digits beta q)%Z by ring. ... @@ -223,7 +223,7 @@ replace (digits beta q * 2)%Z with (digits beta q + digits beta q)%Z by ring. apply digits_mult_strong. apply digits_mult_strong. omega. omega. omega. omega. (* . rounding *) (* . round *) unfold inbetween_float, F2R. simpl. unfold inbetween_float, F2R. simpl. rewrite sqrt_mult. rewrite sqrt_mult. 2: now apply (Z2R_le 0) ; apply Zlt_le_weak. 2: now apply (Z2R_le 0) ; apply Zlt_le_weak. ... @@ -233,7 +233,7 @@ rewrite He1, Zplus_0_r in Hev. clear He1. ... @@ -233,7 +233,7 @@ rewrite He1, Zplus_0_r in Hev. clear He1. rewrite Hev. rewrite Hev. replace (Zdiv2 (2 * e2)) with e2 by now case e2. replace (Zdiv2 (2 * e2)) with e2 by now case e2. replace (2 * e2)%Z with (e2 + e2)%Z by ring. replace (2 * e2)%Z with (e2 + e2)%Z by ring. rewrite bpow_add. rewrite bpow_plus. fold (Rsqr (bpow e2)). fold (Rsqr (bpow e2)). rewrite sqrt_Rsqr. rewrite sqrt_Rsqr. 2: apply Rlt_le ; apply bpow_gt_0. 2: apply Rlt_le ; apply bpow_gt_0. ... @@ -242,7 +242,7 @@ apply bpow_gt_0. ... @@ -242,7 +242,7 @@ apply bpow_gt_0. rewrite Hq. rewrite Hq. case Zeq_bool_spec ; intros Hr'. case Zeq_bool_spec ; intros Hr'. (* .. r = 0 *) (* .. r = 0 *) rewrite Hr', Zplus_0_r, mult_Z2R. rewrite Hr', Zplus_0_r, Z2R_mult. fold (Rsqr (Z2R q)). fold (Rsqr (Z2R q)). rewrite sqrt_Rsqr. rewrite sqrt_Rsqr. now constructor. now constructor. ... @@ -253,14 +253,14 @@ constructor. ... @@ -253,14 +253,14 @@ constructor. split. split. (* ... bounds *) (* ... bounds *) apply Rle_lt_trans with (sqrt (Z2R (q * q))). apply Rle_lt_trans with (sqrt (Z2R (q * q))). rewrite mult_Z2R. rewrite Z2R_mult. fold (Rsqr (Z2R q)). fold (Rsqr (Z2R q)). rewrite sqrt_Rsqr. rewrite sqrt_Rsqr. apply Rle_refl. apply Rle_refl. apply (Z2R_le 0). apply (Z2R_le 0). omega. omega. apply sqrt_lt_1. apply sqrt_lt_1. rewrite mult_Z2R. rewrite Z2R_mult. apply Rle_0_sqr. apply Rle_0_sqr. rewrite <- Hq. rewrite <- Hq. apply (Z2R_le 0). apply (Z2R_le 0). ... @@ -272,12 +272,12 @@ apply sqrt_lt_1. ... @@ -272,12 +272,12 @@ apply sqrt_lt_1. rewrite <- Hq. rewrite <- Hq. apply (Z2R_le 0). apply (Z2R_le 0). now apply Zlt_le_weak. now apply Zlt_le_weak. rewrite mult_Z2R. rewrite Z2R_mult. apply Rle_0_sqr. apply Rle_0_sqr. apply Z2R_lt. apply Z2R_lt. ring_simplify. ring_simplify. omega. omega. rewrite mult_Z2R. rewrite Z2R_mult. fold (Rsqr (Z2R (q + 1))). fold (Rsqr (Z2R (q + 1))). rewrite sqrt_Rsqr. rewrite sqrt_Rsqr. apply Rle_refl. apply Rle_refl. ... @@ -290,7 +290,7 @@ replace ((2 * sqrt (Z2R (q * q + r))) * (2 * sqrt (Z2R (q * q + r))))%R ... @@ -290,7 +290,7 @@ replace ((2 * sqrt (Z2R (q * q + r))) * (2 * sqrt (Z2R (q * q + r))))%R with (4 * Rsqr (sqrt (Z2R (q * q + r))))%R by (unfold Rsqr ; ring). with (4 * Rsqr (sqrt (Z2R (q * q + r))))%R by (unfold Rsqr ; ring). rewrite Rsqr_sqrt. rewrite Rsqr_sqrt. change 4%R with (Z2R 4). change 4%R with (Z2R 4). rewrite <- plus_Z2R, <- 2!mult_Z2R. rewrite <- Z2R_plus, <- 2!Z2R_mult. rewrite Rcompare_Z2R. rewrite Rcompare_Z2R. replace ((q + (q + 1)) * (q + (q + 1)))%Z with (4 * (q * q) + 4 * q + 1)%Z by ring. replace ((q + (q + 1)) * (q + (q + 1)))%Z with (4 * (q * q) + 4 * q + 1)%Z by ring. generalize (Zle_cases r q). generalize (Zle_cases r q). ... @@ -305,7 +305,7 @@ now apply Zlt_le_weak. ... @@ -305,7 +305,7 @@ now apply Zlt_le_weak. apply Rmult_le_pos. apply Rmult_le_pos. now apply (Z2R_le 0 2). now apply (Z2R_le 0 2). apply sqrt_ge_0. apply sqrt_ge_0. rewrite <- plus_Z2R. rewrite <- Z2R_plus. apply (Z2R_le 0). apply (Z2R_le 0). omega. omega. Qed. Qed. ... ...
 ... @@ -58,9 +58,9 @@ exact FIX_exp_correct. ... @@ -58,9 +58,9 @@ exact FIX_exp_correct. Qed. Qed. Theorem Rnd_NE_pt_FIX : Theorem Rnd_NE_pt_FIX : rounding_pred (Rnd_NE_pt beta FIX_exp). round_pred (Rnd_NE_pt beta FIX_exp). Proof. Proof. apply Rnd_NE_pt_rounding. apply Rnd_NE_pt_round. apply FIX_exp_correct. apply FIX_exp_correct. right. right. split ; easy. split ; easy. ... ...
 ... @@ -84,7 +84,7 @@ apply lt_Z2R. ... @@ -84,7 +84,7 @@ apply lt_Z2R. rewrite Z2R_Zpower. 2: now apply Zlt_le_weak. rewrite Z2R_Zpower. 2: now apply Zlt_le_weak. apply Rmult_lt_reg_r with (bpow ex). apply Rmult_lt_reg_r with (bpow ex). apply bpow_gt_0. apply bpow_gt_0. rewrite <- bpow_add. rewrite <- bpow_plus. change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R. change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R. rewrite <- abs_F2R. rewrite <- abs_F2R. rewrite <- Hx. rewrite <- Hx. ... @@ -170,11 +170,11 @@ now apply FLX_format_generic. ... @@ -170,11 +170,11 @@ now apply FLX_format_generic. Qed. Qed. Theorem FLT_rounding_FLX : forall rnd x, Theorem FLT_round_FLX : forall rnd x, (bpow (emin + prec - 1) <= Rabs x)%R -> (bpow (emin + prec - 1) <= Rabs x)%R -> rounding beta FLT_exp rnd x = rounding beta (FLX_exp prec) rnd x. round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x. intros rnd x Hx. intros rnd x Hx. unfold rounding, scaled_mantissa. unfold round, scaled_mantissa. rewrite ->FLT_canonic_FLX; trivial. rewrite ->FLT_canonic_FLX; trivial. intros H; contradict Hx. intros H; contradict Hx. rewrite H, Rabs_R0; apply Rlt_not_le. rewrite H, Rabs_R0; apply Rlt_not_le. ... @@ -278,7 +278,7 @@ Qed. ... @@ -278,7 +278,7 @@ Qed. Theorem generic_NE_pt_FLT : Theorem generic_NE_pt_FLT : forall x, forall x, Rnd_NE_pt beta FLT_exp x (rounding beta FLT_exp ZrndNE x). Rnd_NE_pt beta FLT_exp x (round beta FLT_exp rndNE x). Proof. Proof. intros x. intros x. apply generic_NE_pt. apply generic_NE_pt. ... @@ -287,9 +287,9 @@ apply NE_ex_prop_FLT. ... @@ -287,9 +287,9 @@ apply NE_ex_prop_FLT. Qed. Qed. Theorem Rnd_NE_pt_FLT : Theorem Rnd_NE_pt_FLT : rounding_pred (Rnd_NE_pt beta FLT_exp). round_pred (Rnd_NE_pt beta FLT_exp). Proof. Proof. apply Rnd_NE_pt_rounding. apply Rnd_NE_pt_round. apply FLT_exp_correct. apply FLT_exp_correct. apply NE_ex_prop_FLT. apply NE_ex_prop_FLT. Qed. Qed. ... ...
 ... @@ -54,7 +54,7 @@ eexists ; repeat split. ... @@ -54,7 +54,7 @@ eexists ; repeat split. apply lt_Z2R. apply lt_Z2R. apply Rmult_lt_reg_r with (bpow (e - prec)). apply Rmult_lt_reg_r with (bpow (e - prec)). apply bpow_gt_0. apply bpow_gt_0. rewrite Z2R_Zpower, <- bpow_add. rewrite Z2R_Zpower, <- bpow_plus. ring_simplify (prec + (e - prec))%Z. ring_simplify (prec + (e - prec))%Z. rewrite <- H2. rewrite <- H2. simpl. simpl. ... @@ -156,14 +156,14 @@ cut (d - 1 < prec)%Z. omega. ... @@ -156,14 +156,14 @@ cut (d - 1 < prec)%Z. omega. apply <- (bpow_lt beta). apply <- (bpow_lt beta). apply Rle_lt_trans with (Rabs (Z2R xm)). apply Rle_lt_trans with (Rabs (Z2R xm)). apply H4. apply H4. rewrite <- Z2R_Zpower, <- abs_Z2R. rewrite <- Z2R_Zpower, <- Z2R_abs. now apply Z2R_lt. now apply Z2R_lt. now apply Zlt_le_weak. now apply Zlt_le_weak. exists (Float beta (xm * Zpower beta (prec - d)) (xe + d - prec)). exists (Float beta (xm * Zpower beta (prec - d)) (xe + d - prec)). split. split. unfold F2R. simpl. unfold F2R. simpl. rewrite mult_Z2R, Z2R_Zpower. rewrite Z2R_mult, Z2R_Zpower. rewrite Rmult_assoc, <- bpow_add. rewrite Rmult_assoc, <- bpow_plus. rewrite H1. rewrite H1. now ring_simplify (prec - d + (xe + d - prec))%Z. now ring_simplify (prec - d