proposition: Theorem errorBoundedMultClosest_Can: forall f1 f2 g : float, Fbounded bo f1 -> Fbounded bo f2 -> Closest bo radix (f1* f2) g -> (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (f1*f2))%R -> Fcanonic radix bo g -> (exists s : float, Fbounded bo s /\ (FtoRradix s = f1*f2 - g)%R /\ Fexp s = (Fexp g - precision)%Z /\ (Rabs (Fnum s) <= powerRZ radix (Z.pred precision))%R).
proof: Proof. intros. generalize errorBoundedMultClosest; intros T. elim T with (b:=bo) (radix:=radix) (precision:=precision) (p:=f1) (q:=f2) (pq:=g); auto with zarith real; clear T; fold FtoRradix. intros g' T1; elim T1; intros dg T2; elim T2; intros H5 T3; elim T3; intros H6 T4; elim T4; intros H7 T5; elim T5; intros H8 T6; elim T6; intros H9 H10; clear T1 T2 T3 T4 T5 T6. exists dg; split; auto; split. rewrite <- H8; auto with real. split; [replace g with g'; auto with zarith|idtac]. apply FcanonicUnique with radix bo precision; auto with zarith. apply Rmult_le_reg_l with (powerRZ radix (Fexp dg)); auto with zarith real. apply powerRZ_lt, IZR_lt; auto with zarith. apply Rle_trans with (Rabs dg);[right; unfold FtoRradix, FtoR|idtac]. rewrite Rabs_mult;rewrite (Rabs_right (powerRZ radix (Fexp dg)));auto with real. apply Rle_ge; auto with real zarith. apply powerRZ_le, IZR_lt; auto with zarith. rewrite H9; rewrite <- powerRZ_add; auto with real zarith. apply Rmult_le_reg_l with 2%R; auto with real zarith. apply Rle_trans with (Fulp bo radix precision g'). unfold FtoRradix; apply ClosestUlp; auto. replace g' with g; auto. apply FcanonicUnique with radix bo precision; auto with zarith. rewrite CanonicFulp; auto. right; apply trans_eq with (powerRZ radix (Fexp g'));[unfold FtoR; simpl; ring|idtac]. apply trans_eq with ((powerRZ radix 1%Z)*(powerRZ radix (Fexp dg+Z.pred precision)))%R;[rewrite <- powerRZ_add; auto with zarith real|idtac]. 2: rewrite powerRZ_1; unfold radix; simpl; ring. rewrite H10; unfold Z.pred; auto with zarith real. ring_simplify (1 + (Fexp g' - precision + (precision + -1)))%Z; auto with real. assert (- dExp bo + 2 * precision - 1 < 2*precision+Fexp f1+Fexp f2)%Z; auto with zarith. apply Zlt_powerRZ with radix; auto with real zarith. apply Rle_lt_trans with (1:=H2). rewrite Rabs_mult; unfold FtoRradix; repeat rewrite <- Fabs_correct; auto. replace (2*precision)%Z with (precision+precision)%Z; auto with zarith. unfold FtoR, Fabs; simpl. repeat rewrite powerRZ_add; auto with real zarith. repeat rewrite <- Rmult_assoc; apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. apply Rle_lt_trans with (Z.abs (Fnum f1)*Z.abs (Fnum f2) * powerRZ 2 (Fexp f1))%R; [unfold radix; right; ring| apply Rmult_lt_compat_r; auto with real zarith]. apply powerRZ_lt, IZR_lt; auto with zarith. apply Rle_lt_trans with (Z.abs (Fnum f1)* powerRZ 2 precision)%R. apply Rmult_le_compat_l; auto with real zarith. apply IZR_le; auto with zarith. apply Rle_trans with (Zpos (vNum bo)). apply IZR_le, Zlt_le_weak; apply H0. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real. apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. apply Rlt_le_trans with (Zpos (vNum bo)). apply IZR_lt; apply H. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real. rewrite FcanonicFnormalizeEq; auto with zarith. assert (powerRZ radix (- dExp bo + 2 * precision - 1) <= Rabs g)%R. cut (exists f:float, Fbounded bo f /\ (FtoRradix f=(powerRZ radix (- dExp bo + 2 * 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) (f1*f2)%R; auto with zarith real. apply ClosestRoundedModeP with precision; auto with zarith. fold FtoRradix; rewrite H5; auto. exists (Float 1 (-dExp bo+2*precision-1)). split;[split|idtac]. simpl; apply vNumbMoreThanOne with radix precision; auto with zarith. apply Z.le_trans with (- dExp bo + 2 * precision - 1)%Z; auto with zarith. unfold FtoRradix, FtoR; simpl; ring. assert (- dExp bo + 2 * precision - 1 < precision+Fexp g)%Z; auto with zarith. apply Zlt_powerRZ with radix; auto with zarith real. apply Rle_lt_trans with (1:=H4). unfold FtoRradix; rewrite <- Fabs_correct; auto. rewrite powerRZ_add; auto with real zarith. unfold FtoR, Fabs; simpl. apply Rmult_lt_compat_r; auto with real zarith. apply powerRZ_lt, IZR_lt; auto with zarith. apply Rlt_le_trans with (Zpos (vNum bo)). apply IZR_lt, H1. rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz