(****************************************************************************
                                                                             
          IEEE754  :  Fprop                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export Fbound.
Section Fprop.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.
 
Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.

Variable b : Fbound.
 
Theorem SterbenzAux :
 forall x y : float,
 Fbounded b x ->
 Fbounded b y ->
 (y <= x)%R -> (x <= 2%nat * y)%R -> Fbounded b (Fminus radix x y).
(* Goal: forall (x y : float) (_ : Fbounded b x) (_ : Fbounded b y) (_ : Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix y)) (FtoRradix x)) (_ : Rle (FtoRradix x) (Rmult (INR (S (S O))) (FtoRradix y))), Fbounded b (Fminus radix x y) *)
intros x y H' H'0 H'1 H'2.
(* Goal: Fbounded b (Fminus radix x y) *)
cut (0 <= Fminus radix x y)%R; [ intros Rle1 | idtac ].
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
cut (Fminus radix x y <= y)%R; [ intros Rle2 | idtac ].
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
case (Zle_or_lt (Fexp x) (Fexp y)); intros Zle1.
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
repeat split.
(* Goal: Z.lt (Z.abs (Fnum (Fminus radix x y))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
apply Zle_lt_trans with (Zabs (Fnum x)); auto with float.
(* Goal: Z.le (Z.abs (Fnum (Fminus radix x y))) (Z.abs (Fnum x)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
change (Fnum (Fabs (Fminus radix x y)) <= Fnum (Fabs x))%Z in |- *.
(* Goal: Z.le (Fnum (Fabs (Fminus radix x y))) (Fnum (Fabs y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix (Fabs (Fminus radix x y))) (FtoR radix (Fabs y)) *)
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
repeat rewrite Fabs_correct.
(* Goal: Rle (Rabs (FtoR radix (Fminus radix x y))) (Rabs (FtoR radix y)) *)
(* Goal: Z.lt Z0 radix *)
(* Goal: Z.lt Z0 radix *)
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
repeat rewrite Rabs_pos_eq; auto.
(* Goal: Rle (IZR Z0) (FtoR radix x) *)
(* Goal: Z.lt Z0 radix *)
(* Goal: Z.lt Z0 radix *)
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs x)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
apply Rle_trans with (2 := H'1); auto.
(* Goal: Rle (IZR Z0) (FtoR radix x) *)
(* Goal: Z.lt Z0 radix *)
(* Goal: Z.lt Z0 radix *)
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs x)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
apply Rle_trans with (2 := H'1); auto.
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Z.lt Z0 radix *)
(* Goal: Z.lt Z0 radix *)
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
apply Rle_trans with (2 := Rle2); auto.
(* Goal: Z.lt Z0 radix *)
apply Zlt_trans with (2 := radixMoreThanOne); auto with zarith.
(* Goal: Z.lt Z0 radix *)
apply Zlt_trans with (2 := radixMoreThanOne); auto with zarith.
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs x)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
unfold Fminus in |- *; simpl in |- *; apply Zmin_le1; auto.
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
unfold Fminus in |- *; simpl in |- *; rewrite Zmin_le1; auto with float.
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
repeat split.
(* Goal: Z.lt (Z.abs (Fnum (Fminus radix x y))) (Zpos (vNum b)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
apply Zle_lt_trans with (Zabs (Fnum y)); auto with float.
(* Goal: Z.le (Z.abs (Fnum (Fminus radix x y))) (Z.abs (Fnum y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
change (Fnum (Fabs (Fminus radix x y)) <= Fnum (Fabs y))%Z in |- *.
(* Goal: Z.le (Fnum (Fabs (Fminus radix x y))) (Fnum (Fabs y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith.
(* Goal: Rle (FtoR radix (Fabs (Fminus radix x y))) (FtoR radix (Fabs y)) *)
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
repeat rewrite Fabs_correct.
(* Goal: Rle (Rabs (FtoR radix (Fminus radix x y))) (Rabs (FtoR radix y)) *)
(* Goal: Z.lt Z0 radix *)
(* Goal: Z.lt Z0 radix *)
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
repeat rewrite Rabs_pos_eq; auto.
(* Goal: Rle (IZR Z0) (FtoR radix y) *)
(* Goal: Z.lt Z0 radix *)
(* Goal: Z.lt Z0 radix *)
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
apply Rle_trans with (2 := Rle2); auto.
(* Goal: Z.lt Z0 radix *)
apply Zlt_trans with (2 := radixMoreThanOne); auto with zarith.
(* Goal: Z.lt Z0 radix *)
apply Zlt_trans with (2 := radixMoreThanOne); auto with zarith.
(* Goal: @eq Z (Fexp (Fabs (Fminus radix x y))) (Fexp (Fabs y)) *)
(* Goal: Z.le (Z.opp (Z.of_N (dExp b))) (Fexp (Fminus radix x y)) *)
(* Goal: Rle (FtoRradix (Fminus radix x y)) (FtoRradix y) *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
unfold Fminus in |- *; simpl in |- *; apply Zmin_le2; auto with zarith.
unfold Fminus in |- *; simpl in |- *; rewrite Zmin_le2;
 auto with float zarith.
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
rewrite (Fminus_correct radix); auto with arith; fold FtoRradix in |- *.
(* Goal: Rle (IZR Z0) (Rminus (FtoRradix x) (FtoRradix y)) *)
(* Goal: Z.lt Z0 radix *)
apply Rplus_le_reg_l with (r := FtoRradix y); auto.
(* Goal: Rle (Rplus (FtoRradix y) (IZR Z0)) (Rplus (FtoRradix y) (Rminus (FtoRradix x) (FtoRradix y))) *)
(* Goal: Z.lt Z0 radix *)
replace (y + (x - y))%R with (FtoRradix x); [ idtac | ring ].
(* Goal: Rle (FtoRradix x) (Rplus (FtoRradix y) (FtoRradix y)) *)
(* Goal: Z.lt Z0 radix *)
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
replace (y + y)%R with (2%nat * y)%R; [ auto | simpl in |- *; ring ].
(* Goal: Z.lt Z0 radix *)
apply Zlt_trans with (2 := radixMoreThanOne); auto with zarith.
(* Goal: Rle (IZR Z0) (FtoRradix (Fminus radix x y)) *)
rewrite (Fminus_correct radix); auto with arith; fold FtoRradix in |- *.
(* Goal: Rle (IZR Z0) (Rminus (FtoRradix x) (FtoRradix y)) *)
(* Goal: Z.lt Z0 radix *)
apply Rplus_le_reg_l with (r := FtoRradix y); auto.
(* Goal: Rle (Rplus (FtoRradix y) (IZR Z0)) (Rplus (FtoRradix y) (Rminus (FtoRradix x) (FtoRradix y))) *)
(* Goal: Z.lt Z0 radix *)
replace (y + (x - y))%R with (FtoRradix x); [ idtac | ring ].
(* Goal: Rle (Rplus (FtoRradix y) (IZR Z0)) (FtoRradix x) *)
(* Goal: Z.lt Z0 radix *)
replace (y + 0)%R with (FtoRradix y); [ auto | simpl in |- *; ring ].
(* Goal: Z.lt Z0 radix *)
apply Zlt_trans with (2 := radixMoreThanOne); auto with zarith.
Qed.
 
Theorem Sterbenz :
 forall x y : float,
 Fbounded b x ->
 Fbounded b y ->
 (/ 2%nat * y <= x)%R -> (x <= 2%nat * y)%R -> Fbounded b (Fminus radix x y).
(* Goal: forall (x y : float) (_ : Fbounded b x) (_ : Fbounded b y) (_ : Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix y)) (FtoRradix x)) (_ : Rle (FtoRradix x) (Rmult (INR (S (S O))) (FtoRradix y))), Fbounded b (Fminus radix x y) *)
intros x y H' H'0 H'1 H'2.
(* Goal: Fbounded b (Fminus radix x y) *)
cut (y <= 2%nat * x)%R; [ intros Le1 | idtac ].
(* Goal: Fbounded b (Fminus radix x y) *)
case (Rle_or_lt x y); intros Le2; auto.
(* Goal: Fbounded b (Fminus radix x y) *)
apply oppBoundedInv; auto.
(* Goal: Fbounded b (Fopp (Fminus radix x y)) *)
(* Goal: Fbounded b (Fminus radix x y) *)
rewrite Fopp_Fminus.
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix y) (Rmult (INR (S (S O))) (FtoRradix x)) *)
apply SterbenzAux; auto with real.
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Rle (FtoRradix y) (Rmult (INR (S (S O))) (FtoRradix x)) *)
apply SterbenzAux; auto with real.
(* Goal: Rle (FtoRradix y) (Rmult (INR (S (S O))) (FtoRradix x)) *)
apply Rmult_le_reg_l with (r := (/ 2%nat)%R).
(* Goal: Rlt (IZR Z0) (Rinv (INR (S (S O)))) *)
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix y)) (Rmult (Rinv (INR (S (S O)))) (Rmult (INR (S (S O))) (FtoRradix x))) *)
apply Rinv_0_lt_compat; auto with real.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix y)) (Rmult (Rinv (INR (S (S O)))) (Rmult (INR (S (S O))) (FtoRradix x))) *)
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoRradix y)) (Rmult (IZR (Zpos xH)) (FtoRradix x)) *)
rewrite Rmult_1_l; auto.
Qed.
 
Theorem BminusSameExpAux :
 forall x y : float,
 Fbounded b x ->
 Fbounded b y ->
 (0 <= y)%R -> (y <= x)%R -> Fexp x = Fexp y -> Fbounded b (Fminus radix x y).
(* Goal: forall (x y : float) (_ : Fbounded b x) (_ : Fbounded b y) (_ : Rle (FtoRradix x) (IZR Z0)) (_ : Rle (FtoRradix y) (IZR Z0)) (_ : @eq Z (Fexp x) (Fexp y)), Fbounded b (Fminus radix x y) *)
intros x y H' H'0 H'1 H'2 H'3.
(* Goal: Fbounded b (Fminus radix x y) *)
cut (0 < radix)%Z; [ intros Z1 | idtac ].
(* Goal: Fbounded b (Fminus radix x y) *)
(* Goal: Z.lt Z0 radix *)
rewrite minusSameExp; auto.
(* Goal: Fbounded b (Float (Z.sub (Fnum x) (Fnum y)) (Fexp x)) *)
(* Goal: Z.lt Z0 radix *)
repeat split; simpl in |- *; auto with float.
(* Goal: Z.lt (Z.abs (Z.sub (Fnum x) (Fnum y))) (Zpos (vNum b)) *)
(* Goal: Z.lt Z0 radix *)
apply Zle_lt_trans with (Zabs (Fnum x)); auto with float zarith.
change (Fnum (Fabs (Float (Fnum x - Fnum y) (Fexp x))) <= Fnum (Fabs x))%Z
 in |- *.
(* Goal: Z.le (Fnum (Fabs (Float (Z.sub (Fnum x) (Fnum y)) (Fexp x)))) (Fnum (Fabs x)) *)
(* Goal: Z.lt Z0 radix *)
apply Rle_Fexp_eq_Zle with (radix := radix); auto with zarith.
(* Goal: Rle (FtoR radix (Fabs (Float (Z.sub (Fnum x) (Fnum y)) (Fexp x)))) (FtoR radix (Fabs x)) *)
(* Goal: Z.lt Z0 radix *)
rewrite <- (minusSameExp radix); auto.
repeat rewrite (Fabs_correct radix); try rewrite Fminus_correct;
 auto with zarith.
(* Goal: Rle (Rabs (Rminus (FtoR radix x) (FtoR radix y))) (Rabs (FtoR radix x)) *)
(* Goal: Z.lt Z0 radix *)
repeat rewrite Rabs_pos_eq; auto with real.
(* Goal: Rle (Rminus (FtoR radix x) (FtoR radix y)) (FtoR radix x) *)
(* Goal: Rle (IZR Z0) (FtoR radix x) *)
(* Goal: Rle (IZR Z0) (Rminus (FtoR radix x) (FtoR radix y)) *)
(* Goal: Z.lt Z0 radix *)
apply Rle_trans with (x - 0)%R; auto with real.
(* Goal: Rle (Rminus (FtoRradix x) (FtoRradix x)) (Rminus (FtoR radix x) (FtoR radix y)) *)
(* Goal: Z.lt Z0 radix *)
unfold Rminus in |- *; auto with real.
(* Goal: Rle (IZR Z0) (FtoR radix x) *)
(* Goal: Rle (IZR Z0) (Rminus (FtoR radix x) (FtoR radix y)) *)
(* Goal: Z.lt Z0 radix *)
apply Rle_trans with (FtoRradix y); auto with real.
(* Goal: Rle (IZR Z0) (Rminus (FtoR radix x) (FtoR radix y)) *)
(* Goal: Z.lt Z0 radix *)
replace 0%R with (x - x)%R; auto with real.
(* Goal: Rle (Rminus (FtoRradix x) (FtoRradix x)) (Rminus (FtoR radix x) (FtoR radix y)) *)
(* Goal: Z.lt Z0 radix *)
unfold Rminus in |- *; auto with real.
(* Goal: Z.lt Z0 radix *)
apply Zlt_trans with (2 := radixMoreThanOne); auto with zarith.
Qed.
 
Theorem BminusSameExp :
 forall x y : float,
 Fbounded b x ->
 Fbounded b y ->
 (0 <= x)%R -> (0 <= y)%R -> Fexp x = Fexp y -> Fbounded b (Fminus radix x y).
(* Goal: forall (x y : float) (_ : Fbounded b x) (_ : Fbounded b y) (_ : Rle (FtoRradix x) (IZR Z0)) (_ : Rle (FtoRradix y) (IZR Z0)) (_ : @eq Z (Fexp x) (Fexp y)), Fbounded b (Fminus radix x y) *)
intros x y H' H'0 H'1 H'2 H'3.
(* Goal: Fbounded b (Fminus radix x y) *)
case (Rle_or_lt x y); intros Le2; auto.
(* Goal: Fbounded b (Fminus radix x y) *)
apply oppBoundedInv; auto.
(* Goal: Fbounded b (Fopp (Fminus radix x y)) *)
(* Goal: Fbounded b (Fminus radix x y) *)
rewrite Fopp_Fminus.
(* Goal: Fbounded b (Fminus radix y x) *)
(* Goal: Fbounded b (Fminus radix x y) *)
apply BminusSameExpAux; auto.
(* Goal: Fbounded b (Fminus radix x y) *)
apply BminusSameExpAux; auto with real.
Qed.
 
Theorem BminusSameExpNeg :
 forall x y : float,
 Fbounded b x ->
 Fbounded b y ->
 (x <= 0)%R -> (y <= 0)%R -> Fexp x = Fexp y -> Fbounded b (Fminus radix x y).
(* Goal: forall (x y : float) (_ : Fbounded b x) (_ : Fbounded b y) (_ : Rle (FtoRradix x) (IZR Z0)) (_ : Rle (FtoRradix y) (IZR Z0)) (_ : @eq Z (Fexp x) (Fexp y)), Fbounded b (Fminus radix x y) *)
intros x y H' H'0 H'1 H'2 H'3.
(* Goal: Fbounded b (Fminus radix x y) *)
apply oppBoundedInv; auto.
(* Goal: Fbounded b (Fopp (Fminus radix x y)) *)
rewrite Fopp_Fminus_dist.
(* Goal: Fbounded b (Fminus radix (Fopp x) (Fopp y)) *)
apply BminusSameExp; auto with float.
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp y)) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: Rle (IZR Z0) (Ropp (FtoR radix y)) *)
replace 0%R with (-0)%R; auto with real.
(* Goal: Rle (IZR Z0) (FtoRradix (Fopp y)) *)
unfold FtoRradix in |- *; rewrite Fopp_correct.
(* Goal: Rle (IZR Z0) (Ropp (FtoR radix y)) *)
replace 0%R with (-0)%R; auto with real.
Qed.
End Fprop.
Hint Resolve Sterbenz BminusSameExp BminusSameExpNeg: float.