Stream: Coq users

Topic: Antipatterns


view this post on Zulip Andrej Dudenhefner (Apr 26 2021 at 15:46):

I was looking (without much success) for a condensed collection of Coq antipatterns (common, but greatly discouraged patterns).
A good example of an antipattern is List.v#L763-L764 is the ese of intuitionthat closes 1,5 goals (with a somewhat unpredictable goal left) and will quickly break if somewhere else a hint to core is added.
Similar things can be said about tactic; try lia. tactic2. that often breaks whenever lia gets stronger.
It would be good to have a Coq wiki entry written by experienced developers giving a list of such antipatterns that are bad in the long run.

view this post on Zulip Théo Zimmermann (Apr 26 2021 at 17:00):

@Andrej Dudenhefner Since you already know a few of them, maybe you can start such a wiki page. It's easier to encourage experts to contribute to an existing page than to create a new one from scratch.

view this post on Zulip Joshua Grosso (Apr 26 2021 at 22:44):

Can I propose: Using dependent types where they're not strictly necessary (e.g. see this conversation from here on: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60dependent.20destruction.60.20of.20expressions/near/210084698)?

view this post on Zulip Andrej Dudenhefner (Apr 30 2021 at 11:27):

I started a wiki entry for Anti-patterns. Feel free to contribute.

view this post on Zulip Enrico Tassi (Apr 30 2021 at 12:17):

I could contribute a couple of things, but in SSR syntax. Let me see what I can do.

view this post on Zulip Enrico Tassi (Apr 30 2021 at 12:21):

FTR, a few considerations on proof maintenance can also be found here, page 94, section 5.3 (in the context of mathcomp)

view this post on Zulip Yosuke Ito (May 01 2021 at 02:39):

Thanks, Andrej. This wiki is very helpful!


Last updated: Feb 06 2023 at 13:03 UTC