# Zulip Chat Archive

## Stream: general

### Topic: finset.sum

#### Morenikeji Neri (Aug 06 2018 at 13:07):

I'm having some trouble proving this. Help would be much appreciated.

```
lean lemma sum_keji {α β : Type*} [add_comm_monoid α] {f : β → α}
(s : finset β) (g : Π a ∈ s, β) (h₁ : ∀ a ha, f a + f (g a ha) = 0)
(h₂ : ∀ a ha, g a ha ≠ a) (h₂ : ∀ a₁ a₂ ha₁ ha₂, g a₁ ha₁ = g a₂ ha₂ → a₁ = a₂)
(h₃ : ∀ a ha, ∃ b hb, g b hb = a) : s.sum f = 0 := sorry
```

#### Mario Carneiro (Aug 06 2018 at 13:54):

I guess you should first prove `g a ha ∈ s`

using the pigeonhole principle

#### Mario Carneiro (Aug 06 2018 at 13:55):

then the assumptions say that `g : s -> s`

is a bijection, so you can use `sum_bij`

to shift things around and cancel using `h1`

#### Mario Carneiro (Aug 06 2018 at 13:57):

Oh wait, you only have that it is an `add_comm_monoid`

, that's not enough to conclude

#### Mario Carneiro (Aug 06 2018 at 13:57):

you will be able to prove `s.sum f + s.sum f = 0`

#### Mario Carneiro (Aug 06 2018 at 14:01):

So for example if `α = Z/2Z`

, `β=Z/3Z`

, `s={0,1,2}`

, `f a = 1`

and `g n = n+1`

then we have a counterexample

#### Morenikeji Neri (Aug 06 2018 at 14:37):

sorry about that. I realized I missed out a few assumptions in the theorem.

It should read.

```
lean lemma sum_keji {α β : Type*} [add_comm_monoid α] {f : β → α}
(s : finset β) (g : Π a ∈ s, β) (h₁ : ∀ a ha, f a + f (g a ha) = 0)
(h₂ : ∀ a ha, g a ha ≠ a) (h₂ : ∀ a₁ a₂ ha₁ ha₂, g a₁ ha₁ = g a₂ ha₂ → a₁ = a₂)
(h₃ : ∀ a ha, ∃ b hb, g b hb = a) (h₄ : ∀ a ha, g a ha ∈ s) (h₅ : ∀ a ha, g (g a ha) (h₄ a ha) = a ) : s.sum f = 0 := sorry
```

#### Mario Carneiro (Aug 06 2018 at 14:40):

Oh I see, it's an involution

#### Mario Carneiro (Aug 06 2018 at 14:41):

You can prove this by complete induction on `s`

. Just take out `a`

and `g a ha`

in one step of the induction

#### Chris Hughes (Aug 06 2018 at 14:41):

Is there a short proof using lemmas?

#### Mario Carneiro (Aug 06 2018 at 14:41):

not with those hypotheses

#### Mario Carneiro (Aug 06 2018 at 14:42):

half of the work will be unpacking them

#### Mario Carneiro (Aug 06 2018 at 14:42):

I mean, the stuff about `sum`

is there but most of the work is showing that the reduced `g`

function is still an involution

#### Morenikeji Neri (Aug 06 2018 at 14:43):

yep!

#### Scott Morrison (Nov 24 2018 at 10:15):

Okay... after way too many inequalities (thanks, everyone!), I now have "the right" proof that $\sum_m \binom n m = 2^n$, based on reindexing sums and splitting off and joining single terms. This uses the following four lemmas:

lemma finset.sum.interval_split_left (n m : ℕ) (h₁ : n < m) (f : ℕ → β) : (interval n m).sum f = f n + (interval (n+1) m).sum f := lemma finset.sum.interval_split_right (n m : ℕ) (h : m > n) (f : ℕ → β) : (interval n m).sum f = (interval n (m-1)).sum f + f (m-1) := lemma finset.sum.interval_reindex_left (k n m : ℕ) (h : k ≤ n) (f : ℕ → β) : (interval n m).sum f = (interval (n-k) (m-k)).sum (λ x, f (x + k)) := lemma finset.sum.interval_reindex_right (k n m : ℕ) (f : ℕ → β) : (interval n m).sum f = (interval (n+k) (m+k)).sum (λ x, f (x - k)) :=

which I've proved (and some infrastructure for `interval`

).

#### Scott Morrison (Nov 24 2018 at 10:16):

The proofs still need a lot of golfing, but I think it's progress.

#### Scott Morrison (Nov 24 2018 at 10:18):

I would like to write some tactics to help with this, so you can just write things like "reindex_sum +3" in tactic mode, and it will `conv`

it's way to the first `(interval n m).sum f`

, and replace it with `(interval (n+3) (m+3)).sum (\lambda x, f (x-3))`

, etc.

#### Kevin Buzzard (Nov 24 2018 at 10:18):

Now on to multinomial coefficients!

#### Scott Morrison (Nov 24 2018 at 10:19):

I'd also like to write a `conv`

tactic for rewriting inside the summand of a `finset.sum`

, that gives you a hypothesis saying you're actually in the domain.

#### Scott Morrison (Nov 24 2018 at 10:24):

If I'm going to clean this up for a PR, where should it go? In `big_operators.lean`

? Or start a new file for summations over intervals in `nat`

?

#### Mario Carneiro (Nov 24 2018 at 10:27):

I think a file for summations over intervals is appropriate

#### Mario Carneiro (Nov 24 2018 at 10:28):

I think the name should be `finset.Icc`

though

#### Mario Carneiro (Nov 24 2018 at 10:28):

thiat gives us plenty of room for future variation

#### Mario Carneiro (Nov 24 2018 at 10:28):

er, `Ico`

?

#### Scott Morrison (Nov 24 2018 at 10:29):

does that stand for "interval closed open"?

#### Scott Morrison (Nov 24 2018 at 10:29):

okay

#### Mario Carneiro (Nov 24 2018 at 10:29):

yeah, for compatibility with `set.Ico`

#### Scott Morrison (Nov 24 2018 at 10:30):

how about when I define `Ico`

as a list/multiset/finset? Should those go in those three files, or in the file about summations over intervals?

#### Mario Carneiro (Nov 24 2018 at 10:30):

they can all be in the same file, I think

#### Scott Morrison (Nov 24 2018 at 10:31):

excellent, that means I can safely use tactics :-)

#### Mario Carneiro (Nov 24 2018 at 10:31):

oh, you mean the definitions themselves

#### Scott Morrison (Nov 24 2018 at 10:31):

yes...

#### Mario Carneiro (Nov 24 2018 at 10:31):

I guess they could go near `finset.range`

#### Mario Carneiro (Nov 24 2018 at 10:31):

but the development should go in its own file

#### Mario Carneiro (Nov 24 2018 at 10:32):

especially stuff combining sums and these sets

#### Scott Morrison (Nov 24 2018 at 10:32):

okay, that's what I've done so far --- in fact put them next to `list.range'`

, `multiset.range`

, and `finset.range`

, and then the actual lemmas about dealing with `(Ico n m).sum`

are in their own file.

#### Mario Carneiro (Nov 24 2018 at 10:32):

great

#### Scott Morrison (Nov 24 2018 at 10:33):

a few lemmas about slicing and dicing intervals use `tidy`

to blast through... those proofs will have to be rewritten if they are going to live in `finset.lean`

or earlier.

#### Scott Morrison (Nov 24 2018 at 10:34):

oh well...

#### Scott Morrison (Nov 24 2018 at 10:34):

(Not having `work_on_goal`

available will make me cry, as it means I'll actually have to restructure the proofs `tidy`

outputs.)

#### Mario Carneiro (Nov 24 2018 at 10:36):

oh no, structured proof

#### Scott Morrison (Nov 24 2018 at 10:38):

don't hold your breath :-) This PR is going to have some low-quality tactic proofs, that get the job done.

#### Scott Morrison (Nov 24 2018 at 10:45):

On the subject, if anyone wants to suggest to me some nice examples of proofs that rely on re-indexing and slicing and dicing sums, please do!

#### Mario Carneiro (Nov 24 2018 at 10:52):

you should look at `exp_add`

#### Mario Carneiro (Nov 24 2018 at 10:52):

and possibly quadratic reciprocity

#### Patrick Massot (Nov 24 2018 at 11:21):

Seriously guys, what's wrong with you? What the fuck is this thread?

#### Patrick Massot (Nov 24 2018 at 11:23):

I really think this proof assistant thing is going nowhere if we keep working like this, ignoring everything done by other people, including the ones who proved they can do much more than what we can currently do

#### Patrick Massot (Nov 24 2018 at 11:26):

I've pointed out repeatedly the existence of mathcomp's bigop library. They figured out all the issues, and they use it in linear algebra, in calculus, in finite group theory... I said it would very important to try to port that library to mathlib. Nobody cared. I started trying to do it, nobody cared. I struggled with nat substraction so I gave up for now. Then suddenly Scott asks many nat substraction questions, and, guess what, he is doing big operators again.

#### Mario Carneiro (Nov 24 2018 at 11:27):

The point is to see if our new techniques help with the proofs

#### Patrick Massot (Nov 24 2018 at 11:27):

I think the point is people thinking they are smarter than Gonthier and his friends

#### Mario Carneiro (Nov 24 2018 at 11:28):

if you get ahead of yourself writing theorems before the automation or appropriate structures and idioms come you get a load of unmaintainable hackery

#### Mario Carneiro (Nov 24 2018 at 11:28):

I'm afraid I can't read any of gonthier's proofs

#### Patrick Massot (Nov 24 2018 at 11:28):

Then why don't you ask?

#### Mario Carneiro (Nov 24 2018 at 11:29):

I highly respect him and I know he has a method to the madness but ssreflect style is not something I want to teach

#### Patrick Massot (Nov 24 2018 at 11:29):

We have Assia and Cyril who can read them, and explain everything

#### Patrick Massot (Nov 24 2018 at 11:29):

And they are really puzzled by our attitude

#### Patrick Massot (Nov 24 2018 at 11:29):

It has nothing to do with SSReflect crazyness

#### Patrick Massot (Nov 24 2018 at 11:30):

They thought about what are the right data structures, how to formulate the right induction principles for big operators, in what order to prove stuff

#### Patrick Massot (Nov 24 2018 at 11:30):

And it *works*

#### Mario Carneiro (Nov 24 2018 at 11:31):

sure, that's valuable

#### Mario Carneiro (Nov 24 2018 at 11:31):

it's the reason I periodically bring up metamath here, because many of our new problems are old problems somewhere else

#### Mario Carneiro (Nov 24 2018 at 11:31):

but I can't help that my experience is in metamath, not coq

#### Mario Carneiro (Nov 24 2018 at 11:33):

to get good information about how to do stuff in coq we would need Assia or Cyril guiding the path, and they have better things to do

#### Patrick Massot (Nov 24 2018 at 11:33):

What about letting them decide whether they have better things to do?

#### Patrick Massot (Nov 24 2018 at 11:33):

They both repeatedly offered to help us understand what's in mathcomp

#### Mario Carneiro (Nov 24 2018 at 11:34):

of course, if they actually think that's a good idea I'm all ears, that's not a rejection at all

#### Mario Carneiro (Nov 24 2018 at 11:35):

but in my view it's one more idea on the table, which can be considered equally among others

#### Patrick Massot (Nov 24 2018 at 11:35):

And what about trying to work together? @Scott Morrison could you publicly write why you chose to restart from scratch instead of helping me in my attempt?

#### Mario Carneiro (Nov 24 2018 at 11:35):

I don't think we should blindly port any specific library

#### Patrick Massot (Nov 24 2018 at 11:36):

I'm not saying we should blindly do anything. Quite the contrary, I'm suggesting to open our eyes to the existing stuff

#### Mario Carneiro (Nov 24 2018 at 11:36):

are you referring to the notation for filtered sums of nats?

#### Patrick Massot (Nov 24 2018 at 11:37):

I don't think Lean would be there is Leo had the same attitude with existing software. And it doesn't mean Lean is "blindly ported"

#### Patrick Massot (Nov 24 2018 at 11:38):

It's not only about notations, I proved many lemmas in https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean. I know some stuff should be rethought, and everything could be improved, but why not starting there?

#### Mario Carneiro (Nov 24 2018 at 11:39):

one could ask the same of that approach... try it on `exp_sum`

, try it on quadratic reciprocity, see if it helps

#### Mario Carneiro (Nov 24 2018 at 11:40):

this is not in any way a loaded question, it's a test bed for new ideas

#### Mario Carneiro (Nov 24 2018 at 11:40):

if it's a good approach, the proof will reflect that

#### Mario Carneiro (Nov 24 2018 at 11:41):

I don't know if scott's `Ico`

will make things better than just using `range`

, we need more data

#### Patrick Massot (Nov 24 2018 at 11:41):

It's lunch time, and this conversation is going nowhere anyway. Bye

#### Kevin Buzzard (Nov 24 2018 at 12:23):

@Chris Hughes do you have any comments on this? I remember a couple of times over the summer you saying you were having to battle with finite sums. What did you feel was missing from the library? Maybe it's time to compile a wishlist instead of all writing our own workarounds. Last year I wrote $\sum_{i=1}^na_i=\sum_{j=1}^na_{n+1-j}$ because I needed it for an example sheet question, and I remember it being a real pain.

#### Mario Carneiro (Nov 24 2018 at 12:25):

My impression of nat subtraction is it's best to avoid it appearing in lemmas to start with

#### Kevin Buzzard (Nov 24 2018 at 12:25):

Well it's in my lemma :-/

#### Kevin Buzzard (Nov 24 2018 at 12:25):

oh I see what you mean

#### Mario Carneiro (Nov 24 2018 at 12:26):

I wonder how much mileage you can get out of `finset.diag : finset (nat x nat) := {(0, n), ..., (n, 0)}`

#### Kevin Buzzard (Nov 24 2018 at 12:26):

you want me to prove that the function sending i to n+1-i is a bijection and then have some lemma about summing over a bijection, which actually might be in there already I guess. Is it?

#### Chris Hughes (Nov 24 2018 at 12:26):

I want to be able to sum between integers and naturals, and also do non commutative products over arbitrary lists. I think Patrick's approach seems to unify all these things nicely.

#### Chris Hughes (Nov 24 2018 at 12:27):

`sum_bij`

is the lemma

#### Mario Carneiro (Nov 24 2018 at 12:27):

the function sending i to n+1-i is

nope, you said minus

#### Mario Carneiro (Nov 24 2018 at 12:28):

the goal is to state the whole theorem without using minus

#### Kevin Buzzard (Nov 24 2018 at 12:28):

But I literally needed to prove that the sum of `F i`

was equal to the sum of `F (n + 1 - i)`

#### Mario Carneiro (Nov 24 2018 at 12:28):

`finset.diag.map swap = finset.diag.reverse`

#### Mario Carneiro (Nov 24 2018 at 12:28):

no minus

#### Mario Carneiro (Nov 24 2018 at 12:28):

and `swap`

is a bijection, etc etc

#### Kevin Buzzard (Nov 24 2018 at 12:29):

If I set as an example sheet question `binom n m = binom n (n - m)`

you can't now avoid the minus. Are you suggesting that binom should take integer coefficients?

#### Mario Carneiro (Nov 24 2018 at 12:30):

if it's literally the input statement, then you should apply a lemma to get rid of it first, and work with that

#### Kevin Buzzard (Nov 24 2018 at 12:30):

so what lemma gets me rid of `n - m`

in my input statement? :-/

#### Mario Carneiro (Nov 24 2018 at 12:30):

`binom n i = binom n j`

when `i + j = n`

#### Kevin Buzzard (Nov 24 2018 at 12:30):

*boggle*

#### Mario Carneiro (Nov 24 2018 at 12:30):

aka `(i, j) in finset.diag`

#### Mario Carneiro (Nov 24 2018 at 12:32):

inductions go through so much more smoothly when there is no break in the function

#### Kevin Buzzard (Nov 24 2018 at 12:32):

My theorem isn't even true when `m > n`

#### Mario Carneiro (Nov 24 2018 at 12:33):

my theorem can't even have m > n

#### Kevin Buzzard (Nov 24 2018 at 12:33):

right

#### Mario Carneiro (Nov 24 2018 at 12:33):

of course you can substitute in `n`

in that statement, and then it's an easy induction on i,j

#### Mario Carneiro (Nov 24 2018 at 12:34):

in general you might also want to generalize i,j and do induction on n, or something related

#### Kevin Buzzard (Nov 24 2018 at 12:35):

So one way of proving $s : \mathbb{Z} :=\sum_{i=0}^{2n+1}(-1)^i\binom{2n+1}{i}$ is 0 is to set $j=2n+1-i$ and note that this substitution proves that $s=-s$. You would do all this without any nat subtraction?

#### Scott Morrison (Nov 24 2018 at 19:08):

@Scott Morrison could you publicly write why you chose to restart from scratch instead of helping me in my attempt?

@Patrick Massot, my apologies if it appeared that I was intentionally ignoring your work at <https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean>. In fact I didn't even know that it existed. I remember looking at the top of `big_operators.lean`

and thinking "huh, that's funny, Patrick's name isn't in the `Authors`

line, I thought he helped write this file". But that was the extent of my memory of what you'd done. :-(

I'd be very happy to discuss what you wrote already and to make some plans about how to proceed.

Right now I need to go out for a while, but I'll look more closely at your repo soon. There is a lot there, and I see that working over `int`

rather than `nat`

index sets makes life easier. However I don't much like that you've "rolled your own" subsets built into your `bigop`

notation, containing both a `list I`

and an `I -> Prop`

, rather than using existing technology (e.g. `multiset`

, and `filter`

). I think it's best if we decouple as much as possible here.

#### Scott Morrison (Nov 24 2018 at 23:04):

@Patrick Massot, moreover, I will attempt to read the big operators paper. :-)

#### Scott Morrison (Nov 24 2018 at 23:05):

I see already that your `list I`

and `I -> Prop`

is imitating what they do, although my limited understanding so far is that they do something more general than `list I`

.

#### Patrick Massot (Nov 24 2018 at 23:07):

I just came back from the hospital after some climbing session, so I didn't see your message earlier

#### Patrick Massot (Nov 24 2018 at 23:07):

I'm sorry I was so upset this morning, but I'm really tired of these problems.

#### Patrick Massot (Nov 24 2018 at 23:08):

I didn't "roll my own subset" rather using filter, everything is based on filter. The question is the interface question, and this is precisely the kind of question where I think it makes sense to have a look at what mathcomp successfully used

#### Patrick Massot (Nov 24 2018 at 23:11):

I moved from nat to int mostly because of nat substraction hell, but also because sums indexed by integers do arise, for instance with Fourier series

#### Scott Morrison (Nov 25 2018 at 03:57):

Okay, a few disorganised thoughts post bike-ride:

1) While I absolutely agree that we want "generic operation" big operations, I mostly wanted to explore writing useful tactics for manipulating big operations, and thought that testing this out more narrowly (just with `finset.sum`

at first) would be helpful.

2) The sort of tactics I have in mind are: `shift 5`

(and `shift -2`

, and `shift_left`

, etc.), `split_first`

, `split_at`

, etc, and very importantly making it possible to `conv`

your way inside the summand, and be given a hypothesis that you're in the domain, so you can perform appropriate conditional rewrites. There are many more tactics suitable for multivariable big operations, changing between int and nat, etc. (Does the Coq library provide tactic level support?)

3) I feel pretty dubious about the Coq model where there is apparently a multiset, and a filter, being carried around in the notation. It then seems there are two places we can add an extra filter: on the actual multiset, and composed with the filter. There's then an extra dimension worth of rewriting to move the filters back on forth. Why cause yourself that trouble? (I still haven't read the Coq paper -- so this question is perhaps an invitation for someone to point me to a relevant comment.)

4) In Patrick's prototype, I think there's a real semantic problem with using a `list I`

and a `I -> Prop`

. What is the meaning of repeated elements in the list? Presumably that we're summing with multiplicity. What is the meaning of the order of the list? It's strange that the filter removes all copies of some element --- surely you want to be able to control multiplicities directly if you're summing with multiplicity? I suspect here that the answer is just to change from `list I`

to `finset I`

.

5) A more fundamental objection to following the Coq approach is indexing by the binary operation, rather than the carrier type, is completely alien to the rest of the design in Lean. Pursuing this for a big operators library seems likely to cause of lot of friction. In their paper (okay, I've now read the first 3 pages) they say they don't want to index by the carrier type because of course there is more than one relevant operation we want bigops for, for a single type (their example is nat, with +,*, max, min, lcm, gcd, and so on). I think this is actually an easy problem to solve, that we've solved elsewhere in mathlib by "wrapper types", and providing alternative instances for the wrapper. For example we might define

def as_gcd_monoid (X : Type) := X

and then

instance [has_gcd X] : has_mul (as_gcd_monoid X) := ...

and finally

def finset.gcd (t : finset X) (f : X -> Y) [has_gcd Y] := @finset.big_op X (as_gcd_monoid Y) t (\lambda x, f x)

(or something like that... )

#### Kenny Lau (Nov 25 2018 at 03:59):

don't drive and derive...

#### Scott Morrison (Nov 25 2018 at 04:10):

Also, if we're going to make some progress on big ops, I think it would be great if we can ask Assia and Cyril for some advice. I'd like to do a few experiments perhaps first (actually try writing some of the `conv`

style tactics for manipulating sums, and seeing if it really is okay to index by carrier type), but maybe we could even schedule a skype call with whoever is interested so we can ask them some questions.

#### Patrick Massot (Nov 25 2018 at 10:40):

Scott, I think you completely missed the point that we want to handle non-commutative operations

#### Patrick Massot (Nov 25 2018 at 10:41):

Next, I think the list + predicate is there to handle the very common case of summing on a range of integers subjects to conditions, like "sum for n from 1 to N, with n odd"

#### Patrick Massot (Nov 25 2018 at 10:42):

I'm not sure I understand what you'd like your tactic to do that a rewriting lemma couldn't

#### Scott Morrison (Nov 25 2018 at 22:35):

I did miss the intention to also do noncommutative things. What do you have in mind? (And in any case, while we're writing prototypes, I'd prefer to work in simpler special cases, so I suspect I'll propose we ignore the noncommutative stuff for now anyway.)

#### Scott Morrison (Nov 25 2018 at 22:41):

It might be good to at some point list all the things that conceivably could count as "big operations". Here's a sampling of things that could conceivably be in scope:

- sums,
- products,
- unions,
- maxs,
- gcds,
- convergent sums,
- integrals,
- limits (e.g. as x goes to a),
- limits (of a functor over a diagram).

#### Scott Morrison (Nov 25 2018 at 22:42):

But Patrick, why not just filter the list, if you want to sum over odd integers? I really don't understand why you want to carry around an "unapplied" filter.

#### Scott Morrison (Nov 25 2018 at 22:46):

And I think my point stands, even if we're going to do noncommutative operations: a list is a bad way to model a ordered set. Using a list commits us to dealing with multiplicities, and I don't think that's what you intend.

#### Scott Morrison (Nov 25 2018 at 22:52):

Regarding tactics: at the moment, rewriting inside the summand is a royal pain. As far as I can see, you need to use `rw sum_congr`

, having carefully prepared the equation you want to rewrite along ahead of time in the form `\forall x \in t, f x = g x`

. `conv`

completely fails to enter the summand giving you appropriate hypotheses, and this could easily be fixed.

#### Scott Morrison (Nov 25 2018 at 22:55):

Going back to my "big list of big operations"... I think it would be a bad idea to try to write a framework so general it encompasses all of these.

#### Chris Hughes (Nov 25 2018 at 22:56):

So for non commutative stuff, might it be better to use a finset with `linear_order`

on the indexing type? I like that idea.

#### Scott Morrison (Nov 25 2018 at 23:00):

It's possible. I'm not sure though how to make the commutative case a specialisation of the non-commutative case.

#### Scott Morrison (Nov 25 2018 at 23:01):

Another possibility is to have the range of the big operation be a "list without duplicates" (a new type?), and then have extra lemmas that apply when the operation is known to be commutative, and that list comes from a finset.

#### Scott Morrison (Nov 25 2018 at 23:01):

That design would mean lemmas proved about the noncommutative case would specialise.

#### Chris Hughes (Nov 25 2018 at 23:02):

Are there any concrete examples of where a list with duplicates is annoying?

#### Chris Hughes (Nov 25 2018 at 23:03):

I don't want to ask for that proof obligation without a good reason.

#### Scott Morrison (Nov 25 2018 at 23:05):

I ... guess not.

#### Scott Morrison (Nov 25 2018 at 23:06):

One problem is perhaps getting a list back out of a finset in the first place.

#### Scott Morrison (Nov 25 2018 at 23:07):

I'm still unhappy about carrying along unapplied predicates, but I'm now open to the idea of using a list to represent the range.

#### Scott Morrison (Nov 25 2018 at 23:36):

Just thinking out loud for a moment here: I wonder about really embracing the typeclass system here. What if we did big operations over arbitrary types A, and require an extra piece of evidence, possibly depending on the summand function `f : A -> X`

that the big operation makes sense. There could be lots of mechanisms here:

`[fintype A] [ordered A] [monoid X]`

(summing over an ordered finite set)`[fintype A] [comm_monoid X]`

(summing over a unordered finite set)- with
`f : (near a) -> X`

, where`def near {A : Type} (a : A) := A`

, the evidence for`lim_{a : near A} f`

could be computed from something like`[topological_space A] [continuous_at f a]`

`[normed_space X] [absolute_convergence f]`

,`[category A] [category X] [is_functorial f] [has_limits_of_shape A]`

(computing a limit)

Could one prove enough of the needed lemmas in this ridiculous generality that it would be worth doing?

#### Chris Hughes (Nov 25 2018 at 23:52):

distributivity of multiplication is true for lots of types of sums. Not sure how you'd state or prove that though. Unless you made a new class for more or less every lemma.

#### Johan Commelin (Nov 26 2018 at 04:37):

@Scott Morrison I think that limits (in topology or category theory) are a completely different kind of big operators from the others. All the others have some sort of iterative or recursive aspect to them. (Btw, we could add tensor products to your big list.) For those iterative instances I think it will probably be very useful to also have `product L`

if `L`

is a list of matrices. So we do care about the non-commutative case, I think.

About tactics vs rewrites: I completely agree that it is crucial that we have slick rewriting of the summand, and currently this is a pain. I also agree with @Patrick Massot That most of the "slicing and dicing" probably doesn't need tactics, but could be done with regular rewrite lemmas, because that doesn't touch the summand.

But making `conv`

access the summand would be get you a major hooray from my side! I just recently reexperienced how awful it is, when I tried to prove that `boundary_boundary`

lemma in the simplicial branch. You get nested sums over finsets, and manipulating them is a silly gamble where you just hope that `simp`

and `erw`

drill down far enough to make a bit of progress.

#### Scott Morrison (Nov 26 2018 at 07:49):

The other tactic support I realised we can do is unrolling sums of "explicit length". Just like my `fin_cases`

command, we can have a single tactic that takes for example $\sum_{n=k}^{k+3} f(n)$ and replaces it with $f(k) + f(k+1) + f(k+2) + f(k+3)$. This is quite a pain to achieve with pure rewriting, and is not so bad to automate in tactic mode.

#### Scott Morrison (Nov 26 2018 at 07:51):

I'm not sure sure that limits (in category theory or in topology) are completely different big operators. If you just categorify your natural numbers as finite sets, a sum of natural numbers is just the colimit of the discrete diagram of those sets (and a product is just the colimit)! Nevertheless, I wasn't seriously suggested we do this --- in fact I was setting up a straw man to try to argue we should not go for maximum generality. :-)

#### Johan Commelin (Nov 26 2018 at 07:52):

The other tactic support I realised we can do is unrolling sums of "explicit length". Just like my

`fin_cases`

command, we can have a single tactic that takes for example $\sum_{n=k}^{k+3} f(n)$ and replaces it with $f(k) + f(k+1) + f(k+2) + f(k+3)$. This is quite a pain to achieve with pure rewriting, and is not so bad to automate in tactic mode.

I suppose this could be done with `repeat { rw split_last }, simp`

.

#### Johan Commelin (Nov 26 2018 at 07:53):

But I agree that an `unroll_bigop`

tactic might make sense.

#### Scott Morrison (Nov 26 2018 at 07:54):

I'm not quite convinced it's that easy, but perhaps I'm thinking about the `fin_cases`

situation, which was quite a bit more painful.

#### Patrick Massot (Nov 26 2018 at 09:36):

I agree it seems to make sense to drop the predicate part, at least until we see a need for it, although I'll try to ask Cyril and Assia before doing so. But non-commutative operators are crucial. I started this project because I wanted to do group theory. And I still hope that one day we will be able to handle differential forms as well. Now that I think about it, I'm not sure I could find any big operator in one of my papers that uses a commutative operation.

#### Patrick Massot (Nov 26 2018 at 13:42):

I worked on my bigop attempt today, reaching a new sorry-free equilibrium point. I did find a use for the predicate thing as a convenient way to prove stuff, keeping track of information.

#### Patrick Massot (Nov 26 2018 at 14:48):

Ok, I pushed https://github.com/leanprover-community/mathlib/tree/bigop Any contributor is very welcome. In particular, cleaning up https://github.com/leanprover-community/mathlib/blob/bigop/pending_lemmas.lean requires no big operators skills, only knowing mathlib (or searching efficiently), or being good at either list or nat vs int bashing.

Last updated: May 11 2021 at 12:15 UTC