Commit d1c2186e authored by BOLDO Sylvie's avatar BOLDO Sylvie

WIP transition 2.0 (name changes)

parent 1da4c2e2
round_monotone -> round_le
round_monotone_l -> round_ge_generic
round_monotone_r -> round_le_generic
round_monotone_abs_l -> abs_round_ge_generic
round_monotone_abs_r -> abs_round_le_generic
canonic_exponent_round -> canonic_exponent_round_ge
generic_N_pt -> round_N_pt
ulp_le_pos -> ulp_le_id
succ_lt_le -> succ_le_lt
ulp_monotone -> ulp_le
ulp_DN_pt_eq -> ulp_DN
format_pred -> generic_format_pred
pred_ulp -> pred_plus_ulp
pred_lt -> pred_lt_id
FLT_canonic_FLX -> canonic_exp_FLT_FLX
FLT_generic_format_FLX -> generic_format_FLT_FLX
FLX_generic_format_FLT -> generic_format_FLX_FLT
FLT_round_FLX -> round_FLT_FLX
FLT_canonic_FIX -> canonic_FLT_FIX
FIX_generic_format_FLT -> generic_format_FIX_FLT
FLT_generic_format_FIX -> generic_format_FLT_FIX
Type classes (Valid_exp, Valid_rnd, Exp_not_FTZ, Monotone_exp
Exists_NE
Equivalences FIX/FLX (...) cassées
Version 1.4.0:
- improved efficiency of IEEE-754 addition
- fixed compilation with Coq 8.3
......
......@@ -68,7 +68,7 @@ rewrite ln_beta_F2R with (1 := Zmx).
apply Zmax_lub with (2 := H3).
apply Zplus_le_reg_r with (prec - ex)%Z.
ring_simplify.
now apply ln_beta_Z2R_le.
now apply ln_beta_le_Zpower.
Qed.
Theorem FLT_format_generic :
......@@ -87,7 +87,7 @@ apply Rmult_lt_reg_r with (bpow ex).
apply bpow_gt_0.
rewrite <- bpow_plus.
change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R.
rewrite <- abs_F2R.
rewrite F2R_abs.
rewrite <- Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0, Rabs_R0.
......@@ -114,7 +114,7 @@ apply FLT_format_generic.
apply generic_format_FLT.
Qed.
Theorem FLT_canonic_FLX :
Theorem canonic_exp_FLT_FLX :
forall x, x <> R0 ->
(bpow (emin + prec - 1) <= Rabs x)%R ->
canonic_exponent beta FLT_exp x = canonic_exponent beta (FLX_exp prec) x.
......@@ -132,7 +132,7 @@ apply He.
Qed.
(** Links between FLT and FLX *)
Theorem FLT_generic_format_FLX :
Theorem generic_format_FLT_FLX :
forall x : R,
(bpow (emin + prec - 1) <= Rabs x)%R ->
generic_format beta (FLX_exp prec) x ->
......@@ -146,7 +146,7 @@ unfold generic_format, scaled_mantissa.
now rewrite (FLT_canonic_FLX x Hx0 Hx).
Qed.
Theorem FLX_generic_format_FLT :
Theorem generic_format_FLX_FLT :
forall x : R,
generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.
Proof.
......@@ -160,7 +160,7 @@ unfold canonic_exponent, FLX_exp, FLT_exp.
apply Zle_max_l.
Qed.
Theorem FLT_round_FLX : forall rnd x,
Theorem round_FLT_FLX : forall rnd x,
(bpow (emin + prec - 1) <= Rabs x)%R ->
round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
intros rnd x Hx.
......@@ -172,7 +172,7 @@ apply bpow_gt_0.
Qed.
(** Links between FLT and FIX (underflow) *)
Theorem FLT_canonic_FIX :
Theorem canonic_FLT_FIX :
forall x, x <> R0 ->
(Rabs x < bpow (emin + prec))%R ->
canonic_exponent beta FLT_exp x = canonic_exponent beta (FIX_exp emin) x.
......@@ -189,7 +189,7 @@ apply Rle_lt_trans with (2 := Hx).
now apply Hex.
Qed.
Theorem FIX_generic_format_FLT :
Theorem generic_format_FIX_FLT :
forall x : R,
generic_format beta FLT_exp x ->
generic_format beta (FIX_exp emin) x.
......@@ -203,7 +203,7 @@ rewrite <- Hx.
apply Zle_max_r.
Qed.
Theorem FLT_generic_format_FIX :
Theorem generic_format_FLT_FIX :
forall x : R,
(Rabs x <= bpow (emin + prec))%R ->
generic_format beta (FIX_exp emin) x ->
......
......@@ -84,7 +84,7 @@ rewrite <- scaled_mantissa_generic with (1 := H).
rewrite <- scaled_mantissa_abs.
apply Rmult_lt_reg_r with (bpow (canonic_exponent beta FLX_exp (Rabs x))).
apply bpow_gt_0.
rewrite scaled_mantissa_bpow.
rewrite scaled_mantissa_mult_bpow.
rewrite Z2R_Zpower, <- bpow_plus.
2: now apply Zlt_le_weak.
unfold canonic_exponent, FLX_exp.
......@@ -110,7 +110,7 @@ unfold canonic_exponent, FLX_exp.
rewrite ln_beta_F2R with (1 := Zmx).
apply Zplus_le_reg_r with (prec - ex)%Z.
ring_simplify.
now apply ln_beta_Z2R_le.
now apply ln_beta_le_Zpower.
Qed.
Theorem FLX_format_satisfies_any :
......@@ -178,7 +178,7 @@ apply bpow_gt_0.
rewrite <- bpow_plus.
rewrite <- scaled_mantissa_abs.
rewrite <- canonic_exponent_abs.
rewrite scaled_mantissa_bpow.
rewrite scaled_mantissa_mult_bpow.
unfold canonic_exponent, FLX_exp.
rewrite ln_beta_abs.
ring_simplify (prec - 1 + (ln_beta beta x - prec))%Z.
......@@ -194,7 +194,7 @@ apply bpow_gt_0.
rewrite <- bpow_plus.
rewrite <- scaled_mantissa_abs.
rewrite <- canonic_exponent_abs.
rewrite scaled_mantissa_bpow.
rewrite scaled_mantissa_mult_bpow.
unfold canonic_exponent, FLX_exp.
rewrite ln_beta_abs.
ring_simplify (prec + (ln_beta beta x - prec))%Z.
......
......@@ -52,7 +52,7 @@ rewrite H.
now destruct (Rcase_abs y) as [_|_] ; [right|left].
Qed.
Theorem Rabs_Rminus_pos:
Theorem Rabs_minus_le:
forall x y : R,
(0 <= y)%R -> (y <= 2*x)%R ->
(Rabs (x-y) <= x)%R.
......@@ -162,7 +162,7 @@ rewrite 3!(Rmult_comm r).
now apply Rmult_min_distr_r.
Qed.
Theorem exp_increasing_weak :
Theorem exp_le :
forall x y : R,
(x <= y)%R -> (exp x <= exp y)%R.
Proof.
......@@ -1619,7 +1619,7 @@ fold fact.
pattern x at 2 3 ; replace x with (exp (ln x * / fact * fact)).
split.
rewrite Z2R_minus.
apply exp_increasing_weak.
apply exp_le.
apply Rmult_le_compat_r.
now apply Rlt_le.
unfold Rminus.
......@@ -1704,7 +1704,7 @@ apply ln_beta_opp.
apply refl_equal.
Qed.
Theorem ln_beta_monotone_abs :
Theorem ln_beta_le_abs :
forall x y,
(x <> 0)%R -> (Rabs x <= Rabs y)%R ->
(ln_beta x <= ln_beta y)%Z.
......@@ -1725,13 +1725,13 @@ rewrite Hy', Rabs_R0.
apply Rle_refl.
Qed.
Theorem ln_beta_monotone :
Theorem ln_beta_le :
forall x y,
(0 < x)%R -> (x <= y)%R ->
(ln_beta x <= ln_beta y)%Z.
Proof.
intros x y H0x Hxy.
apply ln_beta_monotone_abs.
apply ln_beta_le_abs.
now apply Rgt_not_eq.
rewrite 2!Rabs_pos_eq.
exact Hxy.
......@@ -1755,7 +1755,7 @@ apply Rle_ge.
apply bpow_ge_0.
Qed.
Theorem ln_beta_le :
Theorem ln_beta_le_bpow :
forall x e,
x <> R0 ->
(Rabs x < bpow e)%R ->
......@@ -1768,7 +1768,7 @@ apply bpow_lt_bpow.
now apply Rle_lt_trans with (Rabs x).
Qed.
Theorem ln_beta_gt :
Theorem ln_beta_gt_bpow :
forall x e,
(bpow e <= Rabs x)%R ->
(e < ln_beta x)%Z.
......@@ -1784,14 +1784,14 @@ rewrite Zx, Rabs_R0.
apply bpow_gt_0.
Qed.
Theorem ln_beta_Z2R_le :
Theorem ln_beta_le_Zpower :
forall m e,
m <> Z0 ->
(Zabs m < Zpower r e)%Z->
(ln_beta (Z2R m) <= e)%Z.
Proof.
intros m e Zm Hm.
apply ln_beta_le.
apply ln_beta_le_bpow.
exact (Z2R_neq m 0 Zm).
destruct (Zle_or_lt 0 e).
rewrite <- Z2R_abs, <- Z2R_Zpower with (1 := H).
......@@ -1803,14 +1803,14 @@ clear -Hm H.
now destruct e.
Qed.
Theorem ln_beta_Z2R_gt :
Theorem ln_beta_gt_Zpower :
forall m e,
m <> Z0 ->
(Zpower r e <= Zabs m)%Z ->
(e < ln_beta (Z2R m))%Z.
Proof.
intros m e Zm Hm.
apply ln_beta_gt.
apply ln_beta_gt_bpow.
rewrite <- Z2R_abs.
destruct (Zle_or_lt 0 e).
rewrite <- Z2R_Zpower with (1 := H).
......
......@@ -41,24 +41,6 @@ apply Zlt_irrefl with x.
now rewrite Hn at 1.
Qed.
Theorem Zmin_left :
forall x y : Z,
(x <= y)%Z -> Zmin x y = x.
Proof.
intros x y.
generalize (Zmin_spec x y).
omega.
Qed.
Theorem Zmin_right :
forall x y : Z,
(y <= x)%Z -> Zmin x y = y.
Proof.
intros x y.
generalize (Zmin_spec x y).
omega.
Qed.
End Zmissing.
Section Proof_Irrelevance.
......@@ -158,12 +140,11 @@ End Even_Odd.
Section Zpower.
Theorem Zmult_pow :
Theorem Zpower_plus :
forall n k1 k2, (0 <= k1)%Z -> (0 <= k2)%Z ->
(Zpower n k1 * Zpower n k2)%Z = Zpower n (k1 + k2).
Zpower n (k1 + k2) = (Zpower n k1 * Zpower n k2)%Z.
Proof.
intros n k1 k2 H1 H2.
apply sym_eq.
now apply Zpower_exp ; apply Zle_ge.
Qed.
......@@ -327,7 +308,7 @@ Proof.
intros e1 e2 He.
destruct (Zle_or_lt 0 e1)%Z as [H1|H1].
replace e2 with (e2 - e1 + e1)%Z by ring.
rewrite <- Zmult_pow with (2 := H1).
rewrite Zpower_plus with (2 := H1).
rewrite <- (Zmult_1_l (r ^ e1)) at 1.
apply Zmult_le_compat_r.
apply (Zlt_le_succ 0).
......@@ -347,7 +328,7 @@ Proof.
intros e1 e2 He2 He.
destruct (Zle_or_lt 0 e1)%Z as [H1|H1].
replace e2 with (e2 - e1 + e1)%Z by ring.
rewrite <- Zmult_pow with (2 := H1).
rewrite Zpower_plus with (2 := H1).
rewrite Zmult_comm.
rewrite <- (Zmult_1_r (r ^ e1)) at 1.
apply Zmult_lt_compat2.
......
......@@ -95,7 +95,7 @@ split.
apply Hn.
apply Zlt_le_trans with (1 := proj2 Hn).
replace k with (e + (k - e))%Z by ring.
rewrite <- Zmult_pow.
rewrite Zpower_plus.
rewrite <- (Zmult_1_r (beta ^ e)) at 1.
apply Zmult_le_compat_l.
apply (Zlt_le_succ 0).
......@@ -149,8 +149,7 @@ apply Zpower_ge_0.
replace (beta ^ e * beta)%Z with (beta ^ (e + 1))%Z.
exact Hn2.
rewrite <- (Zmult_1_r beta) at 3.
apply sym_eq.
now apply (Zmult_pow beta e 1).
now apply (Zpower_plus beta e 1).
Qed.
Theorem Zdigit_not_0 :
......@@ -181,7 +180,7 @@ intros k' IHk' Hk' k H.
unfold Zdigit.
apply (f_equal (fun x => ZOmod x beta)).
pattern k at 1 ; replace k with (k - k' + k')%Z by ring.
rewrite <- Zmult_pow with (2 := Hk').
rewrite Zpower_plus with (2 := Hk').
apply ZOdiv_mult_cancel_r.
apply Zgt_not_eq.
now apply Zpower_gt_0.
......@@ -190,7 +189,7 @@ destruct (Zle_or_lt 0 k) as [H0|H0].
rewrite (Zdigit_lt n) by omega.
unfold Zdigit.
replace k' with (k' - k + k)%Z by ring.
rewrite <- Zmult_pow with (2 := H0).
rewrite Zpower_plus with (2 := H0).
rewrite Zmult_assoc, ZO_div_mult.
replace (k' - k)%Z with (k' - k - 1 + 1)%Z by ring.
rewrite Zpower_exp by omega.
......@@ -216,7 +215,7 @@ intros n k k' Hk Hk'.
unfold Zdigit.
rewrite ZOdiv_ZOdiv.
rewrite Zplus_comm.
now rewrite <- Zmult_pow.
now rewrite Zpower_plus.
Qed.
Theorem Zdigit_mod_pow :
......@@ -231,14 +230,14 @@ apply (f_equal (fun x => ZOdiv x (beta ^ k))).
replace k' with (k + 1 + (k' - (k + 1)))%Z by ring.
rewrite Zpower_exp by omega.
rewrite Zmult_comm.
rewrite <- Zmult_pow by easy.
rewrite Zpower_plus by easy.
change (Zpower beta 1) with (beta * 1)%Z.
rewrite Zmult_1_r.
apply ZOmod_mod_mult.
now rewrite 2!Zdigit_lt.
Qed.
Theorem Zdigit_mod_pow_ge :
Theorem Zdigit_mod_pow_out :
forall n k k', (0 <= k' <= k)%Z ->
Zdigit (ZOmod n (Zpower beta k')) k = Z0.
Proof.
......@@ -279,14 +278,13 @@ rewrite Zplus_comm, Zmult_comm.
apply sym_eq.
apply ZO_div_mod_eq.
rewrite inj_S.
apply sym_eq.
rewrite <- (Zmult_1_r beta) at 2.
apply (Zmult_pow beta (Z_of_nat k) 1).
rewrite <- (Zmult_1_r beta) at 3.
apply Zpower_plus.
apply Zle_0_nat.
easy.
Qed.
Theorem Zpower_gt :
Theorem Zpower_gt_id :
forall n, (n < Zpower beta n)%Z.
Proof.
intros [|n|n] ; try easy.
......@@ -338,11 +336,11 @@ apply Zle_trans with (Zabs n1).
apply Zabs_pos.
apply Zle_max_l.
apply Zlt_le_trans with (Zpower beta (Zabs n2)).
apply Zpower_gt.
apply Zpower_gt_id.
apply Zpower_le.
apply Zle_max_r.
apply Zlt_le_trans with (Zpower beta (Zabs n1)).
apply Zpower_gt.
apply Zpower_gt_id.
apply Zpower_le.
apply Zle_max_l.
Qed.
......@@ -403,7 +401,7 @@ rewrite Zplus_0_r.
apply H.
unfold Zsucc.
ring_simplify.
rewrite <- Zmult_pow.
rewrite Zpower_plus.
change (beta ^1)%Z with (beta * 1)%Z.
now rewrite Zmult_1_r.
apply Zle_0_nat.
......@@ -519,18 +517,18 @@ case Zle_bool_spec ; intros Hk'.
rewrite Zle_bool_true.
rewrite <- Zmult_assoc.
apply f_equal.
now apply Zmult_pow.
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.
rewrite <- Zmult_pow by easy.
rewrite Zpower_plus by easy.
rewrite Zmult_assoc, ZO_div_mult.
apply refl_equal.
apply Zgt_not_eq.
now apply Zpower_gt_0.
replace (-k')%Z with (-(k+k') + k)%Z by ring.
rewrite <- Zmult_pow with (2 := Hk).
rewrite Zpower_plus with (2 := Hk).
apply ZOdiv_mult_cancel_r.
apply Zgt_not_eq.
now apply Zpower_gt_0.
......@@ -564,14 +562,14 @@ now rewrite Zopp_involutive, Zplus_comm.
omega.
Qed.
Theorem Zdigit_slice_ge :
Theorem Zdigit_slice_out :
forall n k1 k2 k, (k2 <= k)%Z ->
Zdigit (Zslice n k1 k2) k = Z0.
Proof.
intros n k1 k2 k Hk.
unfold Zslice.
case Zle_bool_spec ; intros Hk2.
apply Zdigit_mod_pow_ge.
apply Zdigit_mod_pow_out.
now split.
apply Zdigit_0.
Qed.
......@@ -613,11 +611,11 @@ destruct (Zle_or_lt 0 k2') as [Hk2'|Hk2'].
apply Zdigit_ext.
intros k Hk.
destruct (Zle_or_lt (Zmin (k2 - k1') k2') k) as [Hk'|Hk'].
rewrite (Zdigit_slice_ge n (k1 + k1')) with (1 := Hk').
rewrite (Zdigit_slice_out n (k1 + k1')) with (1 := Hk').
destruct (Zle_or_lt k2' k) as [Hk''|Hk''].
now apply Zdigit_slice_ge.
now apply Zdigit_slice_out.
rewrite Zdigit_slice by now split.
apply Zdigit_slice_ge.
apply Zdigit_slice_out.
zify ; omega.
rewrite Zdigit_slice by (zify ; omega).
rewrite (Zdigit_slice n (k1 + k1')) by now split.
......@@ -625,7 +623,7 @@ rewrite Zdigit_slice.
now rewrite Zplus_assoc.
zify ; omega.
unfold Zslice.
rewrite Zmin_right.
rewrite Zmin_r.
now rewrite Zle_bool_false.
omega.
Qed.
......@@ -642,7 +640,7 @@ rewrite Zscale_mul_pow with (1 := Hk).
now replace (- (k1 - k))%Z with (k + -k1)%Z by ring.
Qed.
Theorem Zslice_div_pow_ge :
Theorem Zslice_div_pow :
forall n k k1 k2, (0 <= k)%Z -> (0 <= k1)%Z ->
Zslice (n / Zpower beta k) k1 k2 = Zslice n (k1 + k) k2.
Proof.
......@@ -662,7 +660,7 @@ rewrite Zopp_involutive.
apply Zmult_1_r.
rewrite Zle_bool_false by omega.
rewrite 2!Zopp_involutive, Zplus_comm.
rewrite <- Zmult_pow by assumption.
rewrite Zpower_plus by assumption.
apply ZOdiv_ZOdiv.
Qed.
......@@ -674,11 +672,11 @@ intros n k k1 k2 Hk1.
unfold Zscale.
case Zle_bool_spec; intros Hk.
now apply Zslice_mul_pow.
apply Zslice_div_pow_ge with (2 := Hk1).
apply Zslice_div_pow with (2 := Hk1).
omega.
Qed.
Theorem Zslice_div_pow :
Theorem Zslice_div_pow_scale :
forall n k k1 k2, (0 <= k)%Z ->
Zslice (n / Zpower beta k) k1 k2 = Zscale (Zslice n k (k1 + k2)) (-k1).
Proof.
......@@ -689,9 +687,9 @@ rewrite Zdigit_scale with (1 := Hk').
unfold Zminus.
rewrite (Zplus_comm k'), Zopp_involutive.
destruct (Zle_or_lt k2 k') as [Hk2|Hk2].
rewrite Zdigit_slice_ge with (1 := Hk2).
rewrite Zdigit_slice_out with (1 := Hk2).
apply sym_eq.
apply Zdigit_slice_ge.
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'].
......@@ -713,11 +711,11 @@ intros k Hk.
rewrite Zdigit_plus.
rewrite Zdigit_scale with (1 := Hk).
destruct (Zle_or_lt (l1 + l2) k) as [Hk2|Hk2].
rewrite Zdigit_slice_ge with (1 := Hk2).
now rewrite 2!Zdigit_slice_ge by omega.
rewrite Zdigit_slice_out with (1 := Hk2).
now rewrite 2!Zdigit_slice_out by omega.
rewrite Zdigit_slice with (1 := conj Hk Hk2).
destruct (Zle_or_lt l1 k) as [Hk1|Hk1].
rewrite Zdigit_slice_ge with (1 := Hk1).
rewrite Zdigit_slice_out with (1 := Hk1).
rewrite Zdigit_slice by omega.
simpl ; apply f_equal.
ring.
......@@ -739,7 +737,7 @@ clear k Hk ; intros k Hk.
rewrite Zdigit_scale with (1 := Hk).
destruct (Zle_or_lt l1 k) as [Hk1|Hk1].
left.
now apply Zdigit_slice_ge.
now apply Zdigit_slice_out.
right.
apply Zdigit_lt.
omega.
......@@ -813,7 +811,7 @@ intros v Hv U.
case Zlt_bool_spec ; intros K.
now split.
pattern (radix_val beta) at 2 5 ; replace (radix_val beta) with (Zpower beta 1) by apply Zmult_1_r.
rewrite Zmult_pow.
rewrite <- Zpower_plus.
rewrite Zplus_comm.
apply IHu.
clear -Hv ; omega.
......@@ -851,7 +849,7 @@ apply IHn.
now apply Zlt_lt_succ.
Qed.
Theorem Zdigit_ge :
Theorem Zdigit_out :
forall n k, (Zdigits n <= k)%Z ->
Zdigit n k = Z0.
Proof.
......
......@@ -108,9 +108,9 @@ apply Zle_antisym ;
apply Rle_refl.
Qed.
Theorem abs_F2R :
Theorem F2R_abs:
forall m e : Z,
Rabs (F2R (Float beta m e)) = F2R (Float beta (Zabs m) e).
F2R (Float beta (Zabs m) e) = Rabs (F2R (Float beta m e)).
Proof.
intros m e.
unfold F2R.
......@@ -118,14 +118,14 @@ rewrite Rabs_mult.
rewrite <- Z2R_abs.
simpl.
apply f_equal.
apply Rabs_right.
apply sym_eq; apply Rabs_right.
apply Rle_ge.
apply bpow_ge_0.
Qed.
Theorem opp_F2R :
Theorem F2R_opp :
forall m e : Z,
Ropp (F2R (Float beta m e)) = F2R (Float beta (Zopp m) e).
F2R (Float beta (Zopp m) e) = Ropp (F2R (Float beta m e)).
Proof.
intros m e.
unfold F2R. simpl.
......@@ -332,7 +332,7 @@ Theorem F2R_lt_bpow :
(Rabs (F2R f) < bpow e')%R.
Proof.
intros (m, e) e' Hm.
rewrite abs_F2R.
rewrite <- F2R_abs.
destruct (Zle_or_lt e e') as [He|He].
unfold F2R. simpl.
apply Rmult_lt_reg_r with (bpow (-e)).
......@@ -379,7 +379,7 @@ apply F2R_change_exp.
cut (e' - 1 < e + p)%Z. omega.
apply (lt_bpow beta).
apply Rle_lt_trans with (1 := Hf).
rewrite abs_F2R, Zplus_comm, bpow_plus.
rewrite <- F2R_abs, Zplus_comm, bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
rewrite <- Z2R_Zpower.
......@@ -421,7 +421,7 @@ destruct (ln_beta beta (Z2R m)) as (d, Hd).
simpl.
specialize (Hd (Z2R_neq _ _ H)).
apply ln_beta_unique.
rewrite abs_F2R.
rewrite <- F2R_abs.
unfold F2R. simpl.
rewrite <- Z2R_abs in Hd.
split.
......@@ -469,14 +469,14 @@ simpl.
apply sym_eq.
apply ln_beta_unique.
assert (H2 : (bpow (e1' - 1) <= F2R (Float beta m1 e1) < bpow e1')%R).
rewrite <- (Zabs_eq m1), <- abs_F2R.
rewrite <- (Zabs_eq m1), F2R_abs.
apply H1.
apply Rgt_not_eq.
apply Rlt_gt.
now apply F2R_gt_0_compat.
now apply Zlt_le_weak.
clear H1.
rewrite abs_F2R, Zabs_eq.
rewrite <- F2R_abs, Zabs_eq.
split.
apply Rlt_le.
apply Rle_lt_trans with (2 := H12).
......
This diff is collapsed.
......@@ -1007,7 +1007,7 @@ intros F x f (Hf,_) Hx.
now apply Rnd_N_pt_idempotent with F.
Qed.
Theorem round_pred_pos_imp_rnd :
Theorem round_pred_ge_0 :
forall P : R -> R -> Prop,
round_pred_monotone P ->
P 0 0 ->
......@@ -1017,7 +1017,7 @@ intros P HP HP0 x f Hxf Hx.
now apply (HP 0 x).
Qed.
Theorem round_pred_rnd_imp_pos :
Theorem round_pred_gt_0 :
forall P : R -> R -> Prop,
round_pred_monotone P ->
P 0 0 ->
......@@ -1030,7 +1030,7 @@ apply Rlt_not_le with (1 := Hf).
now apply (HP x 0).
Qed.
Theorem round_pred_neg_imp_rnd :
Theorem round_pred_le_0 :
forall P : R -> R -> Prop,
round_pred_monotone P ->
P 0 0 ->
......@@ -1040,7 +1040,7 @@ intros P HP HP0 x f Hxf Hx.
now apply (HP x 0).
Qed.
Theorem round_pred_rnd_imp_neg :
Theorem round_pred_lt_0 :
forall P : R -> R -> Prop,
round_pred_monotone P ->
P 0 0 ->
......
......@@ -95,9 +95,9 @@ rewrite <- Ropp_involutive.
now apply generic_format_opp.
now apply canonic_opp.
now apply canonic_opp.
rewrite round_DN_opp, <- opp_F2R.
rewrite round_DN_opp, F2R_opp.
now apply f_equal.
rewrite round_UP_opp, <- opp_F2R.
rewrite round_UP_opp, F2R_opp.
now apply f_equal.
Qed.
......@@ -335,14 +335,14 @@ apply Rnd_NE_pt_total.
apply Rnd_NE_pt_monotone.
Qed.
Theorem round_NE_pt_pos :
Lemma round_NE_pt_pos :
forall x,
(0 < x)%R ->
Rnd_NE_pt x (round beta fexp ZnearestE x).
Proof with auto with typeclass_instances.
intros x Hx.
split.
now apply generic_N_pt.
now apply round_N_pt.
unfold NE_prop.
set (mx := scaled_mantissa beta fexp x).
set (xr := round beta fexp ZnearestE x).
......@@ -351,11 +351,11 @@ destruct (Req_dec (mx - Z2R (Zfloor mx)) (/2)) as [Hm|Hm].
left.
exists (Float beta (Ztrunc (scaled_mantissa beta fexp xr)) (canonic_exponent beta fexp xr)).
split.
apply generic_N_pt...
apply round_N_pt...
split.
unfold Fcore_generic_fmt.canonic. simpl.
apply f_equal.
apply generic_N_pt...
apply round_N_pt...
simpl.
unfold xr, round, Znearest.
fold mx.
......@@ -371,7 +371,7 @@ rewrite Rmult_0_l.
change R0 with (Z2R 0).
now rewrite (Ztrunc_Z2R 0).
rewrite <- (round_0 beta fexp Zfloor).
apply round_monotone...
apply round_le...
now apply Rlt_le.
rewrite scaled_mantissa_DN...
now rewrite Ztrunc_Z2R.
......@@ -457,8 +457,8 @@ set (u := round beta fexp Zceil x).
apply Rnd_N_pt_unicity with (d := d) (u := u) (4 := Hg).
now apply round_DN_pt.
now apply round_UP_pt.
2: now apply generic_N_pt.
rewrite <- (scaled_mantissa_bpow beta fexp x).
2: now apply round_N_pt.
rewrite <- (scaled_mantissa_mult_bpow beta fexp x).
unfold d, u, round, F2R. simpl. fold mx.