Commit 6bbe7159 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Started proofs on rounding to nearest even.

parent 9016ce65
......@@ -21,9 +21,12 @@ Definition valid_exp :=
Variable prop_exp : valid_exp.
Definition canonic x (f : float beta) :=
x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta (Rabs x))).
Definition generic_format (x : R) :=
exists f : float beta,
x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta (Rabs x))).
canonic x f.
Theorem generic_DN_pt_large_pos_ge_pow :
forall x ex,
......@@ -262,7 +265,7 @@ generalize (proj1 (prop_exp _) He1).
clear.
intros He2.
exists (Float beta (- Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))).
unfold F2R. simpl.
unfold canonic, F2R. simpl.
split.
clear -He2.
pattern ex at 1 ; replace ex with (ex - fexp (ex + 1) + fexp (ex + 1))%Z by ring.
......@@ -334,7 +337,7 @@ rewrite Rmult_1_l.
split.
destruct (proj2 (prop_exp _) He1) as (He2, _).
exists (Float beta (- Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))).
unfold F2R. simpl.
unfold canonic, F2R. simpl.
split.
rewrite opp_Z2R.
pattern (fexp ex) at 1 ; replace (fexp ex) with (fexp ex - fexp (fexp ex + 1) + fexp (fexp ex + 1))%Z by ring.
......@@ -431,14 +434,9 @@ apply epow_gt_0.
exact Hx.
Qed.
Theorem generic_format_satisfies_any :
satisfies_any generic_format.
Theorem generic_format_sym :
forall x, generic_format x -> generic_format (-x).
Proof.
refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
(* symmetric set *)
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
intros x ((m,e),(H1,H2)).
exists (Float beta (-m) _) ; repeat split.
rewrite H1 at 1.
......@@ -446,6 +444,17 @@ rewrite Rabs_Ropp.
rewrite opp_F2R.
apply (f_equal (fun v => F2R (Float beta (- m) v))).
exact H2.
Qed.
Theorem generic_format_satisfies_any :
satisfies_any generic_format.
Proof.
refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
(* symmetric set *)
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
exact generic_format_sym.
(* rounding down *)
exists (fun x =>
match total_order_T 0 x with
......@@ -604,7 +613,7 @@ Proof.
intros x xu ex Hx He (((dm, de), (Hu1, Hu2)), (Hu3, Hu4)).
apply Hu4 with (2 := (Rlt_le _ _ (proj2 Hx))).
exists (Float beta (Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))).
unfold F2R. simpl.
unfold canonic, F2R. simpl.
split.
(* . *)
rewrite Z2R_Zpower.
......
Require Import Flocq_Raux.
Require Import Flocq_defs.
Require Import Flocq_rnd_ex.
Require Import Flocq_rnd_prop.
Require Import Flocq_rnd_generic.
Require Import Flocq_float_prop.
Require Import Flocq_ulp.
Section Flocq_rnd_NE.
Variable beta : radix.
Notation bpow e := (epow beta e).
Variable fexp : Z -> Z.
Variable prop_exp : valid_exp fexp.
Notation generic_format := (generic_format beta fexp).
Notation canonic := (canonic beta fexp).
Definition Rnd_NE_pt (x f : R) :=
Rnd_N_pt generic_format x f /\
( ( exists g : float beta, canonic f g /\ Zeven (Fnum g) ) \/
( forall f2 : R, Rnd_N_pt generic_format x f2 -> f2 = f ) ).
Definition Rnd_NE (rnd : R -> R) :=
forall x : R, Rnd_NE_pt x (rnd x).
Theorem Rnd_NE_pt_sym :
forall x f : R,
Rnd_NE_pt (-x) (-f) -> Rnd_NE_pt x f.
Proof.
intros x f (H1,H2).
split.
apply Rnd_N_pt_sym.
apply generic_format_sym.
exact H1.
(* . *)
destruct H2 as [((m,e),((H2,H3),H4))|H2].
left.
exists (Float beta (-m) e).
repeat split.
now rewrite <- opp_F2R, <- H2, Ropp_involutive.
simpl in H3 |- *.
now rewrite H3, Rabs_Ropp.
simpl in H4 |- *.
rewrite Zopp_eq_mult_neg_1.
now apply Zeven_mult_Zeven_l.
(* . *)
right.
intros f2 H3.
rewrite <- (Ropp_involutive f), <- (Ropp_involutive f2).
apply f_equal.
apply H2.
apply Rnd_N_pt_sym.
apply generic_format_sym.
now rewrite 2!Ropp_involutive.
Qed.
Theorem Rnd_NE_pt_unicity :
forall x f1 f2 : R,
Rnd_NE_pt x f1 -> Rnd_NE_pt x f2 ->
f1 = f2.
Proof.
intros x f1 f2 (H1,[H2|H2]) (H3,H4).
destruct H4 as [H4|H4].
destruct (Req_dec x f1) as [H5|H5].
(* . *)
rewrite <- H5.
apply sym_eq.
apply (Rnd_N_pt_idempotent generic_format).
exact H3.
rewrite H5.
apply H1.
(* . *)
destruct (satisfies_any_imp_DN _ (generic_format_satisfies_any beta fexp prop_exp)) as (rndD, Hd).
destruct (satisfies_any_imp_UP _ (generic_format_satisfies_any beta fexp prop_exp)) as (rndU, Hu).
assert (forall d u, canonic (rndD x) d -> canonic (rndU x) u -> d <> u ->
Zeven (Fnum d) -> Zeven (Fnum u) -> False).
clear -prop_exp Hd Hu.
intros d u Cd Cu Hdu Ed Eu.
apply (Zeven_not_Zodd (Fnum u)).
exact Eu.
Check (ulp_pred_succ_pt beta fexp prop_exp x (rndU x)).
admit.
(* . *)
destruct (Rnd_N_pt_DN_or_UP generic_format x (rndD x) (rndU x) f1) as [H6|H6].
apply Hd.
apply Hu.
apply H1.
destruct (Rnd_N_pt_DN_or_UP generic_format x (rndD x) (rndU x) f2) as [H7|H7].
apply Hd.
apply Hu.
apply H3.
now rewrite H6, H7.
destruct H2 as (d,(H2a,H2b)).
destruct H4 as (u,(H4a,H4b)).
elim (H d u) ; try assumption.
now rewrite <- H6.
now rewrite <- H7.
intros H8. apply H5.
apply Rle_antisym.
rewrite (proj1 H2a), H8, <- (proj1 H4a), H7.
eapply Hu.
rewrite H6.
eapply Hd.
destruct (Rnd_N_pt_DN_or_UP generic_format x (rndD x) (rndU x) f2) as [H7|H7].
apply Hd.
apply Hu.
apply H3.
destruct H2 as (u,(H2a,H2b)).
destruct H4 as (d,(H4a,H4b)).
elim (H d u) ; try assumption.
now rewrite <- H7.
now rewrite <- H6.
intros H8. apply H5.
apply Rle_antisym.
rewrite H6.
eapply Hu.
rewrite (proj1 H2a), <- H8, <- (proj1 H4a), H7.
eapply Hd.
now rewrite H6, H7.
(* . *)
now apply H4.
apply sym_eq.
now apply H2.
Qed.
Theorem Rnd_NE_pt_monotone :
forall x y f g : R,
Rnd_NE_pt x f -> Rnd_NE_pt y g ->
(x <= y)%R -> (f <= g)%R.
Proof.
intros x y f g (Hx1,Hx2) (Hy1,Hy2) [Hxy|Hxy].
eapply Rnd_N_pt_monotone ; eassumption.
apply Req_le.
apply Rnd_NE_pt_unicity with x.
now split.
rewrite Hxy.
now split.
Qed.
End Flocq_rnd_NE.
......@@ -374,6 +374,26 @@ apply Rlt_le_trans with (1 := H).
apply Hu.
Qed.
Theorem Rnd_N_pt_sym :
forall F : R -> Prop,
( forall x, F x -> F (- x) ) ->
forall x f : R,
Rnd_N_pt F (-x) (-f) -> Rnd_N_pt F x f.
Proof.
intros F HF x f (H1,H2).
rewrite <- (Ropp_involutive f).
repeat split.
apply HF.
apply H1.
intros g H3.
rewrite Ropp_involutive.
replace (f - x)%R with (-(-f - -x))%R by ring.
replace (g - x)%R with (-(-g - -x))%R by ring.
rewrite 2!Rabs_Ropp.
apply H2.
now apply HF.
Qed.
Theorem Rnd_N_pt_monotone :
forall F : R -> Prop,
forall x y f g : R,
......
......@@ -252,4 +252,20 @@ now apply ln_beta_monotone.
now apply Rlt_le_trans with x.
Qed.
Theorem ulp_epow :
forall e, ulp (bpow e) = bpow (fexp (e + 1)).
intros e.
unfold ulp.
rewrite (ln_beta_unique beta (Rabs (bpow e)) (e + 1)).
unfold F2R.
now rewrite Rmult_1_l.
rewrite Rabs_pos_eq.
split.
apply -> epow_le.
omega.
apply -> epow_lt.
omega.
apply epow_ge_0.
Qed.
End Flocq_ulp.
......@@ -7,6 +7,7 @@ FILES = \
Flocq_rnd_FLT.v \
Flocq_rnd_FLX.v \
Flocq_rnd_generic.v \
Flocq_rnd_ne.v \
Flocq_rnd_prop.v \
Flocq_ulp.v
......
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