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

Copyright (C) 2010-2013 Sylvie Boldo
#<br />#
Copyright (C) 2010-2013 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 Fcore.
Require Import Fcore_digits.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.

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).

(** Relates location and rounding. *)

Theorem inbetween_float_round :
  forall rnd choice,
  ( forall x m l, inbetween_int m x l -> rnd x = choice m l ) ->
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e x l ->
  round beta fexp rnd x = F2R (Float beta (choice m l) e).
Proof.
(* Goal: forall (rnd : forall _ : R, Z) (choice : forall (_ : Z) (_ : location), Z) (_ : forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (rnd x) (choice m l)) (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e x l, @eq R (round beta fexp rnd x) (@F2R beta (Float beta (choice m l) e)) *)
intros rnd choice Hc x m l e Hl.
(* Goal: @eq R (round beta fexp rnd x) (@F2R beta (Float beta (choice m l) e)) *)
unfold round, F2R. simpl.
(* Goal: @eq R (round beta fexp rnd x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m l)) e)) *)
apply (f_equal (fun m => (Z2R m * bpow e)%R)).
(* Goal: @eq Z (rnd (scaled_mantissa beta fexp x)) (cond_Zopp (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (choice (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) m l)) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (Rlt_bool x (IZR Z0)) *)
apply Hc.
(* Goal: inbetween_int m (Rabs (scaled_mantissa beta fexp x)) l *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (Rlt_bool x (IZR Z0)) *)
apply inbetween_mult_reg with (bpow e).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.opp e)) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) false *)
apply bpow_gt_0.
(* Goal: inbetween (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add m (Zpos xH))) (Fcore_Raux.bpow beta e)) (Rabs (Rmult (scaled_mantissa beta fexp x) (Fcore_Raux.bpow beta e))) l *)
(* Goal: Rge (Fcore_Raux.bpow beta e) (IZR Z0) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (Rlt_bool x (IZR Z0)) *)
now rewrite scaled_mantissa_mult_bpow.
Qed.

Definition cond_incr (b : bool) m := if b then (m + 1)%Z else m.

Theorem inbetween_float_round_sign :
  forall rnd choice,
  ( 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) ) ->
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e (Rabs x) l ->
  round beta fexp rnd x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l)) e).
Proof.
(* Goal: forall (rnd : forall _ : R, Z) (choice : forall (_ : bool) (_ : Z) (_ : location), Z) (_ : forall (x : R) (m : Z) (l : location) (_ : inbetween_int m (Rabs x) l), @eq Z (rnd x) (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m l))) (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e (Rabs x) l, @eq R (round beta fexp rnd x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m l)) e)) *)
intros rnd choice Hc x m l e Hx.
(* Goal: @eq R (round beta fexp rnd x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m l)) e)) *)
apply (f_equal (fun m => (Z2R m * bpow e)%R)).
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (rnd (scaled_mantissa beta fexp x)) (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m l)) *)
replace (Rlt_bool x 0) with (Rlt_bool (scaled_mantissa beta fexp x) 0).
(* *)
(* Goal: @eq Z (rnd (scaled_mantissa beta fexp x)) (cond_Zopp (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (choice (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) m l)) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (Rlt_bool x (IZR Z0)) *)
apply Hc.
(* Goal: inbetween_int m (Rabs (scaled_mantissa beta fexp x)) l *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (Rlt_bool x (IZR Z0)) *)
apply inbetween_mult_reg with (bpow e).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.opp e)) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) false *)
apply bpow_gt_0.
(* Goal: inbetween (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add m (Zpos xH))) (Fcore_Raux.bpow beta e)) (Rmult (Rabs (scaled_mantissa beta fexp x)) (Fcore_Raux.bpow beta e)) l *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (Rlt_bool x (IZR Z0)) *)
rewrite <- (Rabs_right (bpow e)) at 3.
(* Goal: inbetween (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add m (Zpos xH))) (Fcore_Raux.bpow beta e)) (Rmult (Rabs (scaled_mantissa beta fexp x)) (Rabs (Fcore_Raux.bpow beta e))) l *)
(* Goal: Rge (Fcore_Raux.bpow beta e) (IZR Z0) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (Rlt_bool x (IZR Z0)) *)
rewrite <- Rabs_mult.
(* Goal: inbetween (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Rmult (Z2R (Z.add m (Zpos xH))) (Fcore_Raux.bpow beta e)) (Rabs (Rmult (scaled_mantissa beta fexp x) (Fcore_Raux.bpow beta e))) l *)
(* Goal: Rge (Fcore_Raux.bpow beta e) (IZR Z0) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (Rlt_bool x (IZR Z0)) *)
now rewrite scaled_mantissa_mult_bpow.
(* Goal: Rge (Fcore_Raux.bpow beta e) (IZR Z0) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) (Rlt_bool x (IZR Z0)) *)
apply Rle_ge.
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta fexp x))) *)
apply bpow_ge_0.
(* *)
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
destruct (Rlt_bool_spec x 0) as [Zx|Zx] ; simpl.
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) true *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) false *)
apply Rlt_bool_true.
(* Goal: Rlt (scaled_mantissa beta fexp x) (IZR Z0) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) false *)
rewrite <- (Rmult_0_l (bpow (-e))).
(* Goal: Rlt (scaled_mantissa beta fexp x) (Rmult (IZR Z0) (Fcore_Raux.bpow beta (Z.opp e))) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) false *)
apply Rmult_lt_compat_r with (2 := Zx).
(* Goal: Rlt (IZR Z0) (Fcore_Raux.bpow beta (Z.opp e)) *)
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) false *)
apply bpow_gt_0.
(* Goal: @eq bool (Rlt_bool (scaled_mantissa beta fexp x) (IZR Z0)) false *)
apply Rlt_bool_false.
(* Goal: Rle (IZR Z0) (scaled_mantissa beta fexp x) *)
apply Rmult_le_pos with (1 := Zx).
(* Goal: Rle (IZR Z0) (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta fexp x))) *)
apply bpow_ge_0.
Qed.

(** Relates location and rounding down. *)

Theorem inbetween_int_DN :
  forall x m l,
  inbetween_int m x l ->
  Zfloor x = m.
Proof.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
(* Goal: @eq Z (Zfloor x) m *)
refine (Zfloor_imp m _ _).
(* Goal: and (Rle (Z2R m) (Rabs x)) (Rlt (Rabs x) (Z2R (Z.add m (Zpos xH)))) *)
apply inbetween_bounds with (2 := Hl).
(* Goal: Rlt (Z2R m) (Z2R (Z.add m (Zpos xH))) *)
apply Z2R_lt.
(* Goal: Z.lt m (Z.add m (Zpos xH)) *)
apply Zlt_succ.
Qed.

Theorem inbetween_float_DN :
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e x l ->
  round beta fexp Zfloor x = F2R (Float beta m e).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e x l, @eq R (round beta fexp Zfloor x) (@F2R beta (Float beta m e)) *)
apply inbetween_float_round with (choice := fun m l => m).
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Zfloor x) m *)
exact inbetween_int_DN.
Qed.

Definition round_sign_DN s l :=
  match l with
  | loc_Exact => false
  | _ => s
  end.

Theorem inbetween_int_DN_sign :
  forall x m l,
  inbetween_int m (Rabs x) l ->
  Zfloor x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_sign_DN (Rlt_bool x 0) l) m).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
unfold Rabs in Hl.
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
destruct (Rcase_abs x) as [Zx|Zx] .
(* *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
rewrite Rlt_bool_true with (1 := Zx).
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
inversion_clear Hl ; simpl.
(* Goal: @eq Z (Zfloor x) (Z.opp m) *)
(* Goal: @eq Z (Zfloor x) (Z.opp (Z.add m (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite <- (Ropp_involutive x).
(* Goal: @eq Z (Zfloor (Ropp (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (Zfloor x) (Z.opp (Z.add m (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite H, <- Z2R_opp.
(* Goal: @eq Z (Zfloor (Z2R m)) m *)
(* Goal: @eq Z (Zfloor (Ropp x)) m *)
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
apply Zfloor_Z2R.
(* Goal: @eq Z (Zfloor x) m *)
apply Zfloor_imp.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: Rle (Z2R (Z.opp (Z.add m (Zpos xH)))) x *)
(* Goal: Rlt x (Z2R (Z.add (Z.opp (Z.add m (Zpos xH))) (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
apply Rlt_le.
(* Goal: Rlt x (Z2R (Z.opp m)) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite Z2R_opp.
(* Goal: Rlt x (Ropp (Z2R m)) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
apply Ropp_lt_cancel.
(* Goal: Rlt (Ropp (Ropp (Z2R m))) (Ropp x) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
now rewrite Ropp_involutive.
(* Goal: Rlt x (Z2R (Z.add (Z.opp (Z.add m (Zpos xH))) (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
ring_simplify (- (m + 1) + 1)%Z.
(* Goal: Rlt x (Z2R (Z.opp m)) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite Z2R_opp.
(* Goal: Rlt x (Ropp (Z2R m)) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
apply Ropp_lt_cancel.
(* Goal: Rlt (Ropp (Ropp (Z2R m))) (Ropp x) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
now rewrite Ropp_involutive.
(* *)
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite Rlt_bool_false.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
inversion_clear Hl ; simpl.
(* Goal: generic_format beta (fun _ : Z => emin) x *)
rewrite H.
(* Goal: @eq Z (Zfloor (Z2R m)) m *)
(* Goal: @eq Z (Zfloor (Ropp x)) m *)
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
apply Zfloor_Z2R.
(* Goal: @eq Z (Zfloor x) m *)
apply Zfloor_imp.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: Rle (Z2R (Z.opp (Z.add m (Zpos xH)))) x *)
(* Goal: Rlt x (Z2R (Z.add (Z.opp (Z.add m (Zpos xH))) (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
now apply Rlt_le.
(* Goal: Rlt (Ropp x) (Z2R (Z.add m (Zpos xH))) *)
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
apply H.
(* Goal: Rle (IZR Z0) x *)
now apply Rge_le.
Qed.

Theorem inbetween_float_DN_sign :
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e (Rabs x) l ->
  round beta fexp Zfloor x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (cond_incr (round_sign_DN (Rlt_bool x 0) l) m)) e).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e (Rabs x) l, @eq R (round beta fexp Zfloor x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) e)) *)
apply inbetween_float_round_sign with (choice := fun s m l => cond_incr (round_sign_DN s l) m).
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m (Rabs x) l), @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) 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.

Theorem inbetween_int_UP :
  forall x m l,
  inbetween_int m x l ->
  Zceil x = cond_incr (round_UP l) m.
Proof.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
(* Goal: @eq Z (Zceil x) (cond_incr (round_UP l) m) *)
assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)).
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
case l ; try (now left) ; now right ; split.
(* Goal: @eq Z (Zceil x) (cond_incr (round_UP l) m) *)
destruct Hl' as [Hl'|(Hl1, Hl2)].
(* Exact *)
(* Goal: @eq Z (Zceil x) (cond_incr (round_UP l) m) *)
(* Goal: @eq Z (Zceil x) (cond_incr (round_UP l) m) *)
rewrite Hl'.
(* Goal: @eq Z (Zceil x) (cond_incr (round_UP loc_Exact) m) *)
(* Goal: @eq Z (Zceil x) (cond_incr (round_UP l) m) *)
destruct Hl ; try easy.
(* Goal: generic_format beta (fun _ : Z => emin) x *)
rewrite H.
(* Goal: @eq Z (Zceil (Z2R m)) (cond_incr (round_UP loc_Exact) m) *)
(* Goal: @eq Z (Zceil x) (cond_incr (round_UP l) m) *)
exact (Zceil_Z2R _).
(* not Exact *)
(* Goal: @eq Z (Zceil x) (cond_incr (round_UP l) m) *)
rewrite Hl2.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Zceil x) (Z.add m (Zpos xH)) *)
(* Goal: Rle (IZR Z0) x *)
apply Zceil_imp.
(* Goal: and (Rlt (Z2R (Z.sub (Z.add m (Zpos xH)) (Zpos xH))) x) (Rle x (Z2R (Z.add m (Zpos xH)))) *)
ring_simplify (m + 1 - 1)%Z.
(* Goal: and (Rlt (Z2R m) x) (Rle x (Z2R (Z.add m (Zpos xH)))) *)
refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))).
(* Goal: and (Rlt (Z2R m) x) (Rlt x (Z2R (Z.add m (Zpos xH)))) *)
apply inbetween_bounds_not_Eq with (2 := Hl1) (1 := Hl).
Qed.

Theorem inbetween_float_UP :
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e x l ->
  round beta fexp Zceil x = F2R (Float beta (cond_incr (round_UP l) m) e).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e x l, @eq R (round beta fexp Zceil x) (@F2R beta (Float beta (cond_incr (round_UP l) m) e)) *)
apply inbetween_float_round with (choice := fun m l => cond_incr (round_UP l) m).
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Zceil x) (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.

Theorem inbetween_int_UP_sign :
  forall x m l,
  inbetween_int m (Rabs x) l ->
  Zceil x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_sign_UP (Rlt_bool x 0) l) m).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
unfold Rabs in Hl.
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
destruct (Rcase_abs x) as [Zx|Zx] .
(* *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
rewrite Rlt_bool_true with (1 := Zx).
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Zceil x) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
unfold Zceil.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
apply f_equal.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
inversion_clear Hl ; simpl.
(* Goal: generic_format beta (fun _ : Z => emin) x *)
rewrite H.
(* Goal: @eq Z (Zfloor (Z2R m)) m *)
(* Goal: @eq Z (Zfloor (Ropp x)) m *)
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
apply Zfloor_Z2R.
(* Goal: @eq Z (Zfloor x) m *)
apply Zfloor_imp.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: Rle (Z2R (Z.opp (Z.add m (Zpos xH)))) x *)
(* Goal: Rlt x (Z2R (Z.add (Z.opp (Z.add m (Zpos xH))) (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
now apply Rlt_le.
(* Goal: Rlt (Ropp x) (Z2R (Z.add m (Zpos xH))) *)
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
apply H.
(* *)
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite Rlt_bool_false.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
inversion_clear Hl ; simpl.
(* Goal: generic_format beta (fun _ : Z => emin) x *)
rewrite H.
(* Goal: @eq Z (Zceil (Z2R m)) m *)
(* Goal: @eq Z (Zceil x) (Z.add m (Zpos xH)) *)
(* Goal: Rle (IZR Z0) x *)
apply Zceil_Z2R.
(* Goal: @eq Z (Zceil x) (Z.add m (Zpos xH)) *)
(* Goal: Rle (IZR Z0) x *)
apply Zceil_imp.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: Rlt (Z2R (Z.sub (Z.add m (Zpos xH)) (Zpos xH))) x *)
(* Goal: Rle x (Z2R (Z.add m (Zpos xH))) *)
(* Goal: Rle (IZR Z0) x *)
change (m + 1 - 1)%Z with (Zpred (Zsucc m)).
(* Goal: Rlt (Z2R (Z.pred (Z.succ m))) x *)
(* Goal: Rle x (Z2R (Z.add m (Zpos xH))) *)
(* Goal: Rle (IZR Z0) x *)
now rewrite <- Zpred_succ.
(* Goal: Rle (Z2R (Z.opp (Z.add m (Zpos xH)))) x *)
(* Goal: Rlt x (Z2R (Z.add (Z.opp (Z.add m (Zpos xH))) (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
now apply Rlt_le.
(* Goal: Rle (IZR Z0) x *)
now apply Rge_le.
Qed.

Theorem inbetween_float_UP_sign :
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e (Rabs x) l ->
  round beta fexp Zceil x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (cond_incr (round_sign_UP (Rlt_bool x 0) l) m)) e).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e (Rabs x) l, @eq R (round beta fexp Zceil x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) e)) *)
apply inbetween_float_round_sign with (choice := fun s m l => cond_incr (round_sign_UP s l) m).
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m (Rabs x) l), @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) 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.

Theorem inbetween_int_ZR :
  forall x m l,
  inbetween_int m x l ->
  Ztrunc x = cond_incr (round_ZR (Zlt_bool m 0) l) m.
Proof with auto with typeclass_instances.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
rewrite Zrnd_Z2R...
(* not Exact *)
(* Goal: @eq Z (Ztrunc x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
unfold Ztrunc.
assert (Hm: Zfloor x = m).
(* Goal: @eq Z (Zfloor x) m *)
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
rewrite Zceil_floor_neq.
rewrite Hm.
unfold cond_incr.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
case Rlt_bool_spec ; intros Hx' ;
(* Goal: @eq R x (@F2R beta (Float beta m e)) *)
(* Goal: @eq Z e (canonic_exp beta fexp x) *)
  case Zlt_bool_spec ; intros Hm' ; try apply refl_equal.
elim Rlt_not_le with (1 := Hx').
(* Goal: Rle (Z2R (Z.opp (Z.add m (Zpos xH)))) x *)
(* Goal: Rlt x (Z2R (Z.add (Z.opp (Z.add m (Zpos xH))) (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
apply Rlt_le.
apply Rle_lt_trans with (2 := proj1 Hx).
now apply (Z2R_le 0).
elim Rle_not_lt with (1 := Hx').
apply Rlt_le_trans with (1 := proj2 Hx).
apply (Z2R_le _ 0).
now apply Zlt_le_succ.
rewrite Hm.
now apply Rlt_not_eq.
Qed.

Theorem inbetween_float_ZR :
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e x l ->
  round beta fexp Ztrunc x = F2R (Float beta (cond_incr (round_ZR (Zlt_bool m 0) l) m) e).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e x l, @eq R (round beta fexp Ztrunc x) (@F2R beta (Float beta (cond_incr (round_ZR (Z.ltb m Z0) l) m) e)) *)
apply inbetween_float_round with (choice := fun m l => cond_incr (round_ZR (Zlt_bool m 0) l) m).
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Ztrunc x) (cond_incr (round_ZR (Z.ltb m Z0) l) m) *)
exact inbetween_int_ZR.
Qed.

Theorem inbetween_int_ZR_sign :
  forall x m l,
  inbetween_int m (Rabs x) l ->
  Ztrunc x = cond_Zopp (Rlt_bool x 0) m.
Proof.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Ztrunc x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
unfold Ztrunc.
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
destruct (Rlt_le_dec x 0) as [Zx|Zx].
(* *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
rewrite Rlt_bool_true with (1 := Zx).
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Zceil x) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
unfold Zceil.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
apply f_equal.
(* Goal: @eq Z (Zfloor x) m *)
apply Zfloor_imp.
(* Goal: and (Rle (Z2R m) (Ropp x)) (Rlt (Ropp x) (Z2R (Z.add m (Zpos xH)))) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
rewrite <- Rabs_left with (1 := Zx).
(* Goal: and (Rle (Z2R m) (Rabs x)) (Rlt (Rabs x) (Z2R (Z.add m (Zpos xH)))) *)
apply inbetween_bounds with (2 := Hl).
(* Goal: Rlt (Z2R m) (Z2R (Z.add m (Zpos xH))) *)
apply Z2R_lt.
(* Goal: Z.lt m (Z.add m (Zpos xH)) *)
apply Zlt_succ.
(* *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
rewrite Rlt_bool_false with (1 := Zx).
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Zfloor x) m *)
apply Zfloor_imp.
(* Goal: and (Rle (Z2R m) x) (Rlt x (Z2R (Z.add m (Zpos xH)))) *)
rewrite <- Rabs_pos_eq with (1 := Zx).
(* Goal: and (Rle (Z2R m) (Rabs x)) (Rlt (Rabs x) (Z2R (Z.add m (Zpos xH)))) *)
apply inbetween_bounds with (2 := Hl).
(* Goal: Rlt (Z2R m) (Z2R (Z.add m (Zpos xH))) *)
apply Z2R_lt.
(* Goal: Z.lt m (Z.add m (Zpos xH)) *)
apply Zlt_succ.
Qed.

Theorem inbetween_float_ZR_sign :
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e (Rabs x) l ->
  round beta fexp Ztrunc x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) m) e).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e (Rabs x) l, @eq R (round beta fexp Ztrunc x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) m) e)) *)
apply inbetween_float_round_sign with (choice := fun s m l => m).
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m (Rabs x) l), @eq Z (Ztrunc x) (cond_Zopp (Rlt_bool x (IZR Z0)) 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.

Theorem inbetween_int_N :
  forall choice x m l,
  inbetween_int m x l ->
  Znearest choice x = cond_incr (round_N (choice m) l) m.
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_Z2R...
(* not Exact *)
unfold Znearest.
assert (Hm: Zfloor x = m).
(* Goal: @eq Z (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).
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
apply f_equal.
simpl (Z2R 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
Qed.

Theorem inbetween_int_N_sign :
  forall choice x m l,
  inbetween_int m (Rabs x) l ->
  Znearest choice x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (if Rlt_bool x 0 then negb (choice (-(m + 1))%Z) else choice m) l) m).
Proof with auto with typeclass_instances.
intros choice x m l Hl.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
unfold Rabs in Hl.
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
destruct (Rcase_abs x) as [Zx|Zx].
(* *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
rewrite Rlt_bool_true with (1 := Zx).
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Zfloor x) (Z.opp m) *)
(* Goal: @eq Z (Zfloor x) (Z.opp (Z.add m (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite <- (Ropp_involutive x).
rewrite Znearest_opp.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
apply f_equal.
inversion_clear Hl as [Hx|l' Hx Hl'].
rewrite Hx.
apply Zrnd_Z2R...
assert (Hm: Zfloor (-x) = m).
(* Goal: @eq Z (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 - Z2R m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite Z2R_plus.
rewrite <- (Rcompare_plus_r (- Z2R m) (-x)).
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
apply f_equal.
simpl (Z2R 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
(* *)
generalize (Rge_le _ _ Zx).
clear Zx. intros Zx.
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
rewrite Rlt_bool_false with (1 := Zx).
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
inversion_clear Hl as [Hx|l' Hx Hl'].
rewrite Hx.
apply Zrnd_Z2R...
assert (Hm: Zfloor x = m).
(* Goal: @eq Z (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 - Z2R m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite Z2R_plus.
rewrite <- (Rcompare_plus_r (- Z2R m) x).
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
apply f_equal.
simpl (Z2R 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
Qed.

(** Relates location and rounding to nearest even. *)

Theorem inbetween_int_NE :
  forall x m l,
  inbetween_int m x l ->
  ZnearestE x = cond_incr (round_N (negb (Zeven m)) l) m.
Proof.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
(* Goal: @eq Z (Znearest (fun x : Z => negb (Zeven x)) x) (cond_incr (round_N (negb (Zeven m)) l) m) *)
now apply inbetween_int_N with (choice := fun x => negb (Zeven x)).
Qed.

Theorem inbetween_float_NE :
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e x l ->
  round beta fexp ZnearestE x = F2R (Float beta (cond_incr (round_N (negb (Zeven m)) l) m) e).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e x l, @eq R (round beta fexp (Znearest (fun x0 : Z => negb (Zeven x0))) x) (@F2R beta (Float beta (cond_incr (round_N (negb (Zeven m)) l) m) e)) *)
apply inbetween_float_round with (choice := fun m l => cond_incr (round_N (negb (Zeven m)) l) m).
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (fun x0 : Z => negb (Zeven x0)) x) (cond_incr (round_N (negb (Zeven m)) l) m) *)
exact inbetween_int_NE.
Qed.

Theorem inbetween_int_NE_sign :
  forall x m l,
  inbetween_int m (Rabs x) l ->
  ZnearestE x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (negb (Zeven m)) l) m).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
erewrite inbetween_int_N_sign with (choice := fun x => negb (Zeven x)).
2: eexact Hl.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
apply f_equal.
case Rlt_bool.
rewrite Zeven_opp, Zeven_plus.
now case (Zeven m).
(* Goal: @eq R x (@F2R beta (Float beta m e)) *)
(* Goal: @eq Z e (canonic_exp beta fexp x) *)
apply refl_equal.
Qed.

Theorem inbetween_float_NE_sign :
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e (Rabs x) l ->
  round beta fexp ZnearestE x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (cond_incr (round_N (negb (Zeven m)) l) m)) e).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e (Rabs x) l, @eq R (round beta fexp (Znearest (fun x0 : Z => negb (Zeven x0))) x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_N (negb (Zeven m)) l) m)) e)) *)
apply inbetween_float_round_sign with (choice := fun s m l => cond_incr (round_N (negb (Zeven m)) l) m).
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m (Rabs x) l), @eq Z (Znearest (fun x0 : Z => negb (Zeven x0)) x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_N (negb (Zeven m)) l) m)) *)
exact inbetween_int_NE_sign.
Qed.

(** Relates location and rounding to nearest away. *)

Theorem inbetween_int_NA :
  forall x m l,
  inbetween_int m x l ->
  ZnearestA x = cond_incr (round_N (Zle_bool 0 m) l) m.
Proof.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
(* Goal: @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
now apply inbetween_int_N with (choice := fun x => Zle_bool 0 x).
Qed.

Theorem inbetween_float_NA :
  forall x m l,
  let e := canonic_exp beta fexp x in
  inbetween_float beta m e x l ->
  round beta fexp ZnearestA x = F2R (Float beta (cond_incr (round_N (Zle_bool 0 m) l) m) e).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location), let e := canonic_exp beta fexp x in forall _ : inbetween_float beta m e x l, @eq R (round beta fexp (Znearest (Z.leb Z0)) x) (@F2R beta (Float beta (cond_incr (round_N (Z.leb Z0 m) l) m) e)) *)
apply inbetween_float_round with (choice := fun m l => cond_incr (round_N (Zle_bool 0 m) l) m).
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
exact inbetween_int_NA.
Qed.

Theorem inbetween_int_NA_sign :
  forall x m l,
  inbetween_int m (Rabs x) l ->
  ZnearestA x = cond_Zopp (Rlt_bool x 0) (cond_incr (round_N true l) m).
Proof.
(* Goal: forall (x : R) (m : Z) (l : location) (_ : inbetween_int m x l), @eq Z (Znearest (Z.leb Z0) x) (cond_incr (round_N (Z.leb Z0 m) l) m) *)
intros x m l Hl.
erewrite inbetween_int_N_sign with (choice := Zle_bool 0).
2: eexact Hl.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
apply f_equal.
assert (Hm: (0 <= m)%Z).
apply Zlt_succ_le.
apply lt_Z2R.
apply Rle_lt_trans with (Rabs x).
apply Rabs_pos.
refine (proj2 (inbetween_bounds _ _ _ _ _ Hl)).
(* Goal: Rlt (Z2R m) (Z2R (Z.add m (Zpos xH))) *)
apply Z2R_lt.
(* Goal: Z.lt m (Z.add m (Zpos xH)) *)
apply Zlt_succ.
rewrite Zle_bool_true with (1 := Hm).
rewrite Zle_bool_false.
now case Rlt_bool.
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
omega.
Qed.

Definition truncate_aux t k :=
  let '(m, e, l) := t in
  let p := Zpower beta k in
  (Zdiv m p, (e + k)%Z, new_location p (Zmod m p) l).

Theorem truncate_aux_comp :
  forall t k1 k2,
  (0 < k1)%Z ->
  (0 < k2)%Z ->
  truncate_aux t (k1 + k2) = truncate_aux (truncate_aux t k1) k2.
Proof.
(* Goal: forall (t : prod (prod Z Z) location) (k1 k2 : Z) (_ : Z.lt Z0 k1) (_ : Z.lt Z0 k2), @eq (prod (prod Z Z) location) (truncate_aux t (Z.add k1 k2)) (truncate_aux (truncate_aux t k1) k2) *)
intros ((m,e),l) k1 k2 Hk1 Hk2.
(* Goal: let 'pair (pair m' e' as p) l' := truncate_aux (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) k in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
unfold truncate_aux.
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
destruct (inbetween_float_ex beta m e l) as (x,Hx).
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
assert (B1 := inbetween_float_new_location _ _ _ _ _ _ Hk1 Hx).
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
assert (Hk3: (0 < k1 + k2)%Z).
(* Goal: Z.lt Z0 (Z.add k1 k2) *)
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
change Z0 with (0 + 0)%Z.
(* Goal: Z.lt (Z.add Z0 Z0) (Z.add k1 k2) *)
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
now apply Zplus_lt_compat.
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
assert (B3 := inbetween_float_new_location _ _ _ _ _ _ Hk3 Hx).
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
assert (B2 := inbetween_float_new_location _ _ _ _ _ _ Hk2 B1).
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
rewrite Zplus_assoc in B3.
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
destruct (inbetween_float_unique _ _ _ _ _ _ _ B2 B3).
(* Goal: @eq (prod (prod Z Z) location) (@pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.add k1 k2))) (Z.add e (Z.add k1 k2))) (new_location (Z.pow (radix_val beta) (Z.add k1 k2)) (Z.modulo m (Z.pow (radix_val beta) (Z.add k1 k2))) l)) (@pair (prod Z Z) location (@pair Z Z (Z.div (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (Z.add (Z.add e k1) k2)) (new_location (Z.pow (radix_val beta) k2) (Z.modulo (Z.div m (Z.pow (radix_val beta) k1)) (Z.pow (radix_val beta) k2)) (new_location (Z.pow (radix_val beta) k1) (Z.modulo m (Z.pow (radix_val beta) k1)) l))) *)
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.

Theorem truncate_0 :
  forall e l,
  let '(m', e', l') := truncate (0, e, l)%Z in
  m' = Z0.
Proof.
(* Goal: forall (e : Z) (l : location), let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z Z0 e) l) in @eq Z m' Z0 *)
intros e l.
(* Goal: let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
unfold truncate.
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 (Z.sub (fexp (Z.add (Zdigits beta Z0) e)) e) then truncate_aux (@pair (prod Z Z) location (@pair Z Z Z0 e) l) (Z.sub (fexp (Z.add (Zdigits beta Z0) e)) e) else @pair (prod Z Z) location (@pair Z Z Z0 e) l in @eq Z m' Z0 *)
case Zlt_bool.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Z.div Z0 (Z.pow (radix_val beta) (Z.sub (fexp e) e))) Z0 *)
(* Goal: @eq Z Z0 Z0 *)
apply Zdiv_0_l.
(* Goal: @eq R x (@F2R beta (Float beta m e)) *)
(* Goal: @eq Z e (canonic_exp beta fexp x) *)
apply refl_equal.
Qed.

Theorem generic_format_truncate :
  forall m e l,
  (0 <= m)%Z ->
  let '(m', e', l') := truncate (m, e, l) in
  format (F2R (Float beta m' e')).
Proof.
intros m e l Hm.
(* Goal: let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
unfold truncate.
set (k := (fexp (Zdigits beta m + e) - e)%Z).
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 k then truncate_aux (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) k else @pair (prod Z Z) location (@pair Z Z m e) loc_Exact in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
case Zlt_bool_spec ; intros Hk.
(* *)
(* Goal: let 'pair (pair m' e' as p) l' := truncate_aux (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) k in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
unfold truncate_aux.
(* Goal: generic_format beta (fun _ : Z => emin) (@F2R beta (Float beta m e)) *)
apply generic_format_F2R.
intros Hd.
(* Goal: forall _ : not (@eq Z m Z0), Z.le (canonic_exp beta (fun _ : Z => emin) (@F2R beta (Float beta m e))) e *)
unfold canonic_exp.
rewrite ln_beta_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.
(* Goal: @eq Z (Z.add e k) emin *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
unfold k.
ring_simplify.
apply Zle_refl.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
now apply Zlt_le_weak.
apply Znot_gt_le.
contradict Hd.
apply Zdiv_small.
apply conj with (1 := Hm).
rewrite <- Zabs_eq with (1 := Hm).
apply Zpower_gt_Zdigits.
apply Zlt_le_weak.
now apply Zgt_lt.
(* *)
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
(* Goal: generic_format beta (fun _ : Z => emin) (@F2R beta (Float beta m e)) *)
apply generic_format_F2R.
(* Goal: forall _ : not (@eq Z m Z0), Z.le (canonic_exp beta (fun _ : Z => emin) (@F2R beta (Float beta m e))) e *)
unfold canonic_exp.
rewrite ln_beta_F2R_Zdigits.
2: now apply Zgt_not_eq.
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
unfold k in Hk. clear -Hk.
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
omega.
rewrite <- Hm', F2R_0.
apply generic_format_0.
Qed.

Theorem truncate_correct_format :
  forall m e,
  m <> Z0 ->
  let x := F2R (Float beta m e) in
  generic_format beta fexp x ->
  (e <= fexp (Zdigits beta m + e))%Z ->
  let '(m', e', l') := truncate (m, e, loc_Exact) in
  x = F2R (Float beta m' e') /\ e' = canonic_exp beta fexp x.
Proof.
(* Goal: forall (m e : Z) (_ : not (@eq Z m Z0)), let x := @F2R beta (Float beta m e) in forall (_ : generic_format beta fexp x) (_ : Z.le e (fexp (Z.add (Zdigits beta m) e))), let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
intros m e Hm x Fx He.
(* Goal: let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
assert (Hc: canonic_exp beta fexp x = fexp (Zdigits beta m + e)).
(* Goal: @eq Z (canonic_exp beta fexp x) (fexp (Z.add (Zdigits beta m) e)) *)
(* Goal: let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
unfold canonic_exp, x.
now rewrite ln_beta_F2R_Zdigits.
(* Goal: let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
unfold truncate.
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 (Z.sub (fexp (Z.add (Zdigits beta m) e)) e) then truncate_aux (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) (Z.sub (fexp (Z.add (Zdigits beta m) e)) e) else @pair (prod Z Z) location (@pair Z Z m e) loc_Exact in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
rewrite <- Hc.
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 (Z.sub (canonic_exp beta fexp x) e) then truncate_aux (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) (Z.sub (canonic_exp beta fexp x) e) else @pair (prod Z Z) location (@pair Z Z m e) loc_Exact in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
set (k := (canonic_exp beta fexp x - e)%Z).
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 k then truncate_aux (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) k else @pair (prod Z Z) location (@pair Z Z m e) loc_Exact in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
case Zlt_bool_spec ; intros Hk.
(* *)
(* Goal: let 'pair (pair m' e' as p) l' := truncate_aux (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) k in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
unfold truncate_aux.
(* Goal: and (@eq R x (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k)))) (@eq Z (Z.add e k) (canonic_exp beta fexp x)) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
rewrite Fx at 1.
(* Goal: and (@eq R (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta fexp x)) (canonic_exp beta fexp x))) (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k)))) (@eq Z (Z.add e k) (canonic_exp beta fexp x)) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
assert (H: (e + k)%Z = canonic_exp beta fexp x).
(* Goal: @eq Z (Z.add e k) emin *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
unfold k. ring.
(* Goal: and (@eq R (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta fexp x)) (canonic_exp beta fexp x))) (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k)))) (@eq Z (Z.add e k) (canonic_exp beta fexp x)) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
refine (conj _ H).
(* Goal: @eq Z (Zfloor (Rmult x (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta fexp x))))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
rewrite <- H.
(* Goal: @eq R (@F2R beta (Float beta (Ztrunc (scaled_mantissa beta fexp x)) (Z.add e k))) (@F2R beta (Float beta (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k))) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
apply F2R_eq_compat.
(* Goal: @eq Z (Ztrunc (scaled_mantissa beta fexp x)) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
replace (scaled_mantissa beta fexp x) with (Z2R (Zfloor (scaled_mantissa beta fexp x))).
(* Goal: @eq Z (Ztrunc (Z2R (Zfloor (scaled_mantissa beta fexp x)))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
rewrite Ztrunc_Z2R.
(* Goal: @eq Z (Zfloor (scaled_mantissa beta fexp x)) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
unfold scaled_mantissa.
(* Goal: @eq Z (Zfloor (Rmult x (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta fexp x))))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
rewrite <- H.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
unfold x, F2R. simpl.
(* Goal: @eq Z (Zfloor (Rmult (Rmult (Z2R m) (Fcore_Raux.bpow beta e)) (Fcore_Raux.bpow beta (Z.opp (Z.add e k))))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
rewrite Rmult_assoc, <- bpow_plus.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.add e (Z.opp (Z.add e k)))))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
ring_simplify (e + - (e + k))%Z.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp k)))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
clear -Hm Hk.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp k)))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
destruct k as [|k|k] ; try easy.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Rinv (Z2R (Z.pow_pos (radix_val beta) k))))) (Z.div m (Z.pow_pos (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
apply Zfloor_div.
(* Goal: not (@eq Z (Z.pow_pos (radix_val beta) k) Z0) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
intros H.
(* Goal: False *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
generalize (Zpower_pos_gt_0 beta k) (Zle_bool_imp_le _ _ (radix_prop beta)).
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
omega.
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
rewrite scaled_mantissa_generic with (1 := Fx).
(* Goal: @eq R (Z2R (Zfloor (Z2R (Ztrunc (scaled_mantissa beta fexp x))))) (Z2R (Ztrunc (scaled_mantissa beta fexp x))) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
now rewrite Zfloor_Z2R.
(* *)
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: @eq R x (@F2R beta (Float beta m e)) *)
(* Goal: @eq Z e (canonic_exp beta fexp x) *)
apply refl_equal.
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
unfold k in Hk.
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
omega.
Qed.

Theorem truncate_correct_partial :
  forall x m e l,
  (0 < x)%R ->
  inbetween_float beta m e x l ->
  (e <= fexp (Zdigits beta m + e))%Z ->
  let '(m', e', l') := truncate (m, e, l) in
  inbetween_float beta m' e' x l' /\ e' = canonic_exp beta fexp x.
Proof.
intros x m e l Hx H1 H2.
(* Goal: let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
unfold truncate.
set (k := (fexp (Zdigits beta m + e) - e)%Z).
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 k then @pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k)) (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) else @pair (prod Z Z) location (@pair Z Z m e) l in and (inbetween_float beta m' e' x l') (or (@eq Z e' (canonic_exp beta (FIX_exp emin) x)) (and (@eq location l' loc_Exact) (generic_format beta (FIX_exp emin) x))) *)
set (p := Zpower beta k).
(* *)
assert (Hx': (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R).
apply inbetween_float_bounds with (1 := H1).
(* *)
assert (Hm: (0 <= m)%Z).
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
cut (0 < m + 1)%Z. omega.
apply F2R_lt_reg with beta e.
rewrite F2R_0.
apply Rlt_trans with  (1 := Hx).
apply Hx'.
assert (He: (e + k = canonic_exp beta fexp x)%Z).
(* . *)
(* Goal: forall _ : not (@eq Z m Z0), Z.le (canonic_exp beta (fun _ : Z => emin) (@F2R beta (Float beta m e))) e *)
unfold canonic_exp.
destruct (Zle_lt_or_eq _ _ Hm) as [Hm'|Hm'].
(* .. 0 < m *)
rewrite ln_beta_F2R_bounds with (1 := Hm') (2 := Hx').
assert (H: m <> Z0).
apply sym_not_eq.
now apply Zlt_not_eq.
rewrite ln_beta_F2R with (1 := H).
rewrite <- Zdigits_ln_beta with (1 := H).
(* Goal: @eq Z (Z.add e k) emin *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
unfold k.
(* Goal: @eq Z (Z.add e (Z.sub emin e)) emin *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
ring.
(* .. m = 0 *)
rewrite <- Hm' in H2.
destruct (ln_beta beta x) as (ex, Hex).
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
specialize (Hex (Rgt_not_eq _ _ Hx)).
(* Goal: @eq Z (Z.add e k) emin *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
unfold k.
ring_simplify.
rewrite <- Hm'.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
apply sym_eq.
apply valid_exp.
(* Goal: @eq location l loc_Exact *)
(* Goal: generic_format beta (fun _ : Z => emin) x *)
exact H2.
apply Zle_trans with e.
eapply bpow_lt_bpow.
apply Rle_lt_trans with (1 := proj1 Hex).
rewrite Rabs_pos_eq.
rewrite <- F2R_bpow.
rewrite <- Hm' in Hx'.
apply Hx'.
(* Goal: Rle (Z2R (Z.opp (Z.add m (Zpos xH)))) x *)
(* Goal: Rlt x (Z2R (Z.add (Z.opp (Z.add m (Zpos xH))) (Zpos xH))) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
now apply Rlt_le.
(* Goal: @eq location l loc_Exact *)
(* Goal: generic_format beta (fun _ : Z => emin) x *)
exact H2.
(* . *)
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 k then @pair (prod Z Z) location (@pair Z Z (Z.div m p) (Z.add e k)) (new_location p (Z.modulo m p) l) else @pair (prod Z Z) location (@pair Z Z m e) l in and (inbetween_float beta m' e' x l') (or (@eq Z e' emin) (and (@eq location l' loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
generalize (Zlt_cases 0 k).
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
case (Zlt_bool 0 k) ; intros Hk ; unfold k in Hk.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: inbetween_float beta (Z.div m p) (Z.add e k) x (new_location p (Z.modulo m p) l) *)
(* Goal: or (@eq Z (Z.add e k) emin) (and (@eq location (new_location p (Z.modulo m p) l) loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
now apply inbetween_float_new_location.
exact He.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: inbetween_float beta m e x l *)
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
exact H1.
rewrite <- He.
(* Goal: @eq Z (Z.add e k) emin *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
unfold k.
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
omega.
Qed.

Theorem truncate_correct :
  forall x m e l,
  (0 <= x)%R ->
  inbetween_float beta m e x l ->
  (e <= fexp (Zdigits beta m + e))%Z \/ l = loc_Exact ->
  let '(m', e', l') := truncate (m, e, l) in
  inbetween_float beta m' e' x l' /\
  (e' = canonic_exp beta fexp x \/ (l' = loc_Exact /\ format x)).
Proof.
intros x m e l [Hx|Hx] H1 H2.
(* 0 < x *)
destruct (Zle_or_lt e (fexp (Zdigits beta m + e))) as [H3|H3].
(* . enough digits *)
generalize (truncate_correct_partial x m e l Hx H1 H3).
(* Goal: forall _ : let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in and (inbetween_float beta m' e' (Rabs x) l') (or (@eq Z e' (canonic_exp beta fexp (Rabs x))) (and (@eq location l' loc_Exact) (generic_format beta fexp (Rabs x)))), @eq R (round beta fexp rnd x) (let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in @F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m' l')) e')) *)
destruct (truncate (m, e, l)) as ((m', e'), l').
intros (H4, H5).
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
exact H4.
now left.
(* . not enough digits but loc_Exact *)
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
destruct H2 as [H2|H2].
elim (Zlt_irrefl e).
now apply Zle_lt_trans with (1 := H2).
rewrite H2 in H1 |- *.
(* Goal: let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) loc_Exact) in and (@eq R x (@F2R beta (Float beta m' e'))) (@eq Z e' (canonic_exp beta fexp x)) *)
unfold truncate.
generalize (Zlt_cases 0 (fexp (Zdigits beta m + e) - e)).
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 (Z.sub (fexp (Z.add (Zdigits beta Z0) e)) e) then truncate_aux (@pair (prod Z Z) location (@pair Z Z Z0 e) l) (Z.sub (fexp (Z.add (Zdigits beta Z0) e)) e) else @pair (prod Z Z) location (@pair Z Z Z0 e) l in @eq Z m' Z0 *)
case Zlt_bool.
(* Goal: not (@eq Z (Z.pow_pos (radix_val beta) k) Z0) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
intros H.
apply False_ind.
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
omega.
intros _.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: inbetween_float beta m e x l *)
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
exact H1.
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
right.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: @eq R x (@F2R beta (Float beta m e)) *)
(* Goal: @eq Z e (canonic_exp beta fexp x) *)
apply refl_equal.
(* Goal: generic_format beta (fun _ : Z => emin) x *)
inversion_clear H1.
(* Goal: generic_format beta (fun _ : Z => emin) x *)
rewrite H.
(* Goal: generic_format beta (fun _ : Z => emin) (@F2R beta (Float beta m e)) *)
apply generic_format_F2R.
intros Zm.
(* Goal: forall _ : not (@eq Z m Z0), Z.le (canonic_exp beta (fun _ : Z => emin) (@F2R beta (Float beta m e))) e *)
unfold canonic_exp.
rewrite ln_beta_F2R_Zdigits with (1 := Zm).
now apply Zlt_le_weak.
(* x = 0 *)
assert (Hm: m = Z0).
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
cut (m <= 0 < m + 1)%Z. omega.
assert (Hx': (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R).
apply inbetween_float_bounds with (1 := H1).
rewrite <- Hx in Hx'.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
apply F2R_le_0_reg with (1 := proj1 Hx').
apply F2R_gt_0_reg with (1 := proj2 Hx').
rewrite Hm, <- Hx in H1 |- *.
clear -H1.
case H1.
(* . *)
intros _.
assert (exists e', truncate (Z0, e, loc_Exact) = (Z0, e', loc_Exact)).
unfold truncate, truncate_aux.
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 (Z.sub (fexp (Z.add (Zdigits beta Z0) e)) e) then truncate_aux (@pair (prod Z Z) location (@pair Z Z Z0 e) l) (Z.sub (fexp (Z.add (Zdigits beta Z0) e)) e) else @pair (prod Z Z) location (@pair Z Z Z0 e) l in @eq Z m' Z0 *)
case Zlt_bool.
rewrite Zdiv_0_l, Zmod_0_l.
eexists.
(* Goal: @eq Z (Z.opp (Zfloor (Ropp x))) (Z.opp m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
apply f_equal.
unfold new_location.
now case Zeven.
now eexists.
destruct H as (e', H).
(* Goal: generic_format beta (fun _ : Z => emin) x *)
rewrite H.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
constructor.
apply sym_eq.
apply F2R_0.
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
right.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
repeat split.
apply generic_format_0.
(* . *)
intros l' (H, _) _.
rewrite F2R_0 in H.
elim Rlt_irrefl with (1 := H).
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.

Theorem round_any_correct :
  forall x m e l,
  inbetween_float beta m e x l ->
  (e = canonic_exp beta fexp x \/ (l = loc_Exact /\ format x)) ->
  round beta fexp rnd x = F2R (Float beta (choice m l) e).
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.
(* Goal: @eq Z (Zfloor (Rmult x (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta fexp x))))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
rewrite <- H.
apply round_generic...
rewrite <- (Zrnd_Z2R rnd m) at 1.
apply inbetween_int_valid.
now constructor.
Qed.

(** Truncating a triple is sufficient to round a real number. *)

Theorem round_trunc_any_correct :
  forall x m e l,
  (0 <= x)%R ->
  inbetween_float beta m e x l ->
  (e <= fexp (Zdigits beta m + e))%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.
(* Goal: forall (x : R) (m e : Z) (l : location) (_ : Rle (IZR Z0) x) (_ : inbetween_float beta m e x l) (_ : or (Z.le e (fexp (Z.add (Zdigits beta m) e))) (@eq location l loc_Exact)), @eq R (round beta fexp rnd x) (let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in @F2R beta (Float beta (choice m' l') e')) *)
intros x m e l Hx Hl He.
(* Goal: @eq R (round beta fexp rnd x) (let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in @F2R beta (Float beta (choice m' l') e')) *)
generalize (truncate_correct x m e l Hx Hl He).
(* Goal: forall _ : let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in and (inbetween_float beta m' e' (Rabs x) l') (or (@eq Z e' (canonic_exp beta fexp (Rabs x))) (and (@eq location l' loc_Exact) (generic_format beta fexp (Rabs x)))), @eq R (round beta fexp rnd x) (let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in @F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m' l')) e')) *)
destruct (truncate (m, e, l)) as ((m', e'), l').
(* Goal: forall _ : and (inbetween_float beta m' e' (Rabs x) l') (or (@eq Z e' (canonic_exp beta fexp (Rabs x))) (and (@eq location l' loc_Exact) (generic_format beta fexp (Rabs x)))), @eq R (round beta fexp rnd x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m' l')) e')) *)
intros (H1, H2).
(* Goal: @eq R (round beta fexp rnd x) (@F2R beta (Float beta (choice m' l') e')) *)
now apply round_any_correct.
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).

Theorem round_sign_any_correct :
  forall x m e l,
  inbetween_float beta m e (Rabs x) l ->
  (e = canonic_exp beta fexp x \/ (l = loc_Exact /\ format x)) ->
  round beta fexp rnd x = F2R (Float beta (cond_Zopp (Rlt_bool x 0) (choice (Rlt_bool x 0) m l)) e).
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.
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
destruct (Rcase_abs x) as [Zx|Zx].
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
(* Goal: @eq Z (if Rlt_bool x (IZR Z0) then Zceil x else Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) m) *)
rewrite Rlt_bool_true with (1 := Zx).
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
rewrite F2R_Zopp.
rewrite <- H, Ropp_involutive.
apply round_generic...
(* Goal: @eq Z (Zceil x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_UP (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite Rlt_bool_false.
(* Goal: @eq Z (Zfloor (Rmult (Z2R m) (Fcore_Raux.bpow beta (Z.opp (Zpos k))))) (Z.div m (Z.pow (radix_val beta) (Zpos k))) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
simpl.
(* Goal: @eq Z (Zfloor (Rmult x (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta fexp x))))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
rewrite <- H.
now apply round_generic.
(* Goal: Rle (IZR Z0) x *)
now apply Rge_le.
(* *)
destruct (Rlt_bool_spec x 0) as [Zx|Zx].
(* . *)
apply Zopp_inj.
change (- m = cond_Zopp true (choice true m loc_Exact))%Z.
rewrite <- (Zrnd_Z2R rnd (-m)) at 1.
assert (Z2R (-m) < 0)%R.
(* Goal: Rlt x (Z2R (Z.opp m)) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite Z2R_opp.
apply Ropp_lt_gt_0_contravar.
apply (Z2R_lt 0).
apply F2R_gt_0_reg with beta e.
(* Goal: @eq Z (Zfloor (Rmult x (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta fexp x))))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
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).
(* Goal: Rlt x (Z2R (Z.opp m)) *)
(* Goal: @eq Z (Zfloor x) (cond_Zopp (Rlt_bool x (IZR Z0)) (cond_incr (round_sign_DN (Rlt_bool x (IZR Z0)) l) m)) *)
rewrite Z2R_opp.
apply Ropp_involutive.
(* . *)
change (m = cond_Zopp false (choice false m loc_Exact))%Z.
rewrite <- (Zrnd_Z2R rnd m) at 1.
assert (0 <= Z2R m)%R.
apply (Z2R_le 0).
apply F2R_ge_0_reg with beta e.
(* Goal: @eq Z (Zfloor (Rmult x (Fcore_Raux.bpow beta (Z.opp (canonic_exp beta fexp x))))) (Z.div m (Z.pow (radix_val beta) k)) *)
(* Goal: @eq R (Z2R (Zfloor (scaled_mantissa beta fexp x))) (scaled_mantissa beta fexp x) *)
(* Goal: and (@eq R x (@F2R beta (Float beta m e))) (@eq Z e (canonic_exp beta fexp x)) *)
rewrite <- H.
apply Rabs_pos.
rewrite <- Rlt_bool_false with (1 := H0).
apply inbetween_int_valid.
constructor.
now apply Rabs_pos_eq.
Qed.

(** Truncating a triple is sufficient to round a real number. *)

Theorem round_trunc_sign_any_correct :
  forall x m e l,
  inbetween_float beta m e (Rabs x) l ->
  (e <= fexp (Zdigits beta m + e))%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.
(* Goal: forall (x : R) (m e : Z) (l : location) (_ : inbetween_float beta m e (Rabs x) l) (_ : or (Z.le e (fexp (Z.add (Zdigits beta m) e))) (@eq location l loc_Exact)), @eq R (round beta fexp rnd x) (let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in @F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m' l')) e')) *)
intros x m e l Hl He.
(* Goal: @eq R (round beta fexp rnd x) (let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in @F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m' l')) e')) *)
generalize (truncate_correct (Rabs x) m e l (Rabs_pos _) Hl He).
(* Goal: forall _ : let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in and (inbetween_float beta m' e' (Rabs x) l') (or (@eq Z e' (canonic_exp beta fexp (Rabs x))) (and (@eq location l' loc_Exact) (generic_format beta fexp (Rabs x)))), @eq R (round beta fexp rnd x) (let 'pair (pair m' e' as p) l' := truncate (@pair (prod Z Z) location (@pair Z Z m e) l) in @F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m' l')) e')) *)
destruct (truncate (m, e, l)) as ((m', e'), l').
(* Goal: forall _ : and (inbetween_float beta m' e' (Rabs x) l') (or (@eq Z e' (canonic_exp beta fexp (Rabs x))) (and (@eq location l' loc_Exact) (generic_format beta fexp (Rabs x)))), @eq R (round beta fexp rnd x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m' l')) e')) *)
intros (H1, H2).
(* Goal: @eq R (round beta fexp rnd x) (@F2R beta (Float beta (cond_Zopp (Rlt_bool x (IZR Z0)) (choice (Rlt_bool x (IZR Z0)) m' l')) e')) *)
apply round_sign_any_correct.
(* Goal: inbetween_float beta m e x l *)
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
exact H1.
(* Goal: or (@eq Z e' (canonic_exp beta fexp x)) (and (@eq location l' loc_Exact) (generic_format beta fexp x)) *)
destruct H2 as [H2|(H2,H3)].
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
left.
(* Goal: @eq Z e' (canonic_exp beta fexp x) *)
(* Goal: or (@eq Z e' (canonic_exp beta fexp x)) (and (@eq location l' loc_Exact) (generic_format beta fexp x)) *)
now rewrite <- canonic_exp_abs.
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
right.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: @eq location l loc_Exact *)
(* Goal: generic_format beta (fun _ : Z => emin) x *)
exact H2.
(* Goal: generic_format beta fexp x *)
unfold Rabs in H3.
(* Goal: generic_format beta fexp x *)
destruct (Rcase_abs x) in H3.
(* Goal: generic_format beta fexp x *)
(* Goal: generic_format beta fexp x *)
rewrite <- Ropp_involutive.
(* Goal: generic_format beta fexp (Ropp (Ropp x)) *)
(* Goal: generic_format beta fexp x *)
now apply generic_format_opp.
(* Goal: generic_format beta fexp x *)
exact H3.
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_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_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_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_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_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_NE_correct :=
  round_any_correct _ (fun m l => cond_incr (round_N (negb (Zeven m)) l) m) inbetween_int_NE.

Definition round_trunc_NE_correct :=
  round_trunc_any_correct _ (fun m l => cond_incr (round_N (negb (Zeven m)) l) m) inbetween_int_NE.

Definition round_sign_NE_correct :=
  round_sign_any_correct _ (fun s m l => cond_incr (round_N (negb (Zeven 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 (Zeven 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_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.

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
    (Zdiv m p, (e + k)%Z, new_location p (Zmod m p) l)
  else t.

Theorem truncate_FIX_correct :
  forall x m e l,
  inbetween_float beta m e x l ->
  (e <= emin)%Z \/ l = loc_Exact ->
  let '(m', e', l') := truncate_FIX (m, e, l) in
  inbetween_float beta m' e' x l' /\
  (e' = canonic_exp beta (FIX_exp emin) x \/ (l' = loc_Exact /\ generic_format beta (FIX_exp emin) x)).
Proof.
(* Goal: forall (x : R) (m e : Z) (l : location) (_ : inbetween_float beta m e x l) (_ : or (Z.le e emin) (@eq location l loc_Exact)), let 'pair (pair m' e' as p) l' := truncate_FIX (@pair (prod Z Z) location (@pair Z Z m e) l) in and (inbetween_float beta m' e' x l') (or (@eq Z e' (canonic_exp beta (FIX_exp emin) x)) (and (@eq location l' loc_Exact) (generic_format beta (FIX_exp emin) x))) *)
intros x m e l H1 H2.
(* Goal: let 'pair (pair m' e' as p) l' := truncate_FIX (@pair (prod Z Z) location (@pair Z Z m e) l) in and (inbetween_float beta m' e' x l') (or (@eq Z e' (canonic_exp beta (FIX_exp emin) x)) (and (@eq location l' loc_Exact) (generic_format beta (FIX_exp emin) x))) *)
unfold truncate_FIX.
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 (Z.sub emin e) then @pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) (Z.sub emin e))) (Z.add e (Z.sub emin e))) (new_location (Z.pow (radix_val beta) (Z.sub emin e)) (Z.modulo m (Z.pow (radix_val beta) (Z.sub emin e))) l) else @pair (prod Z Z) location (@pair Z Z m e) l in and (inbetween_float beta m' e' x l') (or (@eq Z e' (canonic_exp beta (FIX_exp emin) x)) (and (@eq location l' loc_Exact) (generic_format beta (FIX_exp emin) x))) *)
set (k := (emin - e)%Z).
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 k then @pair (prod Z Z) location (@pair Z Z (Z.div m (Z.pow (radix_val beta) k)) (Z.add e k)) (new_location (Z.pow (radix_val beta) k) (Z.modulo m (Z.pow (radix_val beta) k)) l) else @pair (prod Z Z) location (@pair Z Z m e) l in and (inbetween_float beta m' e' x l') (or (@eq Z e' (canonic_exp beta (FIX_exp emin) x)) (and (@eq location l' loc_Exact) (generic_format beta (FIX_exp emin) x))) *)
set (p := Zpower beta k).
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 k then @pair (prod Z Z) location (@pair Z Z (Z.div m p) (Z.add e k)) (new_location p (Z.modulo m p) l) else @pair (prod Z Z) location (@pair Z Z m e) l in and (inbetween_float beta m' e' x l') (or (@eq Z e' (canonic_exp beta (FIX_exp emin) x)) (and (@eq location l' loc_Exact) (generic_format beta (FIX_exp emin) x))) *)
unfold canonic_exp, FIX_exp.
(* Goal: let 'pair (pair m' e' as p) l' := if Z.ltb Z0 k then @pair (prod Z Z) location (@pair Z Z (Z.div m p) (Z.add e k)) (new_location p (Z.modulo m p) l) else @pair (prod Z Z) location (@pair Z Z m e) l in and (inbetween_float beta m' e' x l') (or (@eq Z e' emin) (and (@eq location l' loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
generalize (Zlt_cases 0 k).
(* Goal: forall _ : if Z.ltb Z0 k then Z.lt Z0 k else Z.ge Z0 k, let 'pair (pair m' e' as p) l' := if Z.ltb Z0 k then @pair (prod Z Z) location (@pair Z Z (Z.div m p) (Z.add e k)) (new_location p (Z.modulo m p) l) else @pair (prod Z Z) location (@pair Z Z m e) l in and (inbetween_float beta m' e' x l') (or (@eq Z e' emin) (and (@eq location l' loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
case (Zlt_bool 0 k) ; intros Hk.
(* shift *)
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: inbetween_float beta (Z.div m p) (Z.add e k) x (new_location p (Z.modulo m p) l) *)
(* Goal: or (@eq Z (Z.add e k) emin) (and (@eq location (new_location p (Z.modulo m p) l) loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
now apply inbetween_float_new_location.
(* Goal: or (@eq Z (Z.add e k) emin) (and (@eq location (new_location p (Z.modulo m p) l) loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
clear H2.
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
left.
(* Goal: @eq Z (Z.add e k) emin *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
unfold k.
(* Goal: @eq Z (Z.add e (Z.sub emin e)) emin *)
(* Goal: and (inbetween_float beta m e x l) (or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x))) *)
ring.
(* no shift *)
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: inbetween_float beta m e x l *)
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
exact H1.
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
unfold k in Hk.
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
destruct H2 as [H2|H2].
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
left.
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
omega.
(* Goal: or (@eq Z e emin) (and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x)) *)
right.
(* Goal: and (@eq location l loc_Exact) (generic_format beta (fun _ : Z => emin) x) *)
split.
(* Goal: @eq location l loc_Exact *)
(* Goal: generic_format beta (fun _ : Z => emin) x *)
exact H2.
(* Goal: generic_format beta (fun _ : Z => emin) x *)
rewrite H2 in H1.
(* Goal: generic_format beta (fun _ : Z => emin) x *)
inversion_clear H1.
(* Goal: generic_format beta (fun _ : Z => emin) x *)
rewrite H.
(* Goal: generic_format beta (fun _ : Z => emin) (@F2R beta (Float beta m e)) *)
apply generic_format_F2R.
(* Goal: forall _ : not (@eq Z m Z0), Z.le (canonic_exp beta (fun _ : Z => emin) (@F2R beta (Float beta m e))) e *)
unfold canonic_exp.
(* Goal: forall _ : not (@eq Z m Z0), Z.le emin e *)
omega.
Qed.

End Fcalc_round.
