Added some new lemmas. Unsuccesfully tried to convert some lemmas from Pff.

src/Core/Fcore_Raux.v

@@ -333,6 +333,18 @@ apply Zfloor_lb.
 now apply Zfloor_lub.
 Qed.
 
+Theorem Zfloor_Z :
+  forall n,
+  Zfloor (Z2R n) = n.
+Proof.
+intros n.
+apply Zfloor_imp.
+split.
+apply Rle_refl.
+apply Z2R_lt.
+apply Zlt_succ.
+Qed.
+
 Definition Zceil (x : R) := (- Zfloor (- x))%Z.
 
 Theorem Zceil_ub :
@@ -380,6 +392,16 @@ rewrite opp_Z2R.
 now apply Ropp_lt_contravar.
 Qed.
 
+Theorem Zceil_Z :
+  forall n,
+  Zceil (Z2R n) = n.
+Proof.
+intros n.
+unfold Zceil.
+rewrite <- opp_Z2R, Zfloor_Z.
+apply Zopp_involutive.
+Qed.
+
 Theorem Zceil_floor_neq :
   forall x : R,
   (Z2R (Zfloor x) <> x)%R ->
@@ -599,15 +621,14 @@ Qed.
 
 Theorem bpow_eq :
   forall e1 e2 : Z,
-  e1 = e2 -> bpow e1 = bpow e2.
+  bpow e1 = bpow e2 -> e1 = e2.
 Proof.
 intros.
-apply Rle_antisym.
-apply -> bpow_le.
-now apply Zeq_le.
-apply -> bpow_le.
-apply Zeq_le.
-now apply sym_eq.
+apply Zle_antisym.
+apply <- bpow_le.
+now apply Req_le.
+apply <- bpow_le.
+now apply Req_le.
 Qed.
 
 Theorem bpow_exp :

src/Core/Fcore_generic_fmt.v

@@ -699,6 +699,69 @@ rewrite Zopp_involutive.
 now apply generic_DN_pt_pos.
 Qed.
 
+Theorem generic_DN_pt :
+  forall x,
+  Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (x * bpow (Zopp (fexp (projT1 (ln_beta beta x)))))) (fexp (projT1 (ln_beta beta x))))).
+Proof.
+intros x.
+destruct (Req_dec x 0) as [Hx|Hx].
+(* x = 0 *)
+rewrite Hx, Rmult_0_l.
+fold (Z2R 0).
+rewrite Zfloor_Z, F2R_0.
+apply Rnd_DN_pt_refl.
+apply generic_format_0.
+(* x <> 0 *)
+destruct (ln_beta beta x) as (ex, Hex).
+simpl.
+specialize (Hex Hx).
+unfold Rabs in Hex.
+destruct (Rcase_abs x) as [Hx'|Hx'].
+now apply generic_DN_pt_neg.
+now apply generic_DN_pt_pos.
+Qed.
+
+Theorem generic_UP_pt :
+  forall x,
+  Rnd_UP_pt generic_format x (F2R (Float beta (Zceil (x * bpow (Zopp (fexp (projT1 (ln_beta beta x)))))) (fexp (projT1 (ln_beta beta x))))).
+Proof.
+intros x.
+destruct (Req_dec x 0) as [Hx|Hx].
+(* x = 0 *)
+rewrite Hx, Rmult_0_l.
+fold (Z2R 0).
+rewrite Zceil_Z, F2R_0.
+apply Rnd_UP_pt_refl.
+apply generic_format_0.
+(* x <> 0 *)
+destruct (ln_beta beta x) as (ex, Hex).
+simpl.
+specialize (Hex Hx).
+unfold Rabs in Hex.
+destruct (Rcase_abs x) as [Hx'|Hx'].
+now apply generic_UP_pt_neg.
+now apply generic_UP_pt_pos.
+Qed.
+
+Theorem generic_format_EM :
+  forall x,
+  generic_format x \/ ~generic_format x.
+Proof.
+intros x.
+destruct (proj1 (satisfies_any_imp_DN _ generic_format_satisfies_any) x) as (d, Hd).
+destruct (Rle_lt_or_eq_dec d x) as [Hxd|Hxd].
+apply Hd.
+right.
+intros Fx.
+apply Rlt_not_le with (1 := Hxd).
+apply Req_le.
+apply sym_eq.
+now apply Rnd_DN_pt_idempotent with (1 := Hd).
+left.
+rewrite <- Hxd.
+apply Hd.
+Qed.
+
 End RND_generic.
 
 Theorem canonic_fun_eq :

src/Core/Fcore_rnd_ne.v

@@ -214,7 +214,6 @@ rewrite ln_beta_unique with beta xu ex.
 rewrite ln_beta_unique with (1 := Hd4).
 rewrite ln_beta_unique with (1 := Hexa).
 simpl.
-rewrite <- Rmult_plus_distr_r.
 intros H.
 replace (Fnum cu) with (Fnum cd + 1)%Z.
 replace (Fnum cd + (Fnum cd + 1))%Z with (2 * Fnum cd + 1)%Z by ring.
@@ -223,7 +222,9 @@ now apply Zeven_mult_Zeven_l.
 apply sym_eq.
 apply eq_Z2R.
 rewrite plus_Z2R.
-apply Rmult_eq_reg_r with (1 := H).
+apply Rmult_eq_reg_r with (bpow (fexp ex)).
+rewrite H.
+simpl. ring.
 apply Rgt_not_eq.
 apply bpow_gt_0.
 rewrite Rabs_pos_eq.

src/Core/Fcore_ulp.v

@@ -14,7 +14,7 @@ Variable fexp : Z -> Z.
 
 Variable prop_exp : valid_exp fexp.
 
-Definition ulp x := F2R (Float beta 1 (fexp (projT1 (ln_beta beta x)))).
+Definition ulp x := bpow (fexp (projT1 (ln_beta beta x))).
 
 Definition F := generic_format beta fexp.
 
@@ -37,11 +37,9 @@ assert (Hu2 := generic_UP_pt_pos _ _ prop_exp _ _ Hx2).
 rewrite (Rnd_DN_pt_unicity _ _ _ _ Hd1 Hd2).
 rewrite (Rnd_UP_pt_unicity _ _ _ _ Hu1 Hu2).
 unfold F2R. simpl.
-rewrite <- Rmult_plus_distr_r.
-change R1 with (Z2R 1).
-rewrite <- plus_Z2R.
-apply (f_equal (fun v => (Z2R v * bpow (fexp ex))%R)).
-apply Zceil_floor_neq.
+rewrite Zceil_floor_neq.
+rewrite plus_Z2R, Rmult_plus_distr_r.
+now rewrite Rmult_1_l.
 intros Hx4.
 assert (Hx5 : x = F2R (Float beta (Zfloor (x * bpow (- fexp ex))) (fexp ex))).
 unfold F2R. simpl.
@@ -56,9 +54,7 @@ apply Hd2.
 (* 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.
-unfold F2R. simpl.
-now rewrite Rmult_1_l.
+now rewrite Rplus_0_l.
 exact Hd1.
 now apply generic_DN_pt_small_pos with ex.
 exact Hu1.
@@ -154,8 +150,6 @@ rewrite (proj2 (proj2 Hrnd)).
 unfold Rminus.
 rewrite Rplus_opp_r.
 rewrite Rabs_R0.
-unfold ulp, F2R. simpl.
-rewrite Rmult_1_l.
 apply bpow_gt_0.
 apply Hd.
 Qed.
@@ -222,7 +216,7 @@ apply Rmult_le_pos.
 apply Rlt_le.
 apply Rinv_0_lt_compat.
 now apply (Z2R_lt 0 2).
-now apply F2R_ge_0_compat.
+apply bpow_ge_0.
 apply Hd.
 Qed.
 
@@ -233,8 +227,6 @@ Theorem ulp_monotone :
   (ulp x <= ulp y)%R.
 Proof.
 intros Hm x y Hx Hxy.
-unfold ulp.
-rewrite 2!F2R_bpow.
 apply -> bpow_le.
 apply Hm.
 now apply ln_beta_monotone.
@@ -245,7 +237,7 @@ Theorem ulp_bpow :
 intros e.
 unfold ulp.
 rewrite (ln_beta_unique beta (bpow e) (e + 1)).
-apply F2R_bpow.
+easy.
 rewrite Rabs_pos_eq.
 split.
 apply -> bpow_le.
@@ -255,4 +247,38 @@ apply Zlt_succ.
 apply bpow_ge_0.
 Qed.
 
+Theorem ulp_DN_pt_eq :
+  forall x d : R,
+  (0 < d)%R ->
+  Rnd_DN_pt F x d ->
+  ulp d = ulp x.
+Proof.
+intros x d Hd Hxd.
+unfold ulp.
+apply (f_equal (fun e => bpow (fexp e))).
+apply ln_beta_unique.
+rewrite (Rabs_pos_eq d).
+destruct (ln_beta beta x) as (ex, He).
+simpl.
+assert (Hx: (0 < x)%R).
+apply Rlt_le_trans with (1 := Hd).
+apply Hxd.
+specialize (He (Rgt_not_eq _ _ Hx)).
+rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
+split.
+assert (Rnd_DN_pt F (bpow (ex - 1)) (bpow (ex - 1))).
+apply Rnd_DN_pt_refl.
+apply generic_format_bpow.
+destruct (Zle_or_lt ex (fexp ex)).
+elim Rgt_not_eq with (1 := Hd).
+apply Rnd_DN_pt_unicity with (1 := Hxd).
+now apply generic_DN_pt_small_pos with (2 := He).
+ring_simplify (ex - 1 + 1)%Z.
+omega.
+apply (Rnd_DN_pt_monotone _ _ _ _ _ H Hxd (proj1 He)).
+apply Rle_lt_trans with (2 := proj2 He).
+apply Hxd.
+now apply Rlt_le.
+Qed.
+
 End Fcore_ulp.

src/Makefile.am

@@ -10,7 +10,9 @@ FILES = \
 	Core/Fcore_generic_fmt.v \
 	Core/Fcore_rnd_ne.v \
 	Core/Fcore_ulp.v \
-	Calc/Fcalc_ops.v
+	Core/Fcore.v \
+	Calc/Fcalc_ops.v \
+	Prop/Fprop_nearest.v
 
 data_DATA = $(FILES:=o)
 EXTRA_DIST = $(FILES)

src/Prop/Fprop_nearest.v

+Require Import Fcore.
+
+Section Fprop_nearest.
+
+Open Scope R_scope.
+
+Theorem Rnd_N_pt_abs :
+  forall F : R -> Prop,
+  F 0 ->
+  ( forall x, F x -> F (- x) ) ->
+  forall x f : R,
+  Rnd_N_pt F x f -> Rnd_N_pt F (Rabs x) (Rabs f).
+Proof.
+intros F HF0 HF x f Hxf.
+unfold Rabs at 1.
+destruct (Rcase_abs x) as [Hx|Hx].
+rewrite Rabs_left1.
+apply Rnd_N_pt_sym.
+exact HF.
+now rewrite 2!Ropp_involutive.
+apply Rnd_N_pt_neg with (3 := Hxf).
+exact HF0.
+now apply Rlt_le.
+rewrite Rabs_pos_eq.
+exact Hxf.
+apply Rnd_N_pt_pos with (3 := Hxf).
+exact HF0.
+now apply Rge_le.
+Qed.
+
+(*
+Variable beta : radix.
+
+Notation bpow e := (bpow beta e).
+
+Variable fexp : Z -> Z.
+
+Variable prop_exp : valid_exp fexp.
+
+Notation format := (generic_format beta fexp).
+
+Theorem half_format_eq_dist :
+  forall x d u : R,
+  format x -> 0 < d ->
+  Rnd_DN_pt format (/2 * x) d -> Rnd_UP_pt format (/2 * x) u ->
+  d + u = x.
+Proof.
+intros x d u Fx H0d Hd Hu.
+destruct Fx as ((mx, ex), Hxc).
+unfold canonic in Hxc.
+destruct (generic_format_EM beta fexp prop_exp (/2 * x)).
+(* x/2 in format *)
+rewrite Rnd_DN_pt_idempotent with (1 := Hd) (2 := H).
+rewrite Rnd_UP_pt_idempotent with (1 := Hu) (2 := H).
+field.
+(* x/2 not in format *)
+rewrite (ulp_pred_succ_pt _ _ _ _ _ _ H Hd Hu).
+destruct (proj1 Hd) as ((md, ed), Hdc).
+assert (He: (ed <= ex)%Z).
+admit.
+assert (Zodd mx).
+destruct (Zeven_odd_dec mx) as [Hm|Hm]. 2: exact Hm.
+elim H. clear H.
+destruct (Zeven_ex mx Hm) as (m, H).
+exists (Float beta (m * Zpower (radix_val beta) (ex - ed)) ed).
+split.
+admit.
+simpl.
+apply bpow_eq with beta.
+destruct Hdc as (Hd1,Hd2).
+simpl in Hd2.
+rewrite Hd2.
+now apply ulp_DN_pt_eq.
+replace (d + (d + ulp beta fexp (/ 2 * x))) with (2 * d + ulp beta fexp (/ 2 * x)) by ring.
+replace d with (Z2R (Zdiv2 (mx * Zpower (radix_val beta) (ex - ed))) * bpow ed).
+rewrite <- (ulp_DN_pt_eq _ _ prop_exp _ _ H0d Hd).
+unfold ulp.
+rewrite <- (proj2 Hdc).
+simpl.
+apply trans_eq with (Z2R (2 * Zdiv2 (mx * radix_val beta ^ (ex - ed)) + 1) * bpow ed).
+rewrite plus_Z2R, mult_Z2R.
+simpl. ring.
+rewrite <- Zodd_div2.
+admit.
+admit.
+SearchAbout Zodd.
+
+
+
+unfold generic_format.
+SearchAbout Zeven.
+Print Zeven.
+
+
+destruct (Rlt_or_le d x) as [Hdx|Hdx].
+
+
+
+Theorem Rnd_N_pt_half :
+  forall x f : R, 0 <= x ->
+  format x -> Rnd_N_pt (/2 * x) f -> Rnd_UP_pt (/2 * x) f.
+
+Theorem half_monotony : (* FmultRadixInv *)
+  forall x y z : R,
+  format x ->
+  Rnd_N_pt format y z -> /2 * x < y -> /2 * x <= z.
+Proof.
+intros x y z Fx Hyz Hxy.
+destruct (satisfies_any_imp_UP format (generic_format_satisfies_any _ _ prop_exp)) as (Hu,_).
+destruct (Hu (/2 * x)) as (xhu, Hxhu).
+destruct (Rlt_or_le xhu y).
+(* . *)
+apply Rle_trans with xhu.
+apply Hxhu.
+apply Rnd_N_pt_monotone with (2 := Hyz) (3 := H).
+apply Rnd_N_pt_refl.
+apply Hxhu.
+(* . *)
+unfold Rnd_UP_pt in Hxhu.
+
+apply Rlt_le.
+apply Rlt_le_trans
+
+
+
+Theorem ClosestExp :
+ forall x f : R,
+ Rnd_N_pt format x f -> Rabs (x - f) <= /2 * bpow (Fexp f).
+*)
+
+End Fprop_nearest.
\ No newline at end of file