# Automatic naming considered harmful

Whenever a user doesn't name a variable in an Ltac script, Coq
will automatically generate a fresh name for it. After doing some
proofs, however, you start to realize that this behavior is more of a
nuisance than a feature. The heuristics used by Coq when choosing new
names are hard to predict and depend on the current proof state,
making proofs likely to break whenever a small change is
introduced. As every experienced Coq user knows, trying to figure out
whether hypothesis H22 now corresponds to H9 or H24 when fixing
a complicated proof script cannot exactly be described as a pleasant
experience, specially when the proof script is 2000 lines long and
you've spent hours dealing with similar horrors.
When writing robust proof scripts, one must ensure that the code
doesn't depend on weird automatically chosen names. Here are some tips
for making the naming problem disappear.
Most of the times, you can get rid of this problem by not being lazy
and naming everything explicitly. Avoid using tactics like intros or
destruct in their unnamed form; instead, use intros v1 v2 v3 ...
or destruct v as [a1 a2|a1 a2 a3|...]. You can also name hypothesis
in the statement of your lemma, using a forall instead of a plain
implication arrow (remember, in Coq, these are actually the same
thing). If you don't pass any names to intros, it will try to keep
the same names that appear in the current goal:

### Name variables explicitly

Lemma l1 : forall (A : Prop) (HYP : A), A.

Proof. intros. exact HYP. Qed.

This also works when reintroducing a variable from the context
into the goal, for instance with generalize dependent.
When working with complicated inductive predicates, naming all new
variables explicitly on every destruct or inversion can be
cumbersome. A reasonable compromise is to name all the arguments to
your constructors in inductive definitions. This makes the names that
are generated by those tactics meaningful, more stable and
predictable. Here's an example of a simple inductively defined
relation with explicit argument names:

### Name constructor arguments

Inductive collatz : nat -> nat -> Prop :=

| collatz_even (n m : nat)

(EVEN : 2 * m = n) : collatz n m

| collatz_odd (n m : nat)

(ODD : 2 * m + 1 = n) : collatz n (3 * n + 1)

| collatz_trans (n m p : nat)

(COLLATZnm : collatz n m)

(COLLATZmp : collatz m p) : collatz n p.

### Don't refer to names in proofs

Lemma collatz_cycle :

forall n m,

(n = 1 \/ n = 4 \/ n = 2) ->

collatz n m ->

m = 1 \/ m = 4 \/ m = 2.

Proof.

intros.

match goal with

| H : collatz _ _ |- _ => induction H

end.

- omega.

- repeat match goal with

| H : _ \/ _ |- _ => destruct H

end; omega.

- match goal with

| H1 : ?P,

H2 : ?P -> ?Q,

H3 : ?Q -> ?R |- ?R =>

apply H3; apply H2; apply H1

end.

Qed.

In the above (admittedly artificial) example, we were able to
refer exactly to what we wanted in the context without having to
resort to the names that Coq chose. Notice how in the third case we
were able to specify how premises and conclusions should match when
picking the hypotheses. In most cases, a simple match suffices to
remove explicit names from proofs.