Commit 2e9b95b4 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Renamed generic_*_pt into round_*_pt.

parent f63e1f7b
......@@ -41,7 +41,7 @@ Theorem Fsqrt_FLT_ne_correct :
Proof.
intros x.
replace (F2R (Fsqrt_FLT_ne x)) with (round beta (FLT_exp emin prec) rndNE (sqrt (F2R x))).
apply generic_NE_pt_FLT.
apply round_NE_pt_FLT.
omega.
now right.
unfold Fsqrt_FLT_ne.
......
......@@ -296,12 +296,12 @@ generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.
Theorem generic_NE_pt_FLT :
Theorem round_NE_pt_FLT :
forall x,
Rnd_NE_pt beta FLT_exp x (round beta FLT_exp rndNE x).
Proof.
intros x.
apply generic_NE_pt.
apply round_NE_pt.
apply FLT_exp_correct.
apply NE_ex_prop_FLT.
Qed.
......
......@@ -256,12 +256,12 @@ unfold FLX_exp.
split ; omega.
Qed.
Theorem generic_NE_pt_FLX :
Theorem round_NE_pt_FLX :
forall x,
Rnd_NE_pt beta FLX_exp x (round beta FLX_exp rndNE x).
Proof.
intros x.
apply generic_NE_pt.
apply round_NE_pt.
apply FLX_exp_correct.
apply NE_ex_prop_FLX.
Qed.
......
......@@ -890,7 +890,7 @@ apply generic_format_0.
now apply generic_format_round_pos.
Qed.
Theorem generic_DN_pt :
Theorem round_DN_pt :
forall x,
Rnd_DN_pt generic_format x (round rndDN x).
Proof.
......@@ -918,10 +918,10 @@ exact generic_format_opp.
(* round down *)
intros x.
exists (round rndDN x).
apply generic_DN_pt.
apply round_DN_pt.
Qed.
Theorem generic_UP_pt :
Theorem round_UP_pt :
forall x,
Rnd_UP_pt generic_format x (round rndUP x).
Proof.
......@@ -930,10 +930,10 @@ rewrite <- (Ropp_involutive x).
rewrite round_UP_opp.
apply Rnd_DN_UP_pt_sym.
apply generic_format_opp.
apply generic_DN_pt.
apply round_DN_pt.
Qed.
Theorem generic_ZR_pt :
Theorem round_ZR_pt :
forall x,
Rnd_ZR_pt generic_format x (round rndZR x).
Proof.
......@@ -941,7 +941,7 @@ intros x.
split ; intros Hx.
(* *)
replace (round rndZR x) with (round rndDN x).
apply generic_DN_pt.
apply round_DN_pt.
apply (f_equal (fun v => F2R (Float beta v _))).
apply sym_eq.
apply Ztrunc_floor.
......@@ -950,7 +950,7 @@ apply Rmult_le_compat_r with (2 := Hx).
apply bpow_ge_0.
(* *)
replace (round rndZR x) with (round rndUP x).
apply generic_UP_pt.
apply round_UP_pt.
apply (f_equal (fun v => F2R (Float beta v _))).
apply sym_eq.
apply Ztrunc_ceil.
......@@ -1040,14 +1040,14 @@ destruct (ln_beta beta x) as (ex, He).
simpl.
assert (Hx: (0 < x)%R).
apply Rlt_le_trans with (1 := Hd).
apply (generic_DN_pt x).
apply (round_DN_pt x).
specialize (He (Rgt_not_eq _ _ Hx)).
rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
split.
apply round_large_pos_ge_pow with (1 := Hd).
apply He.
apply Rle_lt_trans with (2 := proj2 He).
apply (generic_DN_pt x).
apply (round_DN_pt x).
Qed.
Theorem scaled_mantissa_DN :
......@@ -1071,10 +1071,10 @@ intros x f Hxf.
destruct (Rnd_N_pt_DN_or_UP _ _ _ Hxf).
left.
apply Rnd_DN_pt_unicity with (1 := H).
apply generic_DN_pt.
apply round_DN_pt.
right.
apply Rnd_UP_pt_unicity with (1 := H).
apply generic_UP_pt.
apply round_UP_pt.
Qed.
Section not_FTZ.
......@@ -1419,8 +1419,8 @@ apply Zceil_ub.
(* . *)
apply Rnd_DN_UP_pt_N with d u.
now apply generic_format_round.
now apply generic_DN_pt.
now apply generic_UP_pt.
now apply round_DN_pt.
now apply round_UP_pt.
apply Rle_trans with (1 := H).
apply Rmin_l.
apply Rle_trans with (1 := H).
......@@ -1459,7 +1459,7 @@ Section rndNA.
Definition rndNA := rndN (Zle_bool 0).
Theorem generic_NA_pt :
Theorem round_NA_pt :
forall x,
Rnd_NA_pt generic_format x (round rndNA x).
Proof.
......@@ -1480,7 +1480,7 @@ rewrite Rabs_pos_eq.
unfold f, rndNA.
rewrite round_N_middle with (1 := Hm).
rewrite Zle_bool_true.
apply (generic_UP_pt x).
apply (round_UP_pt x).
apply Zfloor_lub.
apply Rmult_le_pos with (1 := Hx).
apply bpow_ge_0.
......@@ -1493,7 +1493,7 @@ apply Ropp_le_contravar.
unfold f, rndNA.
rewrite round_N_middle with (1 := Hm).
rewrite Zle_bool_false.
apply (generic_DN_pt x).
apply (round_DN_pt x).
apply lt_Z2R.
apply Rle_lt_trans with (scaled_mantissa x).
apply Zfloor_lb.
......@@ -1510,8 +1510,8 @@ apply Rxf.
intros g Rxg.
rewrite Rnd_N_pt_unicity with (3 := Hm) (4 := Rxf) (5 := Rxg).
apply Rle_refl.
apply generic_DN_pt.
apply generic_UP_pt.
apply round_DN_pt.
apply round_UP_pt.
Qed.
End rndNA.
......
......@@ -147,15 +147,15 @@ assert (Hd4: (bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R).
rewrite Rabs_pos_eq.
rewrite Hxd.
split.
apply (generic_DN_pt beta fexp prop_exp x).
apply (round_DN_pt beta fexp prop_exp x).
apply generic_format_bpow.
ring_simplify (ex - 1 + 1)%Z.
omega.
apply Hex.
apply Rle_lt_trans with (2 := proj2 Hex).
apply (generic_DN_pt beta fexp prop_exp x).
apply (round_DN_pt beta fexp prop_exp x).
rewrite Hxd.
apply (generic_DN_pt beta fexp prop_exp x).
apply (round_DN_pt beta fexp prop_exp x).
apply generic_format_0.
now apply Rlt_le.
assert (Hxe2 : (fexp (ex + 1) <= ex)%Z) by now eapply prop_exp.
......@@ -242,12 +242,12 @@ rewrite Rabs_pos_eq.
split.
apply Rle_trans with (1 := proj1 Hex).
rewrite Hxu.
apply (generic_UP_pt beta fexp prop_exp x).
apply (round_UP_pt beta fexp prop_exp x).
exact Hu2.
apply Rlt_le.
apply Rlt_le_trans with (1 := H0x).
rewrite Hxu.
apply (generic_UP_pt beta fexp prop_exp x).
apply (round_UP_pt beta fexp prop_exp x).
Qed.
Theorem DN_UP_parity_generic :
......@@ -294,10 +294,10 @@ unfold Fcore_generic_fmt.canonic.
now rewrite <- Hu1.
rewrite <- Hd1.
apply Rnd_DN_pt_unicity with (1 := Hd).
now apply generic_DN_pt.
now apply round_DN_pt.
rewrite <- Hu1.
apply Rnd_UP_pt_unicity with (1 := Hu).
now apply generic_UP_pt.
now apply round_UP_pt.
Qed.
Theorem Rnd_NE_pt_monotone :
......@@ -319,10 +319,10 @@ apply sym_eq.
now apply Rnd_DN_pt_idempotent with (1 := Hd).
rewrite <- Hd1.
apply Rnd_DN_pt_unicity with (1 := Hd).
now apply generic_DN_pt.
now apply round_DN_pt.
rewrite <- Hu1.
apply Rnd_UP_pt_unicity with (1 := Hu).
now apply generic_UP_pt.
now apply round_UP_pt.
Qed.
Theorem Rnd_NE_pt_round :
......@@ -334,7 +334,7 @@ Qed.
Definition rndNE := rndN (fun x => negb (Zeven x)).
Theorem generic_NE_pt_pos :
Theorem round_NE_pt_pos :
forall x,
(0 < x)%R ->
Rnd_NE_pt x (round beta fexp rndNE x).
......@@ -455,8 +455,8 @@ apply Hg.
set (d := round beta fexp rndDN x).
set (u := round beta fexp rndUP x).
apply Rnd_N_pt_unicity with (d := d) (u := u) (4 := Hg).
now apply generic_DN_pt.
now apply generic_UP_pt.
now apply round_DN_pt.
now apply round_UP_pt.
2: now apply generic_N_pt.
rewrite <- (scaled_mantissa_bpow beta fexp x).
unfold d, u, round, F2R. simpl. fold mx.
......@@ -474,7 +474,7 @@ rewrite <- (scaled_mantissa_bpow beta fexp x).
fold mx.
rewrite <- Hxg.
change (Z2R (Zfloor mx) * bpow (canonic_exponent beta fexp x))%R with d.
now eapply generic_DN_pt.
now eapply round_DN_pt.
apply Rgt_not_eq.
apply bpow_gt_0.
Qed.
......@@ -499,7 +499,7 @@ rewrite Zeven_plus.
now rewrite eqb_sym.
Qed.
Theorem generic_NE_pt :
Theorem round_NE_pt :
forall x,
Rnd_NE_pt x (round beta fexp rndNE x).
Proof.
......@@ -517,12 +517,12 @@ now apply canonic_opp.
simpl.
now rewrite Zeven_opp.
rewrite <- round_NE_opp.
apply generic_NE_pt_pos.
apply round_NE_pt_pos.
now apply Ropp_0_gt_lt_contravar.
rewrite Hx, round_0.
apply Rnd_NG_pt_refl.
apply generic_format_0.
now apply generic_NE_pt_pos.
now apply round_NE_pt_pos.
Qed.
End Fcore_rnd_NE.
......@@ -331,28 +331,28 @@ apply Rplus_lt_reg_r with (round beta fexp rndDN x).
rewrite <- ulp_DN_UP with (1 := Hx).
ring_simplify.
assert (Hu: (x <= round beta fexp rndUP x)%R).
apply (generic_UP_pt beta fexp prop_exp x).
apply (round_UP_pt beta fexp prop_exp x).
destruct Hu as [Hu|Hu].
exact Hu.
elim Hx.
rewrite Hu.
now apply generic_format_round.
apply Rle_minus.
apply (generic_DN_pt beta fexp prop_exp x).
apply (round_DN_pt beta fexp prop_exp x).
(* . *)
rewrite Rabs_pos_eq.
rewrite ulp_DN_UP with (1 := Hx).
apply Rplus_lt_reg_r with (x - ulp x)%R.
ring_simplify.
assert (Hd: (round beta fexp rndDN x <= x)%R).
apply (generic_DN_pt beta fexp prop_exp x).
apply (round_DN_pt beta fexp prop_exp x).
destruct Hd as [Hd|Hd].
exact Hd.
elim Hx.
rewrite <- Hd.
now apply generic_format_round.
apply Rle_0_minus.
apply (generic_UP_pt beta fexp prop_exp x).
apply (round_UP_pt beta fexp prop_exp x).
Qed.
Theorem ulp_half_error :
......@@ -378,7 +378,7 @@ destruct (Rle_or_lt (x - d) (d + ulp x - x)) as [H|H].
(* . rnd(x) = rndd(x) *)
apply Rle_trans with (Rabs (d - x)).
apply Hr2.
apply (generic_DN_pt beta fexp prop_exp x).
apply (round_DN_pt beta fexp prop_exp x).
rewrite Rabs_left1.
rewrite Ropp_minus_distr.
apply Rmult_le_reg_r with 2%R.
......@@ -388,7 +388,7 @@ ring_simplify.
apply Rle_trans with (1 := H).
right. field.
apply Rle_minus.
apply (generic_DN_pt beta fexp prop_exp x).
apply (round_DN_pt beta fexp prop_exp x).
(* . rnd(x) = rndu(x) *)
assert (Hu: (d + ulp x)%R = round beta fexp rndUP x).
unfold d.
......@@ -396,7 +396,7 @@ now rewrite <- ulp_DN_UP.
apply Rle_trans with (Rabs (d + ulp x - x)).
apply Hr2.
rewrite Hu.
apply (generic_UP_pt beta fexp prop_exp x).
apply (round_UP_pt beta fexp prop_exp x).
rewrite Rabs_pos_eq.
apply Rmult_le_reg_r with 2%R.
now apply (Z2R_lt 0 2).
......@@ -407,7 +407,7 @@ apply Rlt_le_trans with (1 := H).
right. field.
apply Rle_0_minus.
rewrite Hu.
apply (generic_UP_pt beta fexp prop_exp x).
apply (round_UP_pt beta fexp prop_exp x).
Qed.
Theorem ulp_monotone :
......@@ -474,7 +474,7 @@ apply Rle_not_lt.
apply round_monotone_l; trivial.
apply generic_format_0.
apply Ropp_le_contravar; rewrite Hx.
apply (generic_DN_pt beta fexp prop_exp x).
apply (round_DN_pt beta fexp prop_exp x).
(* *)
rewrite Hx; case (Rle_or_lt 0 (round beta fexp rndUP x)).
intros H; destruct H.
......@@ -485,7 +485,7 @@ intros H1; contradict H.
apply Rle_not_lt.
apply round_monotone_r; trivial.
apply generic_format_0.
apply (generic_UP_pt beta fexp prop_exp x).
apply (round_UP_pt beta fexp prop_exp x).
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
rewrite <- (ulp_opp (round beta fexp rndUP x)).
......@@ -526,7 +526,7 @@ apply Rle_not_lt.
apply round_monotone_l; trivial.
apply generic_format_0.
apply Ropp_le_contravar; rewrite Hx.
apply (generic_DN_pt beta fexp prop_exp x).
apply (round_DN_pt beta fexp prop_exp x).
(* *)
case (Rle_or_lt 0 (round beta fexp rndUP x)).
intros H; destruct H.
......@@ -539,7 +539,7 @@ intros H1; contradict H.
apply Rle_not_lt.
apply round_monotone_r; trivial.
apply generic_format_0.
rewrite Hx; apply (generic_UP_pt beta fexp prop_exp x).
rewrite Hx; apply (round_UP_pt beta fexp prop_exp x).
rewrite Hx in Hfx; contradict Hfx; auto with real.
intros H.
rewrite Hx at 2; rewrite <- (ulp_opp (round beta fexp rndUP x)).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment