Commit 23d52e14 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Moved rounding-specific theorems to Fcalc_round in order to reduce dependencies.

parent 7d4d7827
......@@ -20,7 +20,9 @@ COPYING file for more details.
(** * Locations: where a real number is positioned with respect to
its rounded-down value in an arbitrary format. *)
Require Import Fcore.
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Section Fcalc_bracket.
......@@ -509,10 +511,6 @@ Section Fcalc_bracket_generic.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable fexp : Z -> Z.
Hypothesis prop_exp : valid_exp fexp.
Notation format := (generic_format beta fexp).
(** Specialization of inbetween for two consecutive floating-point numbers. *)
Definition inbetween_float m e x l :=
......@@ -581,115 +579,4 @@ now apply inbetween_float_new_location.
apply Zmult_1_r.
Qed.
(** Relates location and rounding. *)
Theorem inbetween_float_round :
forall rnd choice,
( forall x m l, inbetween_int m x l -> Zrnd rnd x = choice m l ) ->
forall x m l,
let e := canonic_exponent beta fexp x in
inbetween_float m e x l ->
round beta fexp rnd x = F2R (Float beta (choice m l) e).
Proof.
intros rnd choice Hc x m l e Hl.
unfold round, F2R. simpl.
apply (f_equal (fun m => (Z2R m * bpow e)%R)).
apply Hc.
apply inbetween_mult_reg with (bpow e).
apply bpow_gt_0.
now rewrite scaled_mantissa_bpow.
Qed.
(** Gives a computable way to round a real number down. *)
Theorem inbetween_float_DN :
forall x m l,
let e := canonic_exponent beta fexp x in
inbetween_float m e x l ->
round beta fexp rndDN x = F2R (Float beta m e).
Proof.
apply inbetween_float_round with (choice := fun m l => m).
intros x m l Hl.
refine (Zfloor_imp m _ _).
apply inbetween_bounds with (2 := Hl).
apply Z2R_lt.
apply Zlt_succ.
Qed.
Definition cond_incr (b : bool) m := if b then (m + 1)%Z else m.
Definition round_UP l :=
match l with
| loc_Exact => false
| _ => true
end.
(** Gives a computable way to round a real number up. *)
Theorem inbetween_float_UP :
forall x m l,
let e := canonic_exponent beta fexp x in
inbetween_float m e x l ->
round beta fexp rndUP x = F2R (Float beta (cond_incr (round_UP l) m) e).
Proof.
apply inbetween_float_round with (choice := fun m l => cond_incr (round_UP l) m).
intros x m l Hl.
assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)).
case l ; try (now left) ; now right ; split.
destruct Hl' as [Hl'|(Hl1, Hl2)].
(* Exact *)
rewrite Hl'.
destruct Hl ; try easy.
rewrite H.
exact (Zceil_Z2R _).
(* not Exact *)
rewrite Hl2.
simpl.
apply Zceil_imp.
ring_simplify (m + 1 - 1)%Z.
refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))).
apply inbetween_bounds_not_Eq with (2 := Hl1) (1 := Hl).
Qed.
Definition round_NE (p : bool) l :=
match l with
| loc_Exact => false
| loc_Inexact Lt => false
| loc_Inexact Eq => if p then false else true
| loc_Inexact Gt => true
end.
(** Gives a computable way to round a real number to nearest even. *)
Theorem inbetween_float_NE :
forall x m l,
let e := canonic_exponent beta fexp x in
inbetween_float m e x l ->
round beta fexp rndNE x = F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e).
Proof.
apply inbetween_float_round with (choice := fun m l => cond_incr (round_NE (Zeven m) l) m).
intros x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
now rewrite Zrnd_Z2R.
(* not Exact *)
unfold Zrnd, rndNE, rndN, Znearest.
assert (Hm: Zfloor x = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
rewrite Zceil_floor_neq.
rewrite Hm.
replace (Rcompare (x - Z2R m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite Z2R_plus.
rewrite <- (Rcompare_plus_r (- Z2R m) x).
apply f_equal.
simpl (Z2R 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
Qed.
End Fcalc_bracket_generic.
......@@ -32,6 +32,117 @@ Variable fexp : Z -> Z.
Hypothesis prop_exp : valid_exp fexp.
Notation format := (generic_format beta fexp).
(** Relates location and rounding. *)
Theorem inbetween_float_round :
forall rnd choice,
( forall x m l, inbetween_int m x l -> Zrnd rnd x = choice m l ) ->
forall x m l,
let e := canonic_exponent beta fexp x in
inbetween_float beta m e x l ->
round beta fexp rnd x = F2R (Float beta (choice m l) e).
Proof.
intros rnd choice Hc x m l e Hl.
unfold round, F2R. simpl.
apply (f_equal (fun m => (Z2R m * bpow e)%R)).
apply Hc.
apply inbetween_mult_reg with (bpow e).
apply bpow_gt_0.
now rewrite scaled_mantissa_bpow.
Qed.
(** Relates location and rounding down. *)
Theorem inbetween_float_DN :
forall x m l,
let e := canonic_exponent beta fexp x in
inbetween_float beta m e x l ->
round beta fexp rndDN x = F2R (Float beta m e).
Proof.
apply inbetween_float_round with (choice := fun m l => m).
intros x m l Hl.
refine (Zfloor_imp m _ _).
apply inbetween_bounds with (2 := Hl).
apply Z2R_lt.
apply Zlt_succ.
Qed.
(** Relates location and rounding up. *)
Definition cond_incr (b : bool) m := if b then (m + 1)%Z else m.
Definition round_UP l :=
match l with
| loc_Exact => false
| _ => true
end.
Theorem inbetween_float_UP :
forall x m l,
let e := canonic_exponent beta fexp x in
inbetween_float beta m e x l ->
round beta fexp rndUP x = F2R (Float beta (cond_incr (round_UP l) m) e).
Proof.
apply inbetween_float_round with (choice := fun m l => cond_incr (round_UP l) m).
intros x m l Hl.
assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)).
case l ; try (now left) ; now right ; split.
destruct Hl' as [Hl'|(Hl1, Hl2)].
(* Exact *)
rewrite Hl'.
destruct Hl ; try easy.
rewrite H.
exact (Zceil_Z2R _).
(* not Exact *)
rewrite Hl2.
simpl.
apply Zceil_imp.
ring_simplify (m + 1 - 1)%Z.
refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))).
apply inbetween_bounds_not_Eq with (2 := Hl1) (1 := Hl).
Qed.
(** Relates location and rounding to nearest even. *)
Definition round_NE (p : bool) l :=
match l with
| loc_Exact => false
| loc_Inexact Lt => false
| loc_Inexact Eq => if p then false else true
| loc_Inexact Gt => true
end.
Theorem inbetween_float_NE :
forall x m l,
let e := canonic_exponent beta fexp x in
inbetween_float beta m e x l ->
round beta fexp rndNE x = F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e).
Proof.
apply inbetween_float_round with (choice := fun m l => cond_incr (round_NE (Zeven m) l) m).
intros x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
now rewrite Zrnd_Z2R.
(* not Exact *)
unfold Zrnd, rndNE, rndN, Znearest.
assert (Hm: Zfloor x = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
rewrite Zceil_floor_neq.
rewrite Hm.
replace (Rcompare (x - Z2R m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite Z2R_plus.
rewrite <- (Rcompare_plus_r (- Z2R m) x).
apply f_equal.
simpl (Z2R 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
Qed.
(** Given a triple (mantissa, exponent, position), this function
computes a triple with a canonic exponent, assuming the
original triple had enough precision. *)
......@@ -222,26 +333,26 @@ End round_dir.
Definition round_DN_correct :=
round_any_correct _ (fun m _ => m)
(fun _ => refl_equal _) (inbetween_float_DN beta fexp).
(fun _ => refl_equal _) inbetween_float_DN.
Definition round_trunc_DN_correct :=
round_trunc_any_correct _ (fun m _ => m)
(fun _ => refl_equal _) (inbetween_float_DN beta fexp).
(fun _ => refl_equal _) inbetween_float_DN.
Definition round_UP_correct :=
round_any_correct _ (fun m l => cond_incr (round_UP l) m)
(fun _ => refl_equal _) (inbetween_float_UP beta fexp).
(fun _ => refl_equal _) inbetween_float_UP.
Definition round_trunc_UP_correct :=
round_trunc_any_correct _ (fun m l => cond_incr (round_UP l) m)
(fun _ => refl_equal _) (inbetween_float_UP beta fexp).
(fun _ => refl_equal _) inbetween_float_UP.
Definition round_NE_correct :=
round_any_correct _ (fun m l => cond_incr (round_NE (Zeven m) l) m)
(fun _ => refl_equal _) (inbetween_float_NE beta fexp).
(fun _ => refl_equal _) inbetween_float_NE.
Definition round_trunc_NE_correct :=
round_trunc_any_correct _ (fun m l => cond_incr (round_NE (Zeven m) l) m)
(fun _ => refl_equal _) (inbetween_float_NE beta fexp).
(fun _ => refl_equal _) inbetween_float_NE.
End Fcalc_round.
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