Stream: Coq users

Topic: Libraries that are worth learning?

jco (Jul 16 2020 at 06:34):

So in a lot of different contexts (her, SO) I've seen people refer to the Equations package...it makes me think that this is probably a package worth learning and using in general. Is that the case? I'm curious if there are any other packages that are sort of...generally recommended to make ones life more pleasant when using Coq. The downside of equations for example is it seems to be presenting it's own sort of DSL so I imagine there's a learning curve there, but if it's worth it I'll start.

Kenji Maillard (Jul 16 2020 at 06:46):

Hi @jco, wrt Equations, it indeed have some form of a DSL to write agda-style equations based pattern-matching but it is not so much more invasive than Program or Function that are shiped with Coq. It is an interesting asset whenever you want to write code that uses dependent elimination a lot. However the documentation is somewhat lacking.
On the topic of libraries in general, you probably want to look into a "standard library" such as mathcomp, std++, extlib, TLC. Each of them have their own style and purpose but are often more uniform and complete in their own area than the sdtlib coming with Coq.

jco (Jul 16 2020 at 07:08):

Kenji Maillard said:

Hi @jco, wrt Equations, it indeed have some form of a DSL to write agda-style equations based pattern-matching but it is not so much more invasive than Program or Function that are shiped with Coq. It is an interesting asset whenever you want to write code that uses dependent elimination a lot. However the documentation is somewhat lacking.
On the topic of libraries in general, you probably want to look into a "standard library" such as mathcomp, std++, extlib, TLC. Each of them have their own style and purpose but are often more uniform and complete in their own area than the sdtlib coming with Coq.

Ah ok, that makes a lot of sense. yeah I guess I should just spend some more time seeing what each offers and choose the one that fits my needs. It's sort of an overwhelming ecosystem :)

jco (Jul 16 2020 at 07:14):

I'm less worried about adding dependencies and more just sort of figuring out where to spend my time. Anything that makes using dependent types easier would be nice, though!

Théo Winterhalter (Jul 16 2020 at 07:24):

It's important to note that even without using the Equations' syntax, it is worth adding to your dependencies for its tactics. It provides stuff like dependent induction and dependent destruction which can be really useful.

jco (Jul 16 2020 at 07:26):

Théo Winterhalter said:

It's important to note that even without using the Equations' syntax, it is worth adding to your dependencies for its tactics. It provides stuff like dependent induction and dependent destruction which can be really useful.

I thought the coq stdlib had dependent induction (I guess I had just heard it was broken?). perhaps equations has a non-broken version?

jco (Jul 16 2020 at 07:28):

(broken in the sense that it still didn't quite properly handle some cases, though I imagine with the potential complexity of dependent types a perfect tactic is impossible)

jco (Jul 16 2020 at 07:30):

regardless seems like Equations is worth checking out, I see there's a manual, some examples, some papers so shouldn't be tooooo bad to get started (famous last words in the Coq world :D)

Théo Winterhalter (Jul 16 2020 at 07:30):

So Program also provides its own dependent induction (but not dependent destruction I think) but it is not as powerful, it will also use axioms when Equations doesn't. The Equations one is like a newer version of the other.

Théo Winterhalter (Jul 16 2020 at 07:31):

There is an Equations stream on this zulip also if you have questions regarding its use.

jco (Jul 16 2020 at 07:33):

Théo Winterhalter said:

So Program also provides its own dependent induction (but not dependent destruction I think) but it is not as powerful, it will also use axioms when Equations doesn't. The Equations one is like a newer version of the other.

ahh ok I think that is what I had probably seen. ok Equations seems neat then, I imagine a lot of dependent types in my future so I def want to know how to wrangle them

Paolo Giarrusso (Jul 16 2020 at 07:38):

Program has dependent destruction, but @Théo Winterhalter‘s other comments are right.

Théo Winterhalter (Jul 16 2020 at 07:40):

My bad!

Bas Spitters (Jul 16 2020 at 08:03):

@Kenji Maillard I believe @Hugo Herbelin has a point that we should do better in collaborating on the various extensions to the stdlib. Or at least have a somewhat coherent vision of where things should be going.
I'll be off for holiday soon, but hope to come back to the topic afterwards.
Do you have an opinion on the topic?

Kenji Maillard (Jul 16 2020 at 08:31):

I personally think that if there is a standard library, it should be compatible with any other library out there, providing a minimal set of features so that it can be a stable common denominator for all other libraries. Library design in a dependent setting looks to me like an open problem and any of the necessary experiment should be left to its own dedicated library.

As a user of various often slightly incompatible libraries, I can only beg for as much inter-operability as possible but I don't think it should be enforced in the stdlib.

Paolo Giarrusso (Jul 16 2020 at 09:22):

We're getting OT again — but what Kenji describes is one plan for stdlib2.

Meanwhile, today, stdpp still changes some global settings for some stdpp functions (I think mostly to better ones).

Bas Spitters (Jul 17 2020 at 05:58):

@Paolo Giarrusso Yes, sorry for hijacking the discussion.
( ... but it would be good to have a clear goal for stdlib2, I'm not sure I seen this explicitly agreed on.
And... if the change is for the better why not consider making a PR to the stdlib ?
Iris people seem to have created their own eco-system outside main coq. )

jco (Jul 17 2020 at 06:02):

Perhaps it deserves it's own thread. Not because I mind having my thread hijacked (I don't!), but rather b/c it seems like an extremely important topic and the core devs and stakeholders should probably see if they can't find some consensus. This seems like a recurring issue bigger than my little thread

jco (Jul 17 2020 at 06:03):

I will say that as a new user the Coq ecosystem is pretty intense, but I don't think that's necessarily a bad thing (as Coq is so powerful and used for so many different things), but it can of course be managed :)

jco (Jul 17 2020 at 06:04):

people say Scala has a lot of ways to do thing...lol Coq makes the Scala ecosystem feel like a little single celled organism

Bas Spitters (Jul 17 2020 at 06:04):

@jco Welcome to the community !

jco (Jul 17 2020 at 06:04):

Bas Spitters said:

jco Welcome to the community !

thank you!! everyone has been very helpful. it's been a lot of fun

Christian Doczkal (Jul 17 2020 at 07:15):

To come back to the original question:
jco said:

I'm curious if there are any other packages that are sort of...generally recommended to make ones life more pleasant when using Coq.

You could have a look at the mathematical components library, or mathcomp for short. It's a large library of well integrated mathematical results. However, it comes with its own tactic language and follows a design that differs significantly from what one finds elsewhere. So the there is definitely a learning curve there. On the other hand, users of mathcomp tend to not use the standard library much, so looking at mathcomp early may be better than trying to convert later.

jco (Jul 17 2020 at 07:19):

Christian Doczkal said:

To come back to the original question:
jco said:

I'm curious if there are any other packages that are sort of...generally recommended to make ones life more pleasant when using Coq.

You could have a look at the mathematical components library, or mathcomp for short. It's a large library of well integrated mathematical results. However, it comes with its own tactic language and follows a design that differs significantly from what one finds elsewhere. So the there is definitely a learning curve there. On the other hand, users of mathcomp tend to not use the standard library much, so looking at mathcomp early may be better than trying to convert later.

will check it out! do you happen to know if it includes support for proofs that need to leverage probability theory?

Christian Doczkal (Jul 17 2020 at 07:33):

Being the foundation for the proof of the odd-order theorem, a theorem about finite groups, the mathcomp library itself is mostly about finite structures, matrices, groups, etc. However, there is a lot of work based on top of mathcomp, including things like cryptography and (classical) analysis. Maybe someone else knows more than me. I will ask around in the office (now I'm curious myself).

jco (Jul 17 2020 at 07:34):

I'm interested in exploring information theory with Coq, and if I am big brained enough to handle it one day, some cryptography

Bas Spitters (Jul 17 2020 at 07:35):

@Christian Doczkal what kind of crypto is there on top of math-comp? You mean ECC?

Christian Doczkal (Jul 17 2020 at 07:45):

Well, I was thinking about the verification of the Jasmin compiler for high-assurance and high-speed cryptography, but maybe the compiler itself does not qualify as crypto. :thinking:

Bas Spitters (Jul 17 2020 at 07:55):

Thanks. I wasn't aware that jasmin used math-comp, but it makes sense. Most of the verification of jasmin seems to be using EC though...
We have good experiences with fiat-crypto.

Kenji Maillard (Jul 17 2020 at 07:59):

@jco you might be interested by https://github.com/affeldt-aist/infotheo then. And also by this discourse thread on probability theory libraries in Coq.

jco (Jul 17 2020 at 09:02):

Bas Spitters said:

Thanks. I wasn't aware that jasmin used math-comp, but it makes sense. Most of the verification of jasmin seems to be using EC though...
We have good experiences with fiat-crypto.

oh are you on the team behind fiat? that's a project that is high on my list of projects to check out. I'm very interested in the verified spec=>efficient implementation pipeline (spent some time with verified c)

jco (Jul 17 2020 at 09:03):

Kenji Maillard said:

@jco you might be interested by https://github.com/affeldt-aist/infotheo then. And also by this discourse thread on probability theory libraries in Coq.

thanks!!

Bas Spitters (Jul 17 2020 at 09:13):

@jco We're just using it:
https://cs.au.dk/fileadmin/site_files/cs/AA_pdf/COBRA_Paper_-_High-assurance_field_inversion_for_pairing-friendly_primes.pdf
We just created a fiat-crypto stream for discussions on this.

jco (Jul 17 2020 at 09:14):

Bas Spitters said:

jco We're just using it:
https://cs.au.dk/fileadmin/site_files/cs/AA_pdf/COBRA_Paper_-_High-assurance_field_inversion_for_pairing-friendly_primes.pdf
We just created a fiat-crypto stream for discussions on this.

ah nifty, I'll lurk on that stream for sure :) and the paper is def going on The List

Last updated: Sep 28 2023 at 11:01 UTC