(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010-2018 Sylvie Boldo
#<br />#
Copyright (C) 2010-2018 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(** * Helper function for computing the rounded value of a real number. *)

Require Import Core Digits Float_prop Bracket.
Section Fcalc_round.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Section Fcalc_round_fexp.
Variable fexp : Z -> Z.
Context { valid_exp : Valid_exp fexp }.
Notation format := (generic_format beta fexp).
Proof.
Admitted.
Proof.
intros x m e l Px Bx He.
unfold cexp.
apply inbetween_float_bounds in Bx.
assert (0 <= m)%Z as Hm.
{
apply Zlt_succ_le.
eapply gt_0_F2R.
apply Rlt_trans with (1 := Px).
apply Bx.
}
{
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|<-].
{
erewrite <- mag_F2R_bounds_Zdigits with (1 := Hm').
{
easy.
}
{
easy.
}
}
{
clear Hm.
assert (mag beta x <= e)%Z as Hx.
{
apply mag_le_bpow.
{
apply Rgt_not_eq.
easy.
}
{
rewrite Rabs_pos_eq.
{
rewrite <- F2R_bpow.
easy.
}
{
apply Rlt_le.
easy.
}
}
}
{
simpl in He |- *.
clear Bx.
destruct He as [He|He].
{
apply eq_sym, valid_exp with (2 := He).
apply Z.le_trans with e.
{
easy.
}
{
easy.
}
}
{
apply valid_exp with (1 := He).
apply Z.le_trans with e.
{
easy.
}
{
easy.
}
}
}
}
}
Qed.
Proof.
Admitted.
Proof.
intros x m e l Px Bx.
destruct Px as [Px|Px].
{
split.
{
intros [H|H].
{
left.
rewrite <- cexp_inbetween_float with (1 := Px) (2 := Bx).
{
exact H.
}
{
left.
easy.
}
}
{
right.
easy.
}
}
{
intros [H|H].
{
left.
rewrite cexp_inbetween_float with (1 := Px) (2 := Bx).
{
exact H.
}
{
right.
easy.
}
}
{
right.
easy.
}
}
}
{
assert (H := Bx).
destruct Bx as [|c Bx _].
{
split.
{
right.
easy.
}
{
right.
easy.
}
}
{
rewrite <- Px in Bx.
destruct Bx as [Bx1 Bx2].
apply lt_0_F2R in Bx1.
apply gt_0_F2R in Bx2.
omega.
}
}
Qed.
Proof.
Admitted.
Proof.
intros rnd choice Hc x m l e Hl.
unfold round.
unfold F2R.
simpl.
apply (f_equal (fun m => (IZR m * bpow e)%R)).
apply Hc.
apply inbetween_mult_reg with (bpow e).
{
apply bpow_gt_0.
}
{
rewrite scaled_mantissa_mult_bpow.
easy.
}
Qed.
Definition cond_incr (b : bool) m := if b then (m + 1)%Z else m.
Proof.
Admitted.
Proof.
intros rnd choice Hc x m l e Hx.
apply (f_equal (fun m => (IZR m * bpow e)%R)).
simpl.
replace (Rlt_bool x 0) with (Rlt_bool (scaled_mantissa beta fexp x) 0).
{
(* *)
    apply Hc.
apply inbetween_mult_reg with (bpow e).
{
apply bpow_gt_0.
}
{
rewrite <- (Rabs_right (bpow e)) at 3.
{
rewrite <- Rabs_mult.
rewrite scaled_mantissa_mult_bpow.
easy.
}
{
apply Rle_ge.
apply bpow_ge_0.
}
}
}
{
(* *)
    destruct (Rlt_bool_spec x 0) as [Zx|Zx].
{
simpl.
apply Rlt_bool_true.
rewrite <- (Rmult_0_l (bpow (-e))).
apply Rmult_lt_compat_r with (2 := Zx).
apply bpow_gt_0.
}
{
simpl.
apply Rlt_bool_false.
apply Rmult_le_pos with (1 := Zx).
apply bpow_ge_0.
}
}
Qed.
Proof.
Admitted.
Proof.
intros x m l Hl.
refine (Zfloor_imp m _ _).
apply inbetween_bounds with (2 := Hl).
apply IZR_lt.
apply Zlt_succ.
Qed.
Proof.
Admitted.
Proof.
apply inbetween_float_round with (choice := fun m l => m).
exact inbetween_int_DN.
Qed.
Definition round_sign_DN s l :=
  match l with
  | loc_Exact => false
  | _ => s
  end.
Proof.
Admitted.
Proof.
intros x m l Hl.
unfold Rabs in Hl.
destruct (Rcase_abs x) as [Zx|Zx] .
{
(* *)
    rewrite Rlt_bool_true with (1 := Zx).
inversion_clear Hl.
{
simpl.
rewrite <- (Ropp_involutive x).
rewrite H.
rewrite  <- opp_IZR.
apply Zfloor_IZR.
}
{
simpl.
apply Zfloor_imp.
split.
{
apply Rlt_le.
rewrite opp_IZR.
apply Ropp_lt_cancel.
rewrite Ropp_involutive.
easy.
}
{
ring_simplify (- (m + 1) + 1)%Z.
rewrite opp_IZR.
apply Ropp_lt_cancel.
rewrite Ropp_involutive.
easy.
}
}
}
{
(* *)
    rewrite Rlt_bool_false.
{
inversion_clear Hl.
{
simpl.
rewrite H.
apply Zfloor_IZR.
}
{
simpl.
apply Zfloor_imp.
split.
{
apply Rlt_le.
easy.
}
{
apply H.
}
}
}
{
apply Rge_le.
easy.
}
}
Qed.
Proof.
Admitted.
Proof.
apply inbetween_float_round_sign with (choice := fun s m l => cond_incr (round_sign_DN s l) m).
exact inbetween_int_DN_sign.
Qed.
(** Relates location and rounding up. *)

Definition round_UP l :=
  match l with
  | loc_Exact => false
  | _ => true
  end.
Proof.
Admitted.
Proof.
intros x m l Hl.
assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)).
{
case l.
{
try ((left ; easy)).
}
{
try ((left ; easy)).
right.
split.
{
easy.
}
{
easy.
}
}
}
{
destruct Hl' as [Hl'|(Hl1, Hl2)].
{
(* Exact *)
      rewrite Hl'.
destruct Hl.
{
try easy.
rewrite H.
exact (Zceil_IZR _).
}
{
try easy.
}
}
{
(* 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.
Proof.
Admitted.
Proof.
apply inbetween_float_round with (choice := fun m l => cond_incr (round_UP l) m).
exact inbetween_int_UP.
Qed.
Definition round_sign_UP s l :=
  match l with
  | loc_Exact => false
  | _ => negb s
  end.
Proof.
Admitted.
Proof.
intros x m l Hl.
unfold Rabs in Hl.
destruct (Rcase_abs x) as [Zx|Zx] .
{
(* *)
    rewrite Rlt_bool_true with (1 := Zx).
simpl.
unfold Zceil.
apply f_equal.
inversion_clear Hl.
{
simpl.
rewrite H.
apply Zfloor_IZR.
}
{
simpl.
apply Zfloor_imp.
split.
{
apply Rlt_le.
easy.
}
{
apply H.
}
}
}
{
(* *)
    rewrite Rlt_bool_false.
{
simpl.
inversion_clear Hl.
{
simpl.
rewrite H.
apply Zceil_IZR.
}
{
simpl.
apply Zceil_imp.
split.
{
change (m + 1 - 1)%Z with (Z.pred (Z.succ m)).
rewrite <- Zpred_succ.
easy.
}
{
apply Rlt_le.
easy.
}
}
}
{
apply Rge_le.
easy.
}
}
Qed.
Proof.
Admitted.
Proof.
apply inbetween_float_round_sign with (choice := fun s m l => cond_incr (round_sign_UP s l) m).
exact inbetween_int_UP_sign.
Qed.
(** Relates location and rounding toward zero. *)

Definition round_ZR (s : bool) l :=
  match l with
  | loc_Exact => false
  | _ => s
  end.
Proof.
Admitted.
Proof with auto with typeclass_instances.
intros x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
rewrite Zrnd_IZR...
(* not Exact *)
unfold Ztrunc.
assert (Hm: Zfloor x = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
rewrite Zceil_floor_neq.
rewrite Hm.
unfold cond_incr.
simpl.
case Rlt_bool_spec ; intros Hx' ;
  case Zlt_bool_spec ; intros Hm' ; try apply refl_equal.
elim Rlt_not_le with (1 := Hx').
apply Rlt_le.
apply Rle_lt_trans with (2 := proj1 Hx).
now apply IZR_le.
elim Rle_not_lt with (1 := Hx').
apply Rlt_le_trans with (1 := proj2 Hx).
apply IZR_le.
now apply Zlt_le_succ.
rewrite Hm.
now apply Rlt_not_eq.
Qed.
Proof.
Admitted.
Proof.
apply inbetween_float_round with (choice := fun m l => cond_incr (round_ZR (Zlt_bool m 0) l) m).
exact inbetween_int_ZR.
Qed.
Proof.
Admitted.
Proof.
intros x m l Hl.
simpl.
unfold Ztrunc.
destruct (Rlt_le_dec x 0) as [Zx|Zx].
{
(* *)
    rewrite Rlt_bool_true with (1 := Zx).
simpl.
unfold Zceil.
apply f_equal.
apply Zfloor_imp.
rewrite <- Rabs_left with (1 := Zx).
apply inbetween_bounds with (2 := Hl).
apply IZR_lt.
apply Zlt_succ.
}
{
(* *)
    rewrite Rlt_bool_false with (1 := Zx).
simpl.
apply Zfloor_imp.
rewrite <- Rabs_pos_eq with (1 := Zx).
apply inbetween_bounds with (2 := Hl).
apply IZR_lt.
apply Zlt_succ.
}
Qed.
Proof.
Admitted.
Proof.
apply inbetween_float_round_sign with (choice := fun s m l => m).
exact inbetween_int_ZR_sign.
Qed.
(** Relates location and rounding to nearest. *)

Definition round_N (p : bool) l :=
  match l with
  | loc_Exact => false
  | loc_Inexact Lt => false
  | loc_Inexact Eq => p
  | loc_Inexact Gt => true
  end.
Proof.
Admitted.
Proof with auto with typeclass_instances.
intros choice x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
rewrite Zrnd_IZR...
(* not Exact *)
unfold 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 - IZR m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite plus_IZR.
rewrite <- (Rcompare_plus_r (- IZR m) x).
apply f_equal.
field.
rewrite Hm.
now apply Rlt_not_eq.
Qed.
Proof.
Admitted.
Proof with auto with typeclass_instances.
intros choice x m l Hl.
simpl.
unfold Rabs in Hl.
destruct (Rcase_abs x) as [Zx|Zx].
(* *)
rewrite Rlt_bool_true with (1 := Zx).
simpl.
rewrite <- (Ropp_involutive x).
rewrite Znearest_opp.
apply f_equal.
inversion_clear Hl as [Hx|l' Hx Hl'].
rewrite Hx.
apply Zrnd_IZR...
assert (Hm: Zfloor (-x) = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
unfold Znearest.
rewrite Zceil_floor_neq.
rewrite Hm.
replace (Rcompare (- x - IZR m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite plus_IZR.
rewrite <- (Rcompare_plus_r (- IZR m) (-x)).
apply f_equal.
field.
rewrite Hm.
now apply Rlt_not_eq.
(* *)
generalize (Rge_le _ _ Zx).
clear Zx.
intros Zx.
rewrite Rlt_bool_false with (1 := Zx).
simpl.
inversion_clear Hl as [Hx|l' Hx Hl'].
rewrite Hx.
apply Zrnd_IZR...
assert (Hm: Zfloor x = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
unfold Znearest.
rewrite Zceil_floor_neq.
rewrite Hm.
replace (Rcompare (x - IZR m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite plus_IZR.
rewrite <- (Rcompare_plus_r (- IZR m) x).
apply f_equal.
field.
rewrite Hm.
now apply Rlt_not_eq.
Qed.
Proof.
intros x.
unfold inbetween_int.
intros m.
apply inbetween_int_N.
Qed.
Proof.
intros x m l Hl.
apply inbetween_int_N with (choice := fun x => negb (Z.even x)).
easy.
Qed.
Proof.
Admitted.
Proof.
apply inbetween_float_round with (choice := fun m l => cond_incr (round_N (negb (Z.even m)) l) m).
exact inbetween_int_NE.
Qed.
Proof.
Admitted.
Proof.
intros x m l Hl.
erewrite inbetween_int_N_sign with (choice := fun x => negb (Z.even x)).
{
apply f_equal.
case Rlt_bool.
{
rewrite Z.even_opp.
rewrite  Z.even_add.
case (Z.even m).
{
easy.
}
{
easy.
}
}
{
apply refl_equal.
}
}
{
eexact Hl.
}
Qed.
Proof.
Admitted.
Proof.
apply inbetween_float_round_sign with (choice := fun s m l => cond_incr (round_N (negb (Z.even m)) l) m).
exact inbetween_int_NE_sign.
Qed.
Proof.
intros.
apply inbetween_int_N.
eauto.
Qed.
Proof.
intros x m l Hl.
apply inbetween_int_N with (choice := fun x => Zle_bool 0 x).
easy.
Qed.
Proof.
Admitted.
Proof.
apply inbetween_float_round with (choice := fun m l => cond_incr (round_N (Zle_bool 0 m) l) m).
exact inbetween_int_NA.
Qed.
Proof.
Admitted.
Proof.
intros x m l Hl.
erewrite inbetween_int_N_sign with (choice := Zle_bool 0).
{
apply f_equal.
assert (Hm: (0 <= m)%Z).
{
apply Zlt_succ_le.
apply lt_IZR.
apply Rle_lt_trans with (Rabs x).
{
apply Rabs_pos.
}
{
refine (proj2 (inbetween_bounds _ _ _ _ _ Hl)).
apply IZR_lt.
apply Zlt_succ.
}
}
{
rewrite Zle_bool_true with (1 := Hm).
rewrite Zle_bool_false.
{
case Rlt_bool.
{
easy.
}
{
easy.
}
}
{
omega.
}
}
}
{
eexact Hl.
}
Qed.
Definition truncate_aux t k :=
  let '(m, e, l) := t in
  let p := Zpower beta k in
  (Z.div m p, (e + k)%Z, new_location p (Zmod m p) l).
Proof.
Admitted.
Proof.
intros ((m,e),l) k1 k2 Hk1 Hk2.
unfold truncate_aux.
destruct (inbetween_float_ex beta m e l) as (x,Hx).
assert (B1 := inbetween_float_new_location _ _ _ _ _ _ Hk1 Hx).
assert (Hk3: (0 < k1 + k2)%Z).
change Z0 with (0 + 0)%Z.
now apply Zplus_lt_compat.
assert (B3 := inbetween_float_new_location _ _ _ _ _ _ Hk3 Hx).
assert (B2 := inbetween_float_new_location _ _ _ _ _ _ Hk2 B1).
rewrite Zplus_assoc in B3.
destruct (inbetween_float_unique _ _ _ _ _ _ _ B2 B3).
now rewrite H, H0, Zplus_assoc.
Qed.
(** Given a triple (mantissa, exponent, position), this function
    computes a triple with a canonic exponent, assuming the
    original triple had enough precision. *)

Definition truncate t :=
  let '(m, e, l) := t in
  let k := (fexp (Zdigits beta m + e) - e)%Z in
  if Zlt_bool 0 k then truncate_aux t k
  else t.
Proof.
Admitted.
Proof.
intros e l.
unfold truncate.
case Zlt_bool.
{
simpl.
apply Zdiv_0_l.
}
{
apply refl_equal.
}
Qed.
Proof.
Admitted.
Proof.
intros m e l Hm.
unfold truncate.
set (k := (fexp (Zdigits beta m + e) - e)%Z).
case Zlt_bool_spec.
{
intros Hk.
(* *)
    unfold truncate_aux.
apply generic_format_F2R.
intros Hd.
unfold cexp.
rewrite mag_F2R_Zdigits with (1 := Hd).
rewrite Zdigits_div_Zpower with (1 := Hm).
{
replace (Zdigits beta m - k + (e + k))%Z with (Zdigits beta m + e)%Z by ring.
unfold k.
ring_simplify.
apply Z.le_refl.
}
{
split.
{
apply Zlt_le_weak.
easy.
}
{
apply Znot_gt_le.
contradict Hd.
apply Zdiv_small.
apply conj with (1 := Hm).
rewrite <- Z.abs_eq with (1 := Hm).
apply Zpower_gt_Zdigits.
apply Zlt_le_weak.
apply Z.gt_lt.
easy.
}
}
}
{
intros Hk.
(* *)
    destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
{
apply generic_format_F2R.
unfold cexp.
rewrite mag_F2R_Zdigits.
{
unfold k in Hk.
clear -Hk.
omega.
}
{
apply Zgt_not_eq.
easy.
}
}
{
rewrite <- Hm'.
rewrite  F2R_0.
apply generic_format_0.
}
}
Qed.
Proof.
Admitted.
Proof.
intros m e Hm x Fx He.
assert (Hc: cexp beta fexp x = fexp (Zdigits beta m + e)).
{
unfold cexp.
unfold x.
rewrite mag_F2R_Zdigits.
{
easy.
}
{
easy.
}
}
{
unfold truncate.
rewrite <- Hc.
set (k := (cexp beta fexp x - e)%Z).
case Zlt_bool_spec.
{
intros Hk.
(* *)
      unfold truncate_aux.
rewrite Fx at 1.
assert (H: (e + k)%Z = cexp beta fexp x).
{
unfold k.
ring.
}
{
refine (conj _ H).
rewrite <- H.
apply F2R_eq.
replace (scaled_mantissa beta fexp x) with (IZR (Zfloor (scaled_mantissa beta fexp x))).
{
rewrite Ztrunc_IZR.
unfold scaled_mantissa.
rewrite <- H.
unfold x.
unfold F2R.
simpl.
rewrite Rmult_assoc.
rewrite  <- bpow_plus.
ring_simplify (e + - (e + k))%Z.
clear -Hm Hk.
destruct k as [|k|k].
{
try easy.
}
{
try easy.
simpl.
apply Zfloor_div.
intros H.
generalize (Zpower_pos_gt_0 beta k) (Zle_bool_imp_le _ _ (radix_prop beta)).
omega.
}
{
try easy.
}
}
{
rewrite scaled_mantissa_generic with (1 := Fx).
rewrite Zfloor_IZR.
easy.
}
}
}
{
intros Hk.
(* *)
      split.
{
apply refl_equal.
}
{
unfold k in Hk.
omega.
}
}
}
Qed.
Proof.
Admitted.
Proof.
intros x m e l Hx H1 H2.
unfold truncate.
rewrite <- cexp_inbetween_float with (1 := Hx) (2 := H1).
{
idtac.
generalize (Zlt_cases 0 (cexp beta fexp x - e)).
destruct Zlt_bool.
{
intros Hk.
split.
{
apply inbetween_float_new_location.
{
easy.
}
{
easy.
}
}
{
ring.
}
}
{
intros Hk.
apply (conj H1).
omega.
}
}
{
left.
easy .
}
Qed.
Proof.
Admitted.
Proof.
intros x m e l Hx H1 H2.
apply truncate_correct_partial' with (1 := Hx) (2 := H1).
rewrite cexp_inbetween_float with (1 := Hx) (2 := H1).
{
exact H2.
}
{
right.
easy.
}
Qed.
Proof.
Admitted.
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).
left.
easy.
}
{
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).
left.
easy.
}
{
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).
apply Zlt_le_weak.
easy.
}
}
}
}
{
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 gt_0_F2R with (1 := proj2 Hx').
}
}
}
}
{
rewrite Hm  in H1 |- *.
rewrite  <- Hx in H1 |- *.
clear -H1.
destruct H1 as [_ | l' [H _] _].
{
assert (exists e', truncate (Z0, e, loc_Exact) = (Z0, e', loc_Exact)).
{
unfold truncate.
unfold truncate_aux.
case Zlt_bool.
{
rewrite Zdiv_0_l.
rewrite  Zmod_0_l.
eexists.
apply f_equal.
unfold new_location.
case Z.even.
{
easy.
}
{
easy.
}
}
{
eexists.
easy.
}
}
{
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.
Proof.
Admitted.
Proof.
intros x m e l Hx H1 H2.
apply truncate_correct' with (1 := Hx) (2 := H1).
apply cexp_inbetween_float_loc_Exact with (2 := H1).
{
easy.
}
{
easy.
}
Qed.
Section round_dir.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Variable choice : Z -> location -> Z.
Hypothesis inbetween_int_valid :
  forall x m l,
  inbetween_int m x l ->
  rnd x = choice m l.
Proof.
Admitted.
Proof with auto with typeclass_instances.
intros x m e l Hin [He|(Hl,Hf)].
rewrite He in Hin |- *.
apply inbetween_float_round with (2 := Hin).
exact inbetween_int_valid.
rewrite Hl in Hin.
inversion_clear Hin.
rewrite Hl.
replace (choice m loc_Exact) with m.
rewrite <- H.
apply round_generic...
rewrite <- (Zrnd_IZR rnd m) at 1.
apply inbetween_int_valid.
now constructor.
Qed.
Proof.
Admitted.
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).
apply round_any_correct.
{
easy.
}
{
easy.
}
Qed.
Proof.
Admitted.
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].
apply round_any_correct.
{
easy.
}
{
easy.
}
Qed.
End round_dir.
Section round_dir_sign.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Variable choice : bool -> Z -> location -> Z.
Hypothesis inbetween_int_valid :
  forall x m l,
  inbetween_int m (Rabs x) l ->
  rnd x = cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l).
Proof.
Admitted.
Proof with auto with typeclass_instances.
intros x m e l Hin [He|(Hl,Hf)].
rewrite He in Hin |- *.
apply inbetween_float_round_sign with (2 := Hin).
exact inbetween_int_valid.
rewrite Hl in Hin.
inversion_clear Hin.
rewrite Hl.
replace (choice (Rlt_bool x 0) m loc_Exact) with m.
(* *)
unfold Rabs in H.
destruct (Rcase_abs x) as [Zx|Zx].
rewrite Rlt_bool_true with (1 := Zx).
simpl.
rewrite F2R_Zopp.
rewrite <- H, Ropp_involutive.
apply round_generic...
rewrite Rlt_bool_false.
simpl.
rewrite <- H.
now apply round_generic.
now apply Rge_le.
(* *)
destruct (Rlt_bool_spec x 0) as [Zx|Zx].
(* . *)
apply Z.opp_inj.
change (- m = cond_Zopp true (choice true m loc_Exact))%Z.
rewrite <- (Zrnd_IZR rnd (-m)) at 1.
assert (IZR (-m) < 0)%R.
rewrite opp_IZR.
apply Ropp_lt_gt_0_contravar.
apply IZR_lt.
apply gt_0_F2R with beta e.
rewrite <- H.
apply Rabs_pos_lt.
now apply Rlt_not_eq.
rewrite <- Rlt_bool_true with (1 := H0).
apply inbetween_int_valid.
constructor.
rewrite Rabs_left with (1 := H0).
rewrite opp_IZR.
apply Ropp_involutive.
(* . *)
change (m = cond_Zopp false (choice false m loc_Exact))%Z.
rewrite <- (Zrnd_IZR rnd m) at 1.
assert (0 <= IZR m)%R.
apply IZR_le.
apply ge_0_F2R with beta e.
rewrite <- H.
apply Rabs_pos.
rewrite <- Rlt_bool_false with (1 := H0).
apply inbetween_int_valid.
constructor.
now apply Rabs_pos_eq.
Qed.
Proof.
Admitted.
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.
rewrite <- cexp_abs.
easy.
}
{
right.
apply (conj H2).
apply generic_format_abs_inv.
easy.
}
}
Qed.
Proof.
Admitted.
Proof.
intros x m e l Hl He.
apply round_trunc_sign_any_correct' with (1 := Hl).
rewrite <- cexp_abs.
apply cexp_inbetween_float_loc_Exact with (2 := Hl) (3 := He).
apply Rabs_pos.
Qed.
End round_dir_sign.
(** * Instances of the theorems above, for the usual rounding modes. *)

Definition round_DN_correct :=
  round_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_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. *)

Variable emin : Z.
Definition truncate_FIX t :=
  let '(m, e, l) := t in
  let k := (emin - e)%Z in
  if Zlt_bool 0 k then
    let p := Zpower beta k in
    (Z.div m p, (e + k)%Z, new_location p (Zmod m p) l)
  else t.
Proof.
Admitted.
Proof.
intros x m e l H1 H2.
unfold truncate_FIX.
set (k := (emin - e)%Z).
set (p := Zpower beta k).
unfold cexp.
unfold FIX_exp.
generalize (Zlt_cases 0 k).
case (Zlt_bool 0 k).
{
intros Hk.
(* shift *)
    split.
{
apply inbetween_float_new_location.
{
easy.
}
{
easy.
}
}
{
clear H2.
left.
unfold k.
ring.
}
}
{
intros Hk.
(* no shift *)
    split.
{
exact H1.
}
{
unfold k in Hk.
destruct H2 as [H2|H2].
{
left.
omega.
}
{
right.
split.
{
exact H2.
}
{
rewrite H2 in H1.
inversion_clear H1.
rewrite H.
apply generic_format_F2R.
unfold cexp.
omega.
}
}
}
}
Qed.
End Fcalc_round.