Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit f8badec9 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Finished ulp_pred_succ_pt.

parent 0525e118
......@@ -3,6 +3,7 @@ Require Import Flocq_defs.
Require Import Flocq_rnd_ex.
Require Import Flocq_rnd_prop.
Require Import Flocq_rnd_generic.
Require Import Flocq_float_prop.
Section Flocq_ulp.
......@@ -30,55 +31,28 @@ unfold F2R. simpl.
now rewrite Rmult_0_l.
Qed.
Theorem ulp_pred_succ_pt :
Theorem ulp_pred_succ_pt_pos :
forall x xd xu,
~ F x -> Rnd_DN_pt F x xd -> Rnd_UP_pt F x xu ->
Rlt 0 x -> ~ F x ->
Rnd_DN_pt F x xd -> Rnd_UP_pt F x xu ->
(xu = xd + ulp x)%R.
Proof.
intros x xd xu Fx Hd1 Hu1.
intros x xd xu Hx1 Fx Hd1 Hu1.
unfold ulp.
destruct (Req_EM_T x 0) as [Hx1|Hx1].
now elim zero_not_in_format with x.
destruct (Rdichotomy x 0 Hx1) as [Hx2|Hx2].
(* negative *)
destruct (ln_beta beta (Rabs x)) as (ex, Hx3).
rewrite Rabs_pos_eq.
destruct (ln_beta beta x) as (ex, Hx2).
simpl.
specialize (Hx3 (Rabs_pos_lt x Hx1)).
specialize (Hx2 Hx1).
destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
(* . negative big *)
admit.
(* . negative small *)
rewrite (Rabs_left _ Hx2) in Hx3.
rewrite Rnd_UP_pt_unicity with F x xu R0.
rewrite Rnd_DN_pt_unicity with F x xd (- bpow (fexp ex))%R.
unfold F2R. simpl.
rewrite Rmult_1_l.
now rewrite Rplus_opp_l.
exact Hd1.
apply Rnd_UP_DN_pt_sym.
now eapply generic_format_satisfies_any.
rewrite Ropp_involutive.
now apply generic_UP_pt_small_pos.
exact Hu1.
apply Rnd_DN_UP_pt_sym.
now eapply generic_format_satisfies_any.
rewrite Ropp_0.
now apply generic_DN_pt_small_pos with ex.
(* positive *)
destruct (ln_beta beta (Rabs x)) as (ex, Hx3).
simpl.
specialize (Hx3 (Rabs_pos_lt x Hx1)).
rewrite (Rabs_pos_eq _ (Rlt_le _ _ Hx2)) in Hx3.
destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
(* . positive big *)
assert (Hd2 := generic_DN_pt_pos _ _ prop_exp _ _ Hx3).
(* positive big *)
assert (Hd2 := generic_DN_pt_pos _ _ prop_exp _ _ Hx2).
assert (Hu2 : Rnd_DN_pt F (-x) (-xu)).
apply Rnd_UP_DN_pt_sym.
now eapply generic_format_satisfies_any.
now rewrite 2!Ropp_involutive.
assert (Hx4 : (bpow (ex - 1)%Z <= --x < bpow ex)%R).
assert (Hx3 : (bpow (ex - 1)%Z <= --x < bpow ex)%R).
now rewrite Ropp_involutive.
assert (Hu3 := generic_DN_pt_neg _ _ prop_exp _ _ Hx4).
assert (Hu3 := generic_DN_pt_neg _ _ prop_exp _ _ Hx3).
rewrite (Rnd_DN_pt_unicity _ _ _ _ Hd1 Hd2).
rewrite <- (Ropp_involutive xu).
rewrite (Rnd_DN_pt_unicity _ _ _ _ Hu2 Hu3).
......@@ -92,18 +66,18 @@ rewrite <- plus_Z2R.
apply f_equal.
rewrite Ropp_mult_distr_l_reverse.
apply Zceil_floor_neq.
intros Hx5.
assert (Hx6 : x = F2R (Float beta (Zfloor (x * bpow (- fexp ex)%Z)) (fexp ex))).
intros Hx4.
assert (Hx5 : x = F2R (Float beta (Zfloor (x * bpow (- fexp ex)%Z)) (fexp ex))).
unfold F2R. simpl.
rewrite Hx5.
rewrite Hx4.
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
now rewrite Rmult_1_r.
apply Fx.
rewrite Hx6.
rewrite Hx5.
apply Hd2.
(* . positive small *)
(* positive small *)
rewrite Rnd_UP_pt_unicity with F x xu (bpow (fexp ex)).
rewrite Rnd_DN_pt_unicity with F x xd R0.
rewrite Rplus_0_l.
......@@ -113,6 +87,46 @@ exact Hd1.
now apply generic_DN_pt_small_pos with ex.
exact Hu1.
now apply generic_UP_pt_small_pos.
(* . *)
now apply Rlt_le.
Qed.
Theorem ulp_pred_succ_pt :
forall x xd xu,
~ F x ->
Rnd_DN_pt F x xd -> Rnd_UP_pt F x xu ->
(xu = xd + ulp x)%R.
Proof.
intros x xd xu Fx Hd1 Hu1.
destruct (Req_EM_T x 0) as [Hx1|Hx1].
now elim zero_not_in_format with x.
destruct (Rdichotomy x 0 Hx1) as [Hx2|Hx2].
(* negative *)
assert (Hu2 : Rnd_DN_pt F (-x) (-xu)).
apply Rnd_UP_DN_pt_sym.
now eapply generic_format_satisfies_any.
now rewrite 2!Ropp_involutive.
assert (Hd2 : Rnd_UP_pt F (-x) (-xd)).
apply Rnd_DN_UP_pt_sym.
now eapply generic_format_satisfies_any.
now rewrite 2!Ropp_involutive.
rewrite <- (Ropp_involutive xd).
rewrite ulp_pred_succ_pt_pos with (3 := Hu2) (4 := Hd2).
unfold ulp.
rewrite Rabs_Ropp.
ring.
rewrite <- Ropp_0.
now apply Ropp_lt_contravar.
intros ((xm, xe), (H1, H2)).
apply Fx.
exists (Float beta (-xm) xe).
split.
rewrite <- opp_F2R.
rewrite <- H1.
now rewrite Ropp_involutive.
now rewrite <- Rabs_Ropp.
(* positive *)
now apply ulp_pred_succ_pt_pos.
Qed.
End Flocq_ulp.
\ No newline at end of file
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