(****************************************************************************
                                                                             
          IEEE754  :  MSBProp                                                     
                                                                             
          Laurent Thery, Sylvie Boldo                                                      
                                                                             
  ******************************************************************************)
Require Export MSB.
Section MSBProp.
Variable b : Fbound.
Variable precision : nat.
Variable radix : Z.
 
Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
 
Let radixMoreThanZERO : (0 < radix)%Z :=
  Zlt_1_O _ (Zlt_le_weak _ _ radixMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Theorem boundOnePrecision :
 forall a : float,
 Fbounded b a -> (Rabs a < Float 1%nat (precision + Fexp a))%R.
(* Goal: forall (a : float) (_ : Fbounded b a), Rlt (Rabs (FtoRradix a)) (FtoRradix (Float (Z.of_nat (S O)) (Z.add (Z.of_nat precision) (Fexp a)))) *)
intros a H.
replace (FtoRradix (Float 1%nat (precision + Fexp a))) with
 (FtoRradix (Fshift radix precision (Float 1%nat (precision + Fexp a))));
 [ idtac | apply (FshiftCorrect radix); auto ].
(* Goal: Rlt (Rabs (FtoRradix a)) (FtoRradix (Fshift radix precision (Float (Z.of_nat (S O)) (Z.add (Z.of_nat precision) (Fexp a))))) *)
unfold Fshift, FtoRradix, FtoR in |- *; simpl in |- *.
(* Goal: Rlt (Rabs (Rmult (IZR (Fnum a)) (powerRZ (IZR radix) (Fexp a)))) (Rmult (IZR match Zpower_nat radix precision with | Z0 => Z0 | Zpos y' => Zpos y' | Zneg y' => Zneg y' end) (powerRZ (IZR radix) (Z.sub (Z.add (Z.of_nat precision) (Fexp a)) (Z.of_nat precision)))) *)
rewrite <- pGivesBound.
(* Goal: Rlt (Rabs (Rmult (IZR (Fnum a)) (powerRZ (IZR radix) (Fexp a)))) (Rmult (IZR (Zpos (vNum b))) (powerRZ (IZR radix) (Z.sub (Z.add (Z.of_nat precision) (Fexp a)) (Z.of_nat precision)))) *)
replace (precision + Fexp a - precision)%Z with (Fexp a); [ idtac | ring ].
rewrite Rabs_mult; rewrite (fun x y => Rabs_pos_eq (powerRZ x y));
 auto with real zarith.
(* Goal: Rlt (Rmult (Rabs (IZR (Fnum a))) (powerRZ (IZR radix) (Fexp a))) (Rmult (IZR (Zpos (vNum b))) (powerRZ (IZR radix) (Fexp a))) *)
apply Rlt_monotony_exp; auto with float real zarith.
(* Goal: Rlt (Rabs (IZR (Fnum a))) (IZR (Zpos (vNum b))) *)
rewrite Faux.Rabsolu_Zabs; auto with float real zarith.
Qed.
 
Theorem boundNormalMult :
 forall x y : float,
 Fnormal radix b x ->
 Fbounded b y ->
 (Rabs y * Float 1%nat (Fexp x) < radix * (Rabs x * Float 1%nat (Fexp y)))%R.
(* Goal: forall (x y : float) (_ : Fnormal radix b x) (_ : Fbounded b y), Rlt (Rmult (Rabs (FtoRradix y)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (Rmult (IZR radix) (Rmult (Rabs (FtoRradix x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y))))) *)
intros x y H H0.
apply
 Rlt_le_trans
  with (Float (Zpos (vNum b)) (Fexp y) * Float 1%nat (Fexp x))%R.
(* Goal: Rlt (Rmult (Rabs (FtoRradix y)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
(* Goal: Rle (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (Rmult (IZR radix) (Rmult (Rabs (FtoRradix x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y))))) *)
apply Rmult_lt_compat_r.
(* Goal: Rle (IZR Z0) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y))) *)
(* Goal: Rle (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (Rmult (IZR radix) (Rabs (FtoRradix x))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *.
replace (1 * powerRZ radix (Fexp x))%R with (powerRZ radix (Fexp x));
 [ idtac | ring ].
(* Goal: Rlt (IZR Z0) (powerRZ (IZR radix) (Fexp x)) *)
(* Goal: Rlt (Rabs (FtoRradix y)) (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) *)
(* Goal: Rle (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (Rmult (IZR radix) (Rmult (Rabs (FtoRradix x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y))))) *)
apply powerRZ_lt; auto with real arith.
(* Goal: Rlt (Rabs (FtoRradix y)) (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) *)
(* Goal: Rle (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (Rmult (IZR radix) (Rmult (Rabs (FtoRradix x)) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y))))) *)
unfold FtoRradix in |- *; apply MaxFloat; auto.
replace (Float (Zpos (vNum b)) (Fexp y) * Float 1%nat (Fexp x))%R with
 (Zpos (vNum b) * Float 1%nat (Fexp x) * Float 1%nat (Fexp y))%R.
replace (radix * (Rabs x * Float 1%nat (Fexp y)))%R with
 (radix * Rabs x * Float 1%nat (Fexp y))%R; [ idtac | ring ].
(* Goal: Rle (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (Rmult (IZR radix) (Rabs (FtoRradix x))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
apply Rmult_le_compat_r.
(* Goal: Rle (IZR Z0) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y))) *)
(* Goal: Rle (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (Rmult (IZR radix) (Rabs (FtoRradix x))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *.
replace (1 * powerRZ radix (Fexp y))%R with (powerRZ radix (Fexp y));
 [ idtac | ring ].
(* Goal: Rle (IZR Z0) (powerRZ (IZR radix) (Fexp y)) *)
(* Goal: Rle (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (Rmult (IZR radix) (Rabs (FtoRradix x))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
apply powerRZ_le; auto with real arith.
replace (Zpos (vNum b) * Float 1%nat (Fexp x))%R with
 (FtoRradix (Float (Zpos (vNum b)) (Fexp x))).
(* Goal: Rle (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) (Rmult (IZR radix) (Rabs (FtoRradix x))) *)
(* Goal: @eq R (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
rewrite <- (Fabs_correct radix); auto with real zarith.
(* Goal: Rle (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) (Rmult (IZR radix) (FtoR radix (Fabs x))) *)
(* Goal: @eq R (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
unfold Fabs, FtoRradix, FtoR in |- *.
(* Goal: Rle (Rmult (IZR (Fnum (Float (Zpos (vNum b)) (Fexp x)))) (powerRZ (IZR radix) (Fexp (Float (Zpos (vNum b)) (Fexp x))))) (Rmult (IZR radix) (Rmult (IZR (Fnum (Float (Z.abs (Fnum x)) (Fexp x)))) (powerRZ (IZR radix) (Fexp (Float (Z.abs (Fnum x)) (Fexp x)))))) *)
(* Goal: @eq R (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
rewrite <- Rmult_assoc.
(* Goal: Rle (Rmult (IZR (Fnum (Float (Zpos (vNum b)) (Fexp x)))) (powerRZ (IZR radix) (Fexp (Float (Zpos (vNum b)) (Fexp x))))) (Rmult (Rmult (IZR radix) (IZR (Fnum (Float (Z.abs (Fnum x)) (Fexp x))))) (powerRZ (IZR radix) (Fexp (Float (Z.abs (Fnum x)) (Fexp x))))) *)
(* Goal: @eq R (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
apply Rle_monotone_exp; auto with real arith.
(* Goal: Rle (IZR (Fnum (Float (Zpos (vNum b)) (Fexp x)))) (Rmult (IZR radix) (IZR (Fnum (Float (Z.abs (Fnum x)) (Fexp x))))) *)
(* Goal: @eq R (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
rewrite <- Rmult_IZR; apply Rle_IZR; simpl in |- *.
rewrite <- (Zabs_eq radix); auto with zarith; rewrite <- Zabs_Zmult;
 auto with float.
(* Goal: Z.le (Zpos (vNum b)) (Z.abs (Z.mul radix (Fnum x))) *)
(* Goal: @eq R (FtoRradix (Float (Zpos (vNum b)) (Fexp x))) (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
case H; simpl in |- *; auto.
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
(* Goal: @eq R (Rmult (Rmult (IZR (Zpos (vNum b))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp y)))) (Rmult (FtoRradix (Float (Zpos (vNum b)) (Fexp y))) (FtoRradix (Float (Z.of_nat (S O)) (Fexp x)))) *)
unfold FtoRradix, FtoR in |- *; simpl in |- *; ring.
Qed.
End MSBProp.