## Stream: math-comp users

### Topic: Learning bigop ?

#### Emilio Jesús Gallego Arias (May 11 2021 at 15:52):

Dear math-comp community,

when introducing math-comp to colleagues and students, a consistent difficulty we have faced has been to help people achieve self-sufficiency with bigops. Common problems are:

• search is difficult, for example if you have \sum  many of the lemmas are generic so using \sum in your search won't work
• there are too many lemmas to display
• there is a lot of black magic, errors are tricky, etc...
• in general, the solution space seems quite large, google doesn't seem too helpful

I am curious as how do you folks approach the above problematic, and what kind of things you think could be improved.

Maybe doing a bigop cheat sheet could help to some extent?

I cc: @Amel Kebbouche as she may want to provide some of their own struggle points.

#### Laurent Théry (May 11 2021 at 16:05):

we talked about that exact matter in the last mathcomp meeting. I like your idea of setting up a bigop cheat shee.t People at the meeting were more looking into making Search more powerfull thanks to attributes, @Enrico Tassi even suggested to add textual search as  Search "pull an item out of bigcup".

#### Emilio Jesús Gallego Arias (May 11 2021 at 16:07):

Good point about Search, indeed Enrico and Cyril were kind enough to present most of their ideas in the Coq Call too I think.

Actually a lot could be improved in Search without the need for more metadata, I think.

#### Emilio Jesús Gallego Arias (May 11 2021 at 16:07):

In terms of having search understand subtyping for example

#### Laurent Théry (May 11 2021 at 16:09):

If you set a sheet. Share the location here I may contribute

#### Enrico Tassi (May 11 2021 at 16:10):

IMO "patterns" are too verbose, even if search was up-to subsumption (find a more general lemma than what you asked). Hence my suggestion to list a few actions (pull out, reindex, ...) and use these keywords for searching (of course one would need to attach reasonable keywords to lemmas)

#### Enrico Tassi (May 11 2021 at 16:11):

I always search by name, but this requires one to be familiar with the conventions

#### Enrico Tassi (May 11 2021 at 16:11):

Having keywords may make this operation simpler for a newcomer

#### Enrico Tassi (May 11 2021 at 16:13):

Another way to put it, if one writes a 1 line comment, in English, per bigop lemma, then google is going to be much better than Coq's Search.

#### Emilio Jesús Gallego Arias (May 11 2021 at 16:15):

oh very good point @Enrico Tassi , actually I am not sure that what coqdoc produces is usable by google in any way, but indeed we should make sure it is at some point

#### Kazuhiko Sakaguchi (May 11 2021 at 16:20):

IMO, one thing everyone should know on this point is that every bigop notation is syntactic sugar for a bigop over a list with a condition. Then it should be a bit clearer which lemma matches with the goal. (Indeed there are other issues.)

#### Cyril Cohen (May 11 2021 at 16:21):

I myself open the file bigop.v or bigop.html and browse through it. I think it is the only file in the whole library that I need to use in this way...

#### Kazuhiko Sakaguchi (May 11 2021 at 16:22):

(I just opened a PR related to this point. I hope this is a good example: https://github.com/math-comp/math-comp/pull/741.)

#### Cyril Cohen (May 11 2021 at 16:23):

Otherwise I use Search with the pattern (\big[_/_]_(_ <- _ | _) _) (which is the most general patttern (we should really make a notation out of it)), because some of the lemmas I might be looking for may not actually by in bigop.v :laughter_tears:

#### Christian Doczkal (May 11 2021 at 16:26):

Cyril Cohen said:

Otherwise I use Search with the pattern (\big[_/_]_(_ <- _ | _) _) (which is the most general patttern (we should really make a notation out of it)), because some of the lemmas I might be looking for may not actually by in bigop.v :laughter_tears:

This has also become my favored approach, if the first approximation (searching for lemmas with "big" in their name) does not yield the result I want. :shrug:

#### Enrico Tassi (May 11 2021 at 16:30):

Search bigop should find them all, really

#### Enrico Tassi (May 11 2021 at 16:31):

(you can name the head symbol behind the huge notation)

#### Cyril Cohen (May 11 2021 at 16:36):

Enrico Tassi said:

Search bigop should find them all, really

You are right... :rolling_on_the_floor_laughing: I don't know why I never thought of it...

#### Emilio Jesús Gallego Arias (May 11 2021 at 18:09):

Actually the one I use is for example Search _ (bigop _ _ _) = _ (bigop _ _ _) (bigop _ _ _) , but indeed when I did show this to Amel, she was like "how on earth would I ever figure this out?"

#### Emilio Jesús Gallego Arias (May 11 2021 at 18:09):

And indeed that motivated me to open this thread

#### Yosuke Ito (May 12 2021 at 12:17):

I make my original list of the lemmas that I used before. But for the first time using a lemma, I sometimes struggle finding an appropriate one from bigop.v as you mention.

#### Ana de Almeida Borges (May 12 2021 at 12:58):

I always search by name, but this requires one to be familiar with the conventions

It would also be nice to signal-boost the conventions. There is already a list in the contributing guide, but perhaps it is not completely exhaustive, and it's unlikely a new-comer will think to read the contributing guide as a means of solving their beginner issues.

Last updated: Jan 29 2023 at 19:02 UTC