Use a private binder name for non-dependent functions

[Kha]

@digama0 and me came up with this simple solution to #1822: Use a more horrible name like _x as the default binder name to disincentivize people from using it in tactic proofs. This is actually consisten with the name introduced by using a placeholder as the binder name.
But perhaps we indeed want to allow people using bad names like a/a_1 in proofs? Well, the code is already written, so I'm opening this PR.

[leodemoura]

@Kha I'm not sure about this change.
Pros:

• It is a workaround for issue Tactic quotations may pick up implicit abstraction names #1822
• It will indirectly force people to name things when using tactics (based on the changes you had to make).

Cons:

• It will break existing proofs. I am pretty sure it will break many proofs in @kenmcmil project.
• It may generate more user complaining. For example, one may claim that the automatically generated lemmas are less readable.

[digama0]

@leodemoura Would it be reasonable to have an option old_binder_auto_names for backwards compatibility, like with old_structure_cmd? This makes it easy to revert to the other naming convention if you happen to use many auto names and don't want to change the proofs.

As for "more user complaining", I don't see how _x_1 is significantly worse than a_1 - they both contain little to no info on their provenance. As much as is reasonable, even auto lemmas should try to name their variables, but when this isn't possible maybe they could select these a_1 names instead? I agree that I would prefer not to see _x_1 printed in the type or proof of an auto lemma - the context we discussed was in situations where it doesn't print, such as in non-dependent functions or other places where it can be safely written as _.

[Kha]

I am pretty sure it will break many proofs in @kenmcmil project.

Okay, that is a good data point to have. The thought that people may not mind this proof style came to me only after testing the patch.

There is an alternative solution that is not much more complicated but keeps the the current names: We "tag" such binder names with a prefix like _fun, then strip it away in intro and the pretty printer. Or we say it's low priority enough to wait for the parser refactoring.

[Kha]

@digama0

As for "more user complaining", I don't see how _x_1 is significantly worse than a_1

If people keep using the auto-generated names, we haven't fixed the issue for them anyway. I now believe there are only two proper solutions:

• make the binder names completely inaccessible (apparently breaks some people's workflow)
• fix the issue without changing any names (see my post above)

[kbuzzard]

End user being caught out by this issue
https://gitter.im/leanprover_public/Lobby?at=59e4ad505c40c1ba79a8d3e0
[so the proposed change would in this case generate less user complaining]

[Kha]

@leodemoura Should I explore this fix or should we postpone the issue?

There is an alternative solution that is not much more complicated but keeps the the current names: We "tag" such binder names with a prefix like _fun, then strip it away in intro and the pretty printer. Or we say it's low priority enough to wait for the parser refactoring.

[leodemoura]

@leodemoura Should I explore this fix or should we postpone the issue?

Let's wait a little bit. I don't want to stack workarounds on top of the existing ones. You and I are seriously considering the parser refactoring. In the new architecture, it will be easier to avoid this kind of problem.