proposition: Theorem power_pos_correct : forall prec n, extension (fun x => Xpower_int x (Zpos n)) (fun x => power_pos prec x n).
proof: Proof. intros prec n [ | xl xu] [ | x] ; try ( intros ; exact I ) ; [now unfold convert; case (_ && _)|]. intros Hxlu. generalize Hxlu. unfold convert at 1. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; exfalso; lra]. unfold contains, convert, power_pos, Xpower_int. intros Vxu Vxl [Hxl Hxu]. generalize (sign_large_correct_ xl xu x Hxlu). case (sign_large_ xl xu) ; intros Hx0 ; simpl in Hx0. { rewrite F.zero_correct. simpl. rewrite (proj1 Hx0), pow_i. rewrite F'.valid_lb_real, ?F'.valid_ub_real; [|now rewrite F.real_correct, F.zero_correct..]. split ; apply Rle_refl. apply lt_O_nat_of_P. } { assert (Hxl_pos : le_upper (Xreal 0) (F.toX (F.abs xl))). { rewrite (proj1 (F.abs_correct _)). now xreal_tac2; apply Rabs_pos. } assert (Hxu_pos : le_lower' (Xreal 0) (F.toX (F.abs xu))). { destruct Hx0 as (_, (_, (rHx0, (Hx0, _)))). rewrite (proj1 (F.abs_correct _)), Hx0. apply Rabs_pos. } generalize (Fpower_pos_up_correct prec _ n (proj2 (F.abs_correct xl)) Hxl_pos). generalize (Fpower_pos_dn_correct prec _ n Hxu_pos). destruct n as [n|n|]. { rewrite !F'.neg_correct, F'.valid_lb_neg, F'.valid_ub_neg. intros (Vpow_DN, Hpow_DN) (Vpow_UP, Hpow_UP). rewrite Vpow_UP, Vpow_DN. split. { revert Hpow_UP. unfold le_upper. rewrite (proj1 (F.abs_correct _)). xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. simpl. intros H. apply Ropp_le_contravar in H. apply Rle_trans with (1 := H). rewrite Rabs_left1; [|now apply Hx0]. rewrite Ropp_mult_distr_l_reverse, Ropp_involutive. change (Pmult_nat n 2) with (nat_of_P (xO n)). rewrite nat_of_P_xO at 2. rewrite pow_sqr. rewrite <- (Rmult_opp_opp x x). rewrite <- pow_sqr, <- nat_of_P_xO. apply Rle_trans with (r0 * (-x) ^ nat_of_P (xO n))%R. { apply Rmult_le_compat_neg_l; [now apply Hx0|]. apply pow_incr. now split; [rewrite <- Ropp_0|]; apply Ropp_le_contravar. } apply Rmult_le_compat_r; [|exact Hxl]. apply pow_le. rewrite <- Ropp_0. now apply Ropp_le_contravar. } revert Hpow_DN. unfold le_lower'. rewrite (proj1 (F.abs_correct _)). xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. simpl. intros H'. apply Ropp_le_contravar in H'. apply Rle_trans with (2 := H'). assert (Hr0 : (r0 <= 0)%R). { destruct Hx0 as (_,(_,(ru,(H1,H2)))). now inversion H1. } rewrite Rabs_left1 with (1 := Hr0). rewrite Ropp_mult_distr_l_reverse, Ropp_involutive. change (Pmult_nat n 2) with (nat_of_P (xO n)). rewrite nat_of_P_xO at 1. rewrite pow_sqr. rewrite <- (Rmult_opp_opp x x). rewrite <- pow_sqr, <- nat_of_P_xO. apply Rle_trans with (x * (-r0) ^ nat_of_P (xO n))%R. { apply Rmult_le_compat_neg_l. apply Hx0. apply pow_incr. now split; [rewrite <- Ropp_0|]; apply Ropp_le_contravar. } apply Rmult_le_compat_r; [|exact Hxu]. apply pow_le. rewrite <- Ropp_0. now apply Ropp_le_contravar. } { intros (Vpow_DN, Hpow_DN) (Vpow_UP, Hpow_UP). rewrite Vpow_UP, Vpow_DN. split. { revert Hpow_DN. unfold le_lower'. rewrite (proj1 (F.abs_correct _)). xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. simpl. intros H. apply Rle_trans with (1 := H). assert (Hr0 : (r0 <= 0)%R). { destruct Hx0 as (_,(_,(ru,(H1,H2)))). now inversion H1. } rewrite Rabs_left1 with (1 := Hr0). change (Pmult_nat n 2) with (nat_of_P (xO n)). rewrite nat_of_P_xO at 2. rewrite pow_sqr. rewrite <- (Rmult_opp_opp x x). rewrite <- pow_sqr, <- nat_of_P_xO. apply pow_incr. now split; [rewrite <- Ropp_0|]; apply Ropp_le_contravar. } revert Hpow_UP. unfold le_upper. rewrite (proj1 (F.abs_correct _)). xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. simpl. intros H. apply Rle_trans with (2 := H). rewrite Rabs_left1; [|now apply Hx0]. change (Pmult_nat n 2) with (nat_of_P (xO n)). rewrite nat_of_P_xO at 1. rewrite pow_sqr. rewrite <- (Rmult_opp_opp x x). rewrite <- pow_sqr, <- nat_of_P_xO. apply pow_incr. now split; [rewrite <- Ropp_0|]; apply Ropp_le_contravar. } intros _ _. rewrite Vxl, Vxu. now simpl; split; xreal_tac2; rewrite Rmult_1_r. } { assert (Hxl_pos : le_lower' (Xreal 0) (F.toX xl)). { destruct Hx0 as (_, (_, (rHx0, (Hx0, Hx0')))). now rewrite Hx0. } assert (Hxu_pos : le_upper (Xreal 0) (F.toX xu)). { apply Hx0. } generalize (Fpower_pos_up_correct prec _ n Vxu Hxu_pos). generalize (Fpower_pos_dn_correct prec _ n Hxl_pos). intros (Vpow_DN, Hpow_DN) (Vpow_UP, Hpow_UP). rewrite Vpow_UP, Vpow_DN. split. { revert Hpow_DN. unfold le_lower'. xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. intros H. assert (Hr0: (0 <= r0)%R). { destruct Hx0 as (_,(_,(rl,(H1,H2)))). now inversion H1. } apply Rle_trans with (1 := H). apply pow_incr. now split. } revert Hpow_UP. unfold le_upper. xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. intros H. refine (Rle_trans _ _ _ _ H). apply pow_incr. now split. } destruct n as [n|n|]. { assert (Hxl_pos : le_upper (Xreal 0) (F.toX (F.abs xl))). { rewrite (proj1 (F.abs_correct _)). now xreal_tac2; apply Rabs_pos. } assert (Hxu_pos : le_upper (Xreal 0) (F.toX xu)). { apply Hx0. } generalize (Fpower_pos_up_correct prec _ n~1 (proj2 (F.abs_correct xl)) Hxl_pos). generalize (Fpower_pos_up_correct prec _ n~1 Vxu Hxu_pos). rewrite F'.neg_correct, F'.valid_lb_neg. intros (Vpow_DN, Hpow_DN) (Vpow_UP, Hpow_UP). rewrite Vpow_UP, Vpow_DN. split. { revert Hpow_UP. unfold le_upper. rewrite (proj1 (F.abs_correct _)). xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. simpl. rewrite Rabs_left1; [|now apply Hx0]. intros H. apply Ropp_le_contravar in H. apply Rle_trans with (1 := H). rewrite Ropp_mult_distr_l_reverse, Ropp_involutive. destruct (Rle_or_lt x 0) as [Hx|Hx]. { change (Pmult_nat n 2) with (nat_of_P (xO n)). rewrite nat_of_P_xO at 2. rewrite pow_sqr. rewrite <- (Rmult_opp_opp x x). rewrite <- pow_sqr, <- nat_of_P_xO. apply Rle_trans with (r0 * (-x) ^ nat_of_P (xO n))%R. { apply Rmult_le_compat_neg_l. { apply Hx0. } apply pow_incr. now split; [rewrite <- Ropp_0|]; apply Ropp_le_contravar. } apply Rmult_le_compat_r; [|exact Hxl]. apply pow_le. rewrite <- Ropp_0. now apply Ropp_le_contravar. } apply Rlt_le in Hx. apply Rle_trans with 0%R. { apply Ropp_le_cancel. rewrite Ropp_0, <- Ropp_mult_distr_l_reverse. now apply Rmult_le_pos; [|apply pow_le]; rewrite <- Ropp_0; apply Ropp_le_contravar. } apply Rmult_le_pos with (1 := Hx). now apply pow_le. } revert Hpow_DN. unfold le_upper. xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. simpl. intros H. refine (Rle_trans _ _ _ _ H). destruct (Rle_or_lt x 0) as [Hx|Hx]. { apply Rle_trans with 0%R. { apply Ropp_le_cancel. rewrite Ropp_0, <- Ropp_mult_distr_l_reverse. change (Pmult_nat n 2) with (nat_of_P (xO n)). rewrite nat_of_P_xO. rewrite pow_sqr. rewrite <- (Rmult_opp_opp x x). rewrite <- pow_sqr, <- nat_of_P_xO. now apply Rmult_le_pos; [|apply pow_le]; rewrite <- Ropp_0; apply Ropp_le_contravar. } apply Rmult_le_pos; [now apply Hx0|]. now apply pow_le. } apply Rlt_le in Hx. apply Rmult_le_compat with (1 := Hx). { now apply pow_le. } { exact Hxu. } apply pow_incr. now split. } { elim (F'.max_valid_ub _ _ (proj2 (F.abs_correct xl)) Vxu). intros Vmax Hmax. assert (Hxu_pos : le_upper (Xreal 0) (F.toX (F.max (F.abs xl) xu))). { rewrite Hmax. rewrite (proj1 (F.abs_correct _)). xreal_tac xl; xreal_tac xu. apply (Rle_trans _ _ _ (proj2 Hx0)), Rmax_r. } generalize (Fpower_pos_up_correct prec _ n~0 Vmax Hxu_pos). intros (Vpow_UP, Hpow_UP). rewrite Vpow_UP. rewrite F'.valid_lb_real; [|now rewrite F.real_correct, F.zero_correct]. split. { rewrite F.zero_correct. rewrite nat_of_P_xO. rewrite pow_sqr. change (x * x)%R with (Rsqr x). simpl. apply pow_le. apply Rle_0_sqr. } revert Hpow_UP. unfold le_upper. rewrite Hmax. rewrite (proj1 (F.abs_correct _)). xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. xreal_tac2; [now simpl|]. simpl. intros H. assert (Hr: (0 <= Rmax (Rabs r0) r1)%R). { apply Rmax_case. { apply Rabs_pos. } apply Hx0. } apply Rle_trans with (2 := H). destruct (Rle_or_lt x 0) as [Hx|Hx]. { change (Pmult_nat n 2) with (nat_of_P (xO n)). rewrite nat_of_P_xO at 1. rewrite pow_sqr. rewrite <- (Rmult_opp_opp x x). rewrite <- pow_sqr, <- nat_of_P_xO. apply pow_incr. split. { rewrite <- Ropp_0. now apply Ropp_le_contravar. } apply Rle_trans with (2 := Rmax_l _ _). rewrite Rabs_left1. { now apply Ropp_le_contravar. } apply Hx0. } apply pow_incr. split. { now apply Rlt_le. } now apply Rle_trans with (2 := Rmax_r _ _). } rewrite Vxl, Vxu. now split; xreal_tac2; simpl; rewrite Rmult_1_r. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval