proposition: Theorem cases: (FtoRradix b=0)%R \/ (a*c=0)%R \/ (FtoRradix d=0)%R \/ (FtoRradix v=0)%R \/ (FtoRradix t=0)%R \/ ((powerRZ radix (-dExp bo+2*precision-1) <= Rabs (b*b))%R /\ (powerRZ radix (-dExp bo+2*precision-1) <= Rabs (a*c))%R /\ (powerRZ radix (-dExp bo+precision) <= Rabs d)%R /\ (powerRZ radix (-dExp bo+precision-1) <= Rabs u)%R /\ (powerRZ radix (-dExp bo+precision-1) <= Rabs v)%R /\ (powerRZ radix (-dExp bo+precision) <= Rabs t)%R).
proof: Proof. case U1; auto; intros. case U2; auto; intros. case (Req_dec b 0); auto with real; intros; right. case (Req_dec (a*c) 0); auto with real; intros; right. assert (True); auto. case (Req_dec d 0); auto with real; intros; right. case (Req_dec v 0); auto with real; intros; right. case (Req_dec t 0); auto with real; intros; right. assert (powerRZ radix (-dExp bo+3*precision-1) <= Rabs (p))%R. apply pGeUnderf; auto with real. assert (powerRZ radix (-dExp bo+3*precision-1) <= Rabs (q))%R. apply qGeUnderf; auto with real. assert (powerRZ radix (-dExp bo+2*precision) <= Rabs v)%R. replace (-dExp bo+2*precision)%Z with ((-dExp bo+3*precision-1)-precision+1)%Z; auto with zarith. apply AddExpGeUnderf2 with p q; auto. elim Roundv; auto. elim Roundp; intros A1 A2; elim A1; auto. elim Roundq; intros A1 A2; elim A1; auto. assert (powerRZ radix (-dExp bo+2*precision) <= Rabs t)%R. replace (-dExp bo+2*precision)%Z with ((-dExp bo+3*precision-1)-precision+1)%Z; auto with zarith. apply AddExpGeUnderf2 with p (Fopp q); auto. unfold FtoRradix; rewrite Fopp_correct; elim Roundt; auto with real. elim Roundp; intros A1 A2; elim A1; auto. apply oppBounded; elim Roundq; intros A1 A2; elim A1; auto. unfold FtoRradix; rewrite Fopp_correct;rewrite Rabs_Ropp; auto with real. assert (powerRZ radix (-dExp bo+precision+1) <= Rabs u)%R. replace (-dExp bo+precision+1)%Z with ((-dExp bo+2*precision)-precision+1)%Z; auto with zarith. apply AddExpGeUnderf2 with (Fabs t) (Fabs (Float (Fnum t) (Fexp t+1))); auto. replace (Fabs t + Fabs (Float (Fnum t) (Fexp t + 1)))%R with (3*Rabs t)%R; [elim Roundu; auto|idtac]. unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl. rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; ring. apply absFBounded; elim Roundt; intros A1 A2; elim A1; auto. elim Roundt; intros A1 A2; elim A1; intros A4 A3; elim A4; intros. split; unfold Fabs; simpl; lia. unfold FtoRradix; rewrite Fabs_correct; auto. rewrite Rabs_right; auto with real. apply Rle_ge, Rabs_pos. apply Rle_trans with (1:=H10). apply Rle_trans with (1*Rabs t)%R; auto with real. apply Rle_trans with (2*Rabs t)%R; auto with real. apply Rmult_le_compat_r; auto with real. apply Rabs_pos. unfold FtoRradix; rewrite Fabs_correct; auto. rewrite Rabs_right with (Rabs (FtoR radix (Float (Fnum t) (Fexp t + 1)))); auto with real. repeat rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl. rewrite powerRZ_add; auto with real zarith. rewrite powerRZ_1; unfold radix; right; ring. apply Rle_ge, Rabs_pos. assert (0 < u)%R; auto with real. apply Rlt_le_trans with (Rabs t); auto with real. assert (Rabs t <> 0)%R; auto with real. apply Rabs_no_R0; auto with real. assert (A:(0 <= Rabs t)%R); try apply Rabs_pos; case A; auto with real. intros; absurd (Rabs t=0)%R; auto with real. unfold FtoRradix; rewrite <- Fabs_correct; auto. apply RleBoundRoundl with bo precision (EvenClosest bo radix precision) (3 * Rabs t)%R; auto with zarith. apply EvenClosestRoundedModeP; auto with zarith. apply absFBounded; elim Roundt; intros A1 A2; elim A1; auto. apply Rle_trans with (1*Rabs t)%R; auto with real. rewrite Fabs_correct; auto; right; unfold FtoRradix; ring. apply Rmult_le_compat_r; auto with real; apply Rabs_pos. split. apply Rle_trans with (2:=H); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; unfold radix; auto with zarith. split. apply Rle_trans with (2:=H0); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; unfold radix; auto with zarith. split. 2: split. 2: apply Rle_trans with (2:=H11); auto with real zarith. 2: apply Rle_powerRZ; try apply IZR_le; unfold radix; auto with zarith. 2:split. 2:apply Rle_trans with (2:=H9); auto with real zarith. 2: apply Rle_powerRZ; try apply IZR_le; unfold radix; auto with zarith. 2:apply Rle_trans with (2:=H10); auto with real zarith. 2: apply Rle_powerRZ; try apply IZR_le; unfold radix; auto with zarith. case (Rle_or_lt v u); intros. assert (powerRZ radix (-dExp bo+2*precision) <= Rabs d)%R. replace (-dExp bo+2*precision)%Z with ((-dExp bo+3*precision-1)-precision+1)%Z; auto with zarith. apply AddExpGeUnderf2 with p (Fopp q); auto. unfold FtoRradix; rewrite Fopp_correct; elim FRoundd; auto with real. elim Roundp; intros A1 A2; elim A1; auto. apply oppBounded; elim Roundq; intros A1 A2; elim A1; auto. unfold FtoRradix; rewrite Fopp_correct;rewrite Rabs_Ropp; auto with real. apply Rle_trans with (2:=H13); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; unfold radix; auto with zarith. replace (-dExp bo+precision)%Z with ((-dExp bo+2*precision)-precision)%Z; auto with zarith. apply AddExpGe1Underf2 with t s; auto with zarith. elim SRoundd; auto with real. elim Roundt; intros A1 A2; elim A1; auto. elim SRounds; auto; intros A1 A2; elim A1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz