proposition: Theorem RND_EvenClosest_correct : forall r : R, EvenClosest b radix p r (RND_EvenClosest r).
proof: Proof. intros r. cut (RND_Min r <= r)%R; [ intros V1 | idtac ]. 2: generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. cut (r <= RND_Max r)%R; [ intros V2 | idtac ]. 2: generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. cut (forall v w : R, (v <= w)%R -> (0 <= w - v)%R); [ intros V3 | idtac ]. 2: intros v w H; apply Rplus_le_reg_l with v; ring_simplify; auto with real. cut (forall v w : R, (v <= w)%R -> (v - w <= 0)%R); [ intros V4 | idtac ]. 2: intros v w H; apply Rplus_le_reg_l with w; ring_simplify; auto with real. unfold RND_EvenClosest in |- *; case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r))); intros H1. case (Rle_lt_or_eq_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) H1); intros H2. split. split. apply FcanonicBound with radix; apply RND_Max_canonic. intros f H3; fold FtoRradix in |- *. rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ]. rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ]. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. case (Rle_or_lt f r); intros H4. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. apply Rle_trans with (1 := H1); apply Ropp_le_contravar; unfold Rminus in |- *; apply Rplus_le_compat_r. generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. unfold Rminus in |- *; apply Rplus_le_compat_r. generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. right; intros q H3. generalize (ClosestMinOrMax b radix); unfold MinOrMaxP in |- *; intros T. case (T r q); auto; intros H4; clear T. contradict H2; apply Rle_not_lt. replace (FtoRradix (RND_Min r)) with (FtoRradix q). elim H3; intros T1 T2; unfold FtoRradix in |- *; apply T2. apply FcanonicBound with radix; apply RND_Max_canonic. generalize (MinUniqueP b radix); unfold UniqueP in |- *; intros T; apply T with r; auto. apply RND_Min_correct. generalize (MaxUniqueP b radix); unfold UniqueP in |- *; intros T; apply T with r; auto. apply RND_Max_correct. case (OddEvenDec (Fnum (RND_Min r))); intros H3. split. split. apply FcanonicBound with radix; apply RND_Max_canonic. intros f H4; fold FtoRradix in |- *. rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ]. rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ]. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. case (Rle_or_lt f r); intros H5. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. apply Rle_trans with (1 := H1); apply Ropp_le_contravar; unfold Rminus in |- *; apply Rplus_le_compat_r. generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. unfold Rminus in |- *; apply Rplus_le_compat_r. generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. case (Req_EM_T (RND_Max r) (RND_Min r)); intros W. right; intros q H4. generalize (ClosestMinOrMax b radix); unfold MinOrMaxP in |- *; intros T. case (T r q); auto; intros H5; clear T. fold FtoRradix in |- *; rewrite W; generalize (MinUniqueP b radix); unfold UniqueP in |- *; intros T; apply T with r; auto. apply RND_Min_correct. generalize (MaxUniqueP b radix); unfold UniqueP in |- *; intros T; apply T with r; auto. apply RND_Max_correct. left; unfold FNeven in |- *. rewrite FcanonicFnormalizeEq; auto with zarith; [ idtac | apply RND_Max_canonic ]. replace (RND_Max r) with (FSucc b radix p (RND_Min r)). apply FoddSuc; auto. unfold RND_Max, RND_Min in |- *; case (Rle_dec 0 r); intros W1. unfold RND_Max_Pos in |- *. case (Req_EM_T r (RND_Min_Pos r)); intros W2; auto. contradict W. pattern r at 1 in |- *; rewrite W2. apply sym_eq; unfold FtoRradix in |- *; apply RoundedModeProjectorIdemEq with b p (isMax b radix); auto. apply MaxRoundedModeP with p; auto. apply FcanonicBound with radix; apply RND_Min_canonic. replace (FtoR radix (RND_Min r)) with (FtoR radix (RND_Min_Pos r)); [ fold FtoRradix in |- *; rewrite <- W2; apply RND_Max_correct | idtac ]. fold FtoRradix in |- *; unfold RND_Min in |- *; auto with real. case (Rle_dec 0 r); auto with real; intros W3; contradict W1; auto with real. unfold RND_Max_Pos in |- *. case (Req_EM_T (- r) (RND_Min_Pos (- r))); intros W2; auto. contradict W. cut (r = FtoRradix (Fopp (RND_Min_Pos (- r)))); [ intros W3 | idtac ]. pattern r at 1 in |- *; rewrite W3. apply sym_eq; unfold FtoRradix in |- *; apply RoundedModeProjectorIdemEq with b p (isMax b radix); auto. apply MaxRoundedModeP with p; auto. apply FcanonicBound with radix; apply RND_Min_canonic. replace (FtoR radix (RND_Min r)) with (- FtoR radix (RND_Min_Pos (- r)))%R; [ fold FtoRradix in |- *; rewrite <- W3 | idtac ]. rewrite <- W2; rewrite Ropp_involutive; apply RND_Max_correct. fold FtoRradix in |- *; unfold RND_Min in |- *; auto with real. case (Rle_dec 0 r). intros W4; contradict W1; auto with real. intros W4; unfold RND_Max_Pos in |- *; case (Req_EM_T (- r) (RND_Min_Pos (- r))); intros W5. unfold FtoRradix in |- *; rewrite Fopp_correct; ring. contradict W2; auto with real. unfold FtoRradix in |- *; rewrite Fopp_correct; fold FtoRradix in |- *; rewrite <- W2; ring. pattern (RND_Min_Pos (- r)) at 1 in |- *; rewrite <- (Fopp_Fopp (RND_Min_Pos (- r))). rewrite <- FPredFopFSucc; auto with zarith. apply FSucPred; auto with zarith. apply FcanonicFopp; apply RND_Min_Pos_canonic; auto with real. rewrite <- Ropp_0; apply Ropp_le_contravar; auto with real. split. split. apply FcanonicBound with radix; apply RND_Min_canonic. intros f H4; fold FtoRradix in |- *. rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ]. rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ]. case (Rle_or_lt f r); intros H5. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. apply Ropp_le_contravar; unfold Rminus in |- *; apply Rplus_le_compat_r. generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. rewrite <- H2. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. unfold Rminus in |- *; apply Rplus_le_compat_r. generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. left; unfold FNeven in |- *. rewrite FcanonicFnormalizeEq; auto with zarith; apply RND_Min_canonic. cut (Rabs (RND_Min r - r) < Rabs (RND_Max r - r))%R; auto with real; intros H'. cut (Rabs (RND_Min r - r) < Rabs (RND_Max r - r))%R; auto with real; intros H''. rewrite Rabs_left1 in H'; [ idtac | apply V4; auto with real ]. rewrite Rabs_right in H'; [ idtac | apply Rle_ge; apply V3; auto with real ]. split. split. apply FcanonicBound with radix; apply RND_Min_canonic. intros f W1. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. case (Rle_or_lt f r); intros H2. rewrite Rabs_left1; [ idtac | apply V4; auto with real ]. apply Ropp_le_contravar; unfold Rminus in |- *; apply Rplus_le_compat_r. generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ]. apply Rle_trans with (RND_Max r - r)%R; auto with real; unfold Rminus in |- *; apply Rplus_le_compat_r. generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2; intros T3 T4; auto with real. right; intros q H3. generalize (ClosestMinOrMax b radix); unfold MinOrMaxP in |- *; intros T. case (T r q); auto; intros H4; clear T. generalize (MinUniqueP b radix); unfold UniqueP in |- *; intros T; apply T with r; auto. apply RND_Min_correct. contradict H''; apply Rle_not_lt. replace (FtoRradix (RND_Max r)) with (FtoRradix q). elim H3; intros T1 T2; unfold FtoRradix in |- *; apply T2. apply FcanonicBound with radix; apply RND_Min_canonic. generalize (MaxUniqueP b radix); unfold UniqueP in |- *; intros T; apply T with r; auto. apply RND_Max_correct. Qed.
imports: Reals ZArith List PeanoNat Psatz