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.
@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.
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)?
I started a wiki entry for Anti-patterns. Feel free to contribute.
I could contribute a couple of things, but in SSR syntax. Let me see what I can do.
FTR, a few considerations on proof maintenance can also be found here, page 94, section 5.3 (in the context of mathcomp)
Thanks, Andrej. This wiki is very helpful!
Last updated: Feb 06 2023 at 13:03 UTC