proposition: Theorem MKnuth1 : forall p q : float, Fbounded b p -> Fbounded b q -> Iminus q (Iminus (Iplus p q) p) = (q - Iminus (Iplus p q) p)%R :>R -> Iminus (Iplus p q) (Iminus (Iplus p q) p) = (Iplus p q - Iminus (Iplus p q) p)%R :>R -> 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 p (Iminus (Iplus p q) (Iminus (Iplus p q) p)) = (p - Iminus (Iplus p q) (Iminus (Iplus p q) p))%R :>R); [ intros H'3 | idtac ]. case (errorBoundedPlus b radix precision) with (p := p) (q := q) (pq := Iplus p q); auto. intros pq H'4; elim H'4; intros H'5 H'6; elim H'6; intros H'7 H'8; clear H'6 H'4. apply IplusCorrectEq with (pq := pq); auto. repeat rewrite H'3; repeat rewrite H'2; repeat rewrite H'1. unfold FtoRradix in |- *; rewrite H'5. ring. rewrite H'2. case (errorBoundedPlus b radix precision) with (p := Iplus p q) (q := Fopp p) (pq := Iminus (Iplus p q) p); auto with zarith. apply oppBounded; auto. apply (ClosestCompatible b radix (Iplus p q - p)%R (Iplus p q + Fopp p)%R (Iminus (Iplus p q) p)); auto. rewrite (Fopp_correct radix); auto. intros pq H'3; elim H'3; intros H'4 H'5; elim H'5; intros H'6 H'7; clear H'5 H'3. rewrite (IminusPlus p); apply IplusCorrectEq with (pq := Fopp pq); auto with zarith. apply oppBounded; auto. apply oppBounded; auto. unfold FtoRradix in |- *; rewrite (Fopp_correct radix); auto; rewrite H'4; rewrite (Fopp_correct radix); auto; ring; ring. unfold FtoRradix in |- *; repeat rewrite (Fopp_correct radix); auto; rewrite H'4; rewrite (Fopp_correct radix); auto. unfold FtoRradix in H'2; rewrite H'2; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz