proposition: Lemma isol_rec_correct : forall c l d a b q acc, a < b -> (0 < d)%N -> q != 0 -> (size l <= d.+1)%N -> q = \sum_(i < d.+1) l`_i *: bernp a b d i -> read (horner q) acc -> head_root (horner q) acc -> read (horner q) (isol_rec c d a b l acc).
proof: Proof. elim=> [// | c IH]. move=> l d a b q acc altb dn0 qn0 sld qq ht hh /=. have anb : a != b by rewrite neq_lt altb. case tst : (changes (seqn0 l)) => [/= | [/= | nc]]. by split=> //; apply (ch0_correct altb qn0 qq). by split=> //; apply (ch1_correct sld altb qq). have help : 2%:R^-1 = ((a + b) / 2%:R - a)/(b - a). rewrite -[X in _ / _ - X]double_half -/(half (a + b)) half_lin half_lin1. rewrite opprD addrCA !addrA addNr add0r /half mulrAC mulfV ?mul1r //. by rewrite subr_eq0 eq_sym. have help2 : 2%:R^-1 = (b - (a + b)/2%:R)/(b - a). rewrite -[X in X - _ / _]double_half -/(half(a + b)) half_lin half_lin1. rewrite opprD addrCA addrK [- _ + _]addrC /half mulrAC mulfV ?mul1r //. by rewrite subr_eq0 eq_sym. have qh' : q = \sum_(i < d.+1) (mkseq (dicho' 2%:R^-1 2%:R^-1 [eta nth 0 l]) d.+1)`_i *: bernp a ((a + b) / 2%:R) d i. have qt : forall i : 'I_d.+1, true -> (mkseq (dicho' 2%:R^-1 2%:R^-1 [eta nth 0 l]) d.+1)`_i *: bernp a ((a + b) / 2%:R) d i = dicho' ((b - half (a + b))/(b - a)) ((half (a + b) - a)/(b - a)) [eta nth 0 l] i *: bernp a ((a + b) / 2%:R) d i. by move => [i ci] _; rewrite -help -help2 /= nth_mkseq. rewrite (eq_bigr _ qt); apply: dicho'_correct => //. rewrite -[X in _ == X]double_half half_lin; apply/negP. by move/eqP/half_inj/addrI/eqP; rewrite eq_sym; apply/negP. have qh : q = \sum_(i < d.+1) (mkseq (dicho 2%:R^-1 2%:R^-1 d [eta nth 0 l]) d.+1)`_i *: bernp ((a + b) / 2%:R) b d i. have qt : forall i : 'I_d.+1, true -> (mkseq (dicho 2%:R^-1 2%:R^-1 d [eta nth 0 l]) d.+1)`_i *: bernp ((a + b) / 2%:R) b d i = dicho ((b - half (a + b))/(b - a)) ((half (a + b) - a)/(b - a)) d [eta nth 0 l] i *: bernp ((a + b) / 2%:R) b d i. by move => [i ci] _; rewrite -help -help2 /= nth_mkseq. rewrite (eq_bigr _ qt); apply: dicho_correct => //. rewrite -[X in _ == X]double_half half_lin; apply/negP. by move/eqP/half_inj/addIr/eqP; apply/negP. apply: (IH) => //. by case/andP : (mid_between altb) => it _; exact it. by rewrite size_mkseq. case ts0: (dicho 2%:R^-1 2%:R^-1 d [eta nth 0 l] 0 == 0). rewrite /=; split. apply/eqP; rewrite -(bernp_first_coeff0 _ dn0 qh). by rewrite nth_mkseq. rewrite -[X in _ == X]double_half half_lin; apply/negP. by move/eqP/half_inj/addIr/eqP; apply/negP. apply: IH => //. by case/andP : (mid_between altb) => _ it; exact it. by rewrite size_mkseq. apply: IH => //. by case/andP : (mid_between altb) => _ it; exact it. by rewrite size_mkseq. case ts0: (dicho 2%:R^-1 2%:R^-1 d [eta nth 0 l] 0 == 0); first by []. apply: isol_rec_head_root. rewrite -(bernp_first_coeff0 _ dn0 qh); last first. rewrite -[X in _ == X]double_half half_lin; apply/negP. by move/eqP/half_inj/addIr/eqP; apply/negP. by rewrite nth_mkseq; move/negbT: ts0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc