proposition: Theorem exp_correct : forall prec, extension Xexp (exp prec).
proof: Proof. intros prec [|xl xu]. easy. intros [|x]. now simpl; case (_ && _)%bool. unfold convert at 1. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; lra]. intros Vxu Vxl [Hxl Hxu]. simpl. assert (Hl := fun H => proj1 (exp_aux_correct xl H)). assert (Hu := fun H => proj2 (exp_aux_correct xu H)). rewrite <- PrimitiveFloat.real_is_finite, F.real_correct, B2Prim_Prim2B in Hl. rewrite <- PrimitiveFloat.real_is_finite, F.real_correct, B2Prim_Prim2B in Hu. set (l := if F.real xl then _ else _). set (u := if F.real xu then _ else _). assert (Vl : F.valid_lb l = true). { unfold l. clear l u. rewrite F.real_correct. destruct (F.toX xl) as [|rxl]. easy. specialize (Hl eq_refl). revert Hl. unfold exp_aux. destruct PrimFloat.ltb. easy. now destruct PrimFloat.ltb. } assert (Vu : F.valid_ub u = true). { unfold u. clear l u Vl. rewrite F.real_correct. destruct (F.toX xu) as [|rxu]. easy. specialize (Hu eq_refl). revert Hu. unfold exp_aux. destruct PrimFloat.ltb. easy. now destruct PrimFloat.ltb. } rewrite Vl, Vu; unfold l, u. split. - clear u Hxu Hu Vu. rewrite F.real_correct. assert (Hxl' := PrimitiveFloat.toX_Prim2B xl). destruct (F.toX xl) as [|rxl]. apply Rlt_le, exp_pos. apply eq_sym, PrimitiveFloat.BtoX_B2R in Hxl'. specialize (Hl eq_refl). revert Hl. unfold exp_aux. intros [_ H]. destruct PrimFloat.ltb. apply Rle_trans with (1 := H). apply Raux.exp_le. now rewrite <- Hxl'. destruct PrimFloat.ltb. apply Rle_trans with (1 := H). apply Raux.exp_le. now rewrite <- Hxl'. revert H. set (yl := next_down _). simpl. destruct F.toX as [|ryl]. easy. intros H. apply Rle_trans with (1 := H). apply Raux.exp_le. now rewrite <- Hxl'. - clear l Hxl Hl Vl. rewrite F.real_correct. assert (Hxu' := PrimitiveFloat.toX_Prim2B xu). destruct (F.toX xu) as [|rxu]. easy. apply eq_sym, PrimitiveFloat.BtoX_B2R in Hxu'. specialize (Hu eq_refl). revert Hu. unfold exp_aux. intros [_ H]. destruct PrimFloat.ltb. apply Rle_trans with (2 := H). apply Raux.exp_le. now rewrite <- Hxu'. destruct PrimFloat.ltb. easy. revert H. set (yl := next_up _). simpl. destruct F.toX as [|ryu]. easy. intros H. apply Rle_trans with (2 := H). apply Raux.exp_le. now rewrite <- Hxu'. Qed.
imports: Coq(Reals Psatz PrimInt63 Uint63 Sint63 PArray Floats) Flocq(Core PrimFloat BinarySingleNaN) Missing.Flocq Xreal Basic Sig Interval Float Float_full Specific_bigint Specific_ops Primitive_ops Lang_expr Lang_tac Interval_helper