(****************************************************************************
                                                                             
          IEEE754  :  Fop                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export Fcomp.
Section operations.
Variable radix : Z.

Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Hypothesis radixNotZero : (0 < radix)%Z.
 
Definition Fplus (x y : float) :=
  Float
    (Fnum x * Zpower_nat radix (Zabs_nat (Fexp x - Zmin (Fexp x) (Fexp y))) +
     Fnum y * Zpower_nat radix (Zabs_nat (Fexp y - Zmin (Fexp x) (Fexp y))))
    (Zmin (Fexp x) (Fexp y)).
 
Theorem Fplus_correct : forall x y : float, Fplus x y = (x + y)%R :>R.
(* Goal: forall x y : float, @eq R (FtoRradix (Fplus x y)) (Rplus (FtoRradix x) (FtoRradix y)) *)
intros x y; unfold Fplus, Fshift, FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Z.add (Z.mul (Fnum x) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y)))))) (Z.mul (Fnum y) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y)))))))) (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y)))) (Rplus (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp y)))) *)
rewrite plus_IZR.
(* Goal: @eq R (Rmult (Rplus (IZR (Z.mul (Fnum x) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))))))) (IZR (Z.mul (Fnum y) (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y)))))))) (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y)))) (Rplus (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp y)))) *)
rewrite Rmult_comm; rewrite Rmult_plus_distr_l; auto.
(* Goal: @eq R (Rmult (IZR (Z.mul (Fnum x) (Fnum y))) (Rmult (powerRZ (IZR radix) (Fexp x)) (powerRZ (IZR radix) (Fexp y)))) (Rmult (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp y)))) *)
repeat rewrite Rmult_IZR.
(* Goal: @eq R (Rplus (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (IZR (Fnum x)) (IZR (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y)))))))) (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (IZR (Fnum y)) (IZR (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))))))) (Rplus (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp y)))) *)
repeat rewrite (Rmult_comm (Fnum x)); repeat rewrite (Rmult_comm (Fnum y)).
(* Goal: @eq R (Rplus (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (IZR (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y)))))) (IZR (Fnum x)))) (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (Rmult (IZR (Zpower_nat radix (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y)))))) (IZR (Fnum y))))) (Rplus (Rmult (powerRZ (IZR radix) (Fexp x)) (IZR (Fnum x))) (Rmult (powerRZ (IZR radix) (Fexp y)) (IZR (Fnum y)))) *)
repeat rewrite Zpower_nat_Z_powerRZ; auto.
(* Goal: @eq R (Rmult (IZR (Fnum x)) (Rmult (Rmult (powerRZ (IZR radix) (Fexp x)) (powerRZ (IZR radix) (Fexp y))) (IZR (Fnum y)))) (Rmult (IZR (Fnum x)) (Rmult (powerRZ (IZR radix) (Fexp x)) (Rmult (powerRZ (IZR radix) (Fexp y)) (IZR (Fnum y))))) *)
repeat rewrite <- Rmult_assoc.
(* Goal: @eq R (Rplus (Rmult (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (powerRZ (IZR radix) (Z.of_nat (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))))))) (IZR (Fnum x))) (Rmult (Rmult (powerRZ (IZR radix) (Z.min (Fexp x) (Fexp y))) (powerRZ (IZR radix) (Z.of_nat (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))))) (IZR (Fnum y)))) (Rplus (Rmult (powerRZ (IZR radix) (Fexp x)) (IZR (Fnum x))) (Rmult (powerRZ (IZR radix) (Fexp y)) (IZR (Fnum y)))) *)
repeat rewrite <- powerRZ_add; auto with real zarith arith.
(* Goal: @eq R (Rplus (Rmult (powerRZ (IZR radix) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.of_nat (Z.abs_nat (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))))))) (IZR (Fnum x))) (Rmult (powerRZ (IZR radix) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.of_nat (Z.abs_nat (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))))) (IZR (Fnum y)))) (Rplus (Rmult (powerRZ (IZR radix) (Fexp x)) (IZR (Fnum x))) (Rmult (powerRZ (IZR radix) (Fexp y)) (IZR (Fnum y)))) *)
repeat rewrite inj_abs; auto with real zarith.
(* Goal: @eq R (Rplus (Rmult (powerRZ (IZR radix) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.sub (Fexp x) (Z.min (Fexp x) (Fexp y))))) (IZR (Fnum x))) (Rmult (powerRZ (IZR radix) (Z.add (Z.min (Fexp x) (Fexp y)) (Z.sub (Fexp y) (Z.min (Fexp x) (Fexp y))))) (IZR (Fnum y)))) (Rplus (Rmult (powerRZ (IZR radix) (Fexp x)) (IZR (Fnum x))) (Rmult (powerRZ (IZR radix) (Fexp y)) (IZR (Fnum y)))) *)
repeat rewrite Zplus_minus; auto.
Qed.
 
Definition Fopp (x : float) := Float (- Fnum x) (Fexp x).
 
Theorem Fopp_correct : forall x : float, Fopp x = (- x)%R :>R.
(* Goal: forall x : float, @eq R (FtoRradix (Fopp x)) (Ropp (FtoRradix x)) *)
unfold FtoRradix, FtoR, Fopp in |- *; simpl in |- *.
(* Goal: forall x : float, @eq R (Rmult (IZR (Z.opp (Fnum x))) (powerRZ (IZR radix) (Fexp x))) (Ropp (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x)))) *)
intros x.
(* Goal: @eq R (Rmult (IZR (Z.opp (Fnum x))) (powerRZ (IZR radix) (Fexp x))) (Ropp (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x)))) *)
rewrite Ropp_Ropp_IZR; auto with real.
Qed.
 
Theorem Fopp_Fopp : forall p : float, Fopp (Fopp p) = p.
(* Goal: forall p : float, @eq float (Fopp (Fopp p)) p *)
intros p; case p; unfold Fopp in |- *; simpl in |- *; auto.
(* Goal: forall Fnum Fexp : Z, @eq float (Float (Z.opp (Z.opp Fnum)) Fexp) (Float Fnum Fexp) *)
intros; rewrite Zopp_involutive; auto.
Qed.
 
Theorem Fzero_opp : forall f : float, ~ is_Fzero f -> ~ is_Fzero (Fopp f).
intros f; case f; intros n e; case n; unfold is_Fzero in |- *; simpl in |- *;
 auto with zarith; intros; red in |- *; intros; discriminate.
Qed.
 
Theorem Fdigit_opp : forall x : float, Fdigit radix (Fopp x) = Fdigit radix x.
(* Goal: forall x : float, @eq nat (Fdigit radix (Fopp x)) (Fdigit radix x) *)
intros x; unfold Fopp, Fdigit in |- *; simpl in |- *.
(* Goal: @eq nat (digit radix (Z.opp (Fnum x))) (digit radix (Fnum x)) *)
rewrite <- (digit_abs radix (- Fnum x)).
(* Goal: @eq nat (digit radix (Z.abs (Z.opp (Fnum x)))) (digit radix (Fnum x)) *)
rewrite <- (digit_abs radix (Fnum x)).
(* Goal: @eq nat (digit radix (Z.abs (Z.opp (Fnum x)))) (digit radix (Z.abs (Fnum x))) *)
case (Fnum x); simpl in |- *; auto.
Qed.
 
Definition Fabs (x : float) := Float (Zabs (Fnum x)) (Fexp x).
 
Theorem Fabs_correct1 :
 forall x : float, (0 <= FtoR radix x)%R -> Fabs x = x :>R.
(* Goal: forall (x : float) (_ : Rle (FtoR radix x) (IZR Z0)), @eq R (FtoRradix (Fabs x)) (Ropp (FtoRradix x)) *)
intros x; case x; unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: forall (Fnum Fexp : Z) (_ : Rle (Rmult (IZR Fnum) (powerRZ (IZR radix) Fexp)) (IZR Z0)), @eq R (Rmult (IZR (Z.abs Fnum)) (powerRZ (IZR radix) Fexp)) (Ropp (Rmult (IZR Fnum) (powerRZ (IZR radix) Fexp))) *)
intros Fnum1 Fexp1 H'.
repeat rewrite <- (Rmult_comm (powerRZ radix Fexp1)); apply Rmult_eq_compat_l;
 auto.
(* Goal: @eq R (IZR (Z.abs Fnum1)) (IZR Fnum1) *)
cut (0 <= Fnum1)%Z.
(* Goal: forall _ : Z.le Fnum1 Z0, @eq R (IZR (Z.abs Fnum1)) (Ropp (IZR Fnum1)) *)
(* Goal: Z.le Fnum1 Z0 *)
unfold Zabs, Zle in |- *.
(* Goal: forall _ : not (@eq comparison (Z.compare Z0 Fnum1) Gt), @eq R (IZR match Fnum1 with | Z0 => Z0 | Zpos p => Zpos p | Zneg p => Zpos p end) (IZR Fnum1) *)
(* Goal: Z.le Z0 Fnum1 *)
case Fnum1; simpl in |- *; auto.
(* Goal: forall (p : positive) (_ : not (@eq comparison (Z.compare (Zpos p) Z0) Gt)), @eq R (IPR p) (Ropp (IPR p)) *)
(* Goal: Z.le Fnum1 Z0 *)
intros p H'0; case H'0; auto.
(* Goal: Z.le Z0 Fnum1 *)
apply Znot_gt_le; auto.
(* Goal: not (@eq nat (Z.abs_nat (Fnum p)) O) *)
Contradict H'.
(* Goal: not (Rle (Rmult (IZR Fnum1) (powerRZ (IZR radix) Fexp1)) (IZR Z0)) *)
apply Rgt_not_le; auto.
(* Goal: Rgt (Rmult (IZR Fnum1) (powerRZ (IZR radix) Fexp1)) (IZR Z0) *)
rewrite Rmult_comm.
(* Goal: Rgt (Rmult (powerRZ (IZR radix) Fexp1) (IZR Fnum1)) (IZR Z0) *)
replace 0%R with (powerRZ radix Fexp1 * 0)%R; auto with real.
(* Goal: Rgt (Rmult (powerRZ (IZR radix) Fexp1) (IZR Z0)) (Rmult (powerRZ (IZR radix) Fexp1) (IZR Fnum1)) *)
red in |- *; apply Rmult_lt_compat_l; auto with real zarith.
Qed.
 
Theorem Fabs_correct2 :
 forall x : float, (FtoR radix x <= 0)%R -> Fabs x = (- x)%R :>R.
(* Goal: forall (x : float) (_ : Rle (FtoR radix x) (IZR Z0)), @eq R (FtoRradix (Fabs x)) (Ropp (FtoRradix x)) *)
intros x; case x; unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: forall (Fnum Fexp : Z) (_ : Rle (Rmult (IZR Fnum) (powerRZ (IZR radix) Fexp)) (IZR Z0)), @eq R (Rmult (IZR (Z.abs Fnum)) (powerRZ (IZR radix) Fexp)) (Ropp (Rmult (IZR Fnum) (powerRZ (IZR radix) Fexp))) *)
intros Fnum1 Fexp1 H'.
rewrite <- Ropp_mult_distr_l_reverse;
 repeat rewrite <- (Rmult_comm (powerRZ radix Fexp1));
 apply Rmult_eq_compat_l; auto.
(* Goal: @eq R (IZR (Z.abs Fnum1)) (Ropp (IZR Fnum1)) *)
cut (Fnum1 <= 0)%Z.
(* Goal: forall _ : Z.le Fnum1 Z0, @eq R (IZR (Z.abs Fnum1)) (Ropp (IZR Fnum1)) *)
(* Goal: Z.le Fnum1 Z0 *)
unfold Zabs, Zle in |- *.
(* Goal: forall _ : not (@eq comparison (Z.compare Fnum1 Z0) Gt), @eq R (IZR match Fnum1 with | Z0 => Z0 | Zpos p => Zpos p | Zneg p => Zpos p end) (Ropp (IZR Fnum1)) *)
(* Goal: Z.le Fnum1 Z0 *)
case Fnum1; unfold IZR; auto with real.
(* Goal: forall (p : positive) (_ : not (@eq comparison (Z.compare (Zpos p) Z0) Gt)), @eq R (IPR p) (Ropp (IPR p)) *)
(* Goal: Z.le Fnum1 Z0 *)
intros p H'0; case H'0; auto.
(* Goal: Z.le Fnum1 Z0 *)
apply Znot_gt_le.
(* Goal: not (@eq nat (Z.abs_nat (Fnum p)) O) *)
Contradict H'.
(* Goal: not (Rle (Rmult (IZR Fnum1) (powerRZ (IZR radix) Fexp1)) (IZR Z0)) *)
apply Rgt_not_le; auto.
(* Goal: Rgt (Rmult (IZR Fnum1) (powerRZ (IZR radix) Fexp1)) (IZR Z0) *)
rewrite Rmult_comm.
(* Goal: Rgt (Rmult (powerRZ (IZR radix) Fexp1) (IZR Fnum1)) (IZR Z0) *)
replace 0%R with (powerRZ radix Fexp1 * 0)%R; auto with real.
(* Goal: Rgt (Rmult (powerRZ (IZR radix) Fexp1) (IZR Fnum1)) (Rmult (powerRZ (IZR radix) Fexp1) (IZR Z0)) *)
red in |- *; apply Rmult_lt_compat_l; auto with real arith.
(* Goal: Rlt (IZR Z0) (IZR Fnum1) *)
replace 0%R with (IZR 0); auto with real zarith arith.
Qed.
 
Theorem Fabs_correct : forall x : float, Fabs x = Rabs x :>R.
(* Goal: forall x : float, @eq R (FtoRradix (Fabs x)) (Rabs (FtoRradix x)) *)
intros x; unfold Rabs in |- *.
(* Goal: @eq R (FtoRradix (Fabs x)) (if Rcase_abs (FtoRradix x) then Ropp (FtoRradix x) else FtoRradix x) *)
case (Rcase_abs x); intros H1.
(* Goal: @eq R (FtoRradix (Fabs x)) (Ropp (FtoRradix x)) *)
(* Goal: @eq R (FtoRradix (Fabs x)) (FtoRradix x) *)
unfold FtoRradix in |- *; apply Fabs_correct2; auto with arith.
(* Goal: Rle (FtoR radix x) (IZR Z0) *)
(* Goal: @eq R (FtoRradix (Fabs x)) (FtoRradix x) *)
apply Rlt_le; auto.
(* Goal: @eq R (FtoRradix (Fabs x)) (FtoRradix x) *)
unfold FtoRradix in |- *; apply Fabs_correct1; auto with arith.
(* Goal: Rle (IZR Z0) (FtoR radix x) *)
apply Rge_le; auto.
Qed.
 
Theorem RleFexpFabs :
 forall p : float, p <> 0%R :>R -> (Float 1%nat (Fexp p) <= Fabs p)%R.
(* Goal: forall (p : float) (_ : not (@eq R (FtoRradix p) (IZR Z0))), Rle (FtoRradix (Float (Z.of_nat (S O)) (Fexp p))) (FtoRradix (Fabs p)) *)
intros p H'.
(* Goal: Rle (FtoRradix (Float (Z.of_nat (S O)) (Fexp p))) (FtoRradix (Fabs p)) *)
unfold FtoRradix, FtoR, Fabs in |- *; simpl in |- *.
(* Goal: Rle (Rmult (IZR (Zpos xH)) (powerRZ (IZR radix) (Fexp p))) (Rmult (IZR (Z.abs (Fnum p))) (powerRZ (IZR radix) (Fexp p))) *)
apply Rmult_le_compat_r; auto with real arith.
(* Goal: Rle (IZR (Zpos xH)) (IZR (Z.abs (Fnum p))) *)
rewrite Zabs_absolu.
(* Goal: Rle (IZR (Zpos xH)) (IZR (Z.of_nat (Z.abs_nat (Fnum p)))) *)
replace 1%R with (INR 1); auto with real.
(* Goal: Rle (INR (S O)) (IZR (Z.of_nat (Z.abs_nat (Fnum p)))) *)
repeat rewrite <- INR_IZR_INZ; apply Rle_INR; auto.
(* Goal: le (S O) (Z.abs_nat (Fnum p)) *)
cut (Zabs_nat (Fnum p) <> 0); auto with zarith.
(* Goal: not (@eq nat (Z.abs_nat (Fnum p)) O) *)
Contradict H'.
(* Goal: @eq R (FtoRradix p) (IZR Z0) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: @eq R (Rmult (IZR (Fnum p)) (powerRZ (IZR radix) (Fexp p))) (IZR Z0) *)
replace (Fnum p) with 0%Z; try (simpl;ring).
generalize H'; case (Fnum p); simpl in |- *; auto with zarith arith;
 intros p0 H'3; Contradict H'3; auto with zarith arith.
Qed.
 
Theorem Fabs_Fzero : forall x : float, ~ is_Fzero x -> ~ is_Fzero (Fabs x).
(* Goal: forall (x : float) (_ : not (is_Fzero x)), not (is_Fzero (Fabs x)) *)
intros x; case x; unfold is_Fzero in |- *; simpl in |- *.
intros n m; case n; simpl in |- *; auto with zarith; intros; red in |- *;
 discriminate.
Qed.
Hint Resolve Fabs_Fzero: float.
 
Theorem Fdigit_abs : forall x : float, Fdigit radix (Fabs x) = Fdigit radix x.
(* Goal: forall x : float, @eq nat (Fdigit radix (Fabs x)) (Fdigit radix x) *)
intros x; unfold Fabs, Fdigit in |- *; simpl in |- *.
(* Goal: @eq nat (digit radix (Z.abs (Fnum x))) (digit radix (Fnum x)) *)
case (Fnum x); auto.
Qed.
 
Definition Fminus (x y : float) := Fplus x (Fopp y).
 
Theorem Fminus_correct : forall x y : float, Fminus x y = (x - y)%R :>R.
(* Goal: forall x y : float, @eq R (FtoRradix (Fminus x y)) (Rminus (FtoRradix x) (FtoRradix y)) *)
intros x y; unfold Fminus in |- *.
(* Goal: @eq R (FtoRradix (Fplus x (Fopp y))) (Rminus (FtoRradix x) (FtoRradix y)) *)
rewrite Fplus_correct.
(* Goal: @eq R (Rplus (FtoRradix x) (FtoRradix (Fopp y))) (Rminus (FtoRradix x) (FtoRradix y)) *)
rewrite Fopp_correct; auto.
Qed.
 
Theorem Fopp_Fminus : forall p q : float, Fopp (Fminus p q) = Fminus q p.
intros p q; case p; case q; unfold Fopp, Fminus, Fplus in |- *; simpl in |- *;
 auto.
intros; apply floatEq; simpl in |- *; repeat rewrite (Zmin_sym Fexp0 Fexp);
 repeat rewrite Zopp_mult_distr_l_reverse; auto with zarith.
Qed.
 
Theorem Fopp_Fminus_dist :
 forall p q : float, Fopp (Fminus p q) = Fminus (Fopp p) (Fopp q).
intros p q; case p; case q; unfold Fopp, Fminus, Fplus in |- *; simpl in |- *;
 auto.
intros; apply floatEq; simpl in |- *; repeat rewrite (Zmin_sym Fexp0 Fexp);
 repeat rewrite Zopp_mult_distr_l_reverse; auto with zarith.
Qed.
 
Theorem minusSameExp :
 forall x y : float,
 Fexp x = Fexp y -> Fminus x y = Float (Fnum x - Fnum y) (Fexp x).
(* Goal: forall (x y : float) (_ : @eq Z (Fexp x) (Fexp y)), @eq float (Fminus x y) (Float (Z.sub (Fnum x) (Fnum y)) (Fexp x)) *)
intros x y; case x; case y; unfold Fminus, Fplus, Fopp in |- *; simpl in |- *.
(* Goal: forall (Fnum Fexp Fnum0 Fexp0 : Z) (_ : @eq Z Fexp0 Fexp), @eq float (Float (Z.add (Z.mul Fnum0 (Zpower_nat radix (Z.abs_nat (Z.sub Fexp0 (Z.min Fexp0 Fexp))))) (Z.mul (Z.opp Fnum) (Zpower_nat radix (Z.abs_nat (Z.sub Fexp (Z.min Fexp0 Fexp)))))) (Z.min Fexp0 Fexp)) (Float (Z.sub Fnum0 Fnum) Fexp0) *)
intros Fnum1 Fexp1 Fnum2 Fexp2 H'; rewrite <- H'.
(* Goal: @eq float (Float (Z.add (Z.mul Fnum2 (Zpower_nat radix (Z.abs_nat (Z.sub Fexp2 (Z.min Fexp2 Fexp2))))) (Z.mul (Z.opp Fnum1) (Zpower_nat radix (Z.abs_nat (Z.sub Fexp2 (Z.min Fexp2 Fexp2)))))) (Z.min Fexp2 Fexp2)) (Float (Z.sub Fnum2 Fnum1) Fexp2) *)
repeat rewrite Zmin_n_n.
(* Goal: @eq float (Float (Z.add (Z.mul Fnum2 (Zpower_nat radix (Z.abs_nat (Z.sub Fexp2 Fexp2)))) (Z.mul (Z.opp Fnum1) (Zpower_nat radix (Z.abs_nat (Z.sub Fexp2 Fexp2))))) Fexp2) (Float (Z.sub Fnum2 Fnum1) Fexp2) *)
apply floatEq; simpl in |- *; auto.
(* Goal: @eq Z (Z.add (Z.mul Fnum2 (Zpower_nat radix (Z.abs_nat (Z.sub Fexp2 Fexp2)))) (Z.mul (Z.opp Fnum1) (Zpower_nat radix (Z.abs_nat (Z.sub Fexp2 Fexp2))))) (Z.sub Fnum2 Fnum1) *)
replace (Zabs_nat (Fexp2 - Fexp2)) with 0; auto with zarith arith.
replace (Zpower_nat radix 0) with (Z_of_nat 1); simpl in |- *;
 auto with zarith arith.
(* Goal: @eq nat O (Z.abs_nat (Z.sub Fexp2 Fexp2)) *)
replace (Fexp2 - Fexp2)%Z with 0%Z; simpl in |- *; auto with zarith arith.
Qed.
 
Definition Fmult (x y : float) := Float (Fnum x * Fnum y) (Fexp x + Fexp y).
 
Definition Fmult_correct : forall x y : float, Fmult x y = (x * y)%R :>R.
(* Goal: forall x y : float, @eq R (FtoRradix (Fmult x y)) (Rmult (FtoRradix x) (FtoRradix y)) *)
intros x y; unfold FtoRradix, FtoR, Fmult in |- *; simpl in |- *; auto.
(* Goal: @eq R (Rmult (IZR (Z.mul (Fnum x) (Fnum y))) (powerRZ (IZR radix) (Z.add (Fexp x) (Fexp y)))) (Rmult (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp y)))) *)
rewrite powerRZ_add; auto with real zarith.
(* Goal: @eq R (Rmult (IZR (Z.mul (Fnum x) (Fnum y))) (Rmult (powerRZ (IZR radix) (Fexp x)) (powerRZ (IZR radix) (Fexp y)))) (Rmult (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp y)))) *)
repeat rewrite Rmult_IZR.
(* Goal: @eq R (Rmult (Rmult (IZR (Fnum x)) (IZR (Fnum y))) (Rmult (powerRZ (IZR radix) (Fexp x)) (powerRZ (IZR radix) (Fexp y)))) (Rmult (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp y)))) *)
repeat rewrite Rmult_assoc.
(* Goal: @eq R (Rmult (IZR (Fnum x)) (Rmult (IZR (Fnum y)) (Rmult (powerRZ (IZR radix) (Fexp x)) (powerRZ (IZR radix) (Fexp y))))) (Rmult (IZR (Fnum x)) (Rmult (powerRZ (IZR radix) (Fexp x)) (Rmult (IZR (Fnum y)) (powerRZ (IZR radix) (Fexp y))))) *)
repeat rewrite (Rmult_comm (Fnum y)).
(* Goal: @eq R (Rmult (IZR (Fnum x)) (Rmult (Rmult (powerRZ (IZR radix) (Fexp x)) (powerRZ (IZR radix) (Fexp y))) (IZR (Fnum y)))) (Rmult (IZR (Fnum x)) (Rmult (powerRZ (IZR radix) (Fexp x)) (Rmult (powerRZ (IZR radix) (Fexp y)) (IZR (Fnum y))))) *)
repeat rewrite <- Rmult_assoc.
(* Goal: @eq R (Rmult (Rmult (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (powerRZ (IZR radix) (Fexp y))) (IZR (Fnum y))) (Rmult (Rmult (Rmult (IZR (Fnum x)) (powerRZ (IZR radix) (Fexp x))) (powerRZ (IZR radix) (Fexp y))) (IZR (Fnum y))) *)
repeat rewrite Zmult_assoc_reverse; auto.
Qed.
 
Theorem oneZplus :
 forall x y : Z,
 Float 1%nat (x + y) = Fmult (Float 1%nat x) (Float 1%nat y).
(* Goal: forall x y : Z, @eq float (Float (Z.of_nat (S O)) (Z.add x y)) (Fmult (Float (Z.of_nat (S O)) x) (Float (Z.of_nat (S O)) y)) *)
intros x y; unfold Fmult in |- *; auto.
Qed.
End operations.
Hint Resolve Fabs_Fzero: float.
Hint Resolve Fzero_opp: float.