Stream: Coq users

Topic: What is beautiful Coq code?


view this post on Zulip Ignat Insarov (Jun 18 2021 at 20:44):

I am looking for some Coq code to read — some examples of meaningful developments written in exemplary style. Please suggest some! The subject matter does not matter — be it mathematics or verified software or whatever else.

view this post on Zulip Ignat Insarov (Jun 19 2021 at 10:32):

This looks delicious: <https://github.com/achlipala/frap/blob/master/BasicSyntax.v>.

view this post on Zulip Théo Winterhalter (Jun 19 2021 at 11:54):

I think good coq code should absolutely use bullets (and have them mandatory so that it's robust) and only use ; when it makes sense (most of the time it doesn't).

view this post on Zulip Ignat Insarov (Jun 19 2021 at 11:56):

What are mandatory robust bullets and where can I get them?

view this post on Zulip Ignat Insarov (Jun 19 2021 at 11:57):

I know the bullets as for example in the book _Software Foundations_, but my understanding is that they are neither.

view this post on Zulip Théo Winterhalter (Jun 19 2021 at 12:12):

Set Bullet Behavior "Strict Subproofs".
Set Default Goal Selector "!".

The first option is only necessary if you use math-comp which deactivates bullet semantics, and the second one makes bullets mandatory.
Basically it forces you to explicitly mention when tactics generate several goals.

Goal forall A B, A -> B -> A * B.
Proof.
  intros A B hA hB.
  split.
  - exact hA.
  - exact hB.
Qed.

view this post on Zulip Ignat Insarov (Jun 19 2021 at 12:18):

Am I still allowed to say like repeat try split; try assumption. by this standard?

view this post on Zulip Théo Winterhalter (Jun 19 2021 at 13:08):

I personally try to avoid and instead use goal selector.

repeat try split. all: try assumption.

This way you can step through. I try to reserve ; to only places where it is mandatory (in an Ltac definition) or where I actually want to use backtracking (because that's what the semicolon does).
For instance in some cases solve [ econstructor ; eauto ] would be interesting because it might try several constructors before finding one that lets eauto conclude the goal afterwards.

But that's just my way of thinking, and I know that not everyone agrees with it.

view this post on Zulip Ignat Insarov (Jun 19 2021 at 14:03):

Makes sense to me!

view this post on Zulip Yannick Forster (Jun 21 2021 at 07:35):

While there is no general guideline how good Coq code looks, there is an effort to document anti-patterns in the wiki: https://github.com/coq/coq/wiki/Anti-patterns I would say that in general for learners of Coq the beauty of code does not matter. But at some intermediate level, understanding why these are anti-patterns makes sense

view this post on Zulip Théo Winterhalter (Jun 21 2021 at 07:54):

I realised I do not agree exactly with everything written on this page. Should we add a disclaimer saying it's still subjective?

view this post on Zulip Yannick Forster (Jun 21 2021 at 07:56):

Yes, that would probably be good :) Also if we can come up with a concise disclaimer that this is targeted at advanced Coq users and not a resource for beginners that would be good I think.

view this post on Zulip Théo Zimmermann (Jun 21 2021 at 07:59):

Maybe it would make sense to add disclaimers specific to each debated anti-pattern?

view this post on Zulip Théo Winterhalter (Jun 21 2021 at 08:03):

It's rather that I was wondering if experts were keeping an eye on this page, as I expect not everyone agrees on everything.

view this post on Zulip Théo Winterhalter (Jun 21 2021 at 08:04):

For now I added my thoughts on it, but I also don't want to claim I speak the truth. It's my experience and preference, but I am not an authority.

view this post on Zulip Kenji Maillard (Jun 21 2021 at 08:06):

If there is some debate on an item wouldn't it be more fruitful to bring the content of the debatable item to a platform more open for discussion (e.g here on zulip or discourse) and keep the wiki page to some synthesis of the various argumented opinion ?

view this post on Zulip Théo Winterhalter (Jun 21 2021 at 08:06):

Yeah I assume github wiki doens't have a discussion "mode" like wikipedia.


Last updated: Mar 29 2024 at 05:40 UTC