Commit 3424cf9b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Duplicate theorems to reason on exact values instead of approximate ones.

parent 1f1fee8f
......@@ -737,6 +737,56 @@ unfold k.
omega.
Qed.
Theorem truncate_correct_partial' :
forall x m e l,
(0 < x)%R ->
inbetween_float beta m e x l ->
(e <= cexp beta fexp x)%Z ->
let '(m', e', l') := truncate (m, e, l) in
inbetween_float beta m' e' x l' /\ e' = cexp beta fexp x.
Proof.
intros x m e l Hx H1 H2.
unfold truncate.
set (k := (fexp (Zdigits beta m + e) - e)%Z).
set (p := Zpower beta k).
assert (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R as Hx'.
apply inbetween_float_bounds with (1 := H1).
assert (0 <= m)%Z as Hm.
cut (0 < m + 1)%Z. omega.
apply lt_F2R with beta e.
rewrite F2R_0.
apply Rlt_trans with (1 := Hx).
apply Hx'.
assert (e + k = cexp beta fexp x)%Z as He.
unfold cexp.
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
rewrite mag_F2R_bounds with (1 := Hm') (2 := Hx').
assert (H: m <> 0%Z) by now apply Zgt_not_eq.
rewrite mag_F2R with (1 := H).
rewrite <- Zdigits_mag with (1 := H).
unfold k.
ring.
unfold k.
ring_simplify.
rewrite <- Hm', Zplus_0_l.
apply valid_exp with (2 := H2).
apply Zle_trans with (2 := H2).
apply mag_le_bpow.
now apply Rgt_not_eq.
rewrite Rabs_pos_eq by now apply Rlt_le.
rewrite <- F2R_bpow.
rewrite <- Hm' in Hx'.
apply Hx'.
generalize (Zlt_cases 0 k).
case (Zlt_bool 0 k) ; intros Hk.
split.
now apply inbetween_float_new_location.
exact He.
split.
exact H1.
omega.
Qed.
Theorem truncate_correct :
forall x m e l,
(0 <= x)%R ->
......@@ -818,6 +868,78 @@ rewrite F2R_0 in H.
elim Rlt_irrefl with (1 := H).
Qed.
Theorem truncate_correct' :
forall x m e l,
(0 <= x)%R ->
inbetween_float beta m e x l ->
(e <= cexp beta fexp x)%Z \/ l = loc_Exact ->
let '(m', e', l') := truncate (m, e, l) in
inbetween_float beta m' e' x l' /\
(e' = cexp beta fexp x \/ (l' = loc_Exact /\ format x)).
Proof.
intros x m e l [Hx|Hx] H1 H2.
- destruct (Zle_or_lt e (fexp (Zdigits beta m + e))) as [H3|H3].
+ generalize (truncate_correct_partial x m e l Hx H1 H3).
destruct (truncate (m, e, l)) as [[m' e'] l'].
intros [H4 H5].
apply (conj H4).
now left.
+ destruct H2 as [H2|H2].
generalize (truncate_correct_partial' x m e l Hx H1 H2).
destruct (truncate (m, e, l)) as [[m' e'] l'].
intros [H4 H5].
apply (conj H4).
now left.
rewrite H2 in H1 |- *.
simpl.
generalize (Zlt_cases 0 (fexp (Zdigits beta m + e) - e)).
destruct Zlt_bool.
intros H.
apply False_ind.
omega.
intros _.
apply (conj H1).
right.
repeat split.
inversion_clear H1.
rewrite H.
apply generic_format_F2R.
intros Zm.
unfold cexp.
rewrite mag_F2R_Zdigits with (1 := Zm).
now apply Zlt_le_weak.
- assert (Hm: m = 0%Z).
cut (m <= 0 < m + 1)%Z. omega.
assert (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R as Hx'.
apply inbetween_float_bounds with (1 := H1).
rewrite <- Hx in Hx'.
split.
apply le_0_F2R with (1 := proj1 Hx').
apply F2R_gt_0_reg with (1 := proj2 Hx').
rewrite Hm, <- Hx in H1 |- *.
clear -H1.
destruct H1 as [_ | l' [H _] _].
+ assert (exists e', truncate (Z0, e, loc_Exact) = (Z0, e', loc_Exact)).
unfold truncate, truncate_aux.
case Zlt_bool.
rewrite Zdiv_0_l, Zmod_0_l.
eexists.
apply f_equal.
unfold new_location.
now case Z.even.
now eexists.
destruct H as [e' H].
rewrite H.
split.
constructor.
apply eq_sym, F2R_0.
right.
repeat split.
apply generic_format_0.
+ rewrite F2R_0 in H.
elim Rlt_irrefl with (1 := H).
Qed.
Section round_dir.
Variable rnd : R -> Z.
......@@ -866,6 +988,20 @@ intros (H1, H2).
now apply round_any_correct.
Qed.
Theorem round_trunc_any_correct' :
forall x m e l,
(0 <= x)%R ->
inbetween_float beta m e x l ->
(e <= cexp beta fexp x)%Z \/ l = loc_Exact ->
round beta fexp rnd x = let '(m', e', l') := truncate (m, e, l) in F2R (Float beta (choice m' l') e').
Proof.
intros x m e l Hx Hl He.
generalize (truncate_correct' x m e l Hx Hl He).
destruct (truncate (m, e, l)) as [[m' e'] l'].
intros [H1 H2].
now apply round_any_correct.
Qed.
End round_dir.
Section round_dir_sign.
......@@ -967,6 +1103,27 @@ now apply generic_format_opp.
exact H3.
Qed.
Theorem round_trunc_sign_any_correct' :
forall x m e l,
inbetween_float beta m e (Rabs x) l ->
(e <= cexp beta fexp x)%Z \/ l = loc_Exact ->
round beta fexp rnd x = let '(m', e', l') := truncate (m, e, l) in F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m' l')) e').
Proof.
intros x m e l Hl He.
rewrite <- cexp_abs in He.
generalize (truncate_correct' (Rabs x) m e l (Rabs_pos _) Hl He).
destruct (truncate (m, e, l)) as [[m' e'] l'].
intros [H1 H2].
apply round_sign_any_correct.
exact H1.
destruct H2 as [H2|[H2 H3]].
left.
now rewrite <- cexp_abs.
right.
apply (conj H2).
now apply generic_format_abs_inv.
Qed.
End round_dir_sign.
(** * Instances of the theorems above, for the usual rounding modes. *)
......@@ -977,60 +1134,90 @@ Definition round_DN_correct :=
Definition round_trunc_DN_correct :=
round_trunc_any_correct _ (fun m _ => m) inbetween_int_DN.
Definition round_trunc_DN_correct' :=
round_trunc_any_correct' _ (fun m _ => m) inbetween_int_DN.
Definition round_sign_DN_correct :=
round_sign_any_correct _ (fun s m l => cond_incr (round_sign_DN s l) m) inbetween_int_DN_sign.
Definition round_trunc_sign_DN_correct :=
round_trunc_sign_any_correct _ (fun s m l => cond_incr (round_sign_DN s l) m) inbetween_int_DN_sign.
Definition round_trunc_sign_DN_correct' :=
round_trunc_sign_any_correct' _ (fun s m l => cond_incr (round_sign_DN s l) m) inbetween_int_DN_sign.
Definition round_UP_correct :=
round_any_correct _ (fun m l => cond_incr (round_UP l) m) inbetween_int_UP.
Definition round_trunc_UP_correct :=
round_trunc_any_correct _ (fun m l => cond_incr (round_UP l) m) inbetween_int_UP.
Definition round_trunc_UP_correct' :=
round_trunc_any_correct' _ (fun m l => cond_incr (round_UP l) m) inbetween_int_UP.
Definition round_sign_UP_correct :=
round_sign_any_correct _ (fun s m l => cond_incr (round_sign_UP s l) m) inbetween_int_UP_sign.
Definition round_trunc_sign_UP_correct :=
round_trunc_sign_any_correct _ (fun s m l => cond_incr (round_sign_UP s l) m) inbetween_int_UP_sign.
Definition round_trunc_sign_UP_correct' :=
round_trunc_sign_any_correct' _ (fun s m l => cond_incr (round_sign_UP s l) m) inbetween_int_UP_sign.
Definition round_ZR_correct :=
round_any_correct _ (fun m l => cond_incr (round_ZR (Zlt_bool m 0) l) m) inbetween_int_ZR.
Definition round_trunc_ZR_correct :=
round_trunc_any_correct _ (fun m l => cond_incr (round_ZR (Zlt_bool m 0) l) m) inbetween_int_ZR.
Definition round_trunc_ZR_correct' :=
round_trunc_any_correct' _ (fun m l => cond_incr (round_ZR (Zlt_bool m 0) l) m) inbetween_int_ZR.
Definition round_sign_ZR_correct :=
round_sign_any_correct _ (fun s m l => m) inbetween_int_ZR_sign.
Definition round_trunc_sign_ZR_correct :=
round_trunc_sign_any_correct _ (fun s m l => m) inbetween_int_ZR_sign.
Definition round_trunc_sign_ZR_correct' :=
round_trunc_sign_any_correct' _ (fun s m l => m) inbetween_int_ZR_sign.
Definition round_NE_correct :=
round_any_correct _ (fun m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE.
Definition round_trunc_NE_correct :=
round_trunc_any_correct _ (fun m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE.
Definition round_trunc_NE_correct' :=
round_trunc_any_correct' _ (fun m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE.
Definition round_sign_NE_correct :=
round_sign_any_correct _ (fun s m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE_sign.
Definition round_trunc_sign_NE_correct :=
round_trunc_sign_any_correct _ (fun s m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE_sign.
Definition round_trunc_sign_NE_correct' :=
round_trunc_sign_any_correct' _ (fun s m l => cond_incr (round_N (negb (Z.even m)) l) m) inbetween_int_NE_sign.
Definition round_NA_correct :=
round_any_correct _ (fun m l => cond_incr (round_N (Zle_bool 0 m) l) m) inbetween_int_NA.
Definition round_trunc_NA_correct :=
round_trunc_any_correct _ (fun m l => cond_incr (round_N (Zle_bool 0 m) l) m) inbetween_int_NA.
Definition round_trunc_NA_correct' :=
round_trunc_any_correct' _ (fun m l => cond_incr (round_N (Zle_bool 0 m) l) m) inbetween_int_NA.
Definition round_sign_NA_correct :=
round_sign_any_correct _ (fun s m l => cond_incr (round_N true l) m) inbetween_int_NA_sign.
Definition round_trunc_sign_NA_correct :=
round_trunc_sign_any_correct _ (fun s m l => cond_incr (round_N true l) m) inbetween_int_NA_sign.
Definition round_trunc_sign_NA_correct' :=
round_trunc_sign_any_correct' _ (fun s m l => cond_incr (round_N true l) m) inbetween_int_NA_sign.
End Fcalc_round_fexp.
(** Specialization of truncate for FIX formats. *)
......
......@@ -889,6 +889,182 @@ Definition binary_round_aux mode sx mx ex lx :=
| _ => F754_nan false xH (* dummy *)
end.
Theorem binary_round_aux_correct' :
forall mode x mx ex lx,
inbetween_float radix2 (Zpos mx) ex (Rabs x) lx ->
(ex <= cexp radix2 fexp x)%Z ->
let z := binary_round_aux mode (Rlt_bool x 0) mx ex lx in
valid_binary z = true /\
if Rlt_bool (Rabs (round radix2 fexp (round_mode mode) x)) (bpow radix2 emax) then
FF2R radix2 z = round radix2 fexp (round_mode mode) x /\
is_finite_FF z = true /\ sign_FF z = Rlt_bool x 0
else
z = binary_overflow mode (Rlt_bool x 0).
Proof with auto with typeclass_instances.
intros m x mx ex lx Bx Ex z.
unfold binary_round_aux in z.
revert z.
rewrite shr_truncate. 2: easy.
refine (_ (round_trunc_sign_any_correct' _ _ (round_mode m) (choice_mode m) _ x (Zpos mx) ex lx Bx (or_introl _ Ex))).
rewrite <- cexp_abs in Ex.
refine (_ (truncate_correct_partial' _ fexp _ _ _ _ _ Bx Ex)).
destruct (truncate radix2 fexp (Zpos mx, ex, lx)) as ((m1, e1), l1).
rewrite loc_of_shr_record_of_loc, shr_m_shr_record_of_loc.
set (m1' := choice_mode m (Rlt_bool x 0) m1 l1).
intros (H1a,H1b) H1c.
rewrite H1c.
assert (Hm: (m1 <= m1')%Z).
(* . *)
unfold m1', choice_mode, cond_incr.
case m ;
try apply Zle_refl ;
match goal with |- (m1 <= if ?b then _ else _)%Z =>
case b ; [ apply Zle_succ | apply Zle_refl ] end.
assert (Hr: Rabs (round radix2 fexp (round_mode m) x) = F2R (Float radix2 m1' e1)).
(* . *)
rewrite <- (Zabs_eq m1').
replace (Zabs m1') with (Zabs (cond_Zopp (Rlt_bool x 0) m1')).
rewrite F2R_Zabs.
now apply f_equal.
apply abs_cond_Zopp.
apply Zle_trans with (2 := Hm).
apply Zlt_succ_le.
apply F2R_gt_0_reg with radix2 e1.
apply Rle_lt_trans with (1 := Rabs_pos x).
exact (proj2 (inbetween_float_bounds _ _ _ _ _ H1a)).
(* . *)
assert (Br: inbetween_float radix2 m1' e1 (Rabs (round radix2 fexp (round_mode m) x)) loc_Exact).
now apply inbetween_Exact.
destruct m1' as [|m1'|m1'].
(* . m1' = 0 *)
rewrite shr_truncate. 2: apply Zle_refl.
generalize (truncate_0 radix2 fexp e1 loc_Exact).
destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2).
rewrite shr_m_shr_record_of_loc.
intros Hm2.
rewrite Hm2.
repeat split.
rewrite Rlt_bool_true.
repeat split.
apply sym_eq.
case Rlt_bool ; apply F2R_0.
rewrite <- F2R_Zabs, abs_cond_Zopp, F2R_0.
apply bpow_gt_0.
(* . 0 < m1' *)
assert (He: (e1 <= fexp (Zdigits radix2 (Zpos m1') + e1))%Z).
rewrite <- mag_F2R_Zdigits, <- Hr, mag_abs.
2: discriminate.
rewrite H1b.
rewrite cexp_abs.
fold (cexp radix2 fexp (round radix2 fexp (round_mode m) x)).
apply cexp_round_ge...
rewrite H1c.
case (Rlt_bool x 0).
apply Rlt_not_eq.
now apply F2R_lt_0.
apply Rgt_not_eq.
now apply F2R_gt_0.
refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Br He)).
2: now rewrite Hr ; apply F2R_gt_0.
refine (_ (truncate_correct_format radix2 fexp (Zpos m1') e1 _ _ He)).
2: discriminate.
rewrite shr_truncate. 2: easy.
destruct (truncate radix2 fexp (Zpos m1', e1, loc_Exact)) as ((m2, e2), l2).
rewrite shr_m_shr_record_of_loc.
intros (H3,H4) (H2,_).
destruct m2 as [|m2|m2].
elim Rgt_not_eq with (2 := H3).
rewrite F2R_0.
now apply F2R_gt_0.
rewrite F2R_cond_Zopp, H3, abs_cond_Ropp, <- F2R_abs.
simpl Zabs.
case_eq (Zle_bool e2 (emax - prec)) ; intros He2.
assert (bounded m2 e2 = true).
apply andb_true_intro.
split.
unfold canonical_mantissa.
apply Zeq_bool_true.
rewrite Zpos_digits2_pos.
rewrite <- mag_F2R_Zdigits.
apply sym_eq.
now rewrite H3 in H4.
discriminate.
exact He2.
apply (conj H).
rewrite Rlt_bool_true.
repeat split.
apply F2R_cond_Zopp.
now apply bounded_lt_emax.
rewrite (Rlt_bool_false _ (bpow radix2 emax)).
refine (conj _ (refl_equal _)).
unfold binary_overflow.
case overflow_to_inf.
apply refl_equal.
unfold valid_binary, bounded.
rewrite Zle_bool_refl.
rewrite Bool.andb_true_r.
apply Zeq_bool_true.
rewrite Zpos_digits2_pos.
replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec.
unfold fexp, FLT_exp, emin.
generalize (prec_gt_0 prec).
clear -Hmax ; zify ; omega.
change 2%Z with (radix_val radix2).
case_eq (Zpower radix2 prec - 1)%Z.
simpl Zdigits.
generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)).
clear ; omega.
intros p Hp.
apply Zle_antisym.
cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; omega.
apply Zdigits_gt_Zpower.
simpl Zabs. rewrite <- Hp.
cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; omega.
apply lt_IZR.
rewrite 2!IZR_Zpower. 2: now apply Zlt_le_weak.
apply bpow_lt.
apply Zlt_pred.
now apply Zlt_0_le_0_pred.
apply Zdigits_le_Zpower.
simpl Zabs. rewrite <- Hp.
apply Zlt_pred.
intros p Hp.
generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)).
clear -Hp ; zify ; omega.
apply Rnot_lt_le.
intros Hx.
generalize (refl_equal (bounded m2 e2)).
unfold bounded at 2.
rewrite He2.
rewrite Bool.andb_false_r.
rewrite bounded_canonical_lt_emax with (2 := Hx).
discriminate.
unfold canonical.
now rewrite <- H3.
elim Rgt_not_eq with (2 := H3).
apply Rlt_trans with R0.
now apply F2R_lt_0.
now apply F2R_gt_0.
rewrite <- Hr.
apply generic_format_abs...
apply generic_format_round...
(* . not m1' < 0 *)
elim Rgt_not_eq with (2 := Hr).
apply Rlt_le_trans with R0.
now apply F2R_lt_0.
apply Rabs_pos.
(* *)
apply Rlt_le_trans with (2 := proj1 (inbetween_float_bounds _ _ _ _ _ Bx)).
now apply F2R_gt_0.
(* all the modes are valid *)
clear. case m.
exact inbetween_int_NE_sign.
exact inbetween_int_ZR_sign.
exact inbetween_int_DN_sign.
exact inbetween_int_UP_sign.
exact inbetween_int_NA_sign.
Qed.
Theorem binary_round_aux_correct :
forall mode x mx ex lx,
inbetween_float radix2 (Zpos mx) ex (Rabs x) lx ->
......
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