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.

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.

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 usesdependent eliminationa 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 :)

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!

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.

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?

(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)

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)

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.

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

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

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

My bad!

@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?

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.

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).

@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. )

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

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 :)

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

@jco Welcome to the community !

Bas Spitters said:

jco Welcome to the community !

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

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.

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?

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).

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

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

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:

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.

@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.

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)

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!!

@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.

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