/
rename_var.lean
83 lines (70 loc) · 2.71 KB
/
rename_var.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
/-
Copyright (c) 2019 Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot
-/
import tactic.interactive
/-!
# 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`.
```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
```
## Tags
teaching, tactic
-/
open expr
/-- Rename bound variable `old` to `new` in an `expr`-/
meta def expr.rename_var (old new : name) : expr → expr
| (pi n bi t b) := (pi (if n = old then new else n) bi (expr.rename_var t) (expr.rename_var b))
| (lam n bi t b) := (lam (if n = old then new else n) bi (expr.rename_var t) (expr.rename_var b))
| (app t b) := (app (expr.rename_var t) (expr.rename_var b))
| e := e
namespace tactic
/-- Rename bound variable `old` to `new` in goal -/
meta def rename_var_at_goal (old new : name) : tactic unit :=
do
old_tgt ← target,
tactic.change (expr.rename_var old new old_tgt)
/-- Rename bound variable `old` to `new` in assumption `h` -/
meta def rename_var_at_hyp (old new : name) (e : expr) : tactic unit :=
do
old_e ← infer_type e,
tactic.change_core (expr.rename_var old new old_e) (some e)
end tactic
namespace tactic.interactive
open tactic
setup_tactic_parser
/--
`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`.
-/
meta def rename_var (old : parse ident) (new : parse ident) (l : parse location) : tactic unit :=
l.apply (rename_var_at_hyp old new) (rename_var_at_goal old new)
end tactic.interactive
/--
`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.
```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
```
-/
add_tactic_doc
{ name := "rename_var",
category := doc_category.tactic,
decl_names := [`tactic.interactive.rename_var],
tags := ["renaming"] }