## Stream: Is there code for X?

### Topic: telescoping sums

#### Scott Morrison (Jun 26 2020 at 11:10):

lemma telescope {M : Type*} [add_comm_group M] (f : ℕ → M) (n : ℕ) :
∑ i in range n, (f (i+1) - f i) = f n - f 0 :=
sorry


I didn't look too hard for this one: I gave up after searching for telescop and only finding something silly involving nat subtraction. :-)

#### Johan Commelin (Jun 26 2020 at 11:17):

I think @Sebastien Gouezel had something similar a little while ago

#### Jalex Stark (Jun 26 2020 at 12:24):

import tactic
open_locale big_operators
open finset

lemma telescope {M : Type*} [add_comm_group M] (f : ℕ → M) (n : ℕ) :
∑ i in range n, (f (i+1) - f i) = f n - f 0 :=
by { apply sum_range_induction; abel, simp }


#### Johan Commelin (Jun 26 2020 at 12:34):

git grep -n "(f (i+1) - f i) = f n - f 0"
src/algebra/big_operators.lean:560:  ∑ i in range n, (f (i+1) - f i) = f n - f 0 :=


#### Johan Commelin (Jun 26 2020 at 12:35):

It's called sum_range_sub_of_monotone...

#### Jalex Stark (Jun 26 2020 at 12:35):

that's the one scott found. it's about nats.

Aaah, I see.

#### Jalex Stark (Jun 26 2020 at 12:36):

i'm working to PR the version for groups right now

#### Patrick Massot (Jun 26 2020 at 12:36):

As you can see from the word monotone which seems completely useless

#### Johan Commelin (Jun 26 2020 at 12:36):

@Jalex Stark Don't forget to tag it with @[to_multiplicative] :stuck_out_tongue_wink:

#### Sebastien Gouezel (Jun 26 2020 at 12:36):

Patrick Massot said:

As you can see from the word monotone which seems completely useless

... but of course isn't.

#### Jalex Stark (Jun 26 2020 at 12:38):

i don't understand how to_additive works. is there also a thing called to_multiplicative?

#### Johan Commelin (Jun 26 2020 at 12:38):

No, hence the :stuck_out_tongue_wink:

#### Johan Commelin (Jun 26 2020 at 12:39):

My point is, there is a multiplicative version of this lemma. Prove that, and @[to_additive] will give you the version we are discussing here.

#### Johan Commelin (Jun 26 2020 at 12:39):

Except that the additive version would then and up with f n + - f 0...

#### Johan Commelin (Jun 26 2020 at 12:39):

Because the multiplicative version will have f n * (f 0)^-1

#### Jalex Stark (Jun 26 2020 at 12:40):

I'll do what's done for range_induction, and write both explicitly but have the proof of the additive case be a call to the multiplicative one

#### Jalex Stark (Jun 26 2020 at 12:40):

why don't we have has_div for groups?

#### Johan Commelin (Jun 26 2020 at 12:40):

I still don't really know

#### Jalex Stark (Jun 26 2020 at 12:44):

does it make sense to import tactic.group in algebra.big_operators?

#### Johan Commelin (Jun 26 2020 at 12:44):

My initial reaction would be, yes please

#### Johan Commelin (Jun 26 2020 at 12:45):

Maybe the big_ops file should be split?

#### Jalex Stark (Jun 26 2020 at 12:45):

it is pretty large

#### Johan Commelin (Jun 26 2020 at 12:45):

I can imagine that tactics like abel and ring want to know about finset.{prod,sum}

#### Reid Barton (Jun 26 2020 at 12:58):

Does it make sense for to_additive to learn to turn x * y^-1 into x - y?

#### Jalex Stark (Jun 26 2020 at 12:59):

we should have has_div for group and to_additive should learn to turn x/y into x-y

#3184

#### Reid Barton (Jun 26 2020 at 13:07):

I feel like this is a bad solution.

#### Reid Barton (Jun 26 2020 at 13:07):

Type classes are hard enough already.

#### Jalex Stark (Jun 26 2020 at 13:11):

I believe you, but I don't understand

#### Reid Barton (Jun 26 2020 at 13:13):

It's just solving the problem in the wrong way. For instance now you will also have to add a bunch of lemmas to deal with this strange new / for groups.

#### Reid Barton (Jun 26 2020 at 13:14):

Plus, no one really wants / for groups in the first place, I think.

#### Reid Barton (Jun 26 2020 at 13:16):

You're gaining notation that you don't want, and then incurring all the headaches of type classes as a cost.