diff --git a/src/Flocq_Raux.v b/src/Flocq_Raux.v index 18d5b7efae9afd015f97338e301147b1892933ec..80e64e266aae57abcc8964e8feb330b3a7ceec7d 100644 --- a/src/Flocq_Raux.v +++ b/src/Flocq_Raux.v @@ -775,6 +775,21 @@ now apply Rlt_le. now apply Rlt_le. Qed. +Theorem ln_beta_bpow : + forall e, projT1 (ln_beta (bpow e)) = (e + 1)%Z. +Proof. +intros e. +apply ln_beta_unique. +rewrite Rabs_right. +replace (e + 1 - 1)%Z with e by ring. +split. +apply Rle_refl. +apply -> bpow_lt. +apply Zlt_succ. +apply Rle_ge. +apply bpow_ge_0. +Qed. + Theorem Zpower_pos_gt_0 : forall b p, (0 < b)%Z -> (0 < Zpower_pos b p)%Z. diff --git a/src/Flocq_rnd_FLT.v b/src/Flocq_rnd_FLT.v index 1f84b843dca8c69314446ce9b047caabe1260b63..e0a87c1828b2f0e41e8fac277952ba914c3245ab 100644 --- a/src/Flocq_rnd_FLT.v +++ b/src/Flocq_rnd_FLT.v @@ -156,6 +156,32 @@ apply Rle_lt_trans with (1 := Hx1). now apply Hx5. Qed. +(* TODO: vérifier si ça implique ^^ *) +Theorem FLT_canonic_FLX : + forall x : R, + (bpow (emin + prec - 1) <= Rabs x)%R -> + forall f : float beta, + ( canonic beta FLT_exp x f <-> canonic beta (FLX_exp prec) x f ). +Proof. +intros x Hx f. +unfold canonic. +replace (FLT_exp (projT1 (ln_beta beta x))) with (FLX_exp prec (projT1 (ln_beta beta x))). +apply iff_refl. +unfold FLX_exp, FLT_exp. +apply sym_eq. +apply Zmax_left. +destruct (ln_beta beta x) as (ex, He). +simpl. +assert (emin + prec - 1 < ex)%Z. 2: omega. +apply <- (bpow_lt beta). +apply Rle_lt_trans with (1 := Hx). +apply He. +intros H. +elim Rlt_not_le with (2 := Hx). +rewrite H, Rabs_R0. +apply bpow_gt_0. +Qed. + Theorem FLT_format_FIX : forall x, (Rabs x <= bpow (emin + prec))%R -> diff --git a/src/Flocq_rnd_generic.v b/src/Flocq_rnd_generic.v index 3e3d0e903d0cbe3cea325b8a66f9ed7aecd69549..b4b25b3be8724dd2c960ae5548e5cf867924afd8 100644 --- a/src/Flocq_rnd_generic.v +++ b/src/Flocq_rnd_generic.v @@ -35,6 +35,23 @@ exists (Float beta 0 _) ; repeat split. now rewrite F2R_0. Qed. +Theorem generic_format_bpow : + forall e, (fexp (e + 1) <= e)%Z -> + generic_format (bpow e). +Proof. +intros e H. +exists (Float beta (1 * Zpower (radix_val beta) (e - fexp (e + 1))) (fexp (e + 1))). +split. +rewrite <- F2R_change_exp. +apply sym_eq. +apply F2R_bpow. +exact H. +simpl. +apply f_equal. +apply sym_eq. +apply ln_beta_bpow. +Qed. + Theorem generic_DN_pt_large_pos_ge_pow : forall x ex, (fexp ex < ex)%Z -> diff --git a/src/Flocq_rnd_ne.v b/src/Flocq_rnd_ne.v index a890ca450671c29074274f623d1815c9e6c876da..a6881660738b319b0995b13b61b4451c1278ff8e 100644 --- a/src/Flocq_rnd_ne.v +++ b/src/Flocq_rnd_ne.v @@ -561,9 +561,89 @@ Proof. intros x xd xu cd cu Hx0 Hfx Hd Hu Hxd Hxu Hed Heu. destruct (Rlt_or_le (bpow (emin + prec - 1)) x) as [Hx|Hx]. (* . *) -admit. +assert (Hn : generic_format beta FLTf (bpow (emin + prec - 1))). +apply generic_format_bpow. +unfold FLT_exp. +replace (emin + prec - 1 + 1 - prec)%Z with emin by ring. +rewrite Zmax_idempotent. +omega. +apply DN_UP_parity_FLX_pos with prec x xd xu cd cu ; try easy. +(* .. *) +intros H. +apply Hfx. +apply -> FLT_format_generic. 2: exact Hp. +apply <- FLT_format_FLX. 3: exact Hp. +now apply <- FLX_format_generic. +rewrite Rabs_pos_eq. +now apply Rlt_le. +now apply Rlt_le. +(* .. *) +apply -> FLT_canonic_FLX. +eexact Hd. +rewrite Rabs_pos_eq. +apply Hxd. +exact Hn. +now apply Rlt_le. +apply Hxd. +apply generic_format_0. +now apply Rlt_le. +(* .. *) +apply -> FLT_canonic_FLX. +eexact Hu. +rewrite Rabs_pos_eq. +apply Rlt_le. +apply Rlt_le_trans with (1 := Hx). +apply Hxu. +apply Rlt_le. +apply Rlt_le_trans with (1 := Hx0). +apply Hxu. +(* .. *) +apply Rnd_DN_pt_equiv_format with (a := bpow (emin + prec - 1)) (b := x) (4 := Hxd). +exact Hn. +intros a (Ha, _). +apply iff_trans with (2 := FLX_format_generic beta prec Hp a). +assert (Ha' : (bpow (emin + prec - 1) <= Rabs a)%R). +rewrite Rabs_pos_eq. +exact Ha. +apply Rle_trans with (2 := Ha). +apply bpow_ge_0. +apply iff_trans with (2 := FLT_format_FLX beta emin prec Hp a Ha'). +apply iff_sym. +now apply FLT_format_generic. +split. +now apply Rlt_le. +apply Rle_refl. +(* .. *) +destruct (ln_beta beta x) as (ex, He). +specialize (He (Rgt_not_eq _ _ Hx0)). +rewrite Rabs_pos_eq in He. +2: now apply Rlt_le. +apply Rnd_UP_pt_equiv_format with (a := x) (b := bpow ex) (4 := Hxu). +apply generic_format_bpow. +unfold FLT_exp. +rewrite Zmax_left. +omega. +assert (emin + prec - 1 <= ex)%Z. 2 : omega. +apply <- (bpow_le beta). +apply Rlt_le. +now apply Rlt_trans with (2 := proj2 He). +intros b (Hb, _). +apply iff_trans with (2 := FLX_format_generic beta prec Hp b). +assert (Hb' : (bpow (emin + prec - 1) <= Rabs b)%R). +rewrite Rabs_pos_eq. +apply Rle_trans with (2 := Hb). +now apply Rlt_le. +apply Rle_trans with (2 := Hb). +now apply Rlt_le. +apply iff_trans with (2 := FLT_format_FLX beta emin prec Hp b Hb'). +apply iff_sym. +now apply FLT_format_generic. +split. +apply Rle_refl. +now apply Rlt_le. (* . *) apply (DN_UP_parity_FIX emin x xd xu cd cu) ; trivial. +(* .. *) intros H. apply Hfx. apply generic_format_fun_eq with (2 := H). @@ -577,6 +657,7 @@ apply Rle_lt_trans with (1 := Hx). apply -> bpow_lt. apply Zlt_pred. now apply Rlt_le. +(* .. *) apply canonic_fun_eq with (2 := Hd). apply sym_eq. apply FIX_FLT_exp_subnormal. @@ -625,6 +706,7 @@ apply Zlt_pred. apply Hxd. apply generic_format_0. now apply Rlt_le. +(* .. *) apply canonic_fun_eq with (2 := Hu). apply sym_eq. apply FIX_FLT_exp_subnormal. @@ -634,16 +716,57 @@ apply Hxu. rewrite Rabs_pos_eq. apply Rle_lt_trans with (bpow (emin + prec - 1)). apply Hxu. -exists (Float beta (Zpower (radix_val beta) (prec - 1)) emin). -admit. +apply generic_format_bpow. +unfold FLT_exp. +replace (emin + prec - 1 + 1 - prec)%Z with emin by ring. +rewrite Zmax_idempotent. +omega. exact Hx. apply -> bpow_lt. apply Zlt_pred. apply Rlt_le. apply Rlt_le_trans with (1 := Hx0). apply Hxu. -admit. -admit. +(* .. *) +apply Rnd_DN_pt_equiv_format with (a := R0) (b := x) (4 := Hxd). +apply generic_format_0. +intros a (Ha1, Ha2). +apply iff_trans with (2 := FIX_format_generic beta emin a). +assert (Ha' : (Rabs a <= bpow (emin + prec))%R). +rewrite Rabs_pos_eq. +apply Rle_trans with (1 := Ha2). +apply Rle_trans with (1 := Hx). +apply -> bpow_le. +apply Zle_pred. +exact Ha1. +apply iff_trans with (2 := FLT_format_FIX beta emin prec Hp a Ha'). +apply iff_sym. +now apply FLT_format_generic. +split. +now apply Rlt_le. +apply Rle_refl. +(* .. *) +apply Rnd_UP_pt_equiv_format with (a := x) (b := bpow (emin + prec - 1)) (4 := Hxu). +apply generic_format_bpow. +unfold FLT_exp. +replace (emin + prec - 1 + 1 - prec)%Z with emin by ring. +rewrite Zmax_idempotent. +omega. +intros a (Ha1, Ha2). +apply iff_trans with (2 := FIX_format_generic beta emin a). +assert (Ha' : (Rabs a <= bpow (emin + prec))%R). +rewrite Rabs_pos_eq. +apply Rle_trans with (1 := Ha2). +apply -> bpow_le. +apply Zle_pred. +apply Rle_trans with (2 := Ha1). +now apply Rlt_le. +apply iff_trans with (2 := FLT_format_FIX beta emin prec Hp a Ha'). +apply iff_sym. +now apply FLT_format_generic. +split. +apply Rle_refl. +exact Hx. Qed. Theorem Rnd_NE_pt_FLT : diff --git a/src/Flocq_rnd_prop.v b/src/Flocq_rnd_prop.v index bfcb83dfb93c9e14467bd3d289dacf99f3004a75..59c146a02fd67db821b1ab6697042a025b310dad 100644 --- a/src/Flocq_rnd_prop.v +++ b/src/Flocq_rnd_prop.v @@ -1037,4 +1037,64 @@ rewrite <- Rnd_0 with (2 := H) ; trivial. now apply H. Qed. +Theorem Rnd_DN_pt_equiv_format : + forall F1 F2 : R -> Prop, + forall a b : R, + F1 a -> + ( forall x, a <= x <= b -> (F1 x <-> F2 x) ) -> + forall x f, a <= x <= b -> Rnd_DN_pt F1 x f -> Rnd_DN_pt F2 x f. +Proof. +intros F1 F2 a b Ha HF x f Hx (H1, (H2, H3)). +split. +apply -> HF. +exact H1. +split. +now apply H3. +now apply Rle_trans with (1 := H2). +split. +exact H2. +intros k Hk Hl. +destruct (Rlt_or_le k a) as [H|H]. +apply Rlt_le. +apply Rlt_le_trans with (1 := H). +now apply H3. +apply H3. +apply <- HF. +exact Hk. +split. +exact H. +now apply Rle_trans with (1 := Hl). +exact Hl. +Qed. + +Theorem Rnd_UP_pt_equiv_format : + forall F1 F2 : R -> Prop, + forall a b : R, + F1 b -> + ( forall x, a <= x <= b -> (F1 x <-> F2 x) ) -> + forall x f, a <= x <= b -> Rnd_UP_pt F1 x f -> Rnd_UP_pt F2 x f. +Proof. +intros F1 F2 a b Hb HF x f Hx (H1, (H2, H3)). +split. +apply -> HF. +exact H1. +split. +now apply Rle_trans with (2 := H2). +now apply H3. +split. +exact H2. +intros k Hk Hl. +destruct (Rle_or_lt k b) as [H|H]. +apply H3. +apply <- HF. +exact Hk. +split. +now apply Rle_trans with (2 := Hl). +exact H. +exact Hl. +apply Rlt_le. +apply Rle_lt_trans with (2 := H). +now apply H3. +Qed. + End RND_prop.