proposition: Theorem MKnuth5 : forall p q : float, (0 < p)%R -> (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. cut (Iminus (Iplus p q) (Iminus (Iplus p q) p) = (Iplus p q - Iminus (Iplus p q) p)%R :>R); [ intros Eq1 | idtac ]. apply MKnuth1; auto. cut (Iminus (Iplus p q) p <= Iplus p q)%R; [ intros Rle1 | idtac ]. cut (Iplus p q <= radix * q)%R; [ intros Rle2 | idtac ]. case (Rle_or_lt q (Iminus (Iplus p q) p)); intros Rle3. 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 (2 := Rle3); 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 Rlt_le; apply Rlt_trans with (1 := H'); auto. apply Rle_trans with (1 := Rle1); auto. apply sym_eq; apply (Fminus_correct radix); auto. apply sym_eq; apply (Fminus_correct radix); auto. case (ExactMinusInterval b radix precision) with (P := Closest b radix) (p := Iminus (Iplus p q) p) (q := Iplus p q) (r := q); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply (RleRoundedR0 b radix precision) 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 := FtoRradix p); auto. replace (p + 0)%R with (FtoRradix p); [ idtac | ring ]. replace (p + (Iplus p q - p))%R with (FtoRradix (Iplus p q)); [ idtac | ring ]. cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ]. apply (Cp p (p + q)%R); auto. apply Rplus_lt_reg_l with (r := (- p)%R); auto. replace (- p + p)%R with 0%R; [ idtac | ring ]. replace (- p + (p + q))%R with (FtoRradix q); [ apply Rlt_trans with (1 := H'); auto | ring ]. apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply ClosestMonotone; auto. exists (Iminus (Iplus p q) (Iminus (Iplus p q) p)); split; auto. apply Rlt_le; auto. cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ]. apply (Cp q (p + q)%R); auto. apply Rplus_lt_reg_l with (r := (- q)%R); auto. replace (- q + q)%R with 0%R; [ idtac | ring ]. replace (- q + (p + q))%R with (FtoRradix p); [ auto | ring ]. apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply ClosestMonotone; auto. intros x H'4; elim H'4; intros H'5 H'6; clear H'4. apply IminusCorrectEq with (pq := x); auto. apply (RoundedModeMult b radix) with (P := Closest b radix) (r := (p + q)%R); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply Rplus_le_reg_l with (r := (- q)%R); auto. replace (- q + (p + q))%R with (FtoRradix p); [ idtac | ring ]. replace (- FtoRradix q + radix * FtoR radix q)%R with (FtoRradix q); [ apply Rlt_le; auto | unfold FtoRradix in |- *; simpl in |- *; unfold radix; ring ]. cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ]. apply (Cp (Iplus p q - p)%R (Iplus p q)); auto. apply Rplus_lt_reg_l with (r := (- Iplus p q)%R); auto. replace (- Iplus p q + (Iplus p q - p))%R with (- p)%R; [ idtac | ring ]. replace (- Iplus p q + Iplus p 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. case (minusRoundRep b radix precision) with (P := Closest b radix) (p := p) (q := Iplus p q) (qmp := Iminus (Iplus p q) p); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply Rlt_le; auto. cut (MonotoneP radix (Closest b radix)); [ intros Cp | idtac ]. apply (Cp (FtoRradix p) (p + q)%R); auto. apply Rplus_lt_reg_l with (r := (- p)%R); auto. replace (- p + p)%R with 0%R; [ idtac | ring ]. replace (- p + (p + q))%R with (FtoRradix q); [ apply Rlt_trans with (1 := H'); auto | ring ]. apply (RoundedModeProjectorIdem b radix (Closest b radix)); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply ClosestMonotone; auto. intros x H'4; elim H'4; intros H'5 H'6; clear H'4; auto with zarith. apply IminusCorrectEq with (pq := x); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz