proposition: Lemma sound_telescoping (cf0 : int -> R := fun _ => 0) (r : nat := size Pseq) (P : (int -> R) -> int -> R := horner_seqop Pseq) (U : int -> R := fun n => \sum_(a <= k < n + b :> int) u n k) (n : int) (range_correct : a <= n + b) (PeqDQ : forall (n k : int), not_D n k -> P (u ^~ k) n = Q u n (int.shift 1 k) - Q u n k) : P U n = Q u n (n + b) - Q u n a + \sum_(a <= k < n + b :> int | ~~ not_D n k) (P (u ^~ k) n - (Q u n (k + 1) - Q u n k)) + \sum_(0 <= i < r) \sum_(0 <= j < i) nth cf0 Pseq i n * u (int.shift i n) (int.shift j (n + b)).
proof: Proof. pose cf_P := nth cf0 Pseq. have step : P U n = \sum_(0 <= i < r) \sum_(a <= k < int.shift i n + b :> int) cf_P i n * u (int.shift i n) k. by rewrite /P horner_seqopP; apply: eq_bigr=> j _; rewrite /U mulr_sumr. pose t1 := \sum_(0 <= i < r) \sum_(a <= k < int.shift r n + b :> int) cf_P i n * u (int.shift i n) k. pose t2 := \sum_(0 <= i < r) \sum_(int.shift i n + b <= k < int.shift r n + b :> int) cf_P i n * u (int.shift i n) k. have {}step : P U n = t1 - t2. apply/eqP; rewrite eq_sym subr_eq; apply/eqP; rewrite {}step -big_split /=. rewrite [LHS]big_seq_cond [RHS]big_seq_cond; apply: eq_bigr=> i; simpl in i. rewrite andbT mem_index_iota; case/andP=> _ hi. rewrite -big_cat_int //= !int.shift2Z. - by apply: le_trans range_correct _; rewrite lerD2r lerDl. - by rewrite lerD2r lerD2l ltW. have t1_step : t1 = \sum_(a <= k < int.shift r n + b :> int) \sum_(0 <= i < r) cf_P i n * u (int.shift i n) k. by rewrite /t1 [in LHS]exchange_big. pose t11 := \sum_(a <= k < n + b :> int) \sum_(0 <= i < r) cf_P i n * u (int.shift i n) k. have t11_step : t11 = \sum_(a <= k < n + b :> int | not_D n k) (Q u n (int.shift 1 k) - Q u n k) + \sum_(a <= k < n + b :> int | ~~ not_D n k) \sum_(0 <= i < r) cf_P i n * u (int.shift i n) k. rewrite /t11. rewrite (bigID (fun k => not_D n k)) /=; congr (_ + _). rewrite [LHS]big_seq_cond [RHS]big_seq_cond; apply: eq_bigr=> i; simpl in i. by case/andP=> _ hi; rewrite -PeqDQ // /P horner_seqopP. have {}t11_step : t11 = Q u n (n + b) - Q u n a - \sum_(a <= k < n + b :> int | ~~ not_D n k) (Q u n (int.shift 1 k) - Q u n k) + \sum_(a <= k < n + b :> int | ~~ not_D n k) \sum_(0 <= i < r) cf_P i n * u (int.shift i n) k. rewrite {}t11_step; congr (_ + _). rewrite -(telescopez (Q u n)) //. by rewrite [X in _ = X - _](bigID (fun k => not_D n k)) /= -addrA subrr addr0. have {}t1_step : t1 = t11 + \sum_(n + b <= k < int.shift r n + b :> int) \sum_(0 <= i < r) cf_P i n * u (int.shift i n) k. by rewrite t1_step /t11 -big_cat_int // lerD2r int.shift2Z cprD. rewrite {}step {}t1_step {}t11_step. rewrite -1![RHS]addrA -3![LHS]addrA; congr (_ + _). rewrite -sumrN [LHS]addrA -big_split /=; congr (_ + _). rewrite [n + b]addrC [LHS]big_seq_cond [RHS]big_seq_cond; apply: eq_bigr=> i _. by rewrite addrC /P horner_seqopP. rewrite exchange_big /= -sumrN -big_split /=. rewrite [LHS]big_seq_cond [RHS]big_seq_cond; apply: eq_bigr=> i /andP []. rewrite mem_index_iota; case/andP=> _ hi _; rewrite !int.shift2Z. have hl : n + b <= n + i + b by rewrite lerD2r lerDl. have hr : n + i + b <= n + r + b by rewrite lerD2r lerD2l ltW. rewrite (big_cat_int _ _ _ hl hr) {hl hr} addrK [n + i + b]addrAC big_addz2l /=. rewrite eq_big_int_nat /=; apply: eq_bigr=> ? _. by rewrite int.shift2Z [n + b + _]addrC. Qed.
imports: mathcomp(all_ssreflect all_algebra) shift bigopz