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.

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"`

.

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.

In terms of having search understand subtyping for example

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

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)

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

Having keywords may make this operation simpler for a newcomer

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.

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

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.)

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...

(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.)

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:

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:

`Search bigop`

should find them all, really

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

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...

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?"

And indeed that motivated me to open this thread

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.

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