proposition: Lemma hxExact: (FtoRradix hx=p+q)%R.
proof: Proof. replace (p+q)%R with (FtoRradix (Fminus radix p (Fopp q))). 2: unfold FtoRradix; rewrite Fminus_correct; auto; rewrite Fopp_correct;ring. apply sym_eq; unfold FtoRradix; apply ClosestIdem with b. 2: rewrite Fminus_correct; auto; rewrite Fopp_correct; auto with real. 2: fold FtoRradix; replace (p-(-q))%R with (q+p)%R; auto with real;ring. apply SterbenzAux; auto with zarith. elim pDef; auto. apply oppBounded; elim qDef; auto. generalize ClosestMonotone; unfold MonotoneP; intros. apply H with b (-(x-p))%R p; auto with zarith real. apply Rplus_lt_reg_r with (x-p)%R. ring_simplify; auto with real. apply ClosestOpp; auto. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b). apply ClosestRoundedModeP with t; auto with zarith. elim pDef; auto. apply Rmult_le_reg_l with (1-(1+(powerRZ radix (1-t))/2)/(powerRZ radix s + 1))%R. apply Rmult_lt_reg_l with (2*(powerRZ radix s + 1))%R; auto with real zarith. apply Rmult_lt_0_compat; auto with real zarith. apply Rplus_lt_0_compat; auto with real. apply powerRZ_lt, IZR_lt; lia. rewrite Rmult_0_r. apply Rlt_le_trans with (2*powerRZ radix s - (powerRZ radix (1- t)))%R;[idtac|right; field]. apply Rplus_lt_reg_r with ((powerRZ radix (1-t)))%R. ring_simplify. apply Rle_lt_trans with (powerRZ radix s); auto with real zarith. apply Rle_powerRZ; auto with zarith; left; apply IZR_lt; lia. apply Rle_lt_trans with (powerRZ radix s + 0)%R; auto with real zarith. apply Rlt_le_trans with (powerRZ radix s + powerRZ radix s)%R; auto with real zarith. apply Rplus_lt_compat_l; apply powerRZ_lt, IZR_lt; lia. right; ring. cut (0 < (powerRZ radix s + 1))%R; auto with real zarith. apply Rplus_lt_0_compat; auto with real. apply powerRZ_lt, IZR_lt; lia. apply Rle_trans with ((FtoR radix (Fopp q))*(1 + (powerRZ radix (1- t))/2))%R. fold FtoRradix; apply Rle_trans with (p-x)%R. apply Rle_trans with (p - (p*(1 + powerRZ radix (1 - t) / 2) / (powerRZ radix s + 1)))%R;[right|unfold Rminus;apply Rplus_le_compat_l]. field; auto with real zarith. cut (0 < (powerRZ radix s + 1))%R; auto with real zarith. apply Rplus_lt_0_compat; auto with real; apply powerRZ_lt, IZR_lt; lia. apply Ropp_le_contravar. apply Rmult_le_reg_l with (powerRZ radix s + 1)%R; auto with real zarith. apply Rplus_lt_0_compat; auto with real; apply powerRZ_lt, IZR_lt; lia. apply Rle_trans with ((p * (1 + powerRZ radix (1 - t)/2)))%R;[idtac|right;field]. replace ((powerRZ radix s + 1)* x)%R with (Rabs ((x * (powerRZ radix s + 1))))%R. replace (FtoRradix p) with (Rabs p). apply RleRRounded; auto. apply Rabs_right; apply Rle_ge; apply pPos. rewrite Rabs_right; auto with real; apply Rle_ge; apply Rmult_le_pos; auto with real zarith. cut (0 < (powerRZ radix s + 1))%R; auto with real zarith. apply Rplus_lt_0_compat; auto with real; apply powerRZ_lt, IZR_lt; lia. apply Rgt_not_eq. apply Rplus_lt_0_compat; auto with real; apply powerRZ_lt, IZR_lt; lia. replace (p - x)%R with (Rabs (x-p))%R. replace (FtoRradix (Fopp q)) with (Rabs q)%R. apply RleRRounded; auto. rewrite Rabs_left1;[idtac|apply qNeg]. unfold FtoRradix; rewrite Fopp_correct; auto with real. rewrite Rabs_left1; auto with real. apply Rplus_le_reg_l with (p)%R; ring_simplify. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H with b x (x * (powerRZ radix s + 1))%R; auto with zarith real. apply Rplus_lt_reg_r with (-x)%R; ring_simplify. apply Rle_lt_trans with (x*0)%R;[right;ring|apply Rmult_lt_compat_l;auto with real zarith]. apply powerRZ_lt, IZR_lt; lia. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto. apply ClosestRoundedModeP with t; auto with zarith. fold FtoRradix;apply Rle_trans with ((Fopp q)*((1 - (1 + powerRZ radix (1 - t) / 2) / (powerRZ radix s + 1)) *S 1))%R;[idtac|right;ring]. apply Rmult_le_compat_l. generalize qNeg; unfold FtoRradix; rewrite Fopp_correct; auto with real. apply Rle_trans with (3/2)%R. apply Rplus_le_reg_l with (-1)%R; ring_simplify ((-1 +(1+powerRZ radix (1 - t) / 2)))%R. apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (powerRZ radix (1 - t))%R;[right;field; auto with real|idtac]. apply Rle_trans with (powerRZ radix (0))%R;[idtac|right;simpl;field]; auto with real zarith. apply Rle_powerRZ; auto with zarith; left; apply IZR_lt; lia. apply Rmult_le_reg_l with (/2)%R; auto with real. apply Rplus_le_reg_l with (-3/4+(1 + powerRZ radix (1 - t) / 2) / (powerRZ radix s + 1))%R. apply Rle_trans with ((1 + powerRZ radix (1 - t) / 2) / (powerRZ radix s + 1))%R;[right; field; auto with real|idtac]. cut (0 < powerRZ radix s + 1)%R; auto with real. apply Rplus_lt_0_compat; auto with real; apply powerRZ_lt, IZR_lt; lia. apply Rmult_le_reg_l with (powerRZ radix s + 1)%R; auto with real zarith. apply Rplus_lt_0_compat; auto with real; apply powerRZ_lt, IZR_lt; lia. apply Rmult_le_reg_l with 4%R. auto with real. apply Rle_trans with (4+ 2*(powerRZ radix (1 - t)))%R;[right; field|idtac]. apply Rgt_not_eq, Rlt_gt. apply Rplus_lt_0_compat; auto with real; apply powerRZ_lt, IZR_lt; lia. apply Rle_trans with (powerRZ radix s + 1)%R;[idtac|right;simpl;field;auto with real]. apply Rplus_le_compat. apply Rle_trans with (powerRZ radix 2)%R; [simpl;auto with real zarith|idtac]. ring_simplify (radix * 1)%R; apply Rmult_le_compat; auto with real zarith arith; replace (R1 +R1)%R with 2%R by easy; apply IZR_le; auto with zarith. apply Rle_powerRZ; auto with zarith real. left; apply IZR_lt; lia. apply Rle_trans with (powerRZ radix (1+(1 - t)))%R. rewrite powerRZ_add. apply Rmult_le_compat_r. apply powerRZ_le, IZR_lt; lia. simpl; ring_simplify (radix*1)%R; apply Rle_trans with (IZR 2); auto with real zarith. apply IZR_le; lia. apply IZR_neq; lia. change 1%R with (powerRZ radix 0). apply Rle_powerRZ; auto with zarith real. apply IZR_le; lia. apply Rgt_not_eq, Rlt_gt. apply Rplus_lt_0_compat; auto with real; apply powerRZ_lt, IZR_lt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz