Stream: new members

Topic: Rw inside a sum

Riccardo Brasca (Oct 15 2020 at 12:41):

Hi all, I have a s : finset a for some a : Type and a function f : a → b, where (b : Type) [add_comm_monoid b], so I can consider the sum ∑ x in s, f x. I also have another function g: a → b and I now that $f = g$ on $s$, but not in general. I want to prove that ∑ x in s, f x = ∑ x in s, g x. How can I prove this? It is something like a rw I guess, but I do not know how tell Lean to use the fact that $f = g$ on $s$ (actually I am not even able to write this in Lean, maybe something like x ∈ s → f x = g x, where x : a?). Thank you!

Anne Baanen (Oct 15 2020 at 12:42):

I think you want to apply finset.sum_congr.

Riccardo Brasca (Oct 15 2020 at 12:45):

Oh, thank you! For some reasons I tried to do it by myself without looking into the library.

Riccardo Brasca (Oct 15 2020 at 12:47):

Is there a reason of having in finset.sum_congr two finsets s1 and s2 with the assumption that s1 = s2?

Anne Baanen (Oct 15 2020 at 12:50):

I guess it's just to make it more general, making it possible to vary the set being summed.

Anne Baanen (Oct 15 2020 at 12:51):

But usually I need finset.sum_bij if s1 and s2 are not literally the same.

Johan Commelin (Oct 15 2020 at 12:56):

sum_bij is what you need if s1 and s2 are not finsets of the same type.

Johan Commelin (Oct 15 2020 at 12:56):

Note that there is even sum_bij_ne_zero which is the most awesome version of all (-;

Johan Commelin (Oct 15 2020 at 12:57):

And fintype.sum_congr if you are looking at two sums over a fintype (i.e. s1 = s2 = (univ : finset X))

Riccardo Brasca (Oct 15 2020 at 12:58):

Wow, sum_bij_ne_zero is scary :grinning:

Kevin Buzzard (Oct 15 2020 at 13:19):

@Riccardo Brasca the difficulty of some of this finite stuff was quite surprising to me. I am pretty sure that when I arrived on the scene in 2017 trying to do 1st year UG problem sheets, if all the machinery of finite sets and finite types hadn't been there I would have been completely lost and unable to use anything. But people like Mario had built this stuff before. How difficult can a finite set be? Well, data.finset was thousands of lines long in 2017, and it imported data.multiset which was also thousands of lines long -- I once printed out data.multiset onto 28 pages and would sit and read it in the bath trying to fathom out what was going on.

Riccardo Brasca (Oct 15 2020 at 13:20):

Yes, the machinery is quite confusing at the beginning, but I guess one gets used to it.

Kevin Buzzard (Oct 15 2020 at 13:20):

It was only much later that I realised that the point was not to see how it was built, it was to understand what the main definitions were (these files are 98% theorems)

Riccardo Brasca (Oct 15 2020 at 13:20):

And probably sooner or later I will have to read it in details too.

Kevin Buzzard (Oct 15 2020 at 13:20):

and to start to understand what kind of things are available

Kevin Buzzard (Oct 15 2020 at 13:21):

Here is the way to read a file in mathilb. First, check to see if there is a module docstring. If there is, then read all of that first.

Kevin Buzzard (Oct 15 2020 at 13:21):

And if there isn't then I guess you could even just make one yourself after you finished reading it.

Kevin Buzzard (Oct 15 2020 at 13:22):

Secondly try and find all the definitions and all the instances (use search functionality of your viewer)

Kevin Buzzard (Oct 15 2020 at 13:22):

Hopefully each one should have a docstring. They should tell you the main objects you're working with in this file.

Kevin Buzzard (Oct 15 2020 at 13:23):

Then scan the theorems to work out the normal form for each new concept, i.e how things are expressed on the right hand side of simp lemmas.

Kevin Buzzard (Oct 15 2020 at 13:23):

because simp moves things from left to right

Kevin Buzzard (Oct 15 2020 at 13:23):

and then scan the theorems, you probably won't see anything surprising, so skip the proofs.

Kevin Buzzard (Oct 15 2020 at 13:24):

Then if there wasn't a module docstring, pop back to the top and write one.

Scott Morrison (Oct 15 2020 at 21:28):

Oh! There is a tactic for this!

Scott Morrison (Oct 15 2020 at 21:30):

https://leanprover-community.github.io/mathlib_docs/tactics.html#apply_congr

Riccardo Brasca (Oct 16 2020 at 14:27):

Very nice, this is exactly what I wanted! :)

Last updated: May 08 2021 at 18:17 UTC