Zulip Chat Archive

Stream: general

Topic: finset.sum


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 13:54):

I guess you should first prove g a ha ∈ s using the pigeonhole principle

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 13:57):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 06 2018 at 14:40):

Oh I see, it's an involution

view this post on Zulip 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

view this post on Zulip Chris Hughes (Aug 06 2018 at 14:41):

Is there a short proof using lemmas?

view this post on Zulip Mario Carneiro (Aug 06 2018 at 14:41):

not with those hypotheses

view this post on Zulip Mario Carneiro (Aug 06 2018 at 14:42):

half of the work will be unpacking them

view this post on Zulip 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

view this post on Zulip Morenikeji Neri (Aug 06 2018 at 14:43):

yep!

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Nov 24 2018 at 10:16):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 10:18):

Now on to multinomial coefficients!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:27):

I think a file for summations over intervals is appropriate

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:28):

I think the name should be finset.Icc though

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:28):

thiat gives us plenty of room for future variation

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:28):

er, Ico?

view this post on Zulip Scott Morrison (Nov 24 2018 at 10:29):

does that stand for "interval closed open"?

view this post on Zulip Scott Morrison (Nov 24 2018 at 10:29):

okay

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:29):

yeah, for compatibility with set.Ico

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:30):

they can all be in the same file, I think

view this post on Zulip Scott Morrison (Nov 24 2018 at 10:31):

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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:31):

oh, you mean the definitions themselves

view this post on Zulip Scott Morrison (Nov 24 2018 at 10:31):

yes...

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:31):

I guess they could go near finset.range

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:31):

but the development should go in its own file

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:32):

especially stuff combining sums and these sets

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:32):

great

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 24 2018 at 10:34):

oh well...

view this post on Zulip 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.)

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:36):

oh no, structured proof

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:52):

you should look at exp_add

view this post on Zulip Mario Carneiro (Nov 24 2018 at 10:52):

and possibly quadratic reciprocity

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:21):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 24 2018 at 11:27):

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

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:27):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 11:28):

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

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:28):

Then why don't you ask?

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:29):

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

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:29):

And they are really puzzled by our attitude

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:29):

It has nothing to do with SSReflect crazyness

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:30):

And it works

view this post on Zulip Mario Carneiro (Nov 24 2018 at 11:31):

sure, that's valuable

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 11:31):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:33):

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

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:33):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 24 2018 at 11:35):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 11:36):

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

view this post on Zulip 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"

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 11:40):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 24 2018 at 11:41):

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

view this post on Zulip 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 i=1nai=j=1nan+1j\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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 12:25):

Well it's in my lemma :-/

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 12:25):

oh I see what you mean

view this post on Zulip 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)}

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Nov 24 2018 at 12:27):

sum_bij is the lemma

view this post on Zulip Mario Carneiro (Nov 24 2018 at 12:27):

the function sending i to n+1-i is

nope, you said minus

view this post on Zulip Mario Carneiro (Nov 24 2018 at 12:28):

the goal is to state the whole theorem without using minus

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Nov 24 2018 at 12:28):

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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 12:28):

no minus

view this post on Zulip Mario Carneiro (Nov 24 2018 at 12:28):

and swap is a bijection, etc etc

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 12:30):

so what lemma gets me rid of n - m in my input statement? :-/

view this post on Zulip Mario Carneiro (Nov 24 2018 at 12:30):

binom n i = binom n j when i + j = n

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 12:30):

boggle

view this post on Zulip Mario Carneiro (Nov 24 2018 at 12:30):

aka (i, j) in finset.diag

view this post on Zulip Mario Carneiro (Nov 24 2018 at 12:32):

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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 12:32):

My theorem isn't even true when m > n

view this post on Zulip Mario Carneiro (Nov 24 2018 at 12:33):

my theorem can't even have m > n

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 12:33):

right

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 12:35):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 24 2018 at 23:04):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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... )

view this post on Zulip Kenny Lau (Nov 25 2018 at 03:59):

don't drive and derive...

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Nov 25 2018 at 10:40):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 25 2018 at 23:01):

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

view this post on Zulip Chris Hughes (Nov 25 2018 at 23:02):

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

view this post on Zulip Chris Hughes (Nov 25 2018 at 23:03):

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

view this post on Zulip Scott Morrison (Nov 25 2018 at 23:05):

I ... guess not.

view this post on Zulip Scott Morrison (Nov 25 2018 at 23:06):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 26 2018 at 07:53):

But I agree that an unroll_bigop tactic might make sense.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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