proposition: Theorem discri4: (Fexp p)=(Fexp q) -> (delta <= 2*(Fulp bo radix precision d))%R.
proof: Proof. intros H1; apply discri3. generalize errorBoundedMultClosest_Can; intros T. elim T with (f1:=b) (f2:=b') (g:=p); auto with zarith real; clear T. intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4 H5; clear T2 T3 T4. 2: elim Roundp; auto. generalize errorBoundedMultClosest_Can; intros T. elim T with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear T. intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4. 2: elim Roundq; auto. 2: left; auto. 2: left; auto. assert ((Rabs (Fnum dp'-Fnum dq') < (powerRZ radix precision))%R \/ (((Rabs dp')= (powerRZ radix (Z.pred (Fexp p))))%R /\ ((Rabs dq')= (powerRZ radix (Z.pred (Fexp p))))%R)). case H5; intros. left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp') (-(Fnum dq'))%R). rewrite Rabs_Ropp. apply Rlt_le_trans with ((powerRZ radix (Z.pred precision)) +(Rabs (Fnum dq')))%R; auto with real zarith. apply Rle_trans with ((powerRZ radix (Z.pred precision))+ (powerRZ radix (Z.pred precision)))%R; auto with real zarith. right; unfold Z.pred; repeat rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2 4; simpl; unfold radix; field. case H5'; intros. left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp') (-(Fnum dq'))%R); rewrite Rabs_Ropp. apply Rle_lt_trans with ((powerRZ radix (Z.pred precision)) +(Rabs (Fnum dq')))%R; auto with real zarith. apply Rlt_le_trans with ((powerRZ radix (Z.pred precision))+ (powerRZ radix (Z.pred precision)))%R; auto with real zarith. right; unfold Z.pred; repeat rewrite powerRZ_add; auto with real zarith. unfold powerRZ at 2 4; simpl; unfold radix; field. right; unfold FtoRradix, FtoR;repeat rewrite Rabs_mult. rewrite (Rabs_right (powerRZ radix (Fexp dp'))); try apply Rle_ge; auto with real zarith. rewrite (Rabs_right (powerRZ radix (Fexp dq'))); try apply Rle_ge; auto with real zarith. rewrite H; rewrite H0. repeat rewrite <- powerRZ_add; auto with real zarith. rewrite H4'; rewrite H4; unfold Z.pred. ring_simplify (precision + -1 + (Fexp p - precision))%Z; ring_simplify (precision + -1 + (Fexp q - precision))%Z; ring_simplify (Fexp p+-1)%Z; rewrite <- H1; auto with zarith real. apply powerRZ_le, IZR_lt; auto with zarith. apply powerRZ_le, IZR_lt; auto with zarith. case H; clear H; intros H. exists (Float ((Fnum dp')-(Fnum dq'))%Z (Fexp dq')). split; [split; auto with zarith|idtac]. simpl; apply lt_IZR. rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto. rewrite <- Rabs_Zabs; unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith. simpl; auto with zarith. apply H2'. rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'. unfold FtoRradix, FtoR; simpl. unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; replace (Fexp dp') with (Fexp dq');[ring|idtac]. rewrite H4'; rewrite <- H1; auto with zarith. rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'. elim H; unfold Rabs; case (Rcase_abs dp'); case (Rcase_abs dq'); intros. exists (Float 0%Z 0%Z); split;[split; unfold Fexp; try lia; auto with zarith|idtac]. apply trans_eq with (-(-dp')+-dq')%R;[rewrite H0; rewrite H6; unfold FtoRradix, FtoR;simpl|idtac];ring. exists (Float (-2)%Z (Z.pred (Fexp p))); split;[split; simpl; auto with zarith|idtac]. rewrite pGivesBound; apply Z.le_lt_trans with (Zpower_nat radix 1); auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. apply Z.le_trans with (Fexp dp'); auto with zarith; apply H2. apply trans_eq with (-(-dp')+-dq')%R;[rewrite H0; rewrite H6; unfold FtoRradix, FtoR; simpl|idtac];ring. exists (Float 2%Z (Z.pred (Fexp p))); split;[split;simpl;auto with zarith|idtac]. rewrite pGivesBound; apply Z.le_lt_trans with (Zpower_nat radix 1); auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. apply Z.le_trans with (Fexp dp'); auto with zarith; apply H2. unfold Rminus;rewrite H0; rewrite H6; unfold FtoRradix, FtoR;simpl; ring. exists (Float 0%Z 0%Z); split;[split; unfold Fexp; try lia; auto with zarith|idtac]. rewrite H0; rewrite H6; unfold FtoRradix, FtoR; simpl;ring. Qed.
imports: Reals ZArith List PeanoNat Psatz