Ignat Insarov (Jun 18 2021 at 16:22): Ignat Insarov (Jun 18 2021 at 16:22):I want to do some algebra in Coq, specifically with polynomials over ℚ but more abstract approach would be fine. Is there a standard library with definitions and maybe some basic theorems that I should wield? Or should I start from scratch? I looked over Coq's standard library and I did not find a word about polynomials.
Bas Spitters (Jun 18 2021 at 17:16):There are many standards :-) math-comp and math-classes/corn have them...
Ali Caglayan (Jun 18 2021 at 17:17):https://github.com/math-comp/multinomials
Ignat Insarov (Jun 18 2021 at 18:55):Wow, this math-comp code is cryptic.
Pierre Roux (Jun 18 2021 at 19:07):You can read the MathComp book https://math-comp.github.io/mcb/
Ignat Insarov (Jun 18 2021 at 19:10):Yes, I have it opened right next to this chat window. But this naming style… It is like they pay a euro for every letter in an identifier after the third one.
Ignat Insarov (Jun 18 2021 at 19:10):Not to mention the only meaningful comment is at the top of the file.
Ignat Insarov (Jun 18 2021 at 19:10):I was expecting something more inviting.
Pierre Roux (Jun 18 2021 at 19:27):The learning curve is indeed a tad steep at the beginning, but it's definitely worth it IMHO.
Ignat Insarov (Jun 18 2021 at 19:29):I appreciate your encouraging advice!
Ignat Insarov (Jun 18 2021 at 20:21):A summary of my thoughts on this: <https://coq.discourse.group/t/standard-library-of-the-future/1357>.
Cody Roux (Jun 18 2021 at 20:34):Pierre Roux said:
The learning curve is indeed a tad steep at the beginning, but it's definitely worth it IMHO.
*shallow :P
Ana de Almeida Borges (Jun 19 2021 at 23:32):Ignat Insarov said:
A summary of my thoughts on this: <https://coq.discourse.group/t/standard-library-of-the-future/1357>.
[...]
This is the official reference for Mathematical Components, the Coq Mathematics standard. 1 Yes, it is an alphabetical index of identifiers. Sounds great, right? (Not really. A reference should have a structure — a tree of contents.)
For what it's worth, mathcomp's library graph is linked right next to that reference in https://math-comp.github.io/.
I do agree that mathcomp has a meaningful learning curve, but I second Pierre's comment that it's worth it. For example, after you learn the conventions, you can rely on them to the point of predicting lemmas' names.
Ignat Insarov (Jun 20 2021 at 08:29):Yes, I noticed the graph, but I did not find it informative. It would be a nice cherry on top of a solid reference, but for it to work there has to be a solid reference in the first place.
I accept that for a chosen few it may be worth the effort to learn the short hand — if eventual savings outweigh the overhead. Ligatures and short hand existed since time immemorial. But they never went beyond narrow circles. Writing a standard library in short hand is a good way to make people stay away from it.
You are making a case that the short hand mathcomp is written in is systematic. All short hands are! Otherwise no one at all could use them. I do not question the usefulness of mathcomp to the few. I only say that being written in short hand makes it hard to wield for the many.
Please do not phrase it as if I am complaining about steep learning curves. Is Coq an easy language in the first place?
Last updated: Oct 08 2024 at 14:01 UTC