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
  • Over-nesting 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.

Over-nesting 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.

Another approach, rather than separating easy from complex goals, would be to separate the main matter and the side conditions. Only the main matters is chained using bullets and the side conditions are handled using goal selectors.

intros x y z.
split.
- assert (h : True -> x = y).
  { (* ... *) }
  rewrite h. 2: auto.
  rewrite lemma_with_complex_side_condition.
  2:{
    (* complex proof *)
  }
  reflexivity. (* simpler than the side condition, but the main matter, what the reader cares about *)
- auto.

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. Alternatively, similar to other tactics the inversion tactic allows specifying explicit names to be generated using inversion ... as [ ... | ... ].

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'.