Require Import Int63Compat.
From Coq Require Import ZArith Reals Floats SpecFloat.
Require Import Zaux BinarySingleNaN.

Module Import Compat.
Definition ldexp f (_ : Z) : float := f.
Definition frexp (f : float) := (f, Z0).
End Compat.
Import FloatOps.
Module Import Z.
Notation ldexp := ldexp.
Notation frexp := frexp.
End Z.
Import Floats.
Import Zaux BinarySingleNaN.

Lemma Z_ldexp_spec f e :
  Prim2SF (Z.ldexp f e) = SFldexp prec emax (Prim2SF f) e.

Lemma Z_frexp_spec f :
  let (m, e) := Z.frexp f in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF f).

Definition Prim2B (x : float) : binary_float prec emax :=
  SF2B (Prim2SF x) (Prim2SF_valid x).

Definition B2Prim (x : binary_float prec emax) : float :=
  SF2Prim (B2SF x).

Lemma B2Prim_Prim2B : ∀ x, B2Prim (Prim2B x) = x.

Lemma Prim2B_B2Prim : ∀ x, Prim2B (B2Prim x) = x.

Lemma Prim2B_inj : ∀ x y, Prim2B x = Prim2B y → x = y.

Lemma B2Prim_inj : ∀ x y, B2Prim x = B2Prim y → x = y.

Lemma B2SF_Prim2B : ∀ x, B2SF (Prim2B x) = Prim2SF x.

Lemma Prim2SF_B2Prim : ∀ x, Prim2SF (B2Prim x) = B2SF x.

Local Instance Hprec : FLX.Prec_gt_0 prec := eq_refl _.

Local Instance Hmax : Prec_lt_emax prec emax := eq_refl _.

Theorem opp_equiv : ∀ x, Prim2B (- x) = Bopp (Prim2B x).

Theorem abs_equiv : ∀ x, Prim2B (abs x) = Babs (Prim2B x).

Theorem compare_equiv :
  ∀ x y,
  (x ?= y)%float = flatten_cmp_opt (Bcompare (Prim2B x) (Prim2B y)).

Lemma round_nearest_even_equiv s m l :
  round_nearest_even m l = choice_mode mode_NE s m l.

Lemma binary_round_aux_equiv sx mx ex lx :
  SpecFloat.binary_round_aux prec emax sx mx ex lx
  = binary_round_aux prec emax mode_NE sx mx ex lx.

Theorem mul_equiv :
  ∀ x y,
  Prim2B (x × y) = Bmult mode_NE (Prim2B x) (Prim2B y).

Lemma binary_round_equiv s m e :
  SpecFloat.binary_round prec emax s m e =
  binary_round prec emax mode_NE s m e.

Lemma binary_normalize_equiv m e szero :
  SpecFloat.binary_normalize prec emax m e szero
  = B2SF (binary_normalize prec emax Hprec Hmax mode_NE m e szero).

Theorem add_equiv :
  ∀ x y,
  Prim2B (x + y) = Bplus mode_NE (Prim2B x) (Prim2B y).

Theorem sub_equiv :
  ∀ x y,
  Prim2B (x - y) = Bminus mode_NE (Prim2B x) (Prim2B y).

Theorem div_equiv :
  ∀ x y,
  Prim2B (x / y) = Bdiv mode_NE (Prim2B x) (Prim2B y).

Theorem sqrt_equiv :
  ∀ x, Prim2B (sqrt x) = Bsqrt mode_NE (Prim2B x).

Theorem normfr_mantissa_equiv :
  ∀ x,
  to_Z (normfr_mantissa x) = Z.of_N (Bnormfr_mantissa (Prim2B x)).

Theorem ldexp_equiv :
  ∀ x e,
  Prim2B (Z.ldexp x e) = Bldexp mode_NE (Prim2B x) e.

Theorem ldshiftexp_equiv :
  ∀ x e,
  Prim2B (ldshiftexp x e) = Bldexp mode_NE (Prim2B x) (to_Z e - shift).

Theorem frexp_equiv :
  ∀ x : float,
  let (m, e) := Z.frexp x in
  (Prim2B m, e) = Bfrexp (Prim2B x).

Theorem frshiftexp_equiv :
  ∀ x : float,
  let (m, e) := frshiftexp x in
  (Prim2B m, (to_Z e - shift)%Z) = Bfrexp (Prim2B x).

Theorem infinity_equiv : infinity = B2Prim (B754_infinity false).

Theorem neg_infinity_equiv : neg_infinity = B2Prim (B754_infinity true).

Theorem nan_equiv : nan = B2Prim B754_nan.

Theorem zero_equiv : zero = B2Prim (B754_zero false).

Theorem neg_zero_equiv : neg_zero = B2Prim (B754_zero true).

Theorem one_equiv : one = B2Prim Bone.

Theorem two_equiv : two = B2Prim (Bplus mode_NE Bone Bone).

Theorem ulp_equiv :
  ∀ x, Prim2B (ulp x) = Bulp' (Prim2B x).

Theorem next_up_equiv :
  ∀ x, Prim2B (next_up x) = Bsucc (Prim2B x).

Theorem next_down_equiv :
  ∀ x, Prim2B (next_down x) = Bpred (Prim2B x).

Theorem is_nan_equiv :
  ∀ x, PrimFloat.is_nan x = is_nan (Prim2B x).

Theorem is_zero_equiv :
  ∀ x,
  is_zero x = match Prim2B x with B754_zero _ ⇒ true | _ ⇒ false end.

Theorem is_infinity_equiv :
  ∀ x,
  is_infinity x = match Prim2B x with B754_infinity _ ⇒ true | _ ⇒ false end.

Theorem get_sign_equiv : ∀ x, get_sign x = Bsign (Prim2B x).

Theorem is_finite_equiv :
  ∀ x, PrimFloat.is_finite x = is_finite (Prim2B x).

Theorem of_int63_equiv :
  ∀ i,
  Prim2B (of_int63 i)
  = binary_normalize prec emax Hprec Hmax mode_NE (to_Z i) 0 false.

Theorem eqb_equiv :
  ∀ x y,
  eqb x y = Beqb (Prim2B x) (Prim2B y).

Theorem ltb_equiv :
  ∀ x y,
  ltb x y = Bltb (Prim2B x) (Prim2B y).

Theorem leb_equiv :
  ∀ x y,
  leb x y = Bleb (Prim2B x) (Prim2B y).