If you're ever written small to moderately large Rocq developments, it's quite likely that you have experienced the following problem:

• You write your proofs using induction or case analysis, carefully making sure to list all (important) cases one by one.
• Later, as your project naturally grows, you decide to add a new case (a new typing rule, a new kind of expression, etc.).
• Suddenly, all proofs that you've written break, usually with no clear indication as to where and why the proof broke.

If this sounds familiar, you've bumped into one of the current pitfalls of goal selection: goals selectors such as bullets and numbers do not match constructors one-to-one (they lack a semantic connection to the constructor they're supposed to apply to).

I'll show in this post how we can improve the experience by automatically generating goal names, yielding a robust and future-proof method of selecting goals.