tactic hygiene (タクティクにおけるマクロ衛生) の例

[Seasawher]

/- # tactic hygine
タクティクの中で参照されている識別子は、タクティクを宣言するときには、
そのタクティクが使用されたときの環境に何があるかわからないため、
衝突する可能性がある。
-/

/-- exfalso タクティクを真似て自作したタクティク -/
macro "my_exfalso" : tactic => `(tactic| apply False.elim)

namespace Foo

/-- `False.elim` とめっちゃよく似た名前の紛らわしい定理 -/
theorem False.elim : 1 + 1 = 2 := by rfl

set_option linter.unusedVariables false in

example (h : False) : 1 + 1 = 2 := by
  -- 上の紛らわしい定理の方が使われてしまう
  apply False.elim

  done

example (h : False) : 1 + 1 = 2 := by
  -- なんと、タクティクも衛生的になっていて、
  -- （実行した環境ではなくて）宣言した環境における `False.elim` が使われる
  -- （すごい!）
  my_exfalso

  show False
  contradiction

set_option hygiene false in

macro "my_exfalso'" : tactic => `(tactic| apply False.elim)

example (h : False) : 1 + 1 = 2 := by
  -- 衛生的ではないので、上の紛らわしい定理が使われてしまう
  my_exfalso'

  done

end Foo