Library Interval.Float.Specific_ops

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/

This library is governed by the CeCILL-C license under French law and abiding by the rules of distribution of free software. You can use, modify and/or redistribute the library under the terms of the CeCILL-C license as circulated by CEA, CNRS and Inria at the following URL: http://www.cecill.info/

As a counterpart to the access to the source code and rights to copy, modify and redistribute granted by the license, users are provided only with a limited warranty and the library's author, the holder of the economic rights, and the successive licensors have only limited liability. See the COPYING file for more details.

From Coq Require Import ZArith Reals Lia Bool Psatz.
From Flocq Require Import Zaux Raux Digits Bracket.
From mathcomp.ssreflect Require Import ssrbool.

Require Import Xreal.
Require Import Basic.
Require Import Generic.
Require Import Generic_proof.
Require Import Sig.
Require Import Specific_sig.

Inductive s_float (smantissa_type exponent_type : Type) : Type :=
  | Fnan : s_float smantissa_type exponent_type
  | Float : smantissa_type → exponent_type → s_float smantissa_type exponent_type.

Arguments Fnan {smantissa_type exponent_type}.
Arguments Float {smantissa_type exponent_type} _ _.

Module SpecificFloat (Carrier : FloatCarrier) <: FloatOps.

Import Carrier.

Definition sensible_format := match radix_val radix with Zpos (xO _) ⇒ true | _ ⇒ false end.

Definition radix := radix.

Definition type := s_float smantissa_type exponent_type.

Definition toF (x : type) : float radix :=
  match x with
  | Fnan ⇒ Basic.Fnan
  | Float m e ⇒
    match mantissa_sign m with
    | Mzero ⇒ Basic.Fzero
    | Mnumber s p ⇒ Basic.Float s (MtoP p) (EtoZ e)
    end
  end.

Definition toX (x : type) := FtoX (toF x).
Definition toR (x : type) := proj_val (toX x).
Definition convert (x : type) := FtoX (toF x).

Definition fromF (f : Basic.float radix) :=
  match f with
  | Basic.Fnan ⇒ Fnan
  | Basic.Fzero ⇒ Float mantissa_zero exponent_zero
  | Basic.Float false m e ⇒ Float (ZtoM (Zpos m)) (ZtoE e)
  | Basic.Float true m e ⇒ Float (ZtoM (Zneg m)) (ZtoE e)
  end.

Definition precision := exponent_type.
Definition sfactor := exponent_type.
Definition prec p := match EtoZ p with Zpos q ⇒ q | _ ⇒ xH end.
Definition ZtoS := ZtoE.
Definition StoZ := EtoZ.
Definition PtoP n := ZtoE (Zpos n).
Definition incr_prec x y := exponent_add x (ZtoE (Zpos y)).

Definition sm1 := ZtoE (-1).

Definition zero := Float mantissa_zero exponent_zero.
Definition nan := @Fnan smantissa_type exponent_type.

Lemma zero_correct :
  toX zero = Xreal 0.

Definition mag (x : type) :=
  match x with
  | Fnan ⇒ exponent_zero
  | Float m e ⇒
    match mantissa_sign m with
    | Mzero ⇒ e
    | Mnumber _ m ⇒ exponent_add e (mantissa_digits m)
    end
  end.

Definition classify (f : type) :=
  match f with Fnan ⇒ Sig.Fnan | _ ⇒ Sig.Freal end.

Definition nan_correct := refl_equal Sig.Fnan.

Definition real (f : type) := match f with Fnan ⇒ false | _ ⇒ true end.

Definition is_nan (f : type) := match f with Fnan ⇒ true | _ ⇒ false end.

Lemma classify_correct :
  ∀ f, real f = match classify f with Freal ⇒ true | _ ⇒ false end.

Lemma real_correct :
  ∀ f, real f = match toX f with Xnan ⇒ false | _ ⇒ true end.

Lemma is_nan_correct :
  ∀ f, is_nan f = match classify f with Sig.Fnan ⇒ true | _ ⇒ false end.

Definition valid_ub (_ : type) := true.
Definition valid_lb (_ : type) := true.

Lemma valid_lb_correct :
  ∀ f, valid_lb f = match classify f with Fpinfty ⇒ false | _ ⇒ true end.

Lemma valid_ub_correct :
  ∀ f, valid_ub f = match classify f with Fminfty ⇒ false | _ ⇒ true end.

Definition fromZ n := Float (ZtoM n) exponent_zero.

Lemma fromZ_correct' :
  ∀ n, toX (fromZ n) = Xreal (IZR n).

Lemma fromZ_correct :
  ∀ n,
  (Z.abs n ≤ 256)%Z →
  toX (fromZ n) = Xreal (IZR n).

Definition fromZ_DN (p : precision) := fromZ.

Lemma fromZ_DN_correct :
  ∀ p n,
  valid_lb (fromZ_DN p n) = true ∧ le_lower (toX (fromZ_DN p n)) (Xreal (IZR n)).

Definition fromZ_UP (p : precision) := fromZ.

Lemma fromZ_UP_correct :
  ∀ p n,
  valid_ub (fromZ_UP p n) = true ∧ le_upper (Xreal (IZR n)) (toX (fromZ_UP p n)).

Lemma match_helper_1 :
  ∀ A B y2, ∀ f : A → B,
  ∀ x y1,
  f (match mantissa_sign x with Mzero ⇒ y1 | Mnumber s p ⇒ y2 s p end) =
  match mantissa_sign x with Mzero ⇒ f y1 | Mnumber s p ⇒ f (y2 s p) end.

Definition float_aux s m e : type :=
  Float ((if s : bool then mantissa_neg else mantissa_pos) m) e.

Lemma toF_float :
  ∀ s p e, valid_mantissa p →
  toF (float_aux s p e) = Basic.Float s (MtoP p) (EtoZ e).

Lemma toX_Float :
  ∀ m e, toX (Float m e) = Xreal (toR (Float m e)).

Definition neg (f : type) :=
  match f with
  | Float m e ⇒
    match mantissa_sign m with
    | Mzero ⇒ f
    | Mnumber s p ⇒ Float ((if s then mantissa_pos else mantissa_neg) p) e
    end
  | _ ⇒ f
  end.

Lemma neg_correct :
  ∀ x,
  match classify x with
  | Freal ⇒ toX (neg x) = Xneg (toX x)
  | Sig.Fnan ⇒ classify (neg x) = Sig.Fnan
  | Fminfty ⇒ classify (neg x) = Fpinfty
  | Fpinfty ⇒ classify (neg x) = Fminfty
  end.

Definition abs (f : type) :=
  match f with
  | Float m e ⇒
    match mantissa_sign m with
    | Mzero ⇒ f
    | Mnumber _ p ⇒ Float (mantissa_pos p) e
    end
  | _ ⇒ f
  end.

Lemma abs_correct :
  ∀ x, toX (abs x) = Xabs (toX x) ∧ (valid_ub (abs x) = true ).

Definition scale (f : type) d :=
  match f with
  | Float m e ⇒ Float m (exponent_add e d)
  | _ ⇒ f
  end.

Definition scale2 (f : type) d :=
  match f with
  | Float m e ⇒
    match mantissa_sign m with
    | Mzero ⇒ f
    | Mnumber s p ⇒
      match mantissa_scale2 p d with
      | (p2, d2 ) ⇒ float_aux s p2 (exponent_add e d2)
      end
    end
  | _ ⇒ f
  end.

Lemma scale2_correct :
  ∀ x d, sensible_format = true →
  toX (scale2 x d) = Xmul (toX x) (Xreal (bpow radix2 (StoZ d))).

Definition pow2_UP (p : precision) e :=
  if sensible_format then scale2 (Float (mantissa_pos mantissa_one) exponent_zero) e else Fnan.

Lemma pow2_UP_correct :
  ∀ p s, (valid_ub (pow2_UP p s) = true ∧
              le_upper (Xscale radix2 (Xreal 1) (StoZ s)) (toX (pow2_UP p s))).

Lemma ZtoS_correct:
  ∀ p z,
  (z ≤ StoZ (ZtoS z))%Z ∨ toX (pow2_UP p (ZtoS z)) = Xnan.

Definition div2 (f : type) := scale2 f sm1.

Lemma div2_correct :
  ∀ x, sensible_format = true →
  (1 / 256 ≤ Rabs (toR x))%R →
  toX (div2 x) = Xdiv (toX x) (Xreal 2).

Definition cmp_aux1 m1 m2 :=
  match mantissa_cmp m1 m2 with
  | Eq ⇒ Xeq
  | Lt ⇒ Xlt
  | Gt ⇒ Xgt
  end.

Definition cmp_aux2 m1 e1 m2 e2 :=
  let d1 := mantissa_digits m1 in
  let d2 := mantissa_digits m2 in
  match exponent_cmp (exponent_add e1 d1) (exponent_add e2 d2) with
  | Lt ⇒ Xlt
  | Gt ⇒ Xgt
  | Eq ⇒
    let nb := exponent_sub e1 e2 in
    match exponent_cmp nb exponent_zero with
    | Gt ⇒ cmp_aux1 (mantissa_shl m1 nb) m2
    | Lt ⇒ cmp_aux1 m1 (mantissa_shl m2 (exponent_neg nb))
    | Eq ⇒ cmp_aux1 m1 m2
    end
  end.

Lemma cmp_aux2_correct :
  ∀ m1 e1 m2 e2,
  valid_mantissa m1 → valid_mantissa m2 →
  cmp_aux2 m1 e1 m2 e2 = Fcmp_aux2 radix (MtoP m1) (EtoZ e1) (MtoP m2) (EtoZ e2).

Definition cmp (f1 f2 : type) :=
  match f1, f2 with
  | Fnan, _ ⇒ Xund
  | _, Fnan ⇒ Xund
  | Float m1 e1, Float m2 e2 ⇒
    match mantissa_sign m1, mantissa_sign m2 with
    | Mzero, Mzero ⇒ Xeq
    | Mzero, Mnumber true _ ⇒ Xgt
    | Mzero, Mnumber false _ ⇒ Xlt
    | Mnumber true _, Mzero ⇒ Xlt
    | Mnumber false _, Mzero ⇒ Xgt
    | Mnumber true _, Mnumber false _ ⇒ Xlt
    | Mnumber false _, Mnumber true _ ⇒ Xgt
    | Mnumber true p1, Mnumber true p2 ⇒ cmp_aux2 p2 e2 p1 e1
    | Mnumber false p1, Mnumber false p2 ⇒ cmp_aux2 p1 e1 p2 e2
    end
  end.

Lemma cmp_correct :
  ∀ x y,
  cmp x y =
  match classify x, classify y with
  | Sig.Fnan, _ | _, Sig.Fnan ⇒ Xund
  | Fminfty, Fminfty ⇒ Xeq
  | Fminfty, _ ⇒ Xlt
  | _, Fminfty ⇒ Xgt
  | Fpinfty, Fpinfty ⇒ Xeq
  | _, Fpinfty ⇒ Xlt
  | Fpinfty, _ ⇒ Xgt
  | Freal, Freal ⇒ Xcmp (toX x) (toX y)
  end.

Definition min x y :=
  match cmp x y with
  | Xlt ⇒ x
  | Xeq ⇒ x
  | Xgt ⇒ y
  | Xund ⇒ nan
  end.

Lemma min_correct :
  ∀ x y,
  match classify x, classify y with
  | Sig.Fnan, _ | _, Sig.Fnan ⇒ classify (min x y) = Sig.Fnan
  | Fminfty, _ | _, Fminfty ⇒ classify (min x y) = Fminfty
  | Fpinfty, _ ⇒ min x y = y
  | _, Fpinfty ⇒ min x y = x
  | Freal, Freal ⇒ toX (min x y) = Xmin (toX x) (toX y)
  end.

Definition max x y :=
  match cmp x y with
  | Xlt ⇒ y
  | Xeq ⇒ y
  | Xgt ⇒ x
  | Xund ⇒ nan
  end.

Lemma max_correct :
  ∀ x y,
  match classify x, classify y with
  | Sig.Fnan, _ | _, Sig.Fnan ⇒ classify (max x y) = Sig.Fnan
  | Fpinfty, _ | _, Fpinfty ⇒ classify (max x y) = Fpinfty
  | Fminfty, _ ⇒ max x y = y
  | _, Fminfty ⇒ max x y = x
  | Freal, Freal ⇒ toX (max x y) = Xmax (toX x) (toX y)
  end.

Definition adjust_mantissa mode m pos sign :=
  if need_change mode (mantissa_even m) pos sign then mantissa_add m mantissa_one else m.

Lemma adjust_mantissa_correct :
  ∀ mode m pos sign,
  valid_mantissa m →
  MtoP (adjust_mantissa mode m pos sign) = Generic.adjust_mantissa mode (MtoP m) pos sign ∧
  valid_mantissa (adjust_mantissa mode m pos sign).

Definition round_aux mode prec sign m1 e1 pos :=
  let prec := match exponent_cmp prec exponent_zero with Gt ⇒ prec | _ ⇒ exponent_one end in
  let nb := exponent_sub (mantissa_digits m1) prec in
  let e2 := exponent_add e1 nb in
  match exponent_cmp nb exponent_zero with
  | Gt ⇒
    let (m2, pos2) := mantissa_shr m1 nb pos in
    float_aux sign (adjust_mantissa mode m2 pos2 sign) e2
  | Eq ⇒ float_aux sign (adjust_mantissa mode m1 pos sign) e1
  | Lt ⇒ float_aux sign m1 e1
  end.

Lemma round_aux_correct :
  ∀ mode p sign m1 e1 pos,
  valid_mantissa m1 →
  FtoX (toF (round_aux mode p sign m1 e1 pos)) =
  FtoX (Fround_at_prec mode (prec p) (@Generic.Ufloat radix sign (MtoP m1) (EtoZ e1) pos)).

Definition round_at_exp_aux mode e2 sign m1 e1 pos :=
  let nb := exponent_sub e2 e1 in
  match exponent_cmp nb exponent_zero with
  | Gt ⇒
    match exponent_cmp (mantissa_digits m1) nb with
    | Gt ⇒
      let (m2, pos2) := mantissa_shr m1 nb pos in
      float_aux sign (adjust_mantissa mode m2 pos2 sign) e2
    | Eq ⇒
      let pos2 := mantissa_shrp m1 nb pos in
      if need_change_zero mode pos2 sign then
        float_aux sign mantissa_one e2
      else zero
    | Lt ⇒
      let pos2 := match pos with pos_Eq ⇒ pos_Eq | _ ⇒ pos_Lo end in
      if need_change_zero mode pos_Lo sign then
        float_aux sign mantissa_one e2
      else zero
    end
  | Eq ⇒ float_aux sign (adjust_mantissa mode m1 pos sign) e1
  | Lt ⇒
    float_aux sign m1 e1
  end.

Lemma toF_zero : toF zero = Fzero.

Lemma round_at_exp_aux_correct :
  ∀ mode e2 sign m1 e1 pos,
  valid_mantissa m1 →
  FtoX (toF (round_at_exp_aux mode e2 sign m1 e1 pos)) =
  FtoX (Fround_at_exp mode (EtoZ e2) (@Generic.Ufloat radix sign (MtoP m1) (EtoZ e1) pos)).

Definition mul mode prec (x y : type) :=
  match x, y with
  | Fnan, _ ⇒ x
  | _, Fnan ⇒ y
  | Float mx ex, Float my ey ⇒
    match mantissa_sign mx, mantissa_sign my with
    | Mzero, _ ⇒ x
    | _, Mzero ⇒ y
    | Mnumber sx mx, Mnumber sy my ⇒
      round_aux mode prec (xorb sx sy) (mantissa_mul mx my) (exponent_add ex ey) pos_Eq
    end
  end.

Lemma mul_correct :
  ∀ mode p x y,
  toX (mul mode p x y) = Xround radix mode (prec p) (Xmul (toX x) (toX y)).

Definition mul_UP := mul rnd_UP.

Definition is_non_neg x :=
  valid_ub x = true
  ∧ match toX x with Xnan ⇒ True | Xreal r ⇒ (0 ≤ r)%R end.

Definition is_pos x :=
  valid_ub x = true
  ∧ match toX x with Xnan ⇒ True | Xreal r ⇒ (0 < r)%R end.

Definition is_non_pos x :=
  valid_lb x = true
  ∧ match toX x with Xnan ⇒ True | Xreal r ⇒ (r ≤ 0)%R end.

Definition is_neg x :=
  valid_lb x = true
  ∧ match toX x with Xnan ⇒ True | Xreal r ⇒ (r < 0)%R end.

Definition is_non_neg_real x :=
  match toX x with Xnan ⇒ False | Xreal r ⇒ (0 ≤ r)%R end.

Definition is_pos_real x :=
  match toX x with Xnan ⇒ False | Xreal r ⇒ (0 < r)%R end.

Definition is_non_pos_real x :=
  match toX x with Xnan ⇒ False | Xreal r ⇒ (r ≤ 0)%R end.

Definition is_neg_real x :=
  match toX x with Xnan ⇒ False | Xreal r ⇒ (r < 0)%R end.

Lemma mul_UP_correct :
  ∀ p x y,
    ((is_non_neg x ∧ is_non_neg y )
     ∨ (is_non_pos x ∧ is_non_pos y )
     ∨ (is_non_pos_real x ∧ is_non_neg_real y )
     ∨ (is_non_neg_real x ∧ is_non_pos_real y ))
    → (valid_ub (mul_UP p x y) = true
        ∧ le_upper (Xmul (toX x) (toX y)) (toX (mul_UP p x y))).

Definition mul_DN := mul rnd_DN.

Lemma mul_DN_correct :
  ∀ p x y,
    ((is_non_neg_real x ∧ is_non_neg_real y )
     ∨ (is_non_pos_real x ∧ is_non_pos_real y )
     ∨ (is_non_neg x ∧ is_non_pos y )
     ∨ (is_non_pos x ∧ is_non_neg y ))
    → (valid_lb (mul_DN p x y) = true
        ∧ le_lower (toX (mul_DN p x y)) (Xmul (toX x) (toX y))).

Definition add_exact_aux1 sx sy mx my e :=
  if eqb sx sy then
    float_aux sx (mantissa_add mx my) e
  else
    match mantissa_cmp mx my with
    | Eq ⇒ zero
    | Gt ⇒ float_aux sx (mantissa_sub mx my) e
    | Lt ⇒ float_aux sy (mantissa_sub my mx) e
    end.

Definition add_exact_aux2 sx sy mx my ex ey :=
  let nb := exponent_sub ex ey in
  match exponent_cmp nb exponent_zero with
  | Gt ⇒ add_exact_aux1 sx sy (mantissa_shl mx nb) my ey
  | Lt ⇒ add_exact_aux1 sx sy mx (mantissa_shl my (exponent_neg nb)) ex
  | Eq ⇒ add_exact_aux1 sx sy mx my ex
  end.

Definition add_exact (x y : type) :=
  match x, y with
  | Fnan, _ ⇒ x
  | _, Fnan ⇒ y
  | Float mx ex, Float my ey ⇒
    match mantissa_sign mx, mantissa_sign my with
    | Mzero, _ ⇒ y
    | _, Mzero ⇒ x
    | Mnumber sx mx, Mnumber sy my ⇒
      add_exact_aux2 sx sy mx my ex ey
    end
  end.

Lemma add_exact_aux_correct :
  ∀ sx mx ex sy my ey,
  valid_mantissa mx → valid_mantissa my →
  FtoX (toF (add_exact_aux2 sx sy mx my ex ey)) =
  FtoX (Fround_none (Fadd_slow_aux2 radix sx sy (MtoP mx) (MtoP my) (EtoZ ex) (EtoZ ey) pos_Eq)).

Lemma add_exact_correct :
  ∀ x y, toX (add_exact x y) = Xadd (toX x) (toX y).

Definition add_slow_aux1 mode prec sx sy mx my e :=
  if eqb sx sy then
    round_aux mode prec sx (mantissa_add mx my) e pos_Eq
  else
    match mantissa_cmp mx my with
    | Eq ⇒ zero
    | Gt ⇒ round_aux mode prec sx (mantissa_sub mx my) e pos_Eq
    | Lt ⇒ round_aux mode prec sy (mantissa_sub my mx) e pos_Eq
    end.

Lemma add_slow_aux1_correct :
  ∀ mode p sx sy mx my e,
  valid_mantissa mx →
  valid_mantissa my →
  FtoX (toF (add_slow_aux1 mode p sx sy mx my e)) =
  FtoX (Fround_at_prec mode (prec p) (Fadd_slow_aux1 radix sx sy (MtoP mx) (MtoP my) (EtoZ e) pos_Eq)).

Definition add_slow_aux2 mode prec sx sy mx my ex ey :=
  let nb := exponent_sub ex ey in
  match exponent_cmp nb exponent_zero with
  | Gt ⇒ add_slow_aux1 mode prec sx sy (mantissa_shl mx nb) my ey
  | Lt ⇒ add_slow_aux1 mode prec sx sy mx (mantissa_shl my (exponent_neg nb)) ex
  | Eq ⇒ add_slow_aux1 mode prec sx sy mx my ex
  end.

Lemma add_slow_aux2_correct :
  ∀ mode p sx sy mx my ex ey,
  valid_mantissa mx →
  valid_mantissa my →
  FtoX (toF (add_slow_aux2 mode p sx sy mx my ex ey)) =
  FtoX (Fround_at_prec mode (prec p) (Fadd_slow_aux2 radix sx sy (MtoP mx) (MtoP my) (EtoZ ex) (EtoZ ey) pos_Eq)).

Definition add_slow mode prec (x y : type) :=
  match x, y with
  | Fnan, _ ⇒ x
  | _, Fnan ⇒ y
  | Float mx ex, Float my ey ⇒
    match mantissa_sign mx, mantissa_sign my with
    | Mzero, Mzero ⇒ x
    | Mzero, Mnumber sy py ⇒ round_aux mode prec sy py ey pos_Eq
    | Mnumber sx px, Mzero ⇒ round_aux mode prec sx px ex pos_Eq
    | Mnumber sx px, Mnumber sy py ⇒
      add_slow_aux2 mode prec sx sy px py ex ey
    end
  end.

Lemma add_slow_correct :
  ∀ mode p x y,
  toX (add_slow mode p x y) = Xround radix mode (prec p) (Xadd (toX x) (toX y)).

Definition add_UP := add_slow rnd_UP.

Lemma add_UP_correct :
  ∀ p x y, valid_ub x = true → valid_ub y = true
    → (valid_ub (add_UP p x y) = true
       ∧ le_upper (Xadd (toX x) (toX y)) (toX (add_UP p x y))).

Definition add_DN := add_slow rnd_DN.

Lemma add_DN_correct :
  ∀ p x y, valid_lb x = true → valid_lb y = true
    → (valid_lb (add_DN p x y) = true
       ∧ le_lower (toX (add_DN p x y)) (Xadd (toX x) (toX y))).

Definition sub_UP prec (x y : type) := add_UP prec x (neg y).

Lemma sub_UP_correct :
  ∀ p x y, valid_ub x = true → valid_lb y = true
    → (valid_ub (sub_UP p x y) = true
       ∧ le_upper (Xsub (toX x) (toX y)) (toX (sub_UP p x y))).

Definition sub_DN prec (x y : type) := add_DN prec x (neg y).

Lemma sub_DN_correct :
  ∀ p x y, valid_lb x = true → valid_ub y = true
    → (valid_lb (sub_DN p x y) = true
       ∧ le_lower (toX (sub_DN p x y)) (Xsub (toX x) (toX y))).

Definition div_aux mode prec s mx my e :=
  let (q, pos) := mantissa_div mx my in
  round_aux mode prec s q e pos.

Definition div mode prec (x y : type) :=
  match x, y with
  | Fnan, _ ⇒ x
  | _, Fnan ⇒ y
  | Float mx ex, Float my ey ⇒
    let prec := match exponent_cmp prec exponent_zero with Gt ⇒ prec | _ ⇒ exponent_one end in
    match mantissa_sign mx, mantissa_sign my with
    | _, Mzero ⇒ Fnan
    | Mzero, _ ⇒ x
    | Mnumber sx px, Mnumber sy py ⇒
      let dx := mantissa_digits px in
      let dy := mantissa_digits py in
      let e := exponent_sub ex ey in
      let nb := exponent_sub (exponent_add dy prec) dx in
      match exponent_cmp nb exponent_zero with
      | Gt ⇒
        div_aux mode prec (xorb sx sy) (mantissa_shl px nb) py (exponent_sub e nb)
      | _ ⇒ div_aux mode prec (xorb sx sy) px py e
      end
    end
  end.

Theorem div_correct :
  ∀ mode p x y,
  toX (div mode p x y) = Xround radix mode (prec p) (Xdiv (toX x) (toX y)).

Definition div_UP := div rnd_UP.

Lemma div_UP_correct :
  ∀ p x y,
    ((is_non_neg x ∧ is_pos_real y )
     ∨ (is_non_pos x ∧ is_neg_real y )
     ∨ (is_non_neg_real x ∧ is_neg_real y )
     ∨ (is_non_pos_real x ∧ is_pos_real y ))
    → (valid_ub (div_UP p x y) = true
        ∧ le_upper (Xdiv (toX x) (toX y)) (toX (div_UP p x y))).

Definition div_DN := div rnd_DN.

Lemma div_DN_correct :
  ∀ p x y,
    ((is_non_neg x ∧ is_neg_real y )
     ∨ (is_non_pos x ∧ is_pos_real y )
     ∨ (is_non_neg_real x ∧ is_pos_real y )
     ∨ (is_non_pos_real x ∧ is_neg_real y ))
    → (valid_lb (div_DN p x y) = true
        ∧ le_lower (toX (div_DN p x y)) (Xdiv (toX x) (toX y))).

Definition sqrt mode prec (f : type) :=
  match f with
  | Fnan ⇒ f
  | Float m e ⇒
    match mantissa_sign m with
    | Mzero ⇒ f
    | Mnumber true _ ⇒ Fnan
    | Mnumber false p ⇒
      let d := mantissa_digits p in
      let prec := match exponent_cmp prec exponent_zero with Gt ⇒ prec | _ ⇒ exponent_one end in
      let s := exponent_sub (exponent_add prec prec) d in
      let s := match exponent_cmp s exponent_zero with Gt ⇒ s | _ ⇒ exponent_zero end in
      let (e', r) := exponent_div2_floor (exponent_sub e s) in
      let s := if r then exponent_add s exponent_one else s in
      let m := match exponent_cmp s exponent_zero with Gt ⇒ mantissa_shl p s | _ ⇒ p end in
      let (m', pos) := mantissa_sqrt m in
      round_aux mode prec false m' e' pos
    end
  end.

Lemma sqrt_correct :
  ∀ mode p x,
  toX (sqrt mode p x) = Xround radix mode (prec p) (Xsqrt_nan (toX x)).

Definition sqrt_UP := sqrt rnd_UP.

Lemma sqrt_UP_correct :
  ∀ p x,
  valid_ub (sqrt_UP p x) = true
  ∧ le_upper (Xsqrt (toX x)) (toX (sqrt_UP p x)).

Definition sqrt_DN := sqrt rnd_DN.

Lemma sqrt_DN_correct :
  ∀ p x,
    valid_lb x = true
    → (valid_lb (sqrt_DN p x) = true
        ∧ le_lower (toX (sqrt_DN p x)) (Xsqrt (toX x))).

Definition nearbyint mode (f : type) :=
  match f with
  | Fnan ⇒ f
  | Float m e ⇒
    match mantissa_sign m with
    | Mnumber s m ⇒ round_at_exp_aux mode exponent_zero s m e pos_Eq
    | Mzero ⇒ zero
    end
  end.

Definition nearbyint_UP := nearbyint.

Definition nearbyint_DN := nearbyint.

Lemma nearbyint_correct :
  ∀ mode x,
  toX (nearbyint mode x) = Xnearbyint mode (toX x).

Lemma nearbyint_UP_correct :
  ∀ mode x,
  valid_ub (nearbyint_UP mode x) = true
  ∧ le_upper (Xnearbyint mode (toX x)) (toX (nearbyint_UP mode x)).

Lemma nearbyint_DN_correct :
  ∀ mode x,
  valid_lb (nearbyint_DN mode x) = true
  ∧ le_lower (toX (nearbyint_DN mode x)) (Xnearbyint mode (toX x)).

Definition midpoint (x y : type) := scale2 (add_exact x y) sm1.

Lemma midpoint_correct :
  ∀ x y,
  sensible_format = true →
  real x = true → real y = true → (toR x ≤ toR y)%R
  → real (midpoint x y) = true ∧ (toR x ≤ toR (midpoint x y) ≤ toR y)%R.

End SpecificFloat.