IEEE-754 arithmetic

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

Section AnyRadix.

Inductive full_float :=
  | F754_zero (s : bool)
  | F754_infinity (s : bool)
  | F754_nan (s : bool) (m : positive)
  | F754_finite (s : bool) (m : positive) (e : Z).

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

End AnyRadix.

Section Binary.

Arguments exist {A} {P}.

Variable prec emax : Z.
Context (prec_gt_0_ : Prec_gt_0 prec).
Hypothesis Hmax : (prec < emax)%Z.

Let emin := (3 - emax - prec)%Z.
Let fexp := FLT_exp emin prec.
Instance fexp_correct : Valid_exp fexp := FLT_exp_valid emin prec.
Instance fexp_monotone : Monotone_exp fexp := FLT_exp_monotone emin prec.

Definition canonical_mantissa m e :=
  Zeq_bool (fexp (Zpos (digits2_pos m) + e)) e.

Definition bounded m e :=
  andb (canonical_mantissa m e) (Zle_bool e (emax - prec)).

Definition nan_pl pl :=
  Zlt_bool (Zpos (digits2_pos pl)) prec.

Definition valid_binary x :=
  match x with
  | F754_finite _ m e => bounded m e
  | F754_nan _ pl => nan_pl pl
  | _ => true
  end.

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

Definition FF2B x :=
  match x as x return valid_binary x = true -> binary_float with
  | F754_finite s m e => B754_finite s m e
  | F754_infinity s => fun _ => B754_infinity s
  | F754_zero s => fun _ => B754_zero s
  | F754_nan b pl => fun H => B754_nan b pl H
  end.

Definition B2FF x :=
  match x with
  | B754_finite s m e _ => F754_finite s m e
  | B754_infinity s => F754_infinity s
  | B754_zero s => F754_zero s
  | B754_nan b pl _ => F754_nan b pl
  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 FF2R_B2FF :
  forall x,
  FF2R radix2 (B2FF x) = B2R x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float, FF2R radix2 (B2FF x) = B2R x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float, FF2R radix2 (B2FF x) = B2R x
now intros [sx|sx|sx plx Hplx|sx mx ex Hx].
Qed.

Theorem B2FF_FF2B :
  forall x Hx,
  B2FF (FF2B x Hx) = x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (Hx : valid_binary x = true),
B2FF (FF2B x Hx) = x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (Hx : valid_binary x = true),
B2FF (FF2B x Hx) = x
now intros [sx|sx|sx plx|sx mx ex] Hx.
Qed.

Theorem valid_binary_B2FF :
  forall x,
  valid_binary (B2FF x) = true.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float, valid_binary (B2FF x) = true
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float, valid_binary (B2FF x) = true
now intros [sx|sx|sx plx Hplx|sx mx ex Hx].
Qed.

Theorem FF2B_B2FF :
  forall x H,
  FF2B (B2FF x) H = x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : binary_float)
  (H : valid_binary (B2FF x) = true),
FF2B (B2FF x) H = x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : binary_float)
  (H : valid_binary (B2FF x) = true),
FF2B (B2FF x) H = x
intros [sx|sx|sx plx Hplx|sx mx ex Hx] H ; try easy.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
Hplx:nan_pl plx = true
H:valid_binary (B2FF (B754_nan sx plx Hplx)) = true
FF2B (B2FF (B754_nan sx plx Hplx)) H =
B754_nan sx plx Hplx
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
H:valid_binary (B2FF (B754_finite sx mx ex Hx)) =
true
FF2B (B2FF (B754_finite sx mx ex Hx)) H =
B754_finite sx mx ex Hx
apply f_equal, eqbool_irrelevance.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
H:valid_binary (B2FF (B754_finite sx mx ex Hx)) =
true
FF2B (B2FF (B754_finite sx mx ex Hx)) H =
B754_finite sx mx ex Hx
apply f_equal, eqbool_irrelevance.
Qed.

Theorem FF2B_B2FF_valid :
  forall x,
  FF2B (B2FF x) (valid_binary_B2FF x) = x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float,
FF2B (B2FF x) (valid_binary_B2FF x) = x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float,
FF2B (B2FF x) (valid_binary_B2FF x) = x
intros x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
FF2B (B2FF x) (valid_binary_B2FF x) = x
apply FF2B_B2FF.
Qed.

Theorem B2R_FF2B :
  forall x Hx,
  B2R (FF2B x Hx) = FF2R radix2 x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (Hx : valid_binary x = true),
B2R (FF2B x Hx) = FF2R radix2 x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (Hx : valid_binary x = true),
B2R (FF2B x Hx) = FF2R radix2 x
now intros [sx|sx|sx plx|sx mx ex] Hx.
Qed.

Theorem match_FF2B :
  forall {T} fz fi fn ff x Hx,
  match FF2B x Hx return T with
  | B754_zero sx => fz sx
  | B754_infinity sx => fi sx
  | B754_nan b p _ => fn b p
  | B754_finite sx mx ex _ => ff sx mx ex
  end =
  match x with
  | F754_zero sx => fz sx
  | F754_infinity sx => fi sx
  | F754_nan b p => fn b p
  | F754_finite sx mx ex => ff sx mx ex
  end.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (T : Type) (fz fi : bool -> T)
  (fn : bool -> positive -> T)
  (ff : bool -> positive -> Z -> T) (x : full_float)
  (Hx : valid_binary x = true),
match FF2B x Hx with
| B754_zero sx => fz sx
| B754_infinity sx => fi sx
| B754_nan b p _ => fn b p
| B754_finite sx mx ex _ => ff sx mx ex
end =
match x with
| F754_zero sx => fz sx
| F754_infinity sx => fi sx
| F754_nan b p => fn b p
| F754_finite sx mx ex => ff sx mx ex
end
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (T : Type) (fz fi : bool -> T)
  (fn : bool -> positive -> T)
  (ff : bool -> positive -> Z -> T) (x : full_float)
  (Hx : valid_binary x = true),
match FF2B x Hx with
| B754_zero sx => fz sx
| B754_infinity sx => fi sx
| B754_nan b p _ => fn b p
| B754_finite sx mx ex _ => ff sx mx ex
end =
match x with
| F754_zero sx => fz sx
| F754_infinity sx => fi sx
| F754_nan b p => fn b p
| F754_finite sx mx ex => ff sx mx ex
end
now intros T fz fi fn ff [sx|sx|sx plx|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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (sx : bool) (mx : positive) (ex : Z),
canonical_mantissa mx ex = true ->
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |}
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (sx : bool) (mx : positive) (ex : Z),
canonical_mantissa mx ex = true ->
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |}
intros sx mx ex H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
H:canonical_mantissa mx ex = true
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |}
assert (Hx := Zeq_bool_eq _ _ H).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
H:canonical_mantissa mx ex = true
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} clear H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |}
apply sym_eq.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
cexp radix2 fexp
  (F2R
     {|
     Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
     Fexp := ex |}) =
Fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |}
simpl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
cexp radix2 fexp
  (F2R
     {|
     Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
cexp radix2 fexp
  (F2R
     {|
     Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
     Fexp := ex |}) =
fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex)
apply (f_equal fexp).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
mag radix2
  (F2R
     {|
     Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
     Fexp := ex |}) =
(Z.pos (SpecFloatCopy.digits2_pos mx) + ex)%Z
rewrite mag_F2R_Zdigits.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
(Zdigits radix2
   (SpecFloatCopy.cond_Zopp sx (Z.pos mx)) + ex)%Z =
(Z.pos (SpecFloatCopy.digits2_pos mx) + ex)%Z
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
SpecFloatCopy.cond_Zopp sx (Z.pos mx) <> 0%Z
rewrite <- Zdigits_abs.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
(Zdigits radix2
   (Z.abs (SpecFloatCopy.cond_Zopp sx (Z.pos mx))) +
 ex)%Z = (Z.pos (SpecFloatCopy.digits2_pos mx) + ex)%Z
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
SpecFloatCopy.cond_Zopp sx (Z.pos mx) <> 0%Z
rewrite Zpos_digits2_pos.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
(Zdigits radix2
   (Z.abs (SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
SpecFloatCopy.cond_Zopp sx (Z.pos mx) <> 0%Z
now case sx.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:fexp (Z.pos (SpecFloatCopy.digits2_pos mx) + ex) =
ex
SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float,
generic_format radix2 fexp (B2R x)
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float,
generic_format radix2 fexp (B2R x)
intros [sx|sx|sx plx Hx |sx mx ex Hx] ; try apply generic_format_0.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
generic_format radix2 fexp
  (F2R
     {|
     Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
     Fexp := ex |})
apply generic_format_canonical.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |}
apply canonical_canonical_mantissa.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float,
FLT_format radix2 emin prec (B2R x)
intros x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
FLT_format radix2 emin prec (B2R x)
apply FLT_format_generic...
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
generic_format radix2 (FLT_exp emin prec) (B2R x)
apply generic_format_B2R.
Qed.

Theorem B2FF_inj :
  forall x y : binary_float,
  B2FF x = B2FF y ->
  x = y.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x y : binary_float, B2FF x = B2FF y -> x = y
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x y : binary_float, B2FF x = B2FF y -> x = y
intros [sx|sx|sx plx Hplx|sx mx ex Hx] [sy|sy|sy ply Hply|sy my ey Hy] ; try easy.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx, sy:bool
B2FF (B754_zero sx) = B2FF (B754_zero sy) ->
B754_zero sx = B754_zero sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx, sy:bool
B2FF (B754_infinity sx) = B2FF (B754_infinity sy) ->
B754_infinity sx = B754_infinity sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
Hplx:nan_pl plx = true
sy:bool
ply:positive
Hply:nan_pl ply = true
B2FF (B754_nan sx plx Hplx) =
B2FF (B754_nan sy ply Hply) ->
B754_nan sx plx Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx, sy:bool
H:B2FF (B754_zero sx) = B2FF (B754_zero sy)
B754_zero sx = B754_zero sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx, sy:bool
B2FF (B754_infinity sx) = B2FF (B754_infinity sy) ->
B754_infinity sx = B754_infinity sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
Hplx:nan_pl plx = true
sy:bool
ply:positive
Hply:nan_pl ply = true
B2FF (B754_nan sx plx Hplx) =
B2FF (B754_nan sy ply Hply) ->
B754_nan sx plx Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx, sy:bool
B2FF (B754_infinity sx) = B2FF (B754_infinity sy) ->
B754_infinity sx = B754_infinity sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
Hplx:nan_pl plx = true
sy:bool
ply:positive
Hply:nan_pl ply = true
B2FF (B754_nan sx plx Hplx) =
B2FF (B754_nan sy ply Hply) ->
B754_nan sx plx Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx, sy:bool
H:B2FF (B754_infinity sx) = B2FF (B754_infinity sy)
B754_infinity sx = B754_infinity sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
Hplx:nan_pl plx = true
sy:bool
ply:positive
Hply:nan_pl ply = true
B2FF (B754_nan sx plx Hplx) =
B2FF (B754_nan sy ply Hply) ->
B754_nan sx plx Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
Hplx:nan_pl plx = true
sy:bool
ply:positive
Hply:nan_pl ply = true
B2FF (B754_nan sx plx Hplx) =
B2FF (B754_nan sy ply Hply) ->
B754_nan sx plx Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
Hplx:nan_pl plx = true
sy:bool
ply:positive
Hply:nan_pl ply = true
H:B2FF (B754_nan sx plx Hplx) =
B2FF (B754_nan sy ply Hply)
B754_nan sx plx Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
Hplx:nan_pl plx = true
sy:bool
ply:positive
Hply:nan_pl ply = true
H:B2FF (B754_nan sx plx Hplx) =
B2FF (B754_nan sy ply Hply)
H1:sx = sy
H2:plx = ply
B754_nan sy plx Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
clear H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
Hplx:nan_pl plx = true
sy:bool
ply:positive
Hply:nan_pl ply = true
H1:sx = sy
H2:plx = ply
B754_nan sy plx Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
revert Hplx.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
sy:bool
ply:positive
Hply:nan_pl ply = true
H1:sx = sy
H2:plx = ply
forall Hplx : nan_pl plx = true,
B754_nan sy plx Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
rewrite H2.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
sy:bool
ply:positive
Hply:nan_pl ply = true
H1:sx = sy
H2:plx = ply
forall Hplx : nan_pl ply = true,
B754_nan sy ply Hplx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
intros Hx.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
plx:positive
sy:bool
ply:positive
Hply:nan_pl ply = true
H1:sx = sy
H2:plx = ply
Hx:nan_pl ply = true
B754_nan sy ply Hx = B754_nan sy ply Hply
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (B754_finite sy my ey Hy) ->
B754_finite sx mx ex Hx = B754_finite sy my ey Hy
apply f_equal, eqbool_irrelevance.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
B2FF (B754_finite sx mx ex Hx) =
B2FF (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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
H:B2FF (B754_finite sx mx ex Hx) =
B2FF (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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
H:B2FF (B754_finite sx mx ex Hx) =
B2FF (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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
sx = sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
Hx:bounded mx ex = true
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |} -> sx = sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |} -> sx = sy
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 := SpecFloatCopy.cond_Zopp true (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp false (Z.pos my);
  Fexp := ey |} -> False
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp false (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp true (Z.pos my);
  Fexp := ey |} -> False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 := SpecFloatCopy.cond_Zopp true (Z.pos mx);
   Fexp := ex |} <
 F2R
   {|
   Fnum := SpecFloatCopy.cond_Zopp false (Z.pos my);
   Fexp := ey |})%R
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp false (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp true (Z.pos my);
  Fexp := ey |} -> False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 := SpecFloatCopy.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 := SpecFloatCopy.cond_Zopp false (Z.pos my);
   Fexp := ey |})%R
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp false (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp true (Z.pos my);
  Fexp := ey |} -> False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 := SpecFloatCopy.cond_Zopp false (Z.pos my);
   Fexp := ey |})%R
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp false (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp true (Z.pos my);
  Fexp := ey |} -> False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 := SpecFloatCopy.cond_Zopp false (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp true (Z.pos my);
  Fexp := ey |} -> False
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 := SpecFloatCopy.cond_Zopp false (Z.pos mx);
   Fexp := ex |} >
 F2R
   {|
   Fnum := SpecFloatCopy.cond_Zopp true (Z.pos my);
   Fexp := ey |})%R
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 := SpecFloatCopy.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 := SpecFloatCopy.cond_Zopp true (Z.pos my);
   Fexp := ey |})%R
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 := SpecFloatCopy.cond_Zopp true (Z.pos my);
   Fexp := ey |})%R
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
{|
Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
Fexp := ex |} =
{|
Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
Fexp := ey |} -> mx = my /\ ex = ey
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
{|
Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos mx);
Fexp := ex |} =
{|
Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
Fexp := ey |} -> mx = my /\ ex = ey
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
Hs:sx = sy
canonical radix2 fexp
  {|
  Fnum := SpecFloatCopy.cond_Zopp sy (Z.pos my);
  Fexp := ey |}
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
sx:bool
mx:positive
ex:Z
sy:bool
my:positive
ey:Z
Hy:bounded my ey = true
Heq:F2R
  {|
  Fnum := SpecFloatCopy.cond_Zopp sx (Z.pos mx);
  Fexp := ex |} =
F2R
  {|
  Fnum := SpecFloatCopy.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 s _ _ => s
  | B754_zero s => s
  | B754_infinity s => s
  | B754_finite s _ _ _ => s
  end.

Definition sign_FF x :=
  match x with
  | F754_nan s _ => s
  | F754_zero s => s
  | F754_infinity s => s
  | F754_finite s _ _ => s
  end.

Theorem Bsign_FF2B :
  forall x H,
  Bsign (FF2B x H) = sign_FF x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (H : valid_binary x = true),
Bsign (FF2B x H) = sign_FF x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (H : valid_binary x = true),
Bsign (FF2B x H) = sign_FF x
now intros [sx|sx|sx plx|sx mx ex] H.
Qed.

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

Definition is_finite_FF f :=
  match f with
  | F754_finite _ _ _ => true
  | F754_zero _ => true
  | _ => false
  end.

Theorem is_finite_FF2B :
  forall x Hx,
  is_finite (FF2B x Hx) = is_finite_FF x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (Hx : valid_binary x = true),
is_finite (FF2B x Hx) = is_finite_FF x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (Hx : valid_binary x = true),
is_finite (FF2B x Hx) = is_finite_FF x
now intros [| | |].
Qed.

Theorem is_finite_FF_B2FF :
  forall x,
  is_finite_FF (B2FF x) = is_finite x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float,
is_finite_FF (B2FF x) = is_finite x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float,
is_finite_FF (B2FF 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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp s0 (Z.pos m);
     Fexp := e |}) = 0%R \/
bpow radix2
  (Fexp
     {|
     Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.cond_Zopp s (Z.pos m);
     Fexp := e |}) = 0%R \/
bpow radix2
  (Fexp
     {|
     Fnum := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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 := SpecFloatCopy.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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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_FF f :=
  match f with
  | F754_nan _ _ => true
  | _ => false
  end.

Theorem is_nan_FF2B :
  forall x Hx,
  is_nan (FF2B x Hx) = is_nan_FF x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (Hx : valid_binary x = true),
is_nan (FF2B x Hx) = is_nan_FF x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall (x : full_float) (Hx : valid_binary x = true),
is_nan (FF2B x Hx) = is_nan_FF x
now intros [| | |].
Qed.

Theorem is_nan_FF_B2FF :
  forall x,
  is_nan_FF (B2FF x) = is_nan x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float, is_nan_FF (B2FF x) = is_nan x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float, is_nan_FF (B2FF x) = is_nan x
now intros [| |? []|].
Qed.

Definition get_nan_pl (x : binary_float) : positive :=
  match x with B754_nan _ pl _ => pl | _ => xH end.

Definition build_nan (x : { x | is_nan x = true }) : binary_float.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:{x0 : binary_float | is_nan x0 = true}
binary_float
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:{x0 : binary_float | is_nan x0 = true}
binary_float
apply (B754_nan (Bsign (proj1_sig x)) (get_nan_pl (proj1_sig x))).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:{x0 : binary_float | is_nan x0 = true}
nan_pl (get_nan_pl (proj1_sig x)) = true
destruct x as [x H].
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
H:is_nan x = true
nan_pl (get_nan_pl (proj1_sig (exist x H))) = true
simpl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
H:is_nan x = true
nan_pl (get_nan_pl x) = true
revert H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
is_nan x = true -> nan_pl (get_nan_pl x) = true
assert (H: false = true -> nan_pl 1 = true) by now destruct (nan_pl 1).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
H:false = true -> nan_pl 1 = true
is_nan x = true -> nan_pl (get_nan_pl x) = true
destruct x; try apply H.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
e:nan_pl pl = true
H:false = true -> nan_pl 1 = true
is_nan (B754_nan s pl e) = true ->
nan_pl (get_nan_pl (B754_nan s pl e)) = true
intros _.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
e:nan_pl pl = true
H:false = true -> nan_pl 1 = true
nan_pl (get_nan_pl (B754_nan s pl e)) = true
apply e.
Defined.

Theorem build_nan_correct :
  forall x : { x | is_nan x = true },
  build_nan x = proj1_sig x.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : {x : binary_float | is_nan x = true},
build_nan x = proj1_sig x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : {x : binary_float | is_nan x = true},
build_nan x = proj1_sig x
intros [x H].
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
H:is_nan x = true
build_nan (exist x H) = proj1_sig (exist x H)
now destruct x.
Qed.

Theorem B2R_build_nan :
  forall x, B2R (build_nan x) = 0%R.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : {x : binary_float | is_nan x = true},
B2R (build_nan x) = 0%R
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : {x : binary_float | is_nan x = true},
B2R (build_nan x) = 0%R
easy.
Qed.

Theorem is_finite_build_nan :
  forall x, is_finite (build_nan x) = false.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : {x : binary_float | is_nan x = true},
is_finite (build_nan x) = false
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : {x : binary_float | is_nan x = true},
is_finite (build_nan x) = false
easy.
Qed.

Theorem is_nan_build_nan :
  forall x, is_nan (build_nan x) = true.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : {x : binary_float | is_nan x = true},
is_nan (build_nan x) = true
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : {x : binary_float | is_nan x = true},
is_nan (build_nan x) = true
easy.
Qed.

Definition erase (x : binary_float) : binary_float.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
binary_float
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
x:binary_float
binary_float
destruct x as [s|s|s pl H|s m e H].
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
binary_float
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
binary_float
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
H:nan_pl pl = true
binary_float
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
m:positive
e:Z
H:bounded m e = true
binary_float
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
binary_float exact (B754_zero s).
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
binary_float exact (B754_infinity s).
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
H:nan_pl pl = true
binary_float apply (B754_nan s pl).
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
H:nan_pl pl = true
nan_pl pl = true
  destruct nan_pl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
H:true = true
true = true
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
H:false = true
false = true
  apply eq_refl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
H:false = true
false = true
  exact H.
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
m:positive
e:Z
H:true = true
true = true
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
m:positive
e:Z
H:false = true
false = true
  apply eq_refl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float, erase x = x
Proof.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
forall x : binary_float, erase x = x
destruct x as [s|s|s pl H|s m e H] ; try easy ; simpl.
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
H:nan_pl pl = true
B754_nan s pl
  ((if nan_pl pl as b return (b = true -> b = true)
    then fun _ : true = true => eq_refl
    else fun H0 : false = true => H0) H) =
B754_nan s pl H
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
s:bool
pl:positive
H:nan_pl pl = true
B754_nan s pl
  ((if nan_pl pl as b return (b = true -> b = true)
    then fun _ : true = true => eq_refl
    else fun H0 : false = true => H0) H) =
B754_nan s pl H apply f_equal, eqbool_irrelevance.
-
prec, emax:Z
prec_gt_0_:Prec_gt_0 prec
Hmax:(prec < emax)%Z
emin:=(3 - emax - prec)%Z:Z
fexp:=FLT_exp emin prec:Z -> Z
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.