proposition: Theorem MKnuth4 : forall p q : float, (0 < - p)%R -> (0 < q)%R -> (radix * - p < q)%R -> Fbounded b p -> Fbounded b q -> Iplus (Iminus p (Iminus (Iplus p q) (Iminus (Iplus p q) p))) (Iminus q (Iminus (Iplus p q) p)) = (p + q - Iplus p q)%R :>R.
proof: Proof. intros p q H' H'0 H'1 H'2 H'3. cut (/ radix * q <= Iplus p q)%R; [ intros Rle1 | idtac ]. cut (Iplus p q <= Iminus (Iplus p q) p)%R; [ intros Rle2 | idtac ]. cut (Iminus (Iplus p q) p <= radix * Iplus p q)%R; [ intros Rle3 | idtac ]. cut (radix * Iplus p q <= radix * q)%R; [ intros Rle4 | idtac ]. apply MKnuth1; auto with zarith. apply IminusCorrectEq with (pq := Fminus radix q (Iminus (Iplus p q) p)); auto with zarith. rewrite <- (Fopp_Fopp (Fminus radix q (Iminus (Iplus p q) p))). apply oppBounded. rewrite Fopp_Fminus. apply Sterbenz; auto. apply Rle_trans with (1 := Rle1); auto. apply Rle_trans with (1 := Rle3); auto. apply sym_eq; apply (Fminus_correct radix); auto. apply sym_eq; apply (Fminus_correct radix); auto. apply IminusCorrectEq with (pq := Fminus radix (Iplus p q) (Iminus (Iplus p q) p)); auto. rewrite <- (Fopp_Fopp (Fminus radix (Iplus p q) (Iminus (Iplus p q) p))). apply oppBounded. rewrite Fopp_Fminus. apply Sterbenz; auto. apply Rle_trans with (2 := Rle2); auto. apply Rmult_le_reg_l with (r := IZR radix); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real arith; rewrite Rmult_1_l. apply Rledouble. apply Rle_trans with (2 := Rle1). apply Rmult_le_reg_l with (r := IZR radix); auto with real. rewrite <- Rmult_assoc; rewrite Rinv_r; auto with real zarith; rewrite Rmult_1_l; rewrite Rmult_0_r; apply Rlt_le; auto. apply sym_eq; apply (Fminus_correct radix); auto. apply sym_eq; apply (Fminus_correct radix); auto. apply Rmult_le_reg_l with (r := (/ radix)%R); auto with real. repeat rewrite <- Rmult_assoc; repeat rewrite Rinv_l; auto with real zarith; repeat rewrite Rmult_1_l; auto with real. cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ]. apply (Cp (p + q)%R q); auto. apply Rplus_lt_reg_l with (r := (- q)%R); auto. replace (- q + (p + q))%R with (- - p)%R; [ idtac | ring ]. replace (- q + q)%R with (-0)%R; [ auto with real | ring ]. apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply ClosestMonotone; auto. apply (RoundedModeMult b radix) with (P := Closest b radix) (r := (Iplus p q - p)%R); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply Rplus_le_reg_l with (r := (- Iplus p q)%R); auto. replace (- Iplus p q + (Iplus p q - p))%R with (- p)%R; [ idtac | ring ]. replace (- FtoRradix (Iplus p q) + radix * FtoR radix (Iplus p q))%R with (FtoRradix (Iplus p q)); [ idtac | unfold FtoRradix in |- *; simpl in |- *; unfold radix; ring; ring ]. rewrite <- (Fopp_correct radix); auto. cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ]. apply (Cp (Fopp p) (p + q)%R); auto. rewrite (Fopp_correct radix); auto. apply Rplus_lt_reg_l with (r := (- p)%R); auto. replace (- p + - FtoR radix p)%R with (radix * - p)%R; [ idtac | simpl in |- *; fold FtoRradix; unfold radix; ring ]. replace (- p + (p + q))%R with (FtoRradix q); [ auto | simpl in |- *; ring ]. apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply oppBounded; auto. apply ClosestMonotone; auto. cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ]. apply (Cp (Iplus p q) (Iplus p q - p)%R); auto. apply Rplus_lt_reg_l with (r := (- Iplus p q)%R); auto. replace (- Iplus p q + Iplus p q)%R with 0%R; [ auto | simpl in |- *; ring ]. replace (- Iplus p q + (Iplus p q - p))%R with (- p)%R; [ auto | simpl in |- *; ring ]. apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply ClosestMonotone; auto. apply (FmultRadixInv b radix precision) with (y := (p + q)%R); auto. apply Rmult_lt_reg_l with (r := IZR radix); auto with real. repeat rewrite <- Rmult_assoc; repeat rewrite Rinv_r; auto with real arith; repeat rewrite Rmult_1_l; auto. apply Rplus_lt_reg_l with (r := (- q)%R); auto. apply Rplus_lt_reg_l with (r := (radix * - p)%R); auto. replace (radix * - p + (- q + FtoR radix q))%R with (radix * - p)%R; [ auto | unfold FtoRradix in |- *; simpl in |- *; ring ]. replace (radix * - p + (- q + radix * (p + q)))%R with (FtoRradix q); [ auto | simpl in |- *; unfold radix; ring ]. Qed.
imports: Reals ZArith List PeanoNat Psatz