11.7. Naming Bound Variables🔗

When the simplifier or the rw tactic introduce new binding forms such as function parameters, they select a name for the bound variable based on the one in the statement of the rewrite rule being applied. This name is made unique if necessary. In some situations, such as preprocessing definitions for termination proofs that use well-founded recursion, the names that appear in termination proof obligations should be the corresponding names written in the original function definition.

The binderNameHint gadget can be used to indicate that a bound variable should be named according to the variables bound in some other term. By convention, the term () is used to indicate that a name should not be taken from the original definition.

🔗def
binderNameHint.{u, v, w} {α : Sort u}
  {β : Sort v} {γ : Sort w} (v : α) (binder : β)
  (e : γ) : γ

The expression binderNameHint v binder e defined to be e.

If it is used on the right-hand side of an equation that is used for rewriting by rw or simp, and v is a local variable, and binder is an expression that (after beta-reduction) is a binder (fun w => … or ∀ w, …), then it will rename v to the name used in that binder, and remove the binderNameHint.

A typical use of this gadget would be as follows; the gadget ensures that after rewriting, the local variable is still name, and not x:

theorem all_eq_not_any_not (l : List α) (p : α → Bool) :
    l.all p = !l.any fun x => binderNameHint x p (!p x) := sorry

example (names : List String) : names.all (fun name => "Waldo".isPrefixOf name) = true := by
  rw [all_eq_not_any_not]
  -- ⊢ (!names.any fun name => !"Waldo".isPrefixOf name) = true

If binder is not a binder, then the name of v attains a macro scope. This only matters when the resulting term is used in a non-hygienic way, e.g. in termination proofs for well-founded recursion.

This gadget is supported by

  • simp, dsimp and rw in the right-hand-side of an equation

  • simp in the assumptions of congruence rules

It is ineffective in other positions (hyptheses of rewrite rules) or when used by other tactics (e.g. apply).