`variable` と `section`¶

variable コマンドは，以降の定義や定理で使う変数をまとめて宣言します．これは前章の証明図に出てきた Γ，つまり「現在使ってよい変数や仮定の集まり」に対応します．

section ... end で囲むと，その中だけで有効な変数を宣言できます．宣言された変数は，後続の定義で実際に使われたとき，その定義の引数として自動的に追加されます．たとえば次の pairFromVariables は，内部的には α，x，y を引数にもつ定義として扱われます．

section VariableExamples

variable (α : Type)
variable (x y : α)

def pairFromVariables : α × α :=
  (x, y)

example : pairFromVariables Nat 2 5 = (2, 5) := by
  rfl

end VariableExamples

波括弧 {α : Type} で宣言した引数は，Lean が推論できる場合には省略できる暗黙引数になります．丸括弧 (α : Type) は通常の明示的な引数，波括弧 {α : Type} は暗黙引数です．次の singletonList 3 では，要素 3 の型から α = Nat が推論されます．

section ImplicitVariableExamples

variable {α : Type}

def singletonList (x : α) : List α :=
  [x]

example : singletonList 3 = [3] := by
  rfl

example : singletonList (-2 : Int) = [(-2 : Int)] := by
  rfl

end ImplicitVariableExamples

引数に現れる `( )`，`{ }`，`⦃ ⦄`，`[ ]`¶

Lean の定義や定理では，引数の括弧に意味があります． Mathlib の定理を読むときに重要なので，ここで整理しておきます．

(x : α): 明示的な引数です．通常，関数や定理を使う側が値を与えます．
{α : Type}: 暗黙引数です．Lean が周囲の式から推論できるなら，通常は書きません．
⦃x : α⦄: strict implicit 引数です．暗黙引数の一種で， Lean が後続の明示的な引数などから推論できるときに補います．
[Add α]: 型クラス引数です．Lean が登録済みの instance から自動的に探します．

たとえば (h : P) は「命題 P の証明 h を明示的な引数として受け取る」という意味です．一方，{α : Type} は命題の仮定ではなく，推論される型パラメータです． ⦃x : α⦄ も推論される引数ですが，通常の暗黙引数よりも，後ろに続く明示的な引数から値が決まる場面を意識した書き方です．入力するときは {{x : α}} と書くこともできますが，pretty printer では ⦃x : α⦄ と表示されます． [Add α] も通常の変数というより，「α には足し算がある」という構造を型クラス探索で要求している，と読みます．型クラスについては，後の class と instance の節で改めて扱います．

def explicitId (α : Type) (x : α) : α :=
  x

def implicitId {α : Type} (x : α) : α :=
  x

def strictImplicitExample ⦃x : Nat⦄ (_h : x = x) : Nat :=
  x

def addWithClass {α : Type} [Add α] (x y : α) : α :=
  x + y

#check explicitId
#check implicitId
#check @implicitId
#check strictImplicitExample
#check @strictImplicitExample
#check addWithClass

example : explicitId Nat 3 = 3 := by
  rfl

example : implicitId 3 = 3 := by
  rfl

example : strictImplicitExample (show (3 : Nat) = 3 from rfl) = 3 := by
  rfl

example : strictImplicitExample (x := 3) rfl = 3 := by
  rfl

example : (∀ ⦃n : Nat⦄, n = n → n = n) := by
  intro n h
  exact h

example (h : ∀ ⦃n : Nat⦄, n = n → n = n) : (3 : Nat) = 3 := by
  exact h rfl

example : addWithClass 2 5 = 7 := by
  rfl

暗黙引数を明示したいときは，名前付き引数 (α := Nat) を使うことがあります．また，@implicitId のように名前の前に @ を付けると，通常は隠れている暗黙引数も含めた型を確認できます． strict implicit 引数も，必要なら (x := 3) のように名前付き引数で明示できます．

#check @implicitId
#check implicitId (α := Nat)
#check @strictImplicitExample

最初は「丸括弧は普通に渡す，引数」，「波括弧は Lean が推論する，引数」，「二重波括弧は，後続の情報から推論される暗黙引数」，「角括弧は型クラス探索で探す，構造」と覚えておけば十分です．

variable と section¶

引数に現れる ( )，{ }，⦃ ⦄，[ ]¶

`variable` と `section`¶

引数に現れる `( )`，`{ }`，`⦃ ⦄`，`[ ]`¶