Zulip Chat Archive

Stream: new members

Topic: Tactics for big operators


view this post on Zulip Walter Moreira (Jun 01 2020 at 02:44):

I'm playing with the big operators, and I'm having trouble finding the right tactics to operate on its elements. In the following dummy example, I'm guessing the first step will use some combination of sum_range_succ' (even though I haven't figured it out yet). But my main question is the second sorry. How can I apply some tactic like ring inside of the big operator?

import data.finset
import algebra.big_operators
import tactic

open_locale big_operators

example (R : Type*) [nonzero_comm_ring R] (n : ) (u v : R) (h : u * v = 1)
    :  i in finset.range (n + 2), u * v^i = u +  i in finset.range (n + 1), v^i :=
begin
calc
     i in finset.range (n + 2), u * v^i  = u +  i in finset.range (n + 1), u * v^(i + 1) : by sorry
    ... = u +  i in finset.range (n + 1), v^i : by sorry
end

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 02:53):

second step should be by simp only [pow_succ, mul_assoc, h, one_mul], possibly with pow_succ' and/or before mul_assoc.

view this post on Zulip Yury G. Kudryashov (Jun 01 2020 at 02:54):

In the first step the only difficulty with applying sum_range_succ' is that you have n + 2 while you need n + 1 + 1. The latter simplifies to the former but I'm not sure that they are defeq.

view this post on Zulip Johan Commelin (Jun 01 2020 at 02:57):

@Walter Moreira Another approach would be to start with rw finset.sum_congr rfl

view this post on Zulip Johan Commelin (Jun 01 2020 at 02:58):

After that it should be intros, straight_forward

view this post on Zulip Walter Moreira (Jun 01 2020 at 03:10):

Ah, I see. finset.sum_congr is exactly what I was looking for before embarking in the calc tactic. Thanks a lot!

By the way, is straight_forward a tactic? Or you just mean that it's easy from then on?

[Thanks @Yury G. Kudryashov for the hint on simp as well]

view this post on Zulip Johan Commelin (Jun 01 2020 at 03:11):

I mean it's easy. (It should be a tactic)

view this post on Zulip Johan Commelin (Jun 01 2020 at 03:11):

(Just like we've been wishing for schoolkid and undergrad....)

view this post on Zulip Johan Commelin (Jun 01 2020 at 03:16):

But using Yury's approach, you could probably get rid of the entire calc block, and prove it in a 1-line simp call.


Last updated: May 10 2021 at 00:31 UTC