Ignat Insarov (Jun 18 2021 at 20:44): 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.
Ignat Insarov (Jun 19 2021 at 10:32):This looks delicious: <https://github.com/achlipala/frap/blob/master/BasicSyntax.v>.
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).
Ignat Insarov (Jun 19 2021 at 11:56):What are mandatory robust bullets and where can I get them?
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.
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.
Am I still allowed to say like repeat try split; try assumption. by this standard?
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.
Ignat Insarov (Jun 19 2021 at 14:03):Makes sense to me!
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
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?
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.
Théo Zimmermann (Jun 21 2021 at 07:59):Maybe it would make sense to add disclaimers specific to each debated anti-pattern?
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.
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.
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 ?
Théo Winterhalter (Jun 21 2021 at 08:06):Yeah I assume github wiki doens't have a discussion "mode" like wikipedia.
Last updated: Oct 13 2024 at 01:02 UTC