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.

source

meta def tactic.get_unused_name_reserved (ns : list name) (reserved : name_set) :

tactic name

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 buto 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.

source

meta def tactic.intro_fresh_reserved (ns : list name) (reserved : name_set) :

tactic expr

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.

source

meta def tactic.intro_lst_fresh_reserved (ns : list (name ⊕ list name)) (reserved : name_set) :

tactic (list expr)

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).

source

meta def tactic.rename_fresh (renames : name_map (name ⊕ list name)) (reserved : name_set) :

tactic (list (expr × expr))

rename_fresh renames reserved, given a map renames which associates the unique names of some hypotheses hᵢ with either a name nᵢ or a nonempty (!) name list nsᵢ, renames each hᵢ as follows:

If hᵢ is associated with a name nᵢ, it is renamed to nᵢ. This may introduce shadowing if there is another hypothesis nᵢ in the context.
If hᵢ is associated with a name list nsᵢ, it is renamed to the first unused name from nsᵢ. If none of the names is unused, hᵢ is renamed to a fresh name based on the first name of nᵢ. A name is considered used if it appears in the context or in the environment or in reserved.

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.