Pierre Jouvelot (Nov 25 2022 at 20:05): 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?
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.
Pierre Jouvelot has marked this topic as resolved.
Last updated: May 31 2023 at 03:30 UTC