Anti patterns

Coq provides a plethora of approaches to formalization. However, some design patterns are less concise, intelligible, robust, or maintainable than others. Such anti-patterns often overcomplicate proof scripts, commonly break with Coq updates, and are greatly discouraged. There are different kinds of anti-patterns including (but not limited to):

• Specification
  • Too much syntactic sugar
  • Overpopulated core hint database
• Module structure
  • One-big-file approach
  • Unscoped global top-level notations
• Proof structure
  • Linear multi-goal proofs
  • Overnesting bullets
  • No names
  • Non-monotone automation

Specification anti-patterns

Too much syntactic sugar

Overuse of syntactic sugar via Notation, Coercion, Class/Instance, Implicit Insertion can lead to an incomprehensible proof state. A common issue is that verbatim automation (e.g. lia) gets stuck on notationally equal (and possibly convertible) terms which are syntactically different. Troubleshooting in presence of too much heuristic syntactic sugar can be laborious.

Overpopulated core hint database

It is unfavorable to put every Hint (especially domain-specific ones) globally into the core hint database. Also, Hint Extern with no pattern (or a too general pattern) in core can cause slowdowns. Consider that global hints in core are loaded on (transitive) Require and decrease auto/eauto predictability/reliability. Instead, a good idea is partition domain-specific hints into separate, domain-specific hint databases.

Module structure anti-patterns

One-big-file approach

It is disadvantageous to put definitions, auxiliary tactics, auxiliary lemmas, and theorems all into one file.

For example see List.v. Say another module just requires the head/tail functions on lists. Unfortunately, Require List will also introduce into the environment facts/hints/tactics for lists, and transitively facts/hints/tactics for natural numbers, setoids, etc... This quickly results in unpredictable automation (e.g. auto) behavior. Another downside is that the compilation of said module cannot happen in parallel with the unwanted dependencies.

For a better layout see Relations in Coq Standard Library.

Unscoped, global, top-level notations

Unscoped, global, top-level notations quickly lead to notation clashes. For example a top-level Notation "l[f]" := (map f l). will quickly clash with ListNotations or ssreflect intro patterns.

Instead, a good idea is to scope (to opt-out) or put such a notation into a Module (to opt-in) (cf. ListNotations).

Proof structure anti-patterns

Linear multi-goal proofs

Consider the proof script tactic. auto. intuition. easy. easy. where tactic. creates two subgoals (first solved by auto), intuition creates two subgoals (both solved by easy). Such a proof script has (at least) two problems. First, if auto gets weaker (e.g. due to different core hints), then intuition will be applied to a wrong goal and lead to an arbitrary proof state. Second, if auto gets stronger (which is part of intuition), then possibly there will be too few subgoals for easy.

Instead, a good idea is to use bullets.

Overnesting bullets

Consider the following proof script where tactic creates two subgoals of which the first one is easy to show

tactic.
- easy.
- tactic.
  + easy.
  + tactic.
    * easy.
    * auto.

Proof scripts with deep nesting are tedious to refactor (e.g. if the number of subgoals of tactic changes). If all but one subgoal are easy to prove, consider instead

tactic; [easy|].
tactic; [easy|].
tactic; [easy|].
auto.

or alternatively (if tactic always creates exactly two subgoals)

tactic. { easy. }
tactic. { easy. }
tactic. { easy. }
auto.

If you use ssreflect, the // operator can be used to get rid of trivial goals, and the ; last by and ; first by tactical to close side conditions. Example:

tactic => //.
rewrite rule1 rule2 //.
tactic; last by tactic.

Using semicolons when they are not necessary

The semicolon tactic operator ; is used for backtracking and should be avoided in the proof mode when unnecessary as it hinders proof update. For instance tac ; auto is not robust and the number of goals afterwards might change depending on imports (which affect auto) and changes in the goal. Another example would be tac1 ; tac2 ; tac3 ; tac4 where many tactics are used in sequence and suddenly fail after a change in a definition. The user will usually have to remove the semicolons to understand what went wrong. It might even not be sufficient, as replacing semicolons by points does not yield an equivalent script because of backtracking. Backtracking should be in any case limited to avoid blow-up. As such, the use of goal selectors would be more robust (and stepped through).

tac1. all: tac2. 1-3: tac3.
tac4.

No names

Consider the proof script inversion H. apply H0. rewrite H1. exact (H2 H3), where the names H0, H1, H2, H3 are automatically generated by inversion. Not only is such a proof script hard to read, it also is quite likely to break if the naming heuristics are changed/improved. Generally, it is a good idea to use proper, manually assigned names.

It might still be interesting to use such tactics as inversion, only then the following proof script should not assume the name of the generated hypotheses. Instead one can use tactics that do not require to mention the names such as assumption or more complex constructions using lazymatch goal for instance.

Non-monotone automation

Consider the proof script tactic; try lia. tactic'., where tactic creates five subgoals, the first four of which are solved by lia and one by tactic'. If the automation tactic lia gets stronger (and solves all five subgoals), then such a proof script will break. It is often a good idea write proof scripts that continue to function with stronger automation. For example tactic; (lia + tactic')., tactic; [lia ..| tactic']., or by manual goal selection.

Particularly bad offenders are tactic; auto with arith. tactic'. and tactic; intuition. tactic'.