variableコマンドの挙動がdefとtheoremでは異なる

[Seasawher]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Variable.20inclusion.20defs.20vs.2E.20theorems/near/532402609

[Seasawher]

variable (n : Nat)

-- this gives an error, unknown identifier 'n'
theorem foo (m : Nat) : m = m :=
  have : n = n := by rfl
  rfl

-- this works fine
def foo' (m : Nat) : m = m :=
  have : n = n := by rfl
  rfl

[Seasawher]

要点は、theorem と def では、外側の variable を自動で取り込む基準が違うという話です。

theorem は「定理の**文(statement)**に出てくる変数」だけを自動で引数にします。一方、def は「定義全体、つまり本体・証明部分で使われた変数」も取り込みます。 

variable (n : Nat)
-- エラー: unknown identifier 'n'
theorem foo (m : Nat) : m = m :=
have : n = n := by rfl
rfl
-- これは通る
def foo' (m : Nat) : m = m :=
have : n = n := by rfl
rfl

theorem で証明内だけに出てくる変数を使いたい場合は、明示的に include n する。

variable (n : Nat)
include n
theorem foo (m : Nat) : m = m :=
have : n = n := by rfl
rfl

なぜ違うのか。理由は主に2つです。第一に、多くの tactic はローカルコンテキスト全体を見るので、証明中で偶然参照された変数まで定理の依存関係に入ると、不要な依存が発生する。第二に、theorem の証明を非同期 elaboration しやすくするためです。 

特に induction / cases のような基本 tactic でも、人工的な依存が生じ得ます。例：

variable (n : Nat) (m : Fin n)
def ex : 0 ≤ n := by
induction n with
| zero => simp
| succ _ _ => simp
#check ex
/-
ex (n : Nat) (m : Fin n) : 0 ≤ n
-/

ここで m は結論 0 ≤ n には不要に見えるが、m : Fin n が n に依存しているため、induction n が内部で m を巻き込む。具体的には、induction n は本質的に revert n から始まり、Fin n が n に依存しているので m も revert され、各ケースで再導入される。これが「人工的な依存」です。 

比較として、m が n に依存しない型なら取り込まれない。

variable (n : Nat) (m : Fin 2)
def ex : 0 ≤ n := by
induction n with
| zero => simp
| succ _ _ => simp

結論：
theorem は、証明内の tactic が偶然触った変数まで定理の引数にしないよう、statement 基準で変数を取り込む。def は、定義本体が実際に値として意味を持つので、本体全体基準で取り込む。証明内だけで使う外側変数を theorem に含めたい場合は include を使う。