proposition: Lemma Fpower_pos_up_correct : forall prec x n, F.valid_ub x = true -> le_upper (Xreal 0) (F.toX x) -> F.valid_ub (Fpower_pos_UP prec x n) = true /\ le_upper (Xpower_int (F.toX x) (Zpos n)) (F.toX (Fpower_pos_UP prec x n)).
proof: Proof. intros prec x n Vx Hx. set (p := Fpower_pos_UP prec x n). cut (F.valid_ub p = true /\ le_upper (Xreal 0) (F.toX p) /\ le_upper (Xpower_int (F.toX x) (Z.pos n)) (F.toX p)). { now simpl. } unfold p; clear p. revert x Vx Hx; induction n; intros x Vx Hx; last first. { do 2 (split; [now simpl|]). simpl. xreal_tac x. now simpl; rewrite Rmult_1_r; right. } { assert (Vxx : F.valid_ub (F.mul_UP prec x x) = true). { now apply F'.mul_UP_correct; left. } assert (Hxx : le_upper (Xreal 0) (F.toX (F.mul_UP prec x x))). { apply (le_upper_trans _ (Xmul (F.toX x) (F.toX x))). { now xreal_tac2; apply Rmult_le_pos. } now apply F'.mul_UP_correct; left. } do 2 (split; [now apply (IHn _ Vxx Hxx)|]). generalize (proj2 (proj2 (IHn _ Vxx Hxx))). apply le_upper_trans. generalize (Xpower_int_correct (Z.pos n) (F.toX (F.mul_UP prec x x))). xreal_tac2; (case (Xpower_int _ _); [intros _; exact I|]); intros r1' Hr1'; [now simpl|]. rewrite <-Hr1'. xreal_tac2. { cut (le_upper (Xnan * Xnan)%XR (Xreal r)); [now simpl|]. rewrite <-X0, <-X. now apply F'.mul_UP_correct; left. } simpl. rewrite Pos2Nat.inj_xO. rewrite pow_sqr. apply pow_incr; split; [now apply Rmult_le_pos|]. change (_ <= _)%R with (le_upper (Xmul (Xreal r0) (Xreal r0)) (Xreal r)). rewrite <-X0, <-X. now apply F'.mul_UP_correct; left; rewrite <-X0 in Hx. } assert (Vxx : F.valid_ub (F.mul_UP prec x x) = true). { now apply F'.mul_UP_correct; left. } assert (Hxx : le_upper (Xreal 0) (F.toX (F.mul_UP prec x x))). { apply (le_upper_trans _ (Xmul (F.toX x) (F.toX x))). { now xreal_tac2; apply Rmult_le_pos. } now apply F'.mul_UP_correct; left. } elim (F'.mul_UP_correct prec x (Fpower_pos_UP prec (F.mul_UP prec x x) n)). { intros Vu Hu. split; [now simpl; rewrite Vu|]. split. { revert Hu; apply le_upper_trans. do 2 xreal_tac2. apply Rmult_le_pos; [now simpl|]. change (_ <= _)%R with (le_upper (Xreal 0) (Xreal r0)). rewrite <-X0. now apply IHn. } revert Hu. apply le_upper_trans. revert Hx; xreal_tac2; [now simpl|]; intro Hr. xreal_tac2. simpl. rewrite Pmult_nat_mult, Nat.mul_comm. apply (Rmult_le_compat_l _ _ _ Hr). rewrite pow_sqr. change (_ <= _)%R with (le_upper (Xreal ((r * r) ^ Pos.to_nat n)) (Xreal r0)). rewrite <-X0. apply (le_upper_trans _ (Xpower_int (F.toX (F.mul_UP prec x x)) (Z.pos n))). { generalize (Xpower_int_correct (Z.pos n) (F.toX (F.mul_UP prec x x))). xreal_tac2; (case (Xpower_int _ _); [intros _; exact I|]); intros r1' Hr1'; [now simpl|]. rewrite <-Hr1'. apply pow_incr; split; [now apply Rmult_le_pos|]. change (_ <= _)%R with (le_upper (Xmul (Xreal r) (Xreal r)) (Xreal r1)). rewrite <-X, <-X1; apply F'.mul_UP_correct. left. unfold F.is_non_neg. now rewrite F'.valid_ub_real, X; [|rewrite F.real_correct, X]. } now apply IHn. } left. split; [now simpl|]. now split; now apply IHn. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval