hygiene
hygiene
オプションは、マクロ衛生機能を有効にするかどうかを制御します。
プログラミング言語に対して、マクロが 衛生的(hygienic) であるとは、マクロ処理の過程で名前衝突の問題が発生しないことを指します。Lean のマクロはデフォルトで衛生的ですが、hygiene
オプションは一時的にこれを無効にすることができます。
/-- 定数関数を定義するマクロ -/
macro "const" e:term : term => `(fun x => $e)
def x : Nat := 42
def y : Nat := 42
-- マクロ衛生がきちんと働いているときの挙動
#guard (const x) 0 = 42
#guard (const y) 0 = 42
-- マクロ衛生を保つ機能を無効にする
set_option hygiene false
/-- マクロ衛生が無効になった定数関数マクロ -/
macro "const'" e:term : term => `(fun x => $e)
-- 引数の値が同じでも、識別子の名前によって値が変わるようになってしまった。
-- これはマクロの中で使用されている変数名も `x` であるため。
#guard (const' x) 0 = 0
#guard (const' y) 0 = 42
タクティクにおけるマクロ衛生
タクティクで導入される識別子についても、実行時の環境にある識別子と衝突しないようにする機能が Lean にはあります。
macro "my_intro" : tactic => `(tactic| intro h)
example (P : Prop) : P → P := by
my_intro
-- `h : P` がマクロ展開によって導入されはするが、
-- 死んでいるので使えない
fail_if_success exact h
assumption
-- マクロ衛生を保つ機能を無効にする
set_option hygiene false
macro "my_intro'" : tactic => `(tactic| intro h)
example (P : Prop) : P → P := by
my_intro'
-- `h : P` が使えてしまう
exact h
また、(驚くべきことに)タクティクマクロの中で導入した識別子だけでなく、「参照した」識別子についても Lean が自動的に衝突を回避します。
/-- exfalso タクティクを真似て自作したタクティク -/
macro "my_exfalso" : tactic => `(tactic| apply False.elim)
namespace Foo
/-- `False.elim` とめっちゃよく似た名前の紛らわしい定理 -/
theorem False.elim : 1 + 1 = 2 := by rfl
example (_h : False) : 1 + 1 = 2 := by
-- 普通に `apply` すると上の紛らわしい定理の方が使われてしまう
apply False.elim
done
example (h : False) : 1 + 1 = 2 := by
-- 実行した環境ではなくて宣言した環境における `False.elim` が使われる。
-- 紛らわしい方の定理は使われない!
my_exfalso
show False
contradiction
end Foo
-- マクロ衛生を保つ機能を無効にする
set_option hygiene false
/-- マクロ衛生が無効になったバージョンの `my_exfalso` -/
macro "my_exfalso'" : tactic => `(tactic| apply False.elim)
namespace Bar
/-- `False.elim` とめっちゃよく似た名前の紛らわしい定理 -/
theorem False.elim : 1 + 1 = 2 := by rfl
example (_h : False) : 1 + 1 = 2 := by
-- 紛らわしい方の `False.elim` が使われてしまう。
my_exfalso'
done
end Bar