The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/02/2014 05:07 AM, Julien Narboux wrote:
> There is a command "Show intros" to display the names which will be
> generated.

I already use PG's ^C^ATab, which uses Show intros to automatically 
generate a completely named intro pattern.  But there are many more 
tactics that introduce names - some of which it's quite hard to control 
(inversion is an example).

>   It is possible to build a script which replace intros. intos
> named intros, a good starting point for writing such a script could be the
> one for indenting writen by Eelis:
> https://github.com/jnarboux/corn/blob/master/tools/coqindenter

I will look at your script.

> We could have also an option to prevent you from using automatically named
> variables (the prefix could be something like a utf8 character for space).
> I think this is the default behaviour in Isabelle/Isar.

I suggested a suffix so as not to interfere with the "fresh" tactic, 
which sets the prefix - in other words, setting a suffix would cause 
fresh to obey that suffix without changing its current semantics - since 
it is already allowed to choose a suffix to keep the name fresh.

Otherwise, this is similar to what I suggested - although I'd rather 
that the prefix/suffix did print visibly, so that the change could be seen.

As for using this to prevent one from using automatically named 
variables instead of allowing one to fix them later:  when working on a 
proof, I don't want to work too hard on preventing automatic names and 
as a result lose my train of thought on the proof itself. I think I'd 
rather go back after finishing the proof, and fix it.

-- Jonathan

> Julien
>
>
> 2014-06-30 21:08 GMT+02:00 Jonathan 
> <jonikelee AT gmail.com>:
>
> > I've been getting careless and not carefully naming all variables in a
> > proof script myself.  Is there any mechanism that can help one to rework a
> > proof script so that all of the variables used in tactics are not of the
> > automatically-named variety?
> >
> > For instance, is there some mechanism in Coq that would alter the
> > automatic naming in a predictable way - say by appending a user-provided
> > suffix to each automatically generated name?  A "Set Auto Naming Suffix"
> > command?  Given that, I could provide some easily distinguishable suffix
> > like "__" (double underscore), and rerun a script to see where it fails -
> > and clean up the instances one by one.
> >
> > This became a bit more important recently, as there was something
> > introduced into the trunk version of Coq that slightly changed the
> > automatic naming scheme in certain cases.
> >
> > -- Jonathan