Let the user customize autogenerated identifiers

[radrow]

Is your feature request related to a problem?

Yes. Sometimes I make the mistake of referring to an autogenerated variable of type Bob, e.g. after it appears in my context as b2 after some destruct or inversion. 10000 lines later, I decide that Bob is a bad name, and change it to Rob. But then, the name of the variable becomes r0. By the way, there used to be a variable b3 : Bamboo which now got the name b2 since it was freed. That easily escalates and now a simple rename turned into a major refactor.

Proposed solution

Give the user control over the base identifier for generating fresh variables of a specific type.

Default Ident (bobTheVariable : Bob).

This would make Coq automatically use the provided identifier, for example:

Goal Bob -> Bob -> False.
  intros.
  destruct bobTheVariable, bobTheVariable0.

For types with parameters, the leftmost applied name counts. Another way out of this is allowing matching types against patterns:

Default Ident (bobTheConstrained : {b : Bob | _}).

I wouldn't bother with reductions - the type should match like a normal constr. If you have Rob := Bob and H : Rob * Rob, you can always do destruct (H : Bob * Bob) or use change.

A bit bold extension to this

Let the user do the generation on their own (performance is on them):

Ltac2 mk_bob_name (actual_type : constr) := 
  match! actual_type with
  | {_ : _ | False} => Fresh.in_goal @bobTheLiar
  | _ => Fresh.in_goal @bobTheConstrained.
  end.

Default Ident ({b : Bob | _}) => mk_bob_name.

Alternative solutions

It can be already circumvented to some extent by explicitly naming all parameters in all definitions and lambdas, but it's not something you always want to do (especially in a functional language with pointfree obsession). You can also assign names while eliminating/introing, although my experience is that dealing with inversion while sticking to this kills my will of life. It also does not really solve the problem, because you need to severely maintain variable names across any code changes anyway.

Additional context

I seriously ended up renaming the type to bRob in my project just to keep that madness away. I acknowledge that it was bad coding since the beginning, but I can hardly find a good way to conveniently avoid doing this (inversion). It also seems that Coq encourages using autogenerated variables by looking at the standard library, tutorials, and examples in the docs.

[Zimmi48]

Doesn't a combination of Set Mangle Names, Set Mangle Name Prefix, and perhaps Set Mangle Names Light address this need? See https://rocq-prover.org/doc/V9.0.0/refman/proofs/writing-proofs/proof-mode.html#proof-maintenance.

[radrow]

I frankly didn't know about it, but it only partially addresses my proposal. I still want Coq to generate identifiers based on types --- but on types-types, not names of types.