proposition: Theorem discri15: (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. assert (forall r:R, forall f:float, EvenClosest bo radix precision r f -> Fbounded bo f). intros r f T; elim T; intros T1 T2; elim T1; auto with zarith. assert (forall f:float, (Fbounded bo f) -> (powerRZ radix (- dExp bo + precision - 1) <= Rabs f)%R -> Fnormal radix bo (Fnormalize radix bo precision f)). intros. assert (Fcanonic radix bo (Fnormalize radix bo precision f)). apply FnormalizeCanonic; auto with zarith. case H2; auto; intros. absurd (FtoR radix (Fabs f) < FtoR radix (firstNormalPos radix bo precision))%R. apply Rle_not_lt; rewrite Fabs_correct; auto. fold FtoRradix; apply Rle_trans with (2:=H1). unfold firstNormalPos, FtoRradix, FtoR, nNormMin; simpl. rewrite Zpower_nat_Z_powerRZ; rewrite inj_pred; auto with zarith; unfold Z.pred. unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith. right; simpl; ring. apply Rle_lt_trans with (FtoR radix (Fabs (Fnormalize radix bo precision f))). repeat rewrite Fabs_correct; auto. rewrite FnormalizeCorrect; auto with zarith real. apply FsubnormalLtFirstNormalPos; auto with zarith. apply FsubnormFabs; auto. rewrite Fabs_correct; auto with zarith real. apply Rabs_pos. unfold delta; unfold FtoRradix. assert (Fbounded bo d). case (Rle_or_lt v u); intros. elim FRoundd; auto; intros T T'; elim T; auto with zarith. elim SRoundd; auto; intros T T'; elim T; auto with zarith. apply Rle_trans with (2 * Fulp bo radix precision (Fnormalize radix bo precision d))%R. 2: unfold Fulp; rewrite FcanonicFnormalizeEq with radix bo precision (Fnormalize radix bo precision d); auto with zarith real. 2: apply FnormalizeCanonic; auto with zarith. rewrite <- FnormalizeCorrect with radix bo precision d; auto with zarith. assert (Fnormal radix bo (Fnormalize radix bo precision d)). apply H0; auto. apply Rle_trans with (2:=U4); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; try unfold radix; auto with zarith. assert (Fnormal radix bo (Fnormalize radix bo precision t)). apply H0. apply H with (p-q)%R; auto. apply Rle_trans with (2:=U7); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; try unfold radix; auto with zarith. apply discri14 with (Fnormalize radix bo precision p) (Fnormalize radix bo precision q) (Fnormalize radix bo precision t) dp dq (Fnormalize radix bo precision s) (Fnormalize radix bo precision u) (Fnormalize radix bo precision v); auto. apply FnormalizeBounded; auto with zarith; apply H with (b*b)%R; auto. apply FnormalizeBounded; auto with zarith; apply H with (a*c)%R; auto. apply FnormalizeBounded; auto with zarith. apply FnormalizeBounded; auto with zarith; apply H with (p-q)%R; auto. repeat rewrite FnormalizeCorrect; auto with real zarith; intros. apply FnormalizeBounded; auto with zarith; apply H with (dp-dq)%R; auto. repeat rewrite FnormalizeCorrect; auto with real zarith. repeat rewrite FnormalizeCorrect; auto with real zarith. apply FnormalizeBounded; auto with zarith; apply H with (3*Rabs t)%R; auto. apply FnormalizeBounded; auto with zarith; apply H with (p+q)%R; auto. intros; apply FnormalizeCanonic; auto with zarith. apply H with (dp-dq)%R; auto. apply SRounds. rewrite FnormalizeCorrect in H4; auto with zarith real. rewrite FnormalizeCorrect in H4; auto with zarith real. assert (- dExp bo + precision < Fexp (Fnormalize radix bo precision d) + precision)%Z; auto with zarith. apply Zlt_powerRZ with radix; auto with real zarith. apply Rle_lt_trans with (1:=U4). unfold FtoRradix; rewrite <- FnormalizeCorrect with radix bo precision d; auto with zarith. rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl. rewrite Rmult_comm; rewrite powerRZ_add; auto with real zarith. apply Rmult_lt_compat_l; auto with real zarith. apply powerRZ_lt; try apply IZR_lt; auto with zarith. apply Rlt_le_trans with (Zpos (vNum bo)); auto with zarith real. apply IZR_lt; apply H2. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. assert (- dExp bo + precision < Fexp (Fnormalize radix bo precision t) + precision)%Z; auto with zarith. apply Zlt_powerRZ with radix; auto with real zarith. apply Rle_lt_trans with (1:=U7). unfold FtoRradix; rewrite <- FnormalizeCorrect with radix bo precision t; auto with zarith. rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl. rewrite Rmult_comm; rewrite powerRZ_add; auto with real zarith. apply Rmult_lt_compat_l; auto with real zarith. apply powerRZ_lt; try apply IZR_lt; auto with zarith. apply Rlt_le_trans with (Zpos (vNum bo)); auto with zarith real. apply IZR_lt; apply H3. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. assert (Fbounded bo (Fnormalize radix bo precision t)); auto with zarith real. elim H3; auto. apply H0; auto. apply H with (b*b)%R; auto. cut (exists f:float, Fbounded bo f /\ (FtoRradix f=(powerRZ radix (- dExp bo + precision - 1)))%R). intros T; elim T; intros f T'; elim T'; intros; clear T T'. rewrite <- H6; unfold FtoRradix. apply RoundAbsMonotonel with bo precision (Closest bo radix) (b*b)%R; auto with zarith real. apply ClosestRoundedModeP with precision; auto with zarith. elim Roundp; auto. fold FtoRradix; rewrite H6; auto. apply Rle_trans with (2:=U1); auto with zarith real. apply Rle_powerRZ; try apply IZR_le; unfold radix; auto with zarith. exists (Float 1 (-dExp bo+precision-1)). split;[split|idtac]. simpl; apply vNumbMoreThanOne with radix precision; auto with zarith. apply Z.le_trans with (- dExp bo + precision - 1)%Z; auto with zarith. unfold FtoRradix, FtoR; simpl; ring. apply H0; auto. apply H with (a*c)%R; auto. cut (exists f:float, Fbounded bo f /\ (FtoRradix f=(powerRZ radix (- dExp bo + precision - 1)))%R). intros T; elim T; intros f T'; elim T'; intros; clear T T'. rewrite <- H5; unfold FtoRradix. apply RoundAbsMonotonel with bo precision (Closest bo radix) (a*c)%R; auto with zarith real. apply ClosestRoundedModeP with precision; auto with zarith. elim Roundq; auto. fold FtoRradix; rewrite H5; auto. apply Rle_trans with (2:=U2); auto with zarith real. apply Rle_powerRZ; unfold radix; try apply IZR_le; auto with zarith. exists (Float 1 (-dExp bo+precision-1)). split;[split|idtac]. simpl; apply vNumbMoreThanOne with radix precision; auto with zarith. apply Z.le_trans with (- dExp bo + precision - 1)%Z; auto with zarith. unfold FtoRradix, FtoR; simpl; ring. apply H0; auto; apply H with (3*Rabs t)%R; auto. apply H0; auto; apply H with (p+q)%R; auto. generalize (EvenClosestCompatible bo radix precision); unfold CompatibleP. intros T; apply T with (b*b)%R p; auto with real zarith. rewrite FnormalizeCorrect; auto with zarith real. apply FnormalizeBounded; auto with zarith;apply H with (b*b)%R; auto. generalize (EvenClosestCompatible bo radix precision); unfold CompatibleP. intros T; apply T with (a*c)%R q; auto with real zarith. rewrite FnormalizeCorrect; auto with zarith real. apply FnormalizeBounded; auto with zarith;apply H with (a*c)%R; auto. repeat rewrite FnormalizeCorrect; auto with zarith real. generalize (EvenClosestCompatible bo radix precision); unfold CompatibleP. intros T; apply T with (p-q)%R t; auto with real zarith. rewrite FnormalizeCorrect; auto with zarith real. apply FnormalizeBounded; auto with zarith;apply H with (p-q)%R; auto. rewrite FnormalizeCorrect; auto with zarith real. generalize (EvenClosestCompatible bo radix precision); unfold CompatibleP. intros T; apply T with (3*Rabs t)%R u; auto with real zarith. rewrite FnormalizeCorrect; auto with zarith real. apply FnormalizeBounded; auto with zarith;apply H with (3*Rabs t)%R; auto. repeat rewrite FnormalizeCorrect; auto with zarith real. generalize (EvenClosestCompatible bo radix precision); unfold CompatibleP. intros T; apply T with (p+q)%R v; auto with real zarith. rewrite FnormalizeCorrect; auto with zarith real. apply FnormalizeBounded; auto with zarith;apply H with (p+q)%R; auto. repeat rewrite FnormalizeCorrect; auto with zarith real. fold FtoRradix; intros. generalize (EvenClosestCompatible bo radix precision); unfold CompatibleP. intros T; apply T with (p-q)%R d; auto with real zarith. rewrite FnormalizeCorrect; auto with zarith real. apply FnormalizeBounded; auto with zarith. rewrite FnormalizeCorrect; auto with zarith real. rewrite FnormalizeCorrect; auto with zarith real. repeat rewrite FnormalizeCorrect; auto with zarith real. fold FtoRradix; intros. generalize (EvenClosestCompatible bo radix precision); unfold CompatibleP. intros T; apply T with (dp-dq)%R s; auto with real zarith. rewrite FnormalizeCorrect; auto with zarith real. apply FnormalizeBounded; auto with zarith;apply H with (dp-dq)%R; auto. repeat rewrite FnormalizeCorrect; auto with zarith real. fold FtoRradix; intros. generalize (EvenClosestCompatible bo radix precision); unfold CompatibleP. intros T; apply T with (t+s)%R d; auto with real zarith. rewrite FnormalizeCorrect; auto with zarith real. apply FnormalizeBounded; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz