Zulip Chat Archive

Stream: general

Topic: Why is there a def for `geom_sum`?


Scott Morrison (May 13 2022 at 07:17):

src#geom_sum is a definition def geom_sum (x : α) (n : ℕ) := ∑ i in range n, x ^ i. Is there any reason to have this definition, instead of just stating the results about the sum itself? Looking through mathlib, it seems that everywhere that people need to use geom_sum, they need to begin by rewriting by geom_sum_def, which seems rather annoying.

It also means that none of the simp lemmas actually apply until you rewrite things in terms of geom_sum, which seems tedious: I'd say if there's reason to keep the definition we probably should restate all its simp lemmas with geom_def unfolded.

Kevin Buzzard (May 13 2022 at 07:19):

Just to remark that I've been using geometric sums in LTE and I didn't use this definition once

Johan Commelin (May 13 2022 at 07:19):

Kevin, did you use finite or infinite geometric sums?

Johan Commelin (May 13 2022 at 07:19):

@Scott Morrison would it help if we make it an abbreviation?

Kevin Buzzard (May 13 2022 at 07:19):

Aah, infinite ones. Is it something to do with ticking off something on the UG list?

Scott Morrison (May 13 2022 at 07:21):

I tried abbreviation, and it doesn't help with the @[simp] lemma problem, because that is working syntactically, so it can't see that explicit sums are geom_sums.

Eric Wieser (May 13 2022 at 07:22):

Yeah, my first thought was "this might be needed by undergrad.yml"

Scott Morrison (May 13 2022 at 07:22):

Can I just make it notation?

Eric Wieser (May 13 2022 at 07:22):

I don't even think there's any point having the notation

Scott Morrison (May 13 2022 at 07:22):

Is there a way to expand geom_sum x n as ∑ i in range n, x ^ i?

Scott Morrison (May 13 2022 at 07:23):

Mostly I just want to notation temporarily to check that the file behaves as expected, without actually having to rewrite it :-)

Scott Morrison (May 13 2022 at 07:25):

Does anyone know if this notation is possible, without a token between the x and n? I can't find an example in mathlib.

Eric Wieser (May 13 2022 at 07:25):

notation `geom_sum` x := λ n, (range n).sum ((^) x) maybe?

Scott Morrison (May 13 2022 at 07:25):

Let me try

Eric Wieser (May 13 2022 at 07:25):

If you can deal with one lingering lambda

Scott Morrison (May 13 2022 at 07:26):

Doesn't seem to work anyway.

Scott Morrison (May 13 2022 at 07:27):

Every geom_sum x n gives a function expected at x term has type ...

Scott Morrison (May 13 2022 at 07:28):

Maybe notation `geom_sum` x:2000 := (λ n, (range n).sum ((^) x))

Scott Morrison (May 13 2022 at 07:29):

Still too much lambda, oh well, I'll bite the bullet and write them out.

Kyle Miller (May 17 2022 at 13:36):

I wonder if it would be worth having an elab_inline attribute, so then we could have synonyms that don't get in the way of rewrites, and we wouldn't need to abuse notation?

Kyle Miller (May 17 2022 at 13:39):

For the "too much lambda" problem, maybe there could be a special elab_beta identity function that causes the elaborator to do beta reduction using its first two arguments.


Last updated: Dec 20 2023 at 11:08 UTC