proposition: Lemma pi4_correct : forall prec, contains (I.convert (pi4 prec)) (Xreal (PI/4)).
proof: Proof. intros prec. rewrite Machin_4_5_239. unfold pi4, constant_getter. set (n := Z.abs_nat _). unfold pi4_seq, constant_generator. generalize xH at 1. induction n as [|n]. 2: intros p ; apply IHn. simpl. intros p. generalize (F.PtoP (p * 31)). clear prec p. intros prec. assert (H: forall p, (2 <= p <= 256)%Z -> contains (I.convert (atan_fast0 prec (I.inv prec (I.fromZ_small p)))) (Xreal (atan (/ IZR p)))). intros p Hp. apply atan_fast0_correct. rewrite Rabs_pos_eq. apply Rle_Rinv_pos. apply Rlt_0_2. now apply IZR_le. apply Rlt_le, Rinv_0_lt_compat. apply IZR_lt. now apply Z.lt_le_trans with 2%Z. replace (Xreal (/ IZR p)) with (Xinv (Xreal (IZR p))). apply I.inv_correct. apply I.fromZ_small_correct. rewrite Z.abs_eq. apply Hp. now apply Z.le_trans with 2%Z. unfold Xinv'. simpl. case is_zero_spec ; try easy. intros H. apply (eq_IZR p 0) in H. elim Hp. now rewrite H. unfold pi4_gen. apply (I.sub_correct _ _ _ (Xreal _) (Xreal _)). rewrite Rmult_comm. replace (Xreal (atan (/ 5) * 4)) with (Xreal (atan (/ 5)) * Xreal 2 * Xreal 2)%XR; [|simpl; apply f_equal; ring]. do 2 apply I.mul2_correct. now apply (H 5%Z). now apply (H 239%Z). Qed.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float