proposition: Lemma LeExp2: (Fexp uh <= Fexp z+1)%Z.
proof: Proof. assert (Rabs (uh-z) <= (1+radix)* Fulp bo radix p uh + Fulp bo radix p z)%R. replace (uh-z)%R with (-(ph+b-uh)+-(a*x-ph)+(a*x+b-z))%R;[idtac|ring]. apply Rle_trans with (1:=Rabs_triang (-(ph+b-uh)+-(a*x-ph)) (a*x+b-z)). apply Rplus_le_compat. apply Rle_trans with (1:=Rabs_triang (-(ph+b-uh)) (-(a*x-ph))). apply Rle_trans with (Fulp bo radix p uh+radix*Fulp bo radix p uh)%R; [apply Rplus_le_compat|right; ring]. rewrite Rabs_Ropp; apply Rlt_le; unfold FtoRradix. apply RoundedModeUlp with (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply Rle_trans with (Fulp bo radix p ph). rewrite Rabs_Ropp; apply Rlt_le; unfold FtoRradix. apply RoundedModeUlp with (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. unfold Fulp; repeat rewrite FcanonicFnormalizeEq; auto with zarith. 2: left; auto. 2: left; auto. apply Rle_trans with (powerRZ radix (Fexp uh+1)); [apply Rle_powerRZ; try apply IZR_le; auto with real zarith; generalize LeExp1; auto with zarith| rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; right;ring]. apply Rlt_le; unfold FtoRradix. apply RoundedModeUlp with (Closest bo radix); auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply Z.le_trans with (Fexp (Float (Fnum z) (Fexp z+1))); auto with zarith. apply Fcanonic_Rle_Zle with radix bo p; auto with zarith. left; auto. elim Nz; intros A1 A2; elim A1; intros. left; split;[split|idtac];simpl; auto with zarith. fold FtoRradix; apply Rle_trans with (radix*Rabs z)%R. 2: unfold FtoRradix; repeat rewrite <- Fabs_correct; auto; unfold FtoR; simpl. 2: rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; right; ring. apply Rmult_le_reg_l with (1-(1+radix)*powerRZ radix (Z.succ (-p)))%R. assert ((1+radix) * powerRZ radix (Z.succ (-p)) < 1)%R; auto with real. 2: apply Rlt_Rminus; auto. apply Rlt_le_trans with ((radix*radix)*powerRZ radix (Z.succ (-p)))%R; [apply Rmult_lt_compat_r; auto with real zarith|idtac]. apply powerRZ_lt, IZR_lt; lia. apply Rlt_le_trans with (radix+radix)%R; auto with real. apply Rplus_lt_compat_r, IZR_lt; auto with zarith. apply Rle_trans with (2*radix)%R; [right; ring|apply Rmult_le_compat_r; auto with real zarith]; apply IZR_le; lia. apply Rle_trans with (powerRZ radix (2+Z.succ (-p))); [right; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; ring|idtac]. apply Rle_trans with (powerRZ radix 0); auto with real zarith. apply Rle_powerRZ; try apply IZR_le; auto with zarith. apply Rle_trans with (Rabs uh-(1+radix)*(Rabs uh*powerRZ radix (Z.succ (-p))))%R; [right; ring|idtac]. apply Rle_trans with (Rabs uh-(1+radix)*Fulp bo radix p uh)%R; [unfold Rminus;apply Rplus_le_compat_l|idtac]. apply Ropp_le_contravar; apply Rmult_le_compat_l; auto with real. apply Rle_trans with (1+0)%R; try apply Rplus_le_compat_l; auto with real. apply Rle_trans with 1%R; auto with real. apply IZR_le; lia. unfold FtoRradix; apply FulpLe2; auto with zarith. elim uhDef; auto. rewrite FcanonicFnormalizeEq; auto with zarith; left; auto. apply Rle_trans with (Rabs z+Fulp bo radix p z)%R. apply Rplus_le_reg_l with (-Rabs z+ (1+radix) * Fulp bo radix p uh)%R. ring_simplify. apply Rle_trans with (Rabs uh - Rabs z)%R;[right; ring|idtac]. apply Rle_trans with (Rabs (uh-z));[apply Rabs_triang_inv|idtac]. apply Rle_trans with (1:=H); right; ring. apply Rle_trans with (Rabs z+(Rabs z*powerRZ radix (Z.succ (-p))))%R; [apply Rplus_le_compat_l|idtac]. unfold FtoRradix; apply FulpLe2; auto with zarith. elim zDef; auto. rewrite FcanonicFnormalizeEq; auto with zarith; left; auto. rewrite <- Rmult_assoc. apply Rle_trans with ((1+ powerRZ radix (Z.succ (- p)))*Rabs z)%R; [right; ring|apply Rmult_le_compat_r; auto with real]. apply Rabs_pos. apply Rplus_le_reg_l with (-1+(1+radix)*radix*powerRZ radix (Z.succ (- p)))%R. apply Rle_trans with ((1+radix+radix*radix)*powerRZ radix (Z.succ (- p)))%R;[right; ring|idtac]. apply Rle_trans with (radix-1)%R;[idtac|right; ring]. apply Rle_trans with ((radix*radix*radix)*powerRZ radix (Z.succ (-p)))%R; [apply Rmult_le_compat_r; auto with real zarith|idtac]. apply powerRZ_le, IZR_lt; lia. apply Rle_trans with (radix+radix+radix*radix)%R; auto with real. apply Rplus_le_compat_r, Rplus_le_compat_r, IZR_le; lia. apply Rle_trans with ((2+radix)*radix)%R; [right; ring|apply Rmult_le_compat_r; auto with real zarith]. apply IZR_le; lia. apply Rle_trans with (radix+radix)%R; auto with real. apply Rplus_le_compat_r, IZR_le; lia. apply Rle_trans with (2*radix)%R; [right; ring|apply Rmult_le_compat_r; auto with real zarith]; apply IZR_le; lia. apply Rle_trans with (powerRZ radix (3+Z.succ (-p))); [right; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith; simpl; ring|idtac]. apply Rle_trans with (powerRZ radix 0); auto with real zarith. unfold Z.succ; apply Rle_powerRZ; try apply IZR_le; auto with real zarith. assert (2 <= radix)%R by (apply IZR_le; auto with zarith). simpl; apply Rplus_le_reg_l with 1%R; auto with real. ring_simplify (1 + (radix - 1))%R; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz