`structure`¶

structure は，複数の field をもつデータ型を定義するコマンドです．数学では，点，群，位相空間，線形写像などを structure として表すことが多くあります． structure は，名前つき field をもつ積型と考えると分かりやすいです．実際，Lean の内部では structure は単一の constructor をもつ inductive 型として扱われ，そこに field や射影関数の情報が登録されています．そのため inductive 型と同様に再帰的な定義も受け付けますが，再帰的な出現は strictly positive でなければなりません． field 名に対して射影関数が自動で作られ，p.x のようなドット notation でアクセスできます．

structure PointStruct where
  x : Int
  y : Int
deriving Repr, DecidableEq

deriving Repr は，PointStruct の値を Lean が表示できるようにする指定です． #eval で値を確認したいときなどに使われます．

deriving DecidableEq は，2 つの PointStruct が等しいかどうかを判定する手続きを自動生成する指定です．たとえば，2 つの点の座標がどちらも等しいかを計算で判定できるようになります．

この定義では，x と y が field です． field は，その型の値が持つ名前つきの成分です．一方，constructor はその型の値を作るものです． structure では通常 PointStruct.mk という constructor が作られ，{ x := 1, y := 2 } はそれを使って点を作る notation です．

#check PointStruct.mk

example : PointStruct.mk 1 2 = { x := 1, y := 2 } := by
  rfl

def originStruct : PointStruct :=
  { x := 0, y := 0 }

def PointStruct.swap (p : PointStruct) : PointStruct :=
  { x := p.y, y := p.x }

example : originStruct.x = 0 := by
  rfl

example : PointStruct.swap { x := 1, y := 2 } = { x := 2, y := 1 } := by
  rfl

PointStruct.x や PointStruct.y は，structure の中で宣言された field です．一方，PointStruct.swap は field ではなく，あとから PointStruct という名前空間に置いた普通の関数です． Lean では，名前空間にある関数や定理も，最初の明示的な引数の型からドット notation で呼べることがあります．そのため，PointStruct.swap p は p.swap とも書けます．このような関数は，プログラミング言語のメソッドのように見えますが， Lean の用語としては「名前空間にある関数」または「定理」をドット notation で適用している，と考えるのが安全です． field かどうかは，それが structure や class の中で宣言された成分かどうかで判断します．

#check PointStruct.x
#check PointStruct.swap

example (p : PointStruct) : PointStruct.swap p = p.swap := by
  rfl

def addPointStruct (p q : PointStruct) : PointStruct :=
  { x := p.x + q.x, y := p.y + q.y }

example : addPointStruct { x := 1, y := 2 } { x := 3, y := 4 } = { x := 4, y := 6 } := by
  rfl

標準ライブラリでは，データの積 Prod も structure です． α × β は Prod α β の notation で，p.1 と p.2 は field を取り出す射影です．

#check Prod
#check Prod.mk
#check Prod.fst

def sampleProduct : Nat × Nat :=
  (3, 5)

example : sampleProduct.1 = 3 := by
  rfl

example : sampleProduct.2 = 5 := by
  rfl

def sampleTriple : Nat × Nat × Nat :=
  (3, 5, 8)

example : sampleTriple.1 = 3 := by
  rfl

example : sampleTriple.2.1 = 5 := by
  rfl

example : sampleTriple.2.2 = 8 := by
  rfl

命題の連言 P ∧ Q も And P Q という structure です． h : P ∧ Q から h.left と h.right を取り出すことは，structure の field を取り出すことと同じ形です．

lean4/src/lean/Init/Prelude.lean

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

ここで intro :: は，この structure の constructor 名を intro にする指定です．つまり，hP : P と hQ : Q から And.intro hP hQ : P ∧ Q を作れます．一方，left と right は field であり，作られた証明から左右の証明を取り出すために使われます．

#check And
#check And.intro
#check And.left
#check Subtype

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
  And.intro hP hQ

example (P Q : Prop) (h : P ∧ Q) : P :=
  h.left

命題の同値 P ↔ Q も Iff P Q という structure です． h : P ↔ Q からは，h.mp : P → Q と h.mpr : Q → P を取り出せます．これは同値命題を，両方向の含意を field としてもつ structure として表しているということです．

lean4/src/lean/Init/Core.lean

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

#check Iff
#check Iff.intro
#check Iff.mp
#check Iff.mpr

example (P Q : Prop) (hPQ : P → Q) (hQP : Q → P) : P ↔ Q :=
  Iff.intro hPQ hQP

example (P Q : Prop) (h : P ↔ Q) (hP : P) : Q :=
  h.mp hP

演習¶

2 つの成分を持つ structure を定義し，field を取り出してください．また，3 つの積 α × β × γ から各成分を取り出す式を書いてください．

structure PointExercise where
  x : Nat
  y : Nat

def pExercise : PointExercise :=
  { x := 2, y := 5 }

example : pExercise.x = 2 := by
  sorry

example (α β γ : Type) (x : α × β × γ) : α :=
  sorry

structure¶

演習¶

`structure`¶