Library Interval.Float.Sig

From Coq Require Import ZArith Reals.
From Flocq Require Import Zaux Raux.

Require Import Xreal.
Require Import Basic.

Variant fclass := Freal | Fnan | Fminfty | Fpinfty.
Module Type FloatOps.

Parameter sensible_format : bool.

Parameter radix : radix.
Parameter type : Type.
Parameter toF : type → float radix.

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

Parameter precision : Type.
Parameter sfactor : Type.
Parameter prec : precision → positive.
Parameter PtoP : positive → precision.
Parameter ZtoS : Z → sfactor.
Parameter StoZ : sfactor → Z.

Parameter incr_prec : precision → positive → precision.

Parameter zero : type.
Parameter nan : type.

Parameter fromZ : Z → type.
Parameter fromZ_DN : precision → Z → type.
Parameter fromZ_UP : precision → Z → type.

Parameter fromF : float radix → type.
Parameter classify : type → fclass.
Parameter real : type → bool.
Parameter is_nan : type → bool.
Parameter mag : type → sfactor.
Parameter valid_ub : type → bool. Parameter valid_lb : type → bool.
Parameter cmp : type → type → Xcomparison.
Parameter min : type → type → type.
Parameter max : type → type → type.
Parameter neg : type → type.
Parameter abs : type → type.
Parameter scale : type → sfactor → type.
Parameter div2 : type → type.
Parameter add_UP : precision → type → type → type.
Parameter add_DN : precision → type → type → type.
Parameter sub_UP : precision → type → type → type.
Parameter sub_DN : precision → type → type → type.
Parameter mul_UP : precision → type → type → type.
Parameter mul_DN : precision → type → type → type.
Parameter pow2_UP : precision → sfactor → type.
Parameter div_UP : precision → type → type → type.
Parameter div_DN : precision → type → type → type.
Parameter sqrt_UP : precision → type → type.
Parameter sqrt_DN : precision → type → type.
Parameter nearbyint_UP : rounding_mode → type → type.
Parameter nearbyint_DN : rounding_mode → type → type.
Parameter midpoint : type → type → type.

Parameter zero_correct : toX zero = Xreal 0.
Parameter nan_correct : classify nan = Fnan.

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

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

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

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

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

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

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

Parameter mag_correct :
  ∀ f, (Rabs (toR f) < bpow radix (StoZ (mag f)))%R.

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

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

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

Parameter min_correct :
  ∀ x y,
  match classify x, classify y with
  | Fnan, _ | _, Fnan ⇒ classify (min x y) = 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.

Parameter max_correct :
  ∀ x y,
  match classify x, classify y with
  | Fnan, _ | _, Fnan ⇒ classify (max x y) = 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.

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

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

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

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

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

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

Parameter 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 is_non_neg x :=
  valid_ub x = true
  ∧ match toX x with Xnan ⇒ True | Xreal r ⇒ (0 ≤ r)%R end.

Definition is_non_neg' x :=
  match toX x with Xnan ⇒ valid_ub x = 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_non_pos' x :=
  match toX x with Xnan ⇒ valid_lb x = 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.

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

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

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

Definition is_real_ub x :=
  match toX x with Xnan ⇒ valid_ub x = true | _ ⇒ True end.

Definition is_real_lb x :=
  match toX x with Xnan ⇒ valid_lb x = true | _ ⇒ True end.

Parameter div_UP_correct :
  ∀ p x y,
  ((is_real_ub x ∧ is_pos_real y) ∨
   (is_real_lb x ∧ is_neg_real y)) →
  valid_ub (div_UP p x y) = true ∧
  le_upper (Xdiv (toX x) (toX y)) (toX (div_UP p x y)).

Parameter div_DN_correct :
  ∀ p x y,
  ((is_real_ub x ∧ is_neg_real y) ∨
   (is_real_lb x ∧ is_pos_real y)) →
  valid_lb (div_DN p x y) = true ∧
  le_lower (toX (div_DN p x y)) (Xdiv (toX x) (toX y)).

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

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

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

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

Parameter 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 FloatOps.

Module FloatExt (F : FloatOps).

Lemma valid_lb_real f : F.real f = true → F.valid_lb f = true.

Lemma valid_ub_real f : F.real f = true → F.valid_ub f = true.

Lemma valid_lb_nan : F.valid_lb F.nan = true.

Lemma valid_ub_nan : F.valid_ub F.nan = true.

Lemma valid_lb_zero : F.valid_lb F.zero = true.

Lemma valid_ub_zero : F.valid_ub F.zero = true.

Lemma nan_correct : F.toX F.nan = Xnan.

Lemma is_nan_nan : F.is_nan F.nan = true.

Lemma neg_correct x : F.toX (F.neg x) = Xneg (F.toX x).

Lemma valid_lb_neg x : F.valid_lb (F.neg x) = F.valid_ub x.

Lemma valid_ub_neg x : F.valid_ub (F.neg x) = F.valid_lb x.

Lemma real_neg x : F.real (F.neg x) = F.real x.

Lemma is_nan_neg x : F.is_nan (F.neg x) = F.is_nan x.

Definition cmp x y:=
  if F.real x then
    if F.real y then
      F.cmp x y
    else Xund
  else Xund.

Lemma cmp_correct :
  ∀ x y,
  cmp x y = Xcmp (F.toX x) (F.toX y).

Definition le' x y :=
  match cmp x y with
  | Xlt | Xeq ⇒ true
  | Xgt | Xund ⇒ false
  end.

Lemma le'_correct :
  ∀ x y,
  le' x y = true →
  match F.toX x, F.toX y with
  | Xreal xr, Xreal yr ⇒ (xr ≤ yr)%R
  | _, _ ⇒ False
  end.

Definition lt' x y :=
  match cmp x y with
  | Xlt ⇒ true
  | _ ⇒ false
  end.

Lemma lt'_correct :
  ∀ x y,
  lt' x y = true →
  match F.toX x, F.toX y with
  | Xreal xr, Xreal yr ⇒ (xr < yr)%R
  | _, _ ⇒ False
  end.

Definition le x y :=
  match F.cmp x y with
  | Xgt ⇒ false
  | _ ⇒ true
  end.

Lemma le_correct :
  ∀ x y,
  F.toX x = Xreal (F.toR x) →
  F.toX y = Xreal (F.toR y) →
  le x y = Rle_bool (F.toR x) (F.toR y).

Definition lt x y :=
  match F.cmp x y with
  | Xlt ⇒ true
  | _ ⇒ false
  end.

Lemma lt_correct :
  ∀ x y,
  F.toX x = Xreal (F.toR x) →
  F.toX y = Xreal (F.toR y) →
  lt x y = Rlt_bool (F.toR x) (F.toR y).

Lemma real_correct :
  ∀ x,
  F.real x = true →
  F.toX x = Xreal (F.toR x).

Lemma real_correct_false :
  ∀ x,
  F.real x = false →
  F.toX x = Xnan.

Inductive toX_prop (x : F.type) : ExtendedR → Prop :=
  | toX_Xnan : toX_prop x Xnan
  | toX_Xreal : F.toX x = Xreal (F.toR x) → toX_prop x (Xreal (F.toR x)).

Lemma toX_spec :
  ∀ x, toX_prop x (F.toX x).

Lemma classify_real :
  ∀ x, F.real x = true → F.classify x = Freal.

Lemma classify_zero : F.classify F.zero = Freal.

Lemma min_valid_lb x y :
  F.valid_lb x = true → F.valid_lb y = true →
  (F.valid_lb (F.min x y) = true
   ∧ F.toX (F.min x y) = Xmin (F.toX x) (F.toX y)).

Lemma max_valid_ub x y :
  F.valid_ub x = true → F.valid_ub y = true →
  (F.valid_ub (F.max x y) = true
   ∧ F.toX (F.max x y) = Xmax (F.toX x) (F.toX y)).

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

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

Lemma sqr_UP_correct :
  ∀ prec x,
  F.valid_lb x = true ∨ F.valid_ub x = true →
  F.valid_ub (F.mul_UP prec x x) = true ∧
  le_upper (F.toX x × F.toX x)%XR (F.toX (F.mul_UP prec x x)).

End FloatExt.