proposition: Lemma ClosestClosest: forall b0:Fbound, forall n:nat, forall z:R, forall f1 f2:float, Zpos (vNum b0)=(Zpower_nat radix n) -> (1 < n) -> (Closest b0 radix z f1) -> (Closest b0 radix z f2) -> Fnormal radix b0 f2 -> (Fexp f1 <= Fexp f2 -2)%Z -> False.
proof: Proof. intros. cut (FtoRradix (Fabs f1) < Fabs f2)%R;[intros|idtac]. absurd (FtoRradix (Fabs f2) = (FNSucc b0 radix n (Fabs f1)))%R. cut (FNSucc b0 radix n (Fabs f1) < (Fabs f2))%R; auto with real. unfold FtoRradix; apply FcanonicPosFexpRlt with b0 n; auto with zarith. apply Rle_trans with (FtoRradix (Fabs f1)). unfold FtoRradix; rewrite Fabs_correct; auto with real. apply Rabs_pos. unfold FtoRradix; apply Rlt_le; apply FNSuccLt; auto with zarith. rewrite Fabs_correct; auto with real. apply Rabs_pos. apply FNSuccCanonic; auto with zarith. apply absFBounded; elim H1; auto. apply FcanonicFabs; auto; left; auto. cut (Fexp (Fnormalize radix b0 n (Fabs f1)) <= Fexp (Fabs f2) - 2)%Z;[intros|idtac]. unfold FNSucc, FSucc. case (Z_eq_bool (Fnum (Fnormalize radix b0 n (Fabs f1)))); auto with zarith. apply Z.le_lt_trans with (Z.succ (Fexp (Fnormalize radix b0 n (Fabs f1)))); auto with zarith. case (Z_eq_bool (Fnum (Fnormalize radix b0 n (Fabs f1))) (- nNormMin radix n)). case (Z_eq_bool (Fexp (Fnormalize radix b0 n (Fabs f1))) (- dExp b0)). apply Z.le_lt_trans with (Fexp (Fnormalize radix b0 n (Fabs f1))); auto with zarith. apply Z.le_lt_trans with (Z.pred (Fexp (Fnormalize radix b0 n (Fabs f1)))); auto with zarith. apply Z.le_lt_trans with (Fexp (Fnormalize radix b0 n (Fabs f1))); auto with zarith. apply Z.le_trans with (Fexp (Fabs f1));[idtac|unfold Fabs; simpl; auto with zarith]. apply FcanonicLeastExp with radix b0 n; auto with zarith. rewrite FnormalizeCorrect; auto with real. apply absFBounded; elim H1; auto. apply FnormalizeCanonic; auto with zarith. apply absFBounded; elim H1; auto. cut (isMin b0 radix (Rabs z) (Fabs f1));[intros K|idtac]. cut (isMax b0 radix (Rabs z) (Fabs f2));[intros K'|idtac]. apply (MaxUniqueP b0 radix (Rabs z)); auto. apply MinMax; auto with zarith. case (Req_dec (Rabs z) (Fabs f1)); auto with real. intros V; absurd (FtoRradix (Fabs f1) = Fabs f2)%R; auto with real. unfold FtoRradix; apply RoundedModeProjectorIdemEq with b0 n (isMax b0 radix); auto with real zarith. apply MaxRoundedModeP with n; auto with zarith. apply absFBounded; elim H1; auto. fold FtoRradix; rewrite <- V; auto. case (ClosestMinOrMax b0 radix (Rabs z) (Fabs f2)); auto. apply ClosestFabs with n; auto. intros H6. absurd (FtoRradix (Fabs f1)=Fabs f2); auto with real. apply (MinUniqueP b0 radix (Rabs z)); auto. case (ClosestMinOrMax b0 radix (Rabs z) (Fabs f1)); auto. apply ClosestFabs with n; auto. intros H6. case (ClosestMinOrMax b0 radix (Rabs z) (Fabs f2)); auto. apply ClosestFabs with n; auto. intros H7; elim H6; elim H7; intros. elim H9; elim H11; intros. absurd ( (Fabs f2) <= (Fabs f1))%R; auto with real. apply Rle_trans with (Rabs z); auto with real. intros H7; absurd (FtoRradix (Fabs f1)=Fabs f2); auto with real. apply (MaxUniqueP b0 radix (Rabs z)); auto. unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b0 n (Fabs f1); auto. apply FcanonicPosFexpRlt with b0 n; auto with zarith. rewrite FnormalizeCorrect; auto; rewrite Fabs_correct; auto with real. apply Rabs_pos. rewrite Fabs_correct; auto with real. apply Rabs_pos. apply FnormalizeCanonic; auto with zarith. apply absFBounded; elim H1; auto. apply FcanonicFabs; auto; left; auto. apply Z.le_lt_trans with (Fexp (Fabs f1)); [idtac|unfold Fabs; simpl; auto with zarith]. apply FcanonicLeastExp with radix b0 n; auto with zarith. rewrite FnormalizeCorrect; auto with real. apply absFBounded; elim H1; auto. apply FnormalizeCanonic; auto with zarith. apply absFBounded; elim H1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz