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.

Name variables explicitly

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:

This also works when reintroducing a variable from the context into the goal, for instance with generalize dependent.

Name constructor arguments

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:

Don't refer to names in proofs

Weird automatically generated names are not a problem if they do not appear in Ltac scripts. Automated proofs can obviously help here, but there are small things you can do even if you're not an automation expert. By using match, you can avoid mentioning automatically generated names without having to convert an unnamed inversion or destruct into a named one:

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.