Commit 99aabd6e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add helper lemmas.

parent 0e0973d7
......@@ -19,7 +19,7 @@ COPYING file for more details.
(** * Helper function for computing the rounded value of a real number. *)
Require Import Core Digits Bracket.
Require Import Core Digits Float_prop Bracket.
Section Fcalc_round.
......@@ -32,6 +32,61 @@ Variable fexp : Z -> Z.
Context { valid_exp : Valid_exp fexp }.
Notation format := (generic_format beta fexp).
Theorem cexp_inbetween_float :
forall x m e l,
(0 < x)%R ->
inbetween_float beta m e x l ->
(e <= cexp beta fexp x <-> e <= fexp (Zdigits beta m + e))%Z.
Proof.
intros x m e l Px Bx.
unfold cexp.
apply inbetween_float_bounds in Bx.
assert (0 <= m)%Z as Hm.
{ apply Zlt_succ_le.
eapply F2R_gt_0_reg.
apply Rlt_trans with (1 := Px).
apply Bx. }
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|<-].
now erewrite <- mag_F2R_bounds_Zdigits with (1 := Hm').
assert (mag beta x <= e)%Z as Hx.
{ apply mag_le_bpow.
now apply Rgt_not_eq.
rewrite Rabs_pos_eq.
now rewrite <- F2R_bpow.
now apply Rlt_le. }
split ; intros He.
- assert (H := Zle_trans _ _ _ Hx He).
apply valid_exp in H.
now rewrite (proj2 H).
- simpl in He.
assert (H := He).
apply valid_exp in H.
rewrite (proj2 H).
exact He.
now apply Zle_trans with e.
Qed.
Theorem cexp_inbetween_float' :
forall x m e l,
(0 <= x)%R ->
inbetween_float beta m e x l ->
(e <= cexp beta fexp x \/ l = loc_Exact <->
e <= fexp (Zdigits beta m + e) \/ l = loc_Exact)%Z.
Proof.
intros x m e l Px Bx.
destruct Px as [Px|Px].
- split ; (intros [H|H] ; [left|now right]) ;
eapply cexp_inbetween_float ; eassumption.
- assert (H := Bx).
destruct Bx as [|c Bx _].
now split ; right.
rewrite <- Px in Bx.
destruct Bx as [Bx1 Bx2].
apply lt_0_F2R in Bx1.
apply F2R_gt_0_reg in Bx2.
omega.
Qed.
(** Relates location and rounding. *)
Theorem inbetween_float_round :
......
......@@ -490,6 +490,18 @@ apply sym_eq.
now apply Zdigits_mag.
Qed.
Theorem mag_F2R_bounds_Zdigits :
forall x m e, (0 < m)%Z ->
(F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
mag beta x = (Zdigits beta m + e)%Z :> Z.
Proof.
intros x m e Hm Bx.
apply mag_F2R_bounds with (1 := Hm) in Bx.
rewrite Bx.
apply mag_F2R_Zdigits.
now apply Zgt_not_eq.
Qed.
Theorem float_distribution_pos :
forall m1 e1 m2 e2 : Z,
(0 < m1)%Z ->
......
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