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.
This looks delicious: <https://github.com/achlipala/frap/blob/master/BasicSyntax.v>.
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).
What are mandatory robust bullets and where can I get them?
I know the bullets as for example in the book _Software Foundations_, but my understanding is that they are neither.
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.
Am I still allowed to say like
repeat try split; try assumption. by this standard?
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.
Makes sense to me!
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
I realised I do not agree exactly with everything written on this page. Should we add a disclaimer saying it's still subjective?
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.
Maybe it would make sense to add disclaimers specific to each debated anti-pattern?
It's rather that I was wondering if experts were keeping an eye on this page, as I expect not everyone agrees on everything.
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.
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 ?
Yeah I assume github wiki doens't have a discussion "mode" like wikipedia.
Last updated: Oct 03 2023 at 20:01 UTC