Rename bound variable tactic #

This files defines a tactic rename_var whose main purpose is to teach renaming of bound variables.

rename_var old new renames all bound variables named old to new in the goal.
rename_var old new at h does the same in hypothesis h.

example (P : ℕ →  ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
  rename_var n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
  rename_var m n, -- goal is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
  exact h -- Lean does not care about those bound variable names
end

Tags #

teaching, tactic

source

meta def expr.rename_var (old new : name) :

expr → expr

Rename bound variable old to new in an expr

source

meta def tactic.rename_var_at_goal (old new : name) :

tactic unit

Rename bound variable old to new in goal

source

meta def tactic.rename_var_at_hyp (old new : name) (e : expr) :

tactic unit

Rename bound variable old to new in assumption h

source

meta def tactic.interactive.rename_var (old new : interactive.parse lean.parser.ident) (l : interactive.parse interactive.types.location) :

tactic unit

rename_var old new renames all bound variables named old to new in the goal. rename_var old new at h does the same in hypothesis h.

source

def tactic_doc.tactic.rename_var :

tactic_doc_entry

rename_var old new renames all bound variables named old to new in the goal. rename_var old new at h does the same in hypothesis h. This is meant for teaching bound variables only. Such a renaming should never be relevant to Lean.

example (P : ℕ →  ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m :=
begin
  rename_var n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
  rename_var m n, -- goal is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
  exact h -- Lean does not care about those bound variable names
end