The goal of this is to end up in a situation where the proof terms constructed by the proof mode do NOT contain the variable names. Such names really should not end up in the proof term. @ppedrot and @janno are convinced this would give us significant speed-up. (We have a bet going here, with the threshold being 40% speedup. Let's see. ;)
@ppedrot, @janno and me recently spent some time thinking about this and I want to write this down before we forget. The basic idea is to have a version of
envs_entails_nameless, that takes two lists of propositions, instead of lists of pairs of strings and propositions. Now, we can
change back and forth between
envs_entails named_env and
envs_entails_nameless nameless_env -- the two are convertible as we always have concrete lists for our environments. So before we apply any Coq tactic like
apply, we always
change the goal to its nameless form, and then
change it back when we are done. These conversions are not actually recorded in the proof term; they only affect the type of the evar as stored in Coq, which is irrelevant at
Qed time. Essentially, we use the type of the evar as per-goal mutable state to store the names in.
The main problem with this is that the
coq_tactics would have to be written in nameless style, and the Ltac tactics wrapping them would have to take care of setting the right names in the subgoals they create. However, this is a problem that any solution to the issue will have -- if strings move out of the proof terms, we can't have them in Coq-level lemmas. Maybe Ltac2/Mtac could provide some other (less hacky) form of per-goal mutable state, but that wouldn't change this problem.