(****************************************************************************
                                                                             
          IEEE754  :  Closest2Plus                                                     
                                                                             
          Laurent Thery                                                      
                                                                             
  ******************************************************************************)
Require Export ClosestPlus.
Require Export Closest2Prop.
Section F2.
Variable b : Fbound.
Variable precision : nat.
 
Let radix := 2%Z.
 
Let FtoRradix := FtoR radix.
Local Coercion FtoRradix : float >-> R.
 
Theorem TwoMoreThanOne : (1 < radix)%Z.
(* Goal: Z.lt (Zpos xH) radix *)
red in |- *; simpl in |- *; auto.
Qed.
Hint Resolve TwoMoreThanOne.
Hypothesis precisionNotZero : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.
 
Theorem plusUpperBound :
 forall P,
 RoundedModeP b 2%nat P ->
 forall p q pq : float,
 P (p + q)%R pq ->
 Fbounded b p ->
 Fbounded b q -> (Rabs pq <= radix * Rmax (Rabs p) (Rabs q))%R.
(* Goal: forall (P : forall (_ : R) (_ : float), Prop) (_ : RoundedModeP b (Z.of_nat (S (S O))) P) (p q pq : float) (_ : P (Rplus (FtoRradix p) (FtoRradix q)) pq) (_ : Fbounded b p) (_ : Fbounded b q), Rle (Rabs (FtoRradix pq)) (Rmult (IZR radix) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q)))) *)
intros P H' p q pq H'0 H'1 H'2.
(* Goal: Rle (Rabs (FtoRradix pq)) (Rmult (IZR radix) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q)))) *)
rewrite <- (Rabs_right radix); auto with real zarith.
(* Goal: Rle (Rabs (FtoRradix pq)) (Rmult (Rabs (IZR radix)) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q)))) *)
rewrite <- RmaxRmult; auto with real.
(* Goal: Rle (Rabs (FtoRradix pq)) (Rmax (Rmult (Rabs (IZR radix)) (Rabs (FtoRradix p))) (Rmult (Rabs (IZR radix)) (Rabs (FtoRradix q)))) *)
repeat rewrite <- Rabs_mult.
(* Goal: Rle (Rabs (FtoRradix pq)) (Rmax (Rabs (Rmult (IZR radix) (FtoRradix p))) (Rabs (Rmult (IZR radix) (FtoRradix q)))) *)
case (Rle_or_lt p q); intros Rltp.
(* Goal: Rle (Rabs (FtoRradix pq)) (Rmax (Rabs (Rmult (IZR radix) (FtoRradix q))) (Rabs (Rmult (IZR radix) (FtoRradix p)))) *)
apply RmaxAbs; auto.
(* Goal: Rle (Rmult (IZR radix) (FtoRradix q)) (FtoRradix pq) *)
(* Goal: Rle (FtoRradix pq) (Rmult (IZR radix) (FtoRradix p)) *)
apply (RoundedModeMultLess b radix) with (P := P) (r := (p + q)%R); auto.
replace (radix * FtoR radix p)%R with (p + p)%R;
 [ auto with real | unfold radix at 1; fold FtoRradix; ring].
unfold FtoRradix in |- *;
 apply (RoundedModeMult b radix) with (P := P) (r := (p + q)%R); 
 auto.
replace (radix * FtoR radix q)%R with (q + q)%R;
 [ auto with real | unfold radix at 1; fold FtoRradix; ring ].
(* Goal: Rle (Rabs (FtoRradix pq)) (Rmax (Rabs (Rmult (IZR radix) (FtoRradix p))) (Rabs (Rmult (IZR radix) (FtoRradix q)))) *)
rewrite RmaxSym.
(* Goal: Rle (Rabs (FtoRradix pq)) (Rmax (Rabs (Rmult (IZR radix) (FtoRradix q))) (Rabs (Rmult (IZR radix) (FtoRradix p)))) *)
apply RmaxAbs; auto.
(* Goal: Rle (Rmult (IZR radix) (FtoRradix q)) (FtoRradix pq) *)
(* Goal: Rle (FtoRradix pq) (Rmult (IZR radix) (FtoRradix p)) *)
apply (RoundedModeMultLess b radix) with (P := P) (r := (p + q)%R); auto.
replace (radix * FtoR radix q)%R with (q + q)%R;
 [ auto with real | unfold radix at 1; fold FtoRradix; ring ].
unfold FtoRradix in |- *;
 apply (RoundedModeMult b radix) with (P := P) (r := (p + q)%R); 
 auto.
replace (radix * FtoR radix p)%R with (p + p)%R;
 [ auto with real zarith | unfold radix at 1; fold FtoRradix; ring].
Qed.
 
Theorem plusErrorBound2 :
 forall p q r : float,
 Fbounded b p ->
 Fbounded b q ->
 Closest b radix (p + q) r ->
 ~ is_Fzero r ->
 (Rabs (r - (p + q)) < radix * / pPred (vNum b) * Rmax (Rabs p) (Rabs q))%R.
(* Goal: forall (p q r : float) (_ : Fbounded b p) (_ : Fbounded b q) (_ : Closest b radix (Rplus (FtoRradix p) (FtoRradix q)) r) (_ : not (is_Fzero r)), Rlt (Rabs (Rminus (FtoRradix r) (Rplus (FtoRradix p) (FtoRradix q)))) (Rmult (Rmult (IZR radix) (Rinv (IZR (pPred (vNum b))))) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q)))) *)
intros p q r H' H'0 H'1 H'2.
apply
 Rlt_le_trans
  with (Rabs (FtoR radix r) * / radix * (radix * / pPred (vNum b)))%R; 
 auto.
unfold FtoRradix in |- *; apply plusErrorBound1 with (precision := precision);
 auto with arith.
replace (Rabs (FtoR radix r) * / radix * (radix * / pPred (vNum b)))%R with
 (radix * / pPred (vNum b) * (Rabs r * / radix))%R; 
 [ idtac | fold FtoRradix; ring ].
(* Goal: Rle (Rmult (Rmult (IZR radix) (Rinv (IZR (pPred (vNum b))))) (Rmult (Rabs (FtoRradix r)) (Rinv (IZR radix)))) (Rmult (Rmult (IZR radix) (Rinv (IZR (pPred (vNum b))))) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q)))) *)
apply Rmult_le_compat_l; auto.
(* Goal: Rle (IZR Z0) (Rmult (IZR radix) (Rinv (IZR (pPred (vNum b))))) *)
(* Goal: Rle (Rmult (Rabs (FtoRradix r)) (Rinv (IZR radix))) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q))) *)
replace 0%R with (radix * 0)%R; [ apply Rmult_le_compat_l | ring ].
(* Goal: Rle (IZR Z0) (IZR radix) *)
(* Goal: Rle (IZR Z0) (Rinv (IZR (pPred (vNum b)))) *)
(* Goal: Rle (Rmult (Rabs (FtoRradix r)) (Rinv (IZR radix))) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q))) *)
cut (0 <= radix)%Z; auto with real zarith.
apply Rlt_le; apply Rinv_0_lt_compat; cut (0 < pPred (vNum b))%Z;
 auto with real zarith.
(* Goal: Z.lt Z0 (pPred (vNum b)) *)
(* Goal: Rle (Rmult (Rabs (FtoRradix r)) (Rinv (IZR radix))) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q))) *)
unfold pPred in |- *; apply Zlt_succ_pred; simpl in |- *.
apply vNumbMoreThanOne with (radix := radix) (precision := precision);
 auto with real arith.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (FtoR radix (Fopp q)) *)
(* Goal: Rle (FtoR radix (Fopp q)) (Rmult (INR (S (S O))) (FtoR radix p)) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
rewrite (Rmult_comm (Rabs r)); rewrite <- Rmult_assoc; rewrite Rinv_r;
(* Goal: Rlt (Rmult (IZR (Zpos xH)) (FtoR radix p)) (Rplus (Rmult (IZR radix) (FtoRradix p)) (Rmult (IZR radix) (FtoRradix q))) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
 auto with real zarith; rewrite Rmult_1_l.
(* Goal: Rle (Rabs (FtoRradix r)) (Rmult (IZR radix) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q)))) *)
apply plusUpperBound with (P := Closest b radix); auto.
(* Goal: RoundedModeP b radix (Closest b radix) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
apply ClosestRoundedModeP with (precision := precision); auto.
Qed.
 
Theorem plusClosestLowerBoundAux1 :
 forall p q pq : float,
 (Rabs q <= p)%R ->
 Closest b radix (p + q) pq ->
 Fbounded b p -> Fbounded b q -> pq <> (p + q)%R :>R -> (/ radix * p <= pq)%R.
(* Goal: forall (p q pq : float) (_ : Closest b radix (Rplus (FtoRradix p) (FtoRradix q)) pq) (_ : Fbounded b p) (_ : Fbounded b q) (_ : not (@eq R (FtoRradix pq) (Rplus (FtoRradix p) (FtoRradix q)))) (_ : Rle (Rabs (FtoRradix p)) (Rabs (FtoRradix q))), Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
intros p q pq H' H'0 H'1 H'2 H'3.
cut (0 <= p)%R;
 [ intros Rl0; Casec Rl0; intros H0
 | apply Rle_trans with (2 := H'); auto with real ].
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply (FmultRadixInv b radix precision) with (5 := H'0); auto.
(* Goal: Rlt (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
case (Rle_or_lt 0 q); intros Rl0.
(* Goal: Rlt (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply Rlt_le_trans with (FtoRradix p); auto.
(* Goal: Rlt (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (FtoRradix p) *)
(* Goal: Rle (FtoRradix p) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rlt (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply Rlt_RinvDouble; auto.
pattern (FtoRradix p) at 1 in |- *; replace (FtoRradix p) with (p + 0)%R;
 auto with real.
(* Goal: Rlt (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply Rmult_lt_reg_l with (r := IZR radix); auto with real.
(* Goal: Rle (Rmult (IZR radix) (Rmult (Rinv (INR (S (S O)))) (FtoR radix p))) (Rmult (IZR radix) (FtoR radix (Fopp q))) *)
(* Goal: Rle (FtoR radix (Fopp q)) (Rmult (INR (S (S O))) (FtoR radix p)) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite <- Rmult_assoc; rewrite Rinv_r.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) (FtoR radix p)) (Rmult (IZR radix) (Rplus (FtoRradix p) (FtoRradix q))) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite Rmult_plus_distr_l.
(* Goal: Rlt (Rmult (IZR (Zpos xH)) (FtoR radix p)) (Rplus (Rmult (IZR radix) (FtoRradix p)) (Rmult (IZR radix) (FtoRradix q))) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite Rmult_1_l.
(* Goal: Rlt (FtoR radix p) (Rplus (Rmult (IZR radix) (FtoRradix p)) (Rmult (IZR radix) (FtoRradix q))) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply Rplus_lt_reg_l with (r := (- (radix * p))%R).
replace (- (radix * p) + FtoR radix p)%R with (- p)%R;
 [ idtac | unfold radix at 1; unfold FtoRradix; ring].
replace (- (radix * p) + (radix * p + radix * q))%R with (radix * q)%R;
 [ idtac | simpl in |- *; ring ].
(* Goal: Rlt (Ropp (FtoRradix p)) (Rmult (IZR radix) (FtoRradix q)) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite <- (Ropp_involutive (radix * q)); apply Ropp_lt_contravar.
(* Goal: Rlt (Ropp (Rmult (IZR radix) (FtoRradix q))) (FtoRradix p) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
replace (- (radix * q))%R with (radix * - q)%R; [ idtac | ring ].
(* Goal: Rlt (Rmult (IZR radix) (Ropp (FtoRradix q))) (FtoRradix p) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
case (Rle_or_lt (FtoRradix p) (radix * - q)); auto.
(* Goal: forall _ : Rle (FtoRradix p) (Rmult (IZR radix) (Ropp (FtoRradix q))), Rlt (Rmult (IZR radix) (Ropp (FtoRradix q))) (FtoRradix p) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
intros H'4; Contradict H'3.
(* Goal: @eq R (FtoRradix pq) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite <- (Fplus_correct radix); auto.
(* Goal: @eq R (FtoRradix pq) (FtoR radix (Fplus radix p q)) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
unfold FtoRradix in |- *; apply sym_eq; apply ClosestIdem with (b := b); auto.
(* Goal: Fbounded b (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
replace (Fplus radix p q) with (Fminus radix p (Fopp q)).
(* Goal: Fbounded b (Fminus radix p (Fopp q)) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite <- Fopp_Fminus.
(* Goal: Fbounded b (Fopp p) *)
(* Goal: not (@eq R (FtoRradix (Fopp pq)) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p)))) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
apply oppBounded; auto.
(* Goal: Fbounded b (Fminus radix (Fopp q) p) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply Sterbenz; auto.
(* Goal: Fbounded b (Fopp p) *)
(* Goal: not (@eq R (FtoRradix (Fopp pq)) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p)))) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
apply oppBounded; auto.
(* Goal: Rle (Rmult (Rinv (INR (S (S O)))) (FtoR radix p)) (FtoR radix (Fopp q)) *)
(* Goal: Rle (FtoR radix (Fopp q)) (Rmult (INR (S (S O))) (FtoR radix p)) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply Rmult_le_reg_l with (r := IZR radix); auto with real.
(* Goal: Rle (Rmult (IZR radix) (Rmult (Rinv (INR (S (S O)))) (FtoR radix p))) (Rmult (IZR radix) (FtoR radix (Fopp q))) *)
(* Goal: Rle (FtoR radix (Fopp q)) (Rmult (INR (S (S O))) (FtoR radix p)) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite <- Rmult_assoc; rewrite Rinv_r.
(* Goal: Rle (Rmult (IZR (Zpos xH)) (FtoR radix p)) (Rmult (IZR radix) (FtoR radix (Fopp q))) *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (FtoR radix (Fopp q)) (Rmult (INR (S (S O))) (FtoR radix p)) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite Rmult_1_l; rewrite Fopp_correct; auto.
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
replace 0%R with (INR 0); auto with real arith.
(* Goal: Rle (FtoR radix (Fopp q)) (Rmult (INR (S (S O))) (FtoR radix p)) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply Rle_trans with (FtoR 2%nat p); auto with real.
(* Goal: Rle (FtoR radix (Fopp q)) (FtoR (Z.of_nat (S (S O))) p) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite Fopp_correct; auto.
(* Goal: Rle (Ropp (FtoR radix q)) (FtoR (Z.of_nat (S (S O))) p) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite <- Faux.Rabsolu_left1; auto.
(* Goal: Rle (FtoR radix q) (IZR Z0) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply Rlt_le; auto.
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
unfold Fminus in |- *; rewrite Fopp_Fopp; auto.
apply
 (ClosestCompatible b radix (p + q)%R (FtoR radix (Fplus radix p q)) pq pq);
 auto.
(* Goal: @eq R (Rplus (FtoRradix p) (FtoRradix q)) (FtoR radix (Fplus radix p q)) *)
(* Goal: Fbounded b pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
apply sym_eq; unfold FtoRradix in |- *; apply Fplus_correct; auto.
apply
 RoundedModeBounded
  with (radix := radix) (P := Closest b radix) (r := (p + q)%R); 
 auto.
(* Goal: RoundedModeP b radix (Closest b radix) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
apply ClosestRoundedModeP with (precision := precision); auto.
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
replace 0%R with (INR 0); auto with real arith.
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
rewrite <- H0; rewrite Rmult_0_r.
(* Goal: Rle (IZR Z0) (FtoRradix pq) *)
replace (FtoRradix pq) with (FtoRradix p); auto.
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix pq) *)
rewrite <- H0; auto with real.
(* Goal: @eq R (FtoRradix p) (FtoRradix pq) *)
unfold FtoRradix in |- *; apply ClosestIdem with (b := b); auto.
(* Goal: Closest b radix (FtoR radix p) pq *)
apply (ClosestCompatible b radix (p + q)%R (FtoR radix p) pq pq); auto.
(* Goal: @eq R (Rplus (FtoRradix p) (FtoRradix q)) (FtoR radix p) *)
(* Goal: Fbounded b pq *)
replace (FtoR 2%nat p) with (FtoRradix p); auto.
(* Goal: @eq R (Rplus (FtoRradix p) (FtoRradix q)) (FtoR radix p) *)
(* Goal: Fbounded b pq *)
fold FtoRradix; rewrite <- H0; replace (FtoRradix q) with 0%R; try ring.
(* Goal: @eq R (IZR Z0) (FtoRradix q) *)
(* Goal: Fbounded b pq *)
generalize H'; unfold Rabs in |- *; case (Rcase_abs q); auto.
(* Goal: Rle (IZR Z0) (FtoRradix p) *)
(* Goal: @eq R (FtoRradix p) (FtoRradix pq) *)
intros H'4 H'5; Contradict H'5; rewrite <- H0; auto with real.
(* Goal: not (Rle (Ropp (FtoRradix q)) (IZR Z0)) *)
(* Goal: forall (_ : Rge (FtoRradix q) (IZR Z0)) (_ : Rle (FtoRradix q) (FtoRradix p)), @eq R (IZR Z0) (FtoRradix q) *)
(* Goal: Fbounded b pq *)
apply Rlt_not_le; auto with real.
(* Goal: forall (_ : Rge (FtoRradix q) (IZR Z0)) (_ : Rle (FtoRradix q) (FtoRradix p)), @eq R (IZR Z0) (FtoRradix q) *)
(* Goal: Fbounded b pq *)
intros H'4 H'5; apply Rle_antisym; auto with real.
(* Goal: Rle (FtoRradix q) (IZR Z0) *)
(* Goal: Fbounded b pq *)
rewrite H0; auto.
apply
 RoundedModeBounded
  with (radix := radix) (P := Closest b radix) (r := (p + q)%R); 
 auto.
(* Goal: RoundedModeP b radix (Closest b radix) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
apply ClosestRoundedModeP with (precision := precision); auto.
Qed.
 
Theorem plusClosestLowerBoundAux2 :
 forall p q pq : float,
 Closest b radix (p + q) pq ->
 Fbounded b p ->
 Fbounded b q ->
 pq <> (p + q)%R :>R ->
 (Rabs p <= Rabs q)%R -> (/ radix * Rabs q <= Rabs pq)%R.
(* Goal: forall (p q pq : float) (_ : Closest b radix (Rplus (FtoRradix p) (FtoRradix q)) pq) (_ : Fbounded b p) (_ : Fbounded b q) (_ : not (@eq R (FtoRradix pq) (Rplus (FtoRradix p) (FtoRradix q)))) (_ : Rle (Rabs (FtoRradix p)) (Rabs (FtoRradix q))), Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
intros p q pq H' H'0 H'1 H'2 H'3.
cut (Fbounded b pq);
 [ intros Fb0
 | apply
    RoundedModeBounded
     with (radix := radix) (P := Closest b radix) (r := (p + q)%R); 
    auto; apply ClosestRoundedModeP with (precision := precision) ]; 
 auto.
case (Rle_or_lt 0 q); intros Rl2;
 [ idtac | cut (q <= 0)%R; [ intros Rl2' | apply Rlt_le; auto ] ].
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
repeat rewrite Rabs_right; auto with real.
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix q)) (FtoRradix pq) *)
(* Goal: Rge (FtoRradix pq) (IZR Z0) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
apply plusClosestLowerBoundAux1 with (q := p); auto.
(* Goal: Rle (Rabs (FtoRradix p)) (FtoRradix q) *)
(* Goal: Closest b radix (Rplus (FtoRradix q) (FtoRradix p)) pq *)
(* Goal: not (@eq R (FtoRradix pq) (Rplus (FtoRradix q) (FtoRradix p))) *)
(* Goal: Rge (FtoRradix pq) (IZR Z0) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
rewrite <- (Rabs_right q); auto with real.
(* Goal: Closest b radix (Rplus (FtoRradix q) (FtoRradix p)) pq *)
(* Goal: not (@eq R (FtoRradix pq) (Rplus (FtoRradix q) (FtoRradix p))) *)
(* Goal: Rle (Rabs (FtoRradix q)) (Rabs (FtoRradix p)) *)
apply (ClosestCompatible b radix (p + q)%R (q + p)%R pq pq); auto; try ring.
(* Goal: not (@eq R (FtoRradix pq) (Rplus (FtoRradix q) (FtoRradix p))) *)
(* Goal: Rge (FtoRradix pq) (IZR Z0) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
rewrite Rplus_comm; auto with real.
apply Rle_ge; unfold FtoRradix in |- *;
 apply
  RleRoundedR0
   with
     (b := b)
     (precision := precision)
     (P := Closest b radix)
     (r := (p + q)%R); auto.
(* Goal: RoundedModeP b radix (Closest b radix) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
apply ClosestRoundedModeP with (precision := precision); auto.
case (Rle_or_lt 0 p); intros Rl3;
 [ idtac | cut (p <= 0)%R; [ intros Rl3' | apply Rlt_le; auto ] ];
 auto with real.
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
replace 0%R with (0 + 0)%R; auto with real.
(* Goal: Rle (IZR Z0) (Rplus (FtoRradix p) (FtoRradix q)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
apply Rplus_le_reg_l with (r := (- p)%R).
(* Goal: Rle (Rplus (Ropp (FtoRradix p)) (IZR Z0)) (Rplus (Ropp (FtoRradix p)) (Rplus (FtoRradix p) (FtoRradix q))) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
replace (- p + 0)%R with (- p)%R; [ idtac | ring ].
(* Goal: Rle (Ropp (FtoRradix p)) (Rplus (Ropp (FtoRradix p)) (Rplus (FtoRradix p) (FtoRradix q))) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
replace (- p + (p + q))%R with (FtoRradix q); [ idtac | ring ].
(* Goal: Rle (Ropp (FtoRradix p)) (FtoRradix q) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
rewrite <- (Faux.Rabsolu_left1 (FtoRradix p)); auto with real.
(* Goal: Rle (Rabs (FtoRradix p)) (FtoRradix q) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
rewrite <- (Rabs_right (FtoRradix q)); auto with real.
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
repeat rewrite Faux.Rabsolu_left1; auto with real.
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Ropp (FtoRradix q))) (Ropp (FtoRradix pq)) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
unfold FtoRradix in |- *; repeat rewrite <- (Fopp_correct 2%nat); auto.
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoR (Z.of_nat (S (S O))) (Fopp q))) (FtoR (Z.of_nat (S (S O))) (Fopp pq)) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
apply plusClosestLowerBoundAux1 with (q := Fopp p); auto.
unfold FtoRradix in |- *; repeat rewrite Fopp_correct; rewrite Rabs_Ropp;
 rewrite <- Faux.Rabsolu_left1; auto with real.
apply
 (ClosestCompatible b radix (- (p + q))%R (Fopp q + Fopp p)%R (
    Fopp pq) (Fopp pq)); auto.
(* Goal: Closest b radix (Ropp (Rplus (FtoRradix p) (FtoRradix q))) (Fopp pq) *)
(* Goal: @eq R (Ropp (Rplus (FtoRradix p) (FtoRradix q))) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p))) *)
(* Goal: Fbounded b (Fopp pq) *)
(* Goal: Fbounded b (Fopp q) *)
(* Goal: Fbounded b (Fopp p) *)
(* Goal: not (@eq R (FtoRradix (Fopp pq)) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p)))) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
apply ClosestOpp; auto.
(* Goal: @eq R (Ropp (Rplus (FtoRradix p) (FtoRradix q))) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p))) *)
(* Goal: Fbounded b (Fopp pq) *)
(* Goal: Fbounded b (Fopp q) *)
(* Goal: Fbounded b (Fopp p) *)
(* Goal: not (@eq R (FtoRradix (Fopp pq)) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p)))) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
unfold FtoRradix in |- *; repeat rewrite Fopp_correct; ring.
(* Goal: Fbounded b (Fopp p) *)
(* Goal: not (@eq R (FtoRradix (Fopp pq)) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p)))) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
apply oppBounded; auto.
(* Goal: Fbounded b (Fopp p) *)
(* Goal: not (@eq R (FtoRradix (Fopp pq)) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p)))) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
apply oppBounded; auto.
(* Goal: Fbounded b (Fopp p) *)
(* Goal: not (@eq R (FtoRradix (Fopp pq)) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p)))) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
apply oppBounded; auto.
(* Goal: not (@eq R (FtoRradix (Fopp pq)) (Rplus (FtoRradix (Fopp q)) (FtoRradix (Fopp p)))) *)
(* Goal: Rle (FtoRradix pq) (IZR Z0) *)
unfold FtoRradix in |- *; repeat rewrite Fopp_correct; Contradict H'2.
unfold FtoRradix in |- *; rewrite <- (Ropp_involutive (FtoR radix pq));
 rewrite H'2; ring.
unfold FtoRradix in |- *;
 apply
  RleRoundedLessR0
   with
     (b := b)
     (precision := precision)
     (P := Closest b radix)
     (r := (p + q)%R); auto.
(* Goal: RoundedModeP b radix (Closest b radix) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
apply ClosestRoundedModeP with (precision := precision); auto.
case (Rle_or_lt 0 p); intros Rl3;
 [ idtac | cut (p <= 0)%R; [ intros Rl3' | apply Rlt_le; auto ] ];
 auto with real.
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
apply Rplus_le_reg_l with (r := (- q)%R).
(* Goal: Rle (Rplus (Ropp (FtoRradix q)) (Rplus (FtoRradix p) (FtoRradix q))) (Rplus (Ropp (FtoRradix q)) (IZR Z0)) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
replace (- q + 0)%R with (- q)%R; [ idtac | ring ].
(* Goal: Rle (Rplus (Ropp (FtoRradix q)) (Rplus (FtoRradix p) (FtoRradix q))) (Ropp (FtoRradix q)) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
replace (- q + (p + q))%R with (FtoRradix p); [ idtac | ring ].
(* Goal: Rle (FtoRradix p) (Ropp (FtoRradix q)) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
rewrite <- (Rabs_right (FtoRradix p)); auto with real.
(* Goal: Rle (Rabs (FtoRradix p)) (Ropp (FtoRradix q)) *)
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
rewrite <- (Rabs_left (FtoRradix q)); auto with real.
(* Goal: Rle (Rplus (FtoRradix p) (FtoRradix q)) (IZR Z0) *)
replace 0%R with (0 + 0)%R; auto with real.
Qed.
 
Theorem plusClosestLowerBound :
 forall p q pq : float,
 Closest b radix (p + q) pq ->
 Fbounded b p ->
 Fbounded b q ->
 pq <> (p + q)%R :>R -> (/ radix * Rmax (Rabs p) (Rabs q) <= Rabs pq)%R.
(* Goal: forall (p q pq : float) (_ : Closest b radix (Rplus (FtoRradix p) (FtoRradix q)) pq) (_ : Fbounded b p) (_ : Fbounded b q) (_ : not (@eq R (FtoRradix pq) (Rplus (FtoRradix p) (FtoRradix q)))), Rle (Rmult (Rinv (IZR radix)) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q)))) (Rabs (FtoRradix pq)) *)
intros p q pq H' H'0 H'1 H'2.
cut (Fbounded b pq);
 [ intros Fb0
 | apply
    RoundedModeBounded
     with (radix := radix) (P := Closest b radix) (r := (p + q)%R); 
    auto; apply ClosestRoundedModeP with (precision := precision) ]; 
 auto.
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rmax (Rabs (FtoRradix p)) (Rabs (FtoRradix q)))) (Rabs (FtoRradix pq)) *)
unfold Rmax in |- *.
(* Goal: Rle (Rmult (Rinv (IZR radix)) (if Rle_dec (Rabs (FtoRradix p)) (Rabs (FtoRradix q)) then Rabs (FtoRradix q) else Rabs (FtoRradix p))) (Rabs (FtoRradix pq)) *)
case (Rle_dec (Rabs p) (Rabs q)); intros Rl1.
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix q))) (Rabs (FtoRradix pq)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix p))) (Rabs (FtoRradix pq)) *)
apply plusClosestLowerBoundAux2 with (p := p); auto.
(* Goal: Rle (Rmult (Rinv (IZR radix)) (Rabs (FtoRradix p))) (Rabs (FtoRradix pq)) *)
apply plusClosestLowerBoundAux2 with (p := q); auto.
(* Goal: Closest b radix (Rplus (FtoRradix q) (FtoRradix p)) pq *)
(* Goal: not (@eq R (FtoRradix pq) (Rplus (FtoRradix q) (FtoRradix p))) *)
(* Goal: Rle (Rabs (FtoRradix q)) (Rabs (FtoRradix p)) *)
apply (ClosestCompatible b radix (p + q)%R (q + p)%R pq pq); auto; try ring.
(* Goal: not (@eq R (FtoRradix pq) (Rplus (FtoRradix q) (FtoRradix p))) *)
(* Goal: Rle (Rabs (FtoRradix q)) (Rabs (FtoRradix p)) *)
rewrite Rplus_comm; auto.
case (Rle_or_lt (Rabs q) (Rabs p)); auto; intros H'3; Contradict Rl1;
(* Goal: Rle (FtoR radix q) (IZR Z0) *)
(* Goal: @eq float (Fminus radix p (Fopp q)) (Fplus radix p q) *)
(* Goal: Closest b radix (FtoR radix (Fplus radix p q)) pq *)
(* Goal: not (@eq R (INR (S (S O))) (IZR Z0)) *)
(* Goal: Rle (Rmult (Rinv (IZR radix)) (FtoRradix p)) (FtoRradix pq) *)
 apply Rlt_le; auto.
Qed.
End F2.