proposition: Theorem AddExpGe1Underf: forall f1:float ,forall f2:float, forall g:float, forall e:Z, Closest bo radix (f1+f2) g -> (Fcanonic radix bo f1) -> (Fcanonic radix bo f2) -> (powerRZ radix e <= Rabs f1)%R -> (-dExp bo <= e-1)%Z -> ((FtoRradix g=0)%R \/ (powerRZ radix (e-precision) <= Rabs g)%R).
proof: Proof. intros. assert (F1:(Fbounded bo f1));[apply FcanonicBound with radix; auto|idtac]. assert (F2:(Fbounded bo f2));[apply FcanonicBound with radix; auto|idtac]. case (Req_dec g 0); auto; intros. right. case (Rle_or_lt (Rabs f1) (Rabs f2)); intros. apply Rle_trans with (powerRZ radix (e-precision+1)). apply Rle_powerRZ; auto with real zarith. apply AddExpGeUnderf2 with f1 f2; auto with real. apply Rle_trans with (1:=H2); auto with real. case (Rle_or_lt (Rabs f2) ((Rabs f1)/2)); intros. apply Rle_trans with (powerRZ radix (e-1)). apply Rle_powerRZ; auto with real zarith. assert (exists f:float, Fbounded bo f /\ (FtoRradix f=powerRZ radix (e - 1))%R). exists (Float 1 (e-1)); split. split; simpl; auto with zarith. apply vNumbMoreThanOne with radix precision; auto with zarith. unfold FtoRradix, FtoR; simpl; ring. elim H7; intros f T; elim T; intros; clear H7 T. rewrite <- H9; unfold FtoRradix. apply RoundAbsMonotonel with bo precision (Closest bo radix) (f1+f2)%R; auto. apply ClosestRoundedModeP with precision; auto with zarith. fold FtoRradix; rewrite H9. unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl. unfold radix; ring_simplify(2*1)%R; apply Rle_trans with ((Rabs f1)/2)%R. unfold Rdiv; apply Rmult_le_compat_r; auto with real. apply Rle_trans with (Rabs f1 -(Rabs f1)/2)%R;[right; field; auto with real|idtac]. apply Rle_trans with (Rabs f1-Rabs f2)%R. unfold Rminus; apply Rplus_le_compat_l; auto with real. rewrite <- (Rabs_Ropp f2). replace (f1+f2)%R with (f1-(-f2))%R; try ring. apply Rabs_triang_inv. elim plusExactExp with bo radix precision f1 f2 g; auto with zarith. intros s T; elim T; intros g' T'; elim T'; intros R1 T''; clear T T'. elim T''; intros R2 T; elim T; intros R3 T'; elim T'; intros R4 TT; clear T T' T''. elim TT; intros R5 T; elim T; intros R6 R7; clear T TT. replace (FtoRradix g) with (FtoRradix g'); auto with real. apply Rle_trans with (powerRZ radix (Fexp g')). apply Rle_powerRZ; auto with real zarith. apply Z.le_trans with (Z.min (Fexp f1) (Fexp f2)); auto with zarith. rewrite Z.min_r. apply Z.le_trans with ((e-1)-precision+1)%Z; auto with zarith. apply FexpGeUnderf; auto. unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl. unfold radix; ring_simplify (2*1)%R; apply Rle_trans with ((Rabs f1)/2)%R; auto with real. unfold Rdiv; apply Rmult_le_compat_r; auto with real. apply Fcanonic_Rle_Zle with radix bo precision; auto with zarith real. unfold FtoRradix; rewrite <- Fabs_correct; auto. unfold Fabs, FtoR; simpl. apply Rle_trans with (1%Z*powerRZ radix (Fexp g'))%R; [simpl; right; ring|apply Rmult_le_compat_r; auto with real zarith]. apply powerRZ_le; try apply IZR_lt; auto with zarith. apply IZR_le. case (Zle_lt_or_eq 0 (Z.abs (Fnum g'))); auto with zarith real; intros. case (Z.eq_dec 0 (Fnum g')); intros. absurd (FtoR radix g=0)%R; auto with real. rewrite <- R3; unfold FtoR; simpl; rewrite <- e0; simpl; ring. lia. Qed.
imports: Reals ZArith List PeanoNat Psatz