【LEAN4】inductive type

inductive typeを明示的に定義

inductive typeと言われてもピンと来ませんが、例えばその型を持つ有限集合を明示的に定義することが出来ます。

実際に有限集合を明示的に定義してみます。

構文

      inductive <型名> : Type
  | <要素1> : <型名>
  | <要素2> : <型名>
        :
  | <要素N> : <型名>
    

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

      inductive Person : Type
  | Euler : Person
  | Gauss : Person
  | Cantor : Person
    

      inductive E : Type
    

※注意　inductive typeは具体的に集まりを書き表すもので、それを使って複製するものでないことに注意してください。
集合や群、圏など概念の型を定義する方法は後述。

自然数のinductive typeを定義する

自然数は無限に存在するので上記のようにして列挙することは出来ません。自然数を定義するためにはペアノの定義を用います。

ペアノの定義とは、(1) 0は自然数、(2) Nが自然数ならNのsuccessorも自然数、による定義です。

(1) 0は自然数

まず(1)の0が自然数であることを表現してみます：

      inductive nat : Type
  | Zero : nat
    

※注意　LEAN4にも自然数の型が組み込まれており、そちらはNatで呼び出される

#print natで定義した型の情報を見てみる

      inductive nat : Type
constructors:
nat.Zero : nat
    

(2) Nが自然数ならNのsuccessorも自然数

0以外の自然数を定義するにはsucccessorを別途用意する必要があります。
プログラム上ではそれをSuccで表現することにします。つまり、

      inductive nat : Type
  | Zero : nat
  | Succ (n: nat) : nat
    

のようにSuccをnatの定義に付け加えます。#print natで定義した型の情報を見て見ます：

      inductive nat : Type
constructors:
nat.Zero : nat
    

上の定義で、1、2などは

      open nat

#print Succ Zero
#print Succ (Succ Zero)
    

により表現可能です。

※注意　open natにより自然数の定義を呼び出しています。
これにより通常nat.Zeroやnat.Succと書く必要がなくなりコードが読みやすくなります。

※注意　NのsuccessorをN+1と表現している記事をよく見かけますが、自然数上の和は自然数を定義したあとに定義されるものであるため、和というよりはNの次の数という意味なので、言葉どおり1を足すものでないことに注意してください。

簡単な定理の証明

せっかくLEAN4を使っているのでここで簡単な定理を証明してみます。

      open nat

def One := Succ Zero
def Two := Succ One
def Two' := Succ (Succ Zero)
    

このように自然数2を二通りの方法で定義することが可能です。これらは残念なことにLEAN4のなかでは別々の型として扱われてしまいます。

      #print Two
-- def Two : nat :=
-- Succ One

#print Two'
-- def Two' : nat :=
-- Succ (Succ Zero)
    

通常のプログラム言語であればTwoとTwo'が等しいことはtest関数などですぐに確かめられそうですが、ここはLEAN4。
自力で証明する必要があります。証明すべき定理は以下の主張です。

      theorem Two_eq_Two' : Two = Two' := sorry
    

証明を保留にするため:= sorryを使います。sorryを使うとデバッグ画面にdeclaration uses 'sorry'と出力されます。

証明は単純で、両者が等しいことがわかっているのでrflを使います：

      theorem Two_eq_Two' : Two = Two' := by
{rfl}

#print Two_eq_Two'
-- theorem Two_eq_Two' : Two = Two' :=
-- rfl
    

カッコの中にカーソルを合わせるとgoals accomplishedが出力され、証明が完了したことが確認出来ます。

全体コード

      inductive nat : Type
  | Zero : nat
  | Succ (n: nat) : nat

open nat

def One := Succ Zero
def Two := Succ One
def Two' := Succ (Succ Zero)

#print Two
#print Two'

theorem Two_eq_Two' : Two = Two' := by
{rfl}

#print Two_eq_Two'