Stream: math-comp devs

Topic: sumn_set_nthE


view this post on Zulip Pierre Jouvelot (Nov 25 2022 at 20:05):

I had to prove the following lemma, and thought it might interesting to extend bigop with it?

Lemma sumn_set_nthE (s : seq nat) x0 n x:
  let: x' := if n < size s
             then x
             else nth x0 s n + sumn (ncons (n - size s) x0 [::x]) in
  sumn (set_nth x0 s n x)  = sumn s + x' - nth x0 s n.

Would a PR be useful for this simple lemma?

view this post on Zulip Pierre Jouvelot (Nov 26 2022 at 10:00):

A nicer version is the following :

Lemma sumn_set_nthE (s : seq nat) x0 n x :
  let x' := x + (size s <= n) * (nth x0 s n + (n - size s) * x0) in
  sumn (set_nth x0 s n x)  = sumn s + x' - nth x0 s n.

which comes with the side lemma sumn_nconsE:

Lemma sumn_nconsE n s (x0 : nat) : sumn (ncons n x0 s) = n * x0 + sumn s.

Last updated: Jan 29 2023 at 16:02 UTC