【LEAN4】structure

structureを定義する

前回ではいくつかの要素を持つinductive typeを定義しました。

      inductive S : Type
  | a : S
  | b : S
    

今回はstructureを定義します。structureはconstructorとして定義されます。即ち以前のように具体的な集まりを定義するのでなく、複製されるものとして定義されます。
structureの（単純化した）定義構文は以下です：

      structure <name> <parameters> where
  <constructor_1> : <fields>
  <constructor_2> : <fields>
        :
  <constructor_N> : <fields>
    

※公式によるとstrutureはinductive typeの特別な場合らしいです。

上の定義の構文を理解するために具体例で見てみます。ここではある与えられた型α : Type uがあったとします。αは例えば自然数、実数、一般の集合などです。

      structure Point (α : Type u) where
  x : α
  y : α
    

この定義は例えば2次元平面上の点の座標を想定しています。αがIntであれば格子点上の点、αが実数なら実平面上の点とみなせます。

このconstructorを使って適当な集合を定義してみましょう。constructorを用いて作られた実態を定義する構文は複数あり、以下のいずれかで実態を生成することが出来ます。a、bは型Natを持つとします。

      constant a : Nat
constant b : Nat

def p : Point Nat :=  { x := a, y := b }

#reduce p.x -- a
#reduce p.y -- b

    

※現状のLEAN4では複数の変数を同時に定義出来ない上に、自分で設定した型を持つ変数を定義することも出来ないらしい。。。