proposition: Theorem minusRoundRep : forall P, RoundedModeP b radix P -> forall p q qmp qmmp : float, (0 <= p)%R -> (p <= q)%R -> P (q - p)%R qmp -> Fbounded b p -> Fbounded b q -> exists r : float, Fbounded b r /\ r = (q - qmp)%R :>R.
proof: Proof. intros P H' p q qmp H'0 H'1 H'2 H'3 H'4 H'5. case (Rle_or_lt (/ 2 * q) p); intros Rle1. exists p; split; auto. replace (FtoRradix qmp) with (FtoRradix (Fminus radix q p)). rewrite (Fminus_correct radix); auto with arith; unfold FtoRradix in |- *; ring. apply (RoundedModeProjectorIdemEq b radix precision) with (P := P); auto. rewrite <- Fopp_Fminus. apply oppBounded; auto. apply Sterbenz; auto. apply Rle_trans with (FtoRradix q); auto with real. apply Rledouble; auto. apply Rle_trans with (FtoRradix p); auto with real. cut (CompatibleP b radix P); [ intros Cp | apply RoundedModeP_inv2 with (1 := H'); auto ]. apply (Cp (q - p)%R (Fminus radix q p) qmp); auto. rewrite (Fminus_correct radix); auto with arith. apply RoundedModeBounded with (radix := radix) (P := P) (r := (q - p)%R); auto; auto. exists (Fminus radix q qmp); split. rewrite <- Fopp_Fminus. apply oppBounded; auto. apply Sterbenz; auto. apply RoundedModeBounded with (radix := radix) (P := P) (r := (q - p)%R); auto; auto. case MaxEx with (r := (/ 2 * FtoR radix q)%R) (3 := pGivesBound); auto with zarith. intros max H'6. apply Rle_trans with (FtoRradix max); [ apply isMax_inv1 with (1 := H'6); auto | idtac ]. apply (RleBoundRoundl b radix precision) with (P := P) (r := (q - p)%R); auto; fold FtoRradix in |- *. case H'6; auto. case MinEx with (r := (/ 2 * FtoR radix q)%R) (3 := pGivesBound); auto with zarith. intros min H'7. replace (FtoRradix max) with (q - min)%R. apply Rplus_le_reg_l with (r := (- q)%R). cut (forall p q : R, (- p + (p - q))%R = (- q)%R); [ intros tmp; repeat rewrite tmp; clear tmp | intros; ring ]. apply Ropp_le_contravar. case H'7. intros H'8 H'9; elim H'9; intros H'10 H'11; apply H'11; clear H'9; auto. apply Rlt_le; auto. unfold FtoRradix in |- *; rewrite (div2IsBetween b radix precision) with (5 := H'7) (6 := H'6); auto. ring. apply Rle_trans with (FtoRradix q); auto with real. apply (RleBoundRoundr b radix precision) with (P := P) (r := (q - p)%R); auto; fold FtoRradix in |- *. apply Rplus_le_reg_l with (r := (- q)%R). cut (forall p q : R, (- p + (p - q))%R = (- q)%R); [ intros tmp; repeat rewrite tmp; clear tmp | intros; ring ]. replace (- q + q)%R with (-0)%R; [ auto with real | ring ]. apply Rle_trans with (FtoRradix q); auto with real. apply Rledouble; auto. apply Rle_trans with (FtoRradix p); auto with real. apply (Fminus_correct radix); auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz