Emilio Jesús Gallego Arias (May 11 2021 at 15:52): 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:
\sum many of the lemmas are generic so using \sum in your search won't workI 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
Searchwith 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 inbigop.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 bigopshould 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