Stream: math-comp users

Topic: Learning bigop ?


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

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.

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2021 at 16:07):

In terms of having search understand subtyping for example

view this post on Zulip Laurent Théry (May 11 2021 at 16:09):

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

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

view this post on Zulip Enrico Tassi (May 11 2021 at 16:11):

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

view this post on Zulip Enrico Tassi (May 11 2021 at 16:11):

Having keywords may make this operation simpler for a newcomer

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

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

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

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

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

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

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

view this post on Zulip Enrico Tassi (May 11 2021 at 16:30):

Search bigop should find them all, really

view this post on Zulip Enrico Tassi (May 11 2021 at 16:31):

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2021 at 18:09):

And indeed that motivated me to open this thread

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

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