Zulip Chat Archive

Stream: new members

Topic: equality of sums of functions


Yakov Pechersky (Aug 26 2020 at 13:28):

If I have a goal of

 (λ (l : fin (n + 2)), ...) =  λ (l : fin (n + 2)), ...

what's the tactic step to get back to a goal of

 ( (l : fin (n + 2)), ...) =   (l : fin (n + 2)), ...

Yakov Pechersky (Aug 26 2020 at 13:28):

Basically, the reverse of a congr step.

Kenny Lau (Aug 26 2020 at 13:30):

don't get there to begin with

Kenny Lau (Aug 26 2020 at 13:30):

use congr' 1

Kenny Lau (Aug 26 2020 at 13:31):

think about it. what you ask doesn't make sense logically

Kenny Lau (Aug 26 2020 at 13:31):

the sum being equal doesn't imply the functions being equal

Yakov Pechersky (Aug 26 2020 at 13:35):

I'm finding it cumbersome to rearrange terms inside a sum of sums. So I was hoping to unwrap two levels down, move things around on the LHS, then revert ...; refine congr_fun _ and then place the sums back.

Kevin Buzzard (Aug 26 2020 at 13:36):

Aren't you asking the following question: "How do I prove that if \sum f(n) = \sum g(n) then f = g"? The answer is "it can't be done because it's not true in general"

Reid Barton (Aug 26 2020 at 13:37):

It seems like your question is backwards, and so the answer is congr

Yakov Pechersky (Aug 26 2020 at 13:38):

I think I get what you mean

Yakov Pechersky (Aug 26 2020 at 13:39):

So I'll have to stick with simp_rw [mul_comm, mul_assoc] etc


Last updated: Dec 20 2023 at 11:08 UTC