IEEE-754 arithmetic

From Coq Require Import Psatz.
Require Import Core Digits Round Bracket Operations Div Sqrt Relative SpecFloatCompat.

Definition SF2R beta x :=
  match x with
  | S754_finite s m e => F2R (Float beta (cond_Zopp s (Zpos m)) e)
  | _ => 0%R
  end.

Class Prec_lt_emax prec emax := prec_lt_emax : (prec < emax)%Z.
Arguments prec_lt_emax prec emax {Prec_lt_emax}.

Section Binary.

Variable prec emax : Z.
Context (prec_gt_0_ : Prec_gt_0 prec).
Context (prec_lt_emax_ : Prec_lt_emax prec emax).

Notation emin := (emin prec emax).
Notation fexp := (fexp prec emax).
Instance fexp_correct : Valid_exp fexp := FLT_exp_valid emin prec.
Instance fexp_monotone : Monotone_exp fexp := FLT_exp_monotone emin prec.

Notation canonical_mantissa := (canonical_mantissa prec emax).

Notation bounded := (bounded prec emax).

Notation valid_binary := (valid_binary prec emax).

Inductive binary_float :=
  | B754_zero (s : bool)
  | B754_infinity (s : bool)
  | B754_nan : binary_float
  | B754_finite (s : bool) (m : positive) (e : Z) :
    bounded m e = true -> binary_float.

Definition SF2B x :=
  match x as x return valid_binary x = true -> binary_float with
  | S754_finite s m e => B754_finite s m e
  | S754_infinity s => fun _ => B754_infinity s
  | S754_zero s => fun _ => B754_zero s
  | S754_nan => fun _ => B754_nan
  end.

Definition B2SF x :=
  match x with
  | B754_finite s m e _ => S754_finite s m e
  | B754_infinity s => S754_infinity s
  | B754_zero s => S754_zero s
  | B754_nan => S754_nan
  end.

Definition B2R f :=
  match f with
  | B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e)
  | _ => 0%R
  end.

Theorem SF2R_B2SF :
  forall x,
  SF2R radix2 (B2SF x) = B2R x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float, SF2R radix2 (B2SF x) = B2R x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float, SF2R radix2 (B2SF x) = B2R x
now intros [sx|sx| |sx mx ex Hx].
Qed.

Theorem B2SF_SF2B :
  forall x Hx,
  B2SF (SF2B x Hx) = x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (Hx : valid_binary x = true),
B2SF (SF2B x Hx) = x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (Hx : valid_binary x = true),
B2SF (SF2B x Hx) = x
now intros [sx|sx| |sx mx ex] Hx.
Qed.

Theorem valid_binary_B2SF :
  forall x,
  valid_binary (B2SF x) = true.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float, valid_binary (B2SF x) = true
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float, valid_binary (B2SF x) = true
now intros [sx|sx| |sx mx ex Hx].
Qed.

Theorem SF2B_B2SF :
  forall x H,
  SF2B (B2SF x) H = x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : binary_float)
  (H : valid_binary (B2SF x) = true),
SF2B (B2SF x) H = x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : binary_float)
  (H : valid_binary (B2SF x) = true),
SF2B (B2SF x) H = x
intros [sx|sx| |sx mx ex Hx] H ; try easy.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
H:valid_binary (B2SF (B754_finite sx mx ex Hx)) =
true
SF2B (B2SF (B754_finite sx mx ex Hx)) H =
B754_finite sx mx ex Hx
apply f_equal, eqbool_irrelevance.
Qed.

Theorem SF2B_B2SF_valid :
  forall x,
  SF2B (B2SF x) (valid_binary_B2SF x) = x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
SF2B (B2SF x) (valid_binary_B2SF x) = x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
SF2B (B2SF x) (valid_binary_B2SF x) = x
intros x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
x:binary_float
SF2B (B2SF x) (valid_binary_B2SF x) = x
apply SF2B_B2SF.
Qed.

Theorem B2R_SF2B :
  forall x Hx,
  B2R (SF2B x Hx) = SF2R radix2 x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (Hx : valid_binary x = true),
B2R (SF2B x Hx) = SF2R radix2 x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (Hx : valid_binary x = true),
B2R (SF2B x Hx) = SF2R radix2 x
now intros [sx|sx| |sx mx ex] Hx.
Qed.

Theorem match_SF2B :
  forall {T} fz fi fn ff x Hx,
  match SF2B x Hx return T with
  | B754_zero sx => fz sx
  | B754_infinity sx => fi sx
  | B754_nan => fn
  | B754_finite sx mx ex _ => ff sx mx ex
  end =
  match x with
  | S754_zero sx => fz sx
  | S754_infinity sx => fi sx
  | S754_nan => fn
  | S754_finite sx mx ex => ff sx mx ex
  end.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (T : Type) (fz fi : bool -> T) (fn : T)
  (ff : bool -> positive -> Z -> T) (x : spec_float)
  (Hx : valid_binary x = true),
match SF2B x Hx with
| B754_zero sx => fz sx
| B754_infinity sx => fi sx
| B754_nan => fn
| B754_finite sx mx ex _ => ff sx mx ex
end =
match x with
| S754_zero sx => fz sx
| S754_infinity sx => fi sx
| S754_nan => fn
| S754_finite sx mx ex => ff sx mx ex
end
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (T : Type) (fz fi : bool -> T) (fn : T)
  (ff : bool -> positive -> Z -> T) (x : spec_float)
  (Hx : valid_binary x = true),
match SF2B x Hx with
| B754_zero sx => fz sx
| B754_infinity sx => fi sx
| B754_nan => fn
| B754_finite sx mx ex _ => ff sx mx ex
end =
match x with
| S754_zero sx => fz sx
| S754_infinity sx => fi sx
| S754_nan => fn
| S754_finite sx mx ex => ff sx mx ex
end
now intros T fz fi fn ff [sx|sx| |sx mx ex] Hx.
Qed.

Theorem canonical_canonical_mantissa :
  forall (sx : bool) mx ex,
  canonical_mantissa mx ex = true ->
  canonical radix2 fexp (Float radix2 (cond_Zopp sx (Zpos mx)) ex).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (sx : bool) (mx : positive) (ex : Z),
canonical_mantissa mx ex = true ->
canonical radix2 fexp
  {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (sx : bool) (mx : positive) (ex : Z),
canonical_mantissa mx ex = true ->
canonical radix2 fexp
  {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}
intros sx mx ex H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
H:canonical_mantissa mx ex = true
canonical radix2 fexp
  {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}
assert (Hx := Zeq_bool_eq _ _ H).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
H:canonical_mantissa mx ex = true
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
canonical radix2 fexp
  {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |} clear H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
canonical radix2 fexp
  {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}
apply sym_eq.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
cexp radix2 fexp
  (F2R
     {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}) =
Fexp {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}
simpl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
cexp radix2 fexp
  (F2R
     {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}) =
ex
pattern ex at 2 ; rewrite <- Hx.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
cexp radix2 fexp
  (F2R
     {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}) =
fexp (Z.pos (digits2_pos mx) + ex)
apply (f_equal fexp).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
mag radix2
  (F2R
     {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}) =
(Z.pos (digits2_pos mx) + ex)%Z
rewrite mag_F2R_Zdigits.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
(Zdigits radix2 (cond_Zopp sx (Z.pos mx)) + ex)%Z =
(Z.pos (digits2_pos mx) + ex)%Z
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
cond_Zopp sx (Z.pos mx) <> 0%Z
rewrite <- Zdigits_abs.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
(Zdigits radix2 (Z.abs (cond_Zopp sx (Z.pos mx))) + ex)%Z =
(Z.pos (digits2_pos mx) + ex)%Z
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
cond_Zopp sx (Z.pos mx) <> 0%Z
rewrite Zpos_digits2_pos.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
(Zdigits radix2 (Z.abs (cond_Zopp sx (Z.pos mx))) + ex)%Z =
(Zdigits radix2 (Z.pos mx) + ex)%Z
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
cond_Zopp sx (Z.pos mx) <> 0%Z
now case sx.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (digits2_pos mx) + ex) = ex
cond_Zopp sx (Z.pos mx) <> 0%Z
now case sx.
Qed.

Theorem generic_format_B2R :
  forall x,
  generic_format radix2 fexp (B2R x).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
generic_format radix2 fexp (B2R x)
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
generic_format radix2 fexp (B2R x)
intros [sx|sx| |sx mx ex Hx] ; try apply generic_format_0.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
generic_format radix2 fexp
  (B2R (B754_finite sx mx ex Hx))
simpl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
generic_format radix2 fexp
  (F2R
     {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |})
apply generic_format_canonical.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
canonical radix2 fexp
  {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}
apply canonical_canonical_mantissa.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
canonical_mantissa mx ex = true
now destruct (andb_prop _ _ Hx) as (H, _).
Qed.

Theorem FLT_format_B2R :
  forall x,
  FLT_format radix2 emin prec (B2R x).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
FLT_format radix2 emin prec (B2R x)
Proof with auto with typeclass_instances.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
FLT_format radix2 emin prec (B2R x)
intros x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
x:binary_float
FLT_format radix2 emin prec (B2R x)
apply FLT_format_generic...
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
x:binary_float
generic_format radix2 (FLT_exp emin prec) (B2R x)
apply generic_format_B2R.
Qed.

Theorem B2SF_inj :
  forall x y : binary_float,
  B2SF x = B2SF y ->
  x = y.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x y : binary_float, B2SF x = B2SF y -> x = y
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x y : binary_float, B2SF x = B2SF y -> x = y
intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx, sy:bool
B2SF (B754_zero sx) = B2SF (B754_zero sy) ->
B754_zero sx = B754_zero sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx, sy:bool
B2SF (B754_infinity sx) = B2SF (B754_infinity sy) ->
B754_infinity sx = B754_infinity sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2SF (B754_finite sx mx ex Hx) =
B2SF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
(* *)
intros H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx, sy:bool
H:B2SF (B754_zero sx) = B2SF (B754_zero sy)
B754_zero sx = B754_zero sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx, sy:bool
B2SF (B754_infinity sx) = B2SF (B754_infinity sy) ->
B754_infinity sx = B754_infinity sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2SF (B754_finite sx mx ex Hx) =
B2SF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
now inversion H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx, sy:bool
B2SF (B754_infinity sx) = B2SF (B754_infinity sy) ->
B754_infinity sx = B754_infinity sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2SF (B754_finite sx mx ex Hx) =
B2SF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
(* *)
intros H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx, sy:bool
H:B2SF (B754_infinity sx) = B2SF (B754_infinity sy)
B754_infinity sx = B754_infinity sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2SF (B754_finite sx mx ex Hx) =
B2SF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
now inversion H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2SF (B754_finite sx mx ex Hx) =
B2SF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
(* *)
intros H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
H:B2SF (B754_finite sx mx ex Hx) =
B2SF (B754_finite sy my ey Hy)
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
inversion H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
H:B2SF (B754_finite sx mx ex Hx) =
B2SF (B754_finite sy my ey Hy)
H1:sx = sy
H2:mx = my
H3:ex = ey
B754_finite sy mx ex Hx = B754_finite sy my ey Hy
clear H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
H1:sx = sy
H2:mx = my
H3:ex = ey
B754_finite sy mx ex Hx = B754_finite sy my ey Hy
revert Hx.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
H1:sx = sy
H2:mx = my
H3:ex = ey
forall Hx : bounded mx ex = true,
B754_finite sy mx ex Hx = B754_finite sy my ey Hy
rewrite H2, H3.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
H1:sx = sy
H2:mx = my
H3:ex = ey
forall Hx : bounded my ey = true,
B754_finite sy my ey Hx = B754_finite sy my ey Hy
intros Hx.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
H1:sx = sy
H2:mx = my
H3:ex = ey
Hx:bounded my ey = true
B754_finite sy my ey Hx = B754_finite sy my ey Hy
apply f_equal, eqbool_irrelevance.
Qed.

Definition is_finite_strict f :=
  match f with
  | B754_finite _ _ _ _ => true
  | _ => false
  end.

Theorem is_finite_strict_B2R :
  forall x,
  B2R x <> 0%R ->
  is_finite_strict x = true.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
B2R x <> 0%R -> is_finite_strict x = true
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
B2R x <> 0%R -> is_finite_strict x = true
now intros [sx|sx| | sx mx ex Bx] Hx.
Qed.

Theorem B2R_inj:
  forall x y : binary_float,
  is_finite_strict x = true ->
  is_finite_strict y = true ->
  B2R x = B2R y ->
  x = y.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x y : binary_float,
is_finite_strict x = true ->
is_finite_strict y = true -> B2R x = B2R y -> x = y
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x y : binary_float,
is_finite_strict x = true ->
is_finite_strict y = true -> B2R x = B2R y -> x = y
intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
is_finite_strict (B754_finite sx mx ex Hx) = true ->
is_finite_strict (B754_finite sy my ey Hy) = true ->
B2R (B754_finite sx mx ex Hx) =
B2R (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
simpl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
true = true ->
true = true ->
F2R {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |} =
F2R {| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |} ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
intros _ _ Heq.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
assert (Hs: sx = sy).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
sx = sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
(* *)
revert Heq.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
F2R {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |} =
F2R {| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |} ->
sx = sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy clear.
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |} =
F2R {| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |} ->
sx = sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
case sx ; case sy ; try easy ;
  intros Heq ; apply False_ind ; revert Heq.
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {| Fnum := cond_Zopp true (Z.pos mx); Fexp := ex |} =
F2R
  {| Fnum := cond_Zopp false (Z.pos my); Fexp := ey |} ->
False
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {| Fnum := cond_Zopp false (Z.pos mx); Fexp := ex |} =
F2R
  {| Fnum := cond_Zopp true (Z.pos my); Fexp := ey |} ->
False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
apply Rlt_not_eq.
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
(F2R
   {| Fnum := cond_Zopp true (Z.pos mx); Fexp := ex |} <
 F2R
   {|
   Fnum := cond_Zopp false (Z.pos my);
   Fexp := ey |})%R
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {| Fnum := cond_Zopp false (Z.pos mx); Fexp := ex |} =
F2R
  {| Fnum := cond_Zopp true (Z.pos my); Fexp := ey |} ->
False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
apply Rlt_trans with R0.
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
(F2R
   {| Fnum := cond_Zopp true (Z.pos mx); Fexp := ex |} <
 R0)%R
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
(R0 <
 F2R
   {|
   Fnum := cond_Zopp false (Z.pos my);
   Fexp := ey |})%R
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {| Fnum := cond_Zopp false (Z.pos mx); Fexp := ex |} =
F2R
  {| Fnum := cond_Zopp true (Z.pos my); Fexp := ey |} ->
False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
now apply F2R_lt_0.
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
(R0 <
 F2R
   {|
   Fnum := cond_Zopp false (Z.pos my);
   Fexp := ey |})%R
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {| Fnum := cond_Zopp false (Z.pos mx); Fexp := ex |} =
F2R
  {| Fnum := cond_Zopp true (Z.pos my); Fexp := ey |} ->
False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
now apply F2R_gt_0.
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {| Fnum := cond_Zopp false (Z.pos mx); Fexp := ex |} =
F2R
  {| Fnum := cond_Zopp true (Z.pos my); Fexp := ey |} ->
False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
apply Rgt_not_eq.
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
(F2R
   {|
   Fnum := cond_Zopp false (Z.pos mx);
   Fexp := ex |} >
 F2R
   {| Fnum := cond_Zopp true (Z.pos my); Fexp := ey |})%R
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
apply Rgt_trans with R0.
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
(F2R
   {|
   Fnum := cond_Zopp false (Z.pos mx);
   Fexp := ex |} > R0)%R
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
(R0 >
 F2R
   {| Fnum := cond_Zopp true (Z.pos my); Fexp := ey |})%R
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
now apply F2R_gt_0.
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
(R0 >
 F2R
   {| Fnum := cond_Zopp true (Z.pos my); Fexp := ey |})%R
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
now apply F2R_lt_0.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
assert (mx = my /\ ex = ey).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
mx = my /\ ex = ey
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
(* *)
refine (_ (canonical_unique _ fexp _ _ _ _ Heq)).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
{| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |} =
{| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |} ->
mx = my /\ ex = ey
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
rewrite Hs.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
{| Fnum := cond_Zopp sy (Z.pos mx); Fexp := ex |} =
{| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |} ->
mx = my /\ ex = ey
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
now case sy ; intro H ; injection H ; split.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {| Fnum := cond_Zopp sx (Z.pos mx); Fexp := ex |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
apply canonical_canonical_mantissa.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical_mantissa mx ex = true
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
exact (proj1 (andb_prop _ _ Hx)).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {| Fnum := cond_Zopp sy (Z.pos my); Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
apply canonical_canonical_mantissa.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical_mantissa my ey = true
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
exact (proj1 (andb_prop _ _ Hy)).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
(* *)
revert Hx.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
forall Hx : bounded mx ex = true,
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
rewrite Hs, (proj1 H), (proj2 H).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
forall Hx : bounded my ey = true,
B754_finite sy my ey Hx = B754_finite sy my ey Hy
intros Hx.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
Hx:bounded my ey = true
B754_finite sy my ey Hx = B754_finite sy my ey Hy
apply f_equal.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
H:mx = my /\ ex = ey
Hx:bounded my ey = true
Hx = Hy
apply eqbool_irrelevance.
Qed.

Definition Bsign x :=
  match x with
  | B754_nan => false
  | B754_zero s => s
  | B754_infinity s => s
  | B754_finite s _ _ _ => s
  end.

Definition sign_SF x :=
  match x with
  | S754_nan => false
  | S754_zero s => s
  | S754_infinity s => s
  | S754_finite s _ _ => s
  end.

Theorem Bsign_SF2B :
  forall x H,
  Bsign (SF2B x H) = sign_SF x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (H : valid_binary x = true),
Bsign (SF2B x H) = sign_SF x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (H : valid_binary x = true),
Bsign (SF2B x H) = sign_SF x
now intros [sx|sx| |sx mx ex] H.
Qed.

Definition is_finite f :=
  match f with
  | B754_finite _ _ _ _ => true
  | B754_zero _ => true
  | _ => false
  end.

Definition is_finite_SF f :=
  match f with
  | S754_finite _ _ _ => true
  | S754_zero _ => true
  | _ => false
  end.

Theorem is_finite_SF2B :
  forall x Hx,
  is_finite (SF2B x Hx) = is_finite_SF x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (Hx : valid_binary x = true),
is_finite (SF2B x Hx) = is_finite_SF x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (Hx : valid_binary x = true),
is_finite (SF2B x Hx) = is_finite_SF x
now intros [| | |].
Qed.

Theorem is_finite_SF_B2SF :
  forall x,
  is_finite_SF (B2SF x) = is_finite x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
is_finite_SF (B2SF x) = is_finite x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float,
is_finite_SF (B2SF x) = is_finite x
now intros [| | |].
Qed.

Theorem B2R_Bsign_inj:
  forall x y : binary_float,
    is_finite x = true ->
    is_finite y = true ->
    B2R x = B2R y ->
    Bsign x = Bsign y ->
    x = y.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x y : binary_float,
is_finite x = true ->
is_finite y = true ->
B2R x = B2R y -> Bsign x = Bsign y -> x = y
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x y : binary_float,
is_finite x = true ->
is_finite y = true ->
B2R x = B2R y -> Bsign x = Bsign y -> x = y
intros.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
x, y:binary_float
H:is_finite x = true
H0:is_finite y = true
H1:B2R x = B2R y
H2:Bsign x = Bsign y
x = y destruct x, y; try (apply B2R_inj; now eauto).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
H:is_finite (B754_zero s) = true
H0:is_finite (B754_zero s0) = true
H1:B2R (B754_zero s) = B2R (B754_zero s0)
H2:Bsign (B754_zero s) = Bsign (B754_zero s0)
B754_zero s = B754_zero s0
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:B2R (B754_zero s) = B2R (B754_finite s0 m e e0)
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:B2R (B754_finite s m e e0) = B2R (B754_zero s0)
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
B754_finite s m e e0 = B754_zero s0
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
H:is_finite (B754_zero s) = true
H0:is_finite (B754_zero s0) = true
H1:B2R (B754_zero s) = B2R (B754_zero s0)
H2:Bsign (B754_zero s) = Bsign (B754_zero s0)
B754_zero s = B754_zero s0 simpl in H2.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
H:is_finite (B754_zero s) = true
H0:is_finite (B754_zero s0) = true
H1:B2R (B754_zero s) = B2R (B754_zero s0)
H2:s = s0
B754_zero s = B754_zero s0 congruence.
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:B2R (B754_zero s) = B2R (B754_finite s0 m e e0)
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0 symmetry in H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:B2R (B754_finite s0 m e e0) = B2R (B754_zero s)
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0 apply Rmult_integral in H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:IZR
  (Fnum
     {|
     Fnum := cond_Zopp s0 (Z.pos m);
     Fexp := e |}) = 0%R \/
bpow radix2
  (Fexp
     {|
     Fnum := cond_Zopp s0 (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0
  destruct H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:IZR
  (Fnum
     {|
     Fnum := cond_Zopp s0 (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:bpow radix2
  (Fexp
     {|
     Fnum := cond_Zopp s0 (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0 apply (eq_IZR _ 0) in H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:Fnum
  {| Fnum := cond_Zopp s0 (Z.pos m); Fexp := e |} =
0%Z
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:bpow radix2
  (Fexp
     {|
     Fnum := cond_Zopp s0 (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0 destruct s0; discriminate H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:bpow radix2
  (Fexp
     {|
     Fnum := cond_Zopp s0 (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0
  simpl in H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:bpow radix2 e = 0%R
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
B754_zero s = B754_finite s0 m e e0 pose proof (bpow_gt_0 radix2 e).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:bpow radix2 e = 0%R
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
H3:(0 < bpow radix2 e)%R
B754_zero s = B754_finite s0 m e e0
  rewrite H1 in H3.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:bpow radix2 e = 0%R
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
H3:(0 < 0)%R
B754_zero s = B754_finite s0 m e e0 apply Rlt_irrefl in H3.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s, s0:bool
m:positive
e:Z
e0:bounded m e = true
H:is_finite (B754_zero s) = true
H0:is_finite (B754_finite s0 m e e0) = true
H1:bpow radix2 e = 0%R
H2:Bsign (B754_zero s) =
Bsign (B754_finite s0 m e e0)
H3:False
B754_zero s = B754_finite s0 m e e0 destruct H3.
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:B2R (B754_finite s m e e0) = B2R (B754_zero s0)
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
B754_finite s m e e0 = B754_zero s0 apply Rmult_integral in H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:IZR
  (Fnum
     {|
     Fnum := cond_Zopp s (Z.pos m);
     Fexp := e |}) = 0%R \/
bpow radix2
  (Fexp
     {|
     Fnum := cond_Zopp s (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
B754_finite s m e e0 = B754_zero s0
  destruct H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:IZR
  (Fnum
     {|
     Fnum := cond_Zopp s (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
B754_finite s m e e0 = B754_zero s0
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:bpow radix2
  (Fexp
     {|
     Fnum := cond_Zopp s (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
B754_finite s m e e0 = B754_zero s0 apply (eq_IZR _ 0) in H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:Fnum
  {| Fnum := cond_Zopp s (Z.pos m); Fexp := e |} =
0%Z
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
B754_finite s m e e0 = B754_zero s0
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:bpow radix2
  (Fexp
     {|
     Fnum := cond_Zopp s (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
B754_finite s m e e0 = B754_zero s0 destruct s; discriminate H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:bpow radix2
  (Fexp
     {|
     Fnum := cond_Zopp s (Z.pos m);
     Fexp := e |}) = 0%R
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
B754_finite s m e e0 = B754_zero s0
  simpl in H1.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:bpow radix2 e = 0%R
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
B754_finite s m e e0 = B754_zero s0 pose proof (bpow_gt_0 radix2 e).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:bpow radix2 e = 0%R
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
H3:(0 < bpow radix2 e)%R
B754_finite s m e e0 = B754_zero s0
  rewrite H1 in H3.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:bpow radix2 e = 0%R
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
H3:(0 < 0)%R
B754_finite s m e e0 = B754_zero s0 apply Rlt_irrefl in H3.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
e0:bounded m e = true
s0:bool
H:is_finite (B754_finite s m e e0) = true
H0:is_finite (B754_zero s0) = true
H1:bpow radix2 e = 0%R
H2:Bsign (B754_finite s m e e0) =
Bsign (B754_zero s0)
H3:False
B754_finite s m e e0 = B754_zero s0 destruct H3.
Qed.

Definition is_nan f :=
  match f with
  | B754_nan => true
  | _ => false
  end.

Definition is_nan_SF f :=
  match f with
  | S754_nan => true
  | _ => false
  end.

Theorem is_nan_SF2B :
  forall x Hx,
  is_nan (SF2B x Hx) = is_nan_SF x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (Hx : valid_binary x = true),
is_nan (SF2B x Hx) = is_nan_SF x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall (x : spec_float) (Hx : valid_binary x = true),
is_nan (SF2B x Hx) = is_nan_SF x
now intros [| | |].
Qed.

Theorem is_nan_SF_B2SF :
  forall x,
  is_nan_SF (B2SF x) = is_nan x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float, is_nan_SF (B2SF x) = is_nan x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float, is_nan_SF (B2SF x) = is_nan x
now intros [| | |].
Qed.

Definition erase (x : binary_float) : binary_float.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
x:binary_float
binary_float
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
x:binary_float
binary_float
destruct x as [s|s| |s m e H].
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
binary_float
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
binary_float
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
binary_float
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
H:bounded m e = true
binary_float
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
binary_float exact (B754_zero s).
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
binary_float exact (B754_infinity s).
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
binary_float exact B754_nan.
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
H:bounded m e = true
binary_float apply (B754_finite s m e).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
H:bounded m e = true
bounded m e = true
  destruct bounded.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
H:true = true
true = true
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
H:false = true
false = true
  apply eq_refl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
H:false = true
false = true
  exact H.
Defined.

Theorem erase_correct :
  forall x, erase x = x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float, erase x = x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
forall x : binary_float, erase x = x
destruct x as [s|s| |s m e H] ; try easy ; simpl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
H:bounded m e = true
B754_finite s m e
  ((if bounded m e as b return (b = true -> b = true)
    then fun _ : true = true => eq_refl
    else fun H0 : false = true => H0) H) =
B754_finite s m e H
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
prec_lt_emax_:Prec_lt_emax prec emax
s:bool
m:positive
e:Z
H:bounded m e = true
B754_finite s m e
  ((if bounded m e as b return (b = true -> b = true)
    then fun _ : true = true => eq_refl
    else fun H0 : false = true => H0) H) =
B754_finite s m e H apply f_equal, eqbool_irrelevance.
Qed.