Fprop.v

(****************************************************************************                                                                                         IEEE754  :  Fprop                                                                                                                                              Laurent Thery                                                                                                                                     ***************************************************************************** *)
Require Import Float.
Require Import Fcomp.
Require Import Fop.
Require Import Fnorm.
Section Fprop.
Variable radix:nat.
Hypothesis radixMoreThanOne:(lt (1) radix).

Local FtoRradix := (FtoR radix).
Coercion FtoRradix : float >-> R.
Variable b:Fbound.

Theorem SterbenzAux:
  (x, y:float)
  (Fbounded b x) ->
  (Fbounded b y) -> (Rle R0 y) -> (Rle y x) -> (Rle x (Rmult (2) y)) ->
  (Fbounded b (Fminus radix x y)).
Intros x y; Case y; Case x; Unfold Fminus Fplus Fopp FtoRradix FtoR; Simpl.
Intros Fnum1 Fexp1 Fnum2 Fexp2 H' H'0 H'1 H'2 H'3; Split; Simpl.
2:Case (Zmin_or Fexp1 Fexp2); Intros Min; Rewrite Min; Generalize H' H'0;
   Intuition.
Rewrite Zopp_Zmult.
Cut (n, m:Z)(Zplus (Zminus m n) n)=m; [Intros Eq1 | Auto with zarith].
Cut (Zle
       (Zmult
          Fnum1 (Zpower_nat radix (absolu (Zminus Fexp1 (Zmin Fexp1 Fexp2)))))
       (Zmult
          (Zs (Zs ZERO))
          (Zmult
             Fnum2 (Zpower_nat radix (absolu (Zminus Fexp2 (Zmin Fexp1 Fexp2))))))).
Cut (Zle
       (Zmult
          Fnum2 (Zpower_nat radix (absolu (Zminus Fexp2 (Zmin Fexp1 Fexp2)))))
       (Zmult
          Fnum1 (Zpower_nat radix (absolu (Zminus Fexp1 (Zmin Fexp1 Fexp2)))))).
Case (Zmin_or Fexp1 Fexp2); Intros Min; Rewrite Min.
Replace (Zminus Fexp1 Fexp1) with ZERO; Auto with zarith.
Replace (Zmult Fnum1 (Zpower_nat radix (absolu ZERO))) with Fnum1;
Auto with zarith.
Cut (Zle Fnum1 (vNum b)); [Intros H1 | Generalize H'; Intuition];
Auto with zarith.
Rewrite Zmult_sym; Auto with zarith.
Replace (Zminus Fexp2 Fexp2) with ZERO; Auto with zarith.
Replace (Zmult Fnum2 (Zpower_nat radix (absolu ZERO))) with Fnum2;
Auto with zarith.
Cut (Zle Fnum2 (vNum b)); [Intros H1 | Generalize H'; Intuition];
Auto with zarith.
Rewrite Zmult_sym; Auto with zarith.
Apply le_IZR.
Repeat Rewrite Rmult_IZR.
Repeat Rewrite <- INR_IZR_INZ.
Repeat Rewrite Zpower_nat_powerRZ_absolu.
Apply (Rle_mult_anticompatibility_exp radix) with z := (Zmin Fexp1 Fexp2);
Auto with real zarith arith.
Repeat Rewrite Rmult_assoc.
Repeat Rewrite <- INR_IZR_INZ.
Repeat Rewrite <- powerRZ_add; Auto with real zarith arith.
Repeat Rewrite Eq1; Auto.
Generalize (Zle_min_l Fexp1 Fexp2); Auto with zarith.
Generalize (Zle_min_r Fexp1 Fexp2); Auto with zarith.
Apply le_IZR.
Repeat Rewrite Rmult_IZR.
Repeat Rewrite <- INR_IZR_INZ; Simpl.
Repeat Rewrite Zpower_nat_powerRZ_absolu.
Apply (Rle_mult_anticompatibility_exp radix) with z := (Zmin Fexp1 Fexp2);
Auto with real zarith arith.
Repeat Rewrite Rmult_assoc.
Repeat Rewrite <- INR_IZR_INZ.
Repeat Rewrite <- powerRZ_add; Auto with real zarith arith.
Repeat Rewrite Eq1; Auto.
Generalize (Zle_min_r Fexp1 Fexp2); Auto with zarith.
Generalize (Zle_min_l Fexp1 Fexp2); Auto with zarith.
Qed.

Theorem Sterbenz:
  (x, y:float)
  (Fbounded b x) ->
  (Fbounded b y) -> (Rle (Rmult (Rinv (2)) y) x) -> (Rle x (Rmult (2) y)) ->
  (Fbounded b (Fminus radix x y)).
Intros x y H' H'0 H'1 H'2.
Cut (Rle y (Rmult (2) x)); [Intros Le1 | Idtac].
2:Apply Rle_mult_anticompatibility with z := (Rinv (2)).
2:Rewrite <- Rmult_assoc; Rewrite Rinv_l; Auto with real.
2:Rewrite Rmult_ne_r; Auto.
2:Apply Rlt_Rinv; Auto with real.
Case (Rle_or_lt x y); Intros Le2; Auto.
Case (Rle_or_lt R0 x); Intros Le3; Auto.
Apply oppBoundedInv; Auto.
Rewrite Fopp_Fminus.
Apply SterbenzAux; Auto with real.
Absurd (Rle x (Rmult (2) x)); Auto.
Apply Rle_not; Auto.
Pattern 1 x; Replace (FtoRradix x) with (Rplus x R0); Auto with real.
Replace (Rmult (2) x) with (Rplus x x); Auto with real.
Apply Rlt_compatibility; Auto.
Simpl; Rewrite Rmult_sym; Rewrite Rmult_Rplus_distr; Repeat Rewrite Rmult_ne_l;
Auto with real.
Apply Rle_trans with r2 := (FtoRradix y); Auto.
Case (Rle_or_lt R0 y); Intros Le3; Auto.
Apply SterbenzAux; Auto with real.
Apply Rlt_le; Auto.
Absurd (Rle y (Rmult (2) y)); Auto.
Apply Rle_not; Auto.
Pattern 1 y; Replace (FtoRradix y) with (Rplus y R0); Auto with real.
Replace (Rmult (2) y) with (Rplus y y); Auto with real.
Apply Rlt_compatibility; Auto.
Simpl; Rewrite Rmult_sym; Rewrite Rmult_Rplus_distr; Repeat Rewrite Rmult_ne_l;
Auto with real.
Apply Rle_trans with r2 := (FtoRradix x); Auto.
Apply Rlt_le; Auto.
Qed.

Theorem BminusSameExpAux:
  (x, y:float)
  (Fbounded b x) ->
  (Fbounded b y) -> (Rle R0 y) -> (Rle y x) -> (Fexp x)=(Fexp y) ->
  (Fbounded b (Fminus radix x y)).
Intros x y H' H'0 H'1 H'2 H'3.
Rewrite minusSameExp; Auto.
Repeat Split; Simpl; Auto.
3:Generalize H'; Intuition.
Apply Zle_trans with ZERO; Auto with zarith.
Apply Zsimpl_le_plus_l with p := (Fnum y); Auto.
Rewrite Zero_right; Rewrite Zle_plus_minus.
Apply Rle_Fexp_eq_Zle with radix := radix; Auto with zarith.
Apply Zle_trans with (Fnum x); Auto with zarith.
2:Generalize H'; Intuition.
Cut (Zle ZERO (Fnum y)); Auto with zarith.
Apply LeR0Fnum with radix := radix; Auto with zarith.
Qed.

Theorem BminusSameExp:
  (x, y:float)
  (Fbounded b x) ->
  (Fbounded b y) -> (Rle R0 x) -> (Rle R0 y) -> (Fexp x)=(Fexp y) ->
  (Fbounded b (Fminus radix x y)).
Intros x y H' H'0 H'1 H'2 H'3.
Case (Rle_or_lt x y); Intros Le2; Auto.
Apply oppBoundedInv; Auto.
Rewrite Fopp_Fminus.
Apply BminusSameExpAux; Auto.
Apply BminusSameExpAux; Auto with real.
Red; Auto.
Qed.

Theorem BminusSameExpNeg:
  (x, y:float)
  (Fbounded b x) ->
  (Fbounded b y) -> (Rle x R0) -> (Rle y R0) -> (Fexp x)=(Fexp y) ->
  (Fbounded b (Fminus radix x y)).
Intros x y H' H'0 H'1 H'2 H'3.
Apply oppBoundedInv; Auto.
Rewrite Fopp_Fminus_dist.
Apply BminusSameExp; Auto with float.
Unfold FtoRradix; Rewrite Fopp_correct.
Replace R0 with (Ropp R0); Auto with real.
Unfold FtoRradix; Rewrite Fopp_correct.
Replace R0 with (Ropp R0); Auto with real.
Qed.
End Fprop.
Hints Resolve Sterbenz BminusSameExp BminusSameExpNeg :float.

14/12/100, 15:23