diff --git a/src/Core/Fcore_Raux.v b/src/Core/Fcore_Raux.v index 2c0ce1cdc95feb0bfe0d03b417d8c70994cae1c7..254708e705bb1a2ff48fb3788e2a255723486606 100644 --- a/src/Core/Fcore_Raux.v +++ b/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 : diff --git a/src/Core/Fcore_generic_fmt.v b/src/Core/Fcore_generic_fmt.v index 02d1d236bcd92f9f80f8683ad1267442ee4905a4..1e83876cb3962116746818bd97c45a15440e710b 100644 --- a/src/Core/Fcore_generic_fmt.v +++ b/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 : diff --git a/src/Core/Fcore_rnd_ne.v b/src/Core/Fcore_rnd_ne.v index c60c22fda39185741fb7e522978ddc22cc2f3dc4..9b619263189ce94c4ac120213e869b7183fb3ae7 100644 --- a/src/Core/Fcore_rnd_ne.v +++ b/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. diff --git a/src/Core/Fcore_ulp.v b/src/Core/Fcore_ulp.v index 4542ad84bb10d990ffceeb4b539bd2fe9e8238f1..8714e2c5fd112d88eec4fc38f08255fdae7e1a53 100644 --- a/src/Core/Fcore_ulp.v +++ b/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. diff --git a/src/Makefile.am b/src/Makefile.am index 488eb92346a452a05ed27ee02d3dfb7a5061111b..e80fa11b0885bff7541a12c66c2e250e4d742b5d 100644 --- a/src/Makefile.am +++ b/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) diff --git a/src/Prop/Fprop_nearest.v b/src/Prop/Fprop_nearest.v new file mode 100644 index 0000000000000000000000000000000000000000..df20c3e86919cd0ed715e9627607ba2568f0117e --- /dev/null +++ b/src/Prop/Fprop_nearest.v @@ -0,0 +1,131 @@ +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