Tactics for giving hypotheses fresh names
When introducing hypotheses, we often want to make sure that their names are fresh, i.e. not used by any other hypothesis in the context. This file provides tactics which allow you to give a list of possible names for each hypothesis, with the tactics picking the first name that is not yet used in the context. If all names are already used, the tactics use a name derived from the first name in the list.
get_unused_name_reserved ns reserved
returns the first name from ns
that
occurs neither in reserved
nor in the environment. If there is no such name in
ns
, it returns a name of the form n_i
, where n
is the first name from ns
and i
is a natural number (like tactic.get_unused_name
). If ns
is empty,
it returns an arbitrary name.
For example, assume we operate in the following context:
n n_1: ℕ
Then we have
get_unused_name_reserved [`n, `m, `list, `o] {m} = `o
since n occurs in the context,
m is reserved, list occurs in the environment
but
o is unused. We also have
get_unused_name_reserved [`n, `m, `list] {m} = `n_2
since all of the names from the list are taken and n_2
is the first unused
variation of n
.
intro_fresh_reserved ns reserved
introduces a hypothesis. The hypothesis
receives a fresh name from ns
, excluding the names in reserved
. ns
must be
nonempty. See tactic.get_unused_name_reserved
for the full algorithm.
intro_lst_fresh_reserved ns reserved
introduces one hypothesis for every
element of ns
. If the element is sum.inl n
, the hypothesis receives the name
n
(which may or may not be fresh). If the element is sum.inr ns'
, the
hypothesis receives a fresh name from ns
, excluding the names in reserved
.
ns
must be nonempty. See tactic.get_unused_name_reserved
for the full
algorithm.
Note that the
order of introductions matters:
intro_lst_fresh_reserved [sum.inr [
n], sum.inr [n]]
will introduce
hypotheses n
and n_1
(assuming that these names are otherwise unused and not
reserved).
rename_fresh renames reserved
, given a map renames
which associates the
unique names of some hypotheses hᵢ
with name lists nsᵢ
, renames each hᵢ
to
a fresh name from nsᵢ
, excluding the names in reserved
. The nsᵢ
must be
nonempty. See tactic.get_unused_name_reserved
for the full algorithm.
The hypotheses are renamed in context order, so hypotheses which occur earlier in the context are renamed before hypotheses that occur later in the context. This is important because earlier renamings may 'steal' names from later renamings.
rename_fresh
returns a list of pairs (oᵢ, nᵢ)
where the oᵢ
are hypotheses
from the context in which rename_fresh
was called and the nᵢ
are the
corresponding hypotheses from the new context created by rename_fresh
. The
pairs are returned in context order. Note that the returned list may contain
hypotheses which do not appear in renames
but had to be temporarily reverted
due to dependencies.