proposition: Theorem ComputeBound_correct prec pi p : pi >:: p -> J.extension (PolR.horner tt p) (ComputeBound prec pi).
proof: Proof. move=> Hnth X x Hx; rewrite /ComputeBound. case E: (2 < Pol.size pi); last by apply: Bnd.ComputeBound_correct. case Eb: I.bounded; last by apply: Bnd.ComputeBound_correct. simpl. set A0 := Pol.nth pi 0. set A1 := Pol.nth pi 1. set A2 := Pol.nth pi 2. set Q3 := Pol.tail 3 pi. pose a0 := PolR.nth p 0. pose a1 := PolR.nth p 1. pose a2 := PolR.nth p 2. pose q3 := PolR.tail 3 p. have Hi3: Pol.size pi = 3 + (Pol.size pi - 3) by rewrite subnKC //. suff->: PolR.horner tt p x = (Rplus (Rplus (Rminus a0 (Rdiv (Rsqr a1) (Rplus (Rplus a2 a2) (Rplus a2 a2)))) (Rmult a2 (Rsqr (Rplus x (Rdiv a1 (Rplus a2 a2)))))) (Rmult (powerRZ x 3) (PolR.horner tt q3 x))). have Hnth3 : Q3 >:: q3 by apply Pol.tail_correct. apply: J.add_correct; [apply: J.add_correct; [apply: J.sub_correct; [apply: Hnth |apply: J.div_correct; [apply: J.sqr_correct; apply: Hnth |apply: J.add_correct; apply: J.add_correct; apply: Hnth]] |apply: J.mul_correct; [apply: Hnth |apply: J.sqr_correct; apply: J.add_correct; [done |apply: J.div_correct; [apply: Hnth|apply: J.add_correct; apply: Hnth ]]]] |apply: J.mul_correct; [exact: J.power_int_correct|exact: Pol.horner_correct]]. rewrite 2!PolR.hornerE. rewrite (@big_nat_leq_idx _ _ _ (3 + (PolR.size p - 3))). rewrite big_mkord. rewrite 3?big_ord_recl -/a0 -/a1 -/a2 ![[the Monoid.law _ of Rplus] _]/= /q3 PolR.size_tail. set x0 := powerRZ x 0. set x1 := powerRZ x 1. set x2 := powerRZ x 2. set x3 := powerRZ x 3. set s1 := bigop _ _ _. set s2 := bigop _ _ _. have H4 : (a2 + a2 + (a2 + a2) <> 0)%R. intro K. move: Eb. have Hzero : contains (I.convert (I.add prec (I.add prec (Pol.nth pi 2) (Pol.nth pi 2)) (I.add prec (Pol.nth pi 2) (Pol.nth pi 2)))) (Xreal 0). rewrite -K. by apply: J.add_correct; apply: J.add_correct; apply: Hnth. case/(I.bounded_correct _) => _. case/(I.upper_bounded_correct _) => _. rewrite /I.bounded_prop. set d := I.div prec _ _. suff->: I.convert d = Inan. { by rewrite /not_empty; move/(_ (@ex_intro _ (fun _ => True) 0%R I)). } apply -> contains_Xnan. rewrite -(Xdiv_0_r (Xsqr (Xreal a1))). apply: I.div_correct =>//. apply: I.sqr_correct. by apply: Hnth; rewrite Hi3. have H2 : (a2 + a2 <> 0)%R by intro K; rewrite K Rplus_0_r in H4. suff->: s1 = Rmult x3 s2. have->: Rmult a0 x0 = a0 by simpl; rewrite /x0 powerRZ_O Rmult_1_r. rewrite -!Rplus_assoc /Rminus; congr Rplus. rewrite /x1 /x2 /Rsqr. rewrite /=; field. split =>//. by rewrite -Rplus_assoc in H4. rewrite /s1 /s2 /x3; clear. rewrite Rmult_comm. rewrite big_mkord big_distrl. apply: eq_bigr=> i _. rewrite /PolR.tail /PolR.nth nth_drop. rewrite -!(pow_powerRZ _ 3). rewrite /= !Rmult_assoc; f_equal; ring. by rewrite addnC leq_subnK. move=> i /andP [Hi _]. by rewrite PolR.nth_default ?Rmult_0_l. Qed.
imports: Coq(ZArith Reals) Flocq(Raux) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Xreal Interval MathComp Datatypes Bound