proposition: Theorem ClosestFabs : forall (p : float) (r : R), Closest b radix r p -> Closest b radix (Rabs r) (Fabs p).
proof: Proof. intros p r H'; case (Rle_or_lt 0 r); intros Rl0. rewrite Rabs_right; auto with real. replace (Fabs p) with p; auto. unfold Fabs in |- *; apply floatEq; simpl in |- *; auto. cut (0 <= Fnum p)%Z. case (Fnum p); simpl in |- *; auto; intros p' H0; contradict H0; apply Zlt_not_le; red in |- *; simpl in |- *; auto with zarith. apply LeR0Fnum with (radix := radix); auto. apply RleRoundedR0 with (b := b) (precision := precision) (P := Closest b radix) (r := r); auto. apply ClosestRoundedModeP with (precision := precision); auto with real. rewrite Rabs_left1; auto. replace (Fabs p) with (Fopp p). apply ClosestOpp; auto. unfold Fabs in |- *; apply floatEq; simpl in |- *; auto. cut (Fnum p <= 0)%Z. case (Fnum p); simpl in |- *; auto; intros p' H0; contradict H0; apply Zlt_not_le; red in |- *; simpl in |- *; auto with zarith. apply R0LeFnum with (radix := radix); auto. apply RleRoundedLessR0 with (b := b) (precision := precision) (P := Closest b radix) (r := r); auto. apply ClosestRoundedModeP with (precision := precision); auto. apply Rlt_le; auto. apply Rlt_le; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz