proposition: Lemma biv_sound_telescoping (biv_cf0 : int -> int -> R := fun _ _ => 0) (s : nat := size Pseq) (r : nat := foldr maxn 0%N (map size Pseq)) (P : (int -> int -> R) -> int -> int -> R := biv_horner_seqop2 Pseq) (U : int -> int -> R := fun n k => \sum_(a <= m < k + b :> int) u n k m) (n k : int) (range_correct : a <= k + b) (PeqDQ : forall (n k m : int), not_D n k m -> P (pfun2 u m) n k = Q u n k (int.shift 1 m) - Q u n k m) : P U n k = Q u n k (k + b) - Q u n k a + \sum_(a <= m < k + b :> int | ~~ not_D n k m) (P (pfun2 u m) n k - (Q u n k (int.shift 1 m) - Q u n k m)) + \sum_(0 <= i < s) \sum_(0 <= j < size (nth [::] Pseq i)) \sum_(0 <= l < i) nth biv_cf0 (nth [::] Pseq i) j n k * u (int.shift j n) (int.shift i k) (int.shift l (k + b)).
proof: Proof. set PUnk := P U n k. set DeltaQ := (X in PUnk = X + _ + _). set exceptions := (X in PUnk = DeltaQ + X + _). set excess := (X in PUnk = DeltaQ + exceptions + X). set rhs := (X in _ = X). have PUnk_value : PUnk = \sum_(0 <= i < s) \sum_(0 <= j < size (nth [::] Pseq i)) nth biv_cf0 (nth [::] Pseq i) j n k * (\sum_(a <= m < k + b :> int) u (int.shift j n) (int.shift i k) m + \sum_(k + b <= m < k + b + Posz i :> int) u (int.shift j n) (int.shift i k) m). rewrite /PUnk /P /U biv_horner_seqop2P. rewrite big_nat_cond [in RHS]big_nat_cond. apply: eq_bigr => i. rewrite andbT -/s. move/andP=> [_ i_bound]. apply: eq_bigr => j _. congr (_ * _). rewrite -big_cat_int ?cprD //=. by rewrite !int.shift2Z addrAC. have {}PUnk_value : PUnk = \sum_(a <= m < k + b :> int) \sum_(0 <= i < s) \sum_(0 <= j < size (nth [::] Pseq i)) nth biv_cf0 (nth [::] Pseq i) j n k * u (int.shift j n) (int.shift i k) m + \sum_(0 <= i < s) \sum_(0 <= j < size (nth [::] Pseq i)) \sum_(0 <= m < i) nth biv_cf0 (nth [::] Pseq i) j n k * u (int.shift j n) (int.shift i k) (int.shift m (k + b)). rewrite {}PUnk_value. do 2! (rewrite [in RHS]exchange_big /= -big_split /=; apply: eq_bigr => ? _). rewrite -2!mulr_sumr -mulrDr. congr (_ * (_ + _)). rewrite -{1}[k + b]add0r big_addz /=. rewrite !int.shift2Z addrAC subrr add0r eq_big_int_nat /=. by apply: eq_bigr=> i; rewrite int.shift2Z [Posz i + _]addrC. set sum1 := (X in PUnk = X + _) in PUnk_value. have sum1_value : sum1 = \sum_(a <= m < k + b :> int) P (pfun2 u m) n k. apply: eq_bigr => m _. by rewrite /P /U biv_horner_seqop2P -/s /pfun2. rewrite {}sum1_value {sum1} in PUnk_value. have split_sum_of_P : \sum_(a <= m < k + b :> int) P (pfun2 u m) n k = \sum_(a <= m < k + b :> int | not_D n k m) (Q u n k (int.shift 1 m) - Q u n k m) + \sum_(a <= m < k + b :> int | ~~ not_D n k m) P (pfun2 u m) n k. rewrite (bigID (not_D n k)) /=. congr (_ + _). apply: eq_bigr => m not_D_m. by apply: PeqDQ. rewrite {}split_sum_of_P in PUnk_value. rewrite {}PUnk_value. congr (_ + _). rewrite -[X in _ + X]add0r addrA. pose complement := \sum_(a <= m < k + b :> int | ~~ not_D n k m) (Q u n k (int.shift 1 m) - Q u n k m). rewrite -[X in _ + X + _](subrr complement). rewrite addrA -addrA. congr (_ + _). rewrite -(bigID (not_D n k) predT) /=. by rewrite telescopez. rewrite -[complement]mul1r -mulNr. rewrite /complement big_distrr /=. rewrite -big_split /=. rewrite /exceptions. apply: eq_bigr => m _. by rewrite mulNr mul1r addrC. Qed.
imports: mathcomp(all_ssreflect all_algebra) shift bigopz