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.

There are many standards :-) math-comp and math-classes/corn have them...

https://github.com/math-comp/multinomials

Wow, this `math-comp`

code is cryptic.

You can read the MathComp book https://math-comp.github.io/mcb/

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.

Not to mention the only meaningful comment is at the top of the file.

I was expecting something more inviting.

The learning curve is indeed a tad steep at the beginning, but it's definitely worth it IMHO.

I appreciate your encouraging advice!

A summary of my thoughts on this: <https://coq.discourse.group/t/standard-library-of-the-future/1357>.

Pierre Roux said:

The learning curve is indeed a tad steep at the beginning, but it's definitely worth it IMHO.

*shallow :P

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.

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 03 2023 at 20:01 UTC