Lean Theorem Prover で Maybe モナド

Lean Theorem Prover で Maybe モナドを作ってみる。

[2016/12/11 追記]下記はlean2の場合。[/追記]
その前にセットアップ関連のメモ。私は Windows ユーザーなので、Windows の場合について。このダウンロードページ からバイナリをダウンロードできるが、ライブラリが古い感じなので、GitHub からソースコードを取得してビルドする。
GitHubに手順が書いてあるのでそれに従うだけ。Windowsの場合、msys2かCygwinが必要ですが、私はmsys2で。このページに書いてある通りに、まずはmsys2をインストールし、次に依存ライブラリをインストール、そしてGitHubからソースを取得してビルド。特に問題なく終了。
[2016/12/11 追記]
lean3の場合は次のようにする。

1. バイナリはまだないようなので、GitHub からソースコードを取得。
2. Cygwinの記述がなくなっているので、msys2で。
3. Build Lean に記述されている「cmake ../src -G Ninja -D CMAKE_BUILD_TYPE=Release」は「cmake ../src -G Ninja -DCMAKE_BUILD_TYPE=Release」が正しいので注意する。

[/追記]

なお、ドキュメントとしてオンラインとPDFのバージョンのチュートリアルがあり、このページからリンクまたはダウンロードできる。

[2016/12/11 追記]
以下の記述は lean2 のものです。lean3 ではそのままでは動きません。
[/追記]

ではモナドクラスを作ってみる。

monad1.lean

structure Monad [class] (M : Type → Type) :=
  (return : Π {A : Type}, A → M A)
  (bind : Π {A B : Type}, M A → (A → M B) → M B)
  (left_identity : Π {A B : Type} (a : A) (f : A → M B),
    (bind (return a) f) = (f a))
  (right_identity : Π {A : Type} (m : M A), bind m return = m)
  (associativity : Π {A B C : Type} (m : M A) (f : A → M B) (g : B → M C),
    bind (bind m f) g = bind m (λx, bind (f x) g))

maybeインスタンスを作る。optionはすでに定義されているので、それを使ってreturnとbindを定義。次のコードを下に追加。

monad1.lean

namespace maybe

  definition return {A : Type} (x : A) := option.some x

  definition bind {A B : Type} : option A → (A → option B) → option B
  | bind (option.none) f := (option.none)
  | bind (option.some x) f := f x

end maybe

続いて、left_identity の定義、というか証明をする。bindの下に次を追加。

monad1.lean

  theorem left_identity {A B : Type} (a : A) (f : A → option B) :
    bind (return a) f = f a :=
  begin
  end

ここで monad1.lean を lean.exe にかけてみると次のエラーがでる。

c:\example\monad1.lean:21:2: error: 1 unsolved subgoal
A : Type,
B : Type,
a : A,
f : A → option B
⊢ bind (return a) f = f a
c:\example\monad1.lean:21:2: error: failed to add declaration 'maybe.left_identity' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
  ?M_1

そこで、left_identityのbeginとendの間に apply rfl をいれてみる。

monad1.lean

  theorem left_identity {A B : Type} (a : A) (f : A → option B) :
    bind (return a) f = f a :=
  begin
    apply rfl
  end

こうするとエラーが発生しなくなる。つまり証明できた。
続いて、right_identity の証明は次の通り。さきほどのleft_identityの下に追加する。

monad1.lean

  theorem right_identity {A : Type} (m : option A) :
    bind m return = m :=
  begin
    cases m,
    apply rfl,
    apply rfl
  end

m のパターンによって場合分けして、それぞれ計算する、ということですね。
最後に associativity の証明。right_identity の下に追加。

monad1.lean

  theorem associativity {A B C : Type} (m : option A)
    (f : A → option B) (g : B → option C) :
    bind (bind m f) g = bind m (λx, bind (f x) g) :=
  begin
    cases m,
    apply rfl,
    apply rfl
  end

こちらもm のパターンによって場合分けして、それぞれ計算、で証明できる。

最後にMaybeインスタンスを作成する。end maybe のあと。

monad1.lean

definition Maybe [instance] {A : Type} : Monad option :=
Monad.mk (@maybe.return) (@maybe.bind)
  (@maybe.left_identity) (@maybe.right_identity)
  (@maybe.associativity)

ちなみに「@」を指定しているのは、型変数を省略しないようにするため。
これでMaybeモナドができた。最終的なコードは次の通り。

monad1.lean

structure Monad [class] (M : Type → Type) :=
  (return : Π {A : Type}, A → M A)
  (bind : Π {A B : Type}, M A → (A → M B) → M B)
  (left_identity : Π {A B : Type} (a : A) (f : A → M B),
    (bind (return a) f) = (f a))
  (right_identity : Π {A : Type} (m : M A), bind m return = m)
  (associativity : Π {A B C : Type} (m : M A) (f : A → M B) (g : B → M C),
    bind (bind m f) g = bind m (λx, bind (f x) g))

namespace maybe

  definition return {A : Type} (x : A) := option.some x

  definition bind {A B : Type} : option A → (A → option B) → option B
  | bind (option.none) f := (option.none)
  | bind (option.some x) f := f x

  theorem left_identity {A B : Type} (a : A) (f : A → option B) :
    bind (return a) f = f a :=
  begin
    apply rfl
  end

  theorem right_identity {A : Type} (m : option A) :
    bind m return = m :=
  begin
    cases m,
    apply rfl,
    apply rfl
  end

  theorem associativity {A B C : Type} (m : option A)
    (f : A → option B) (g : B → option C) :
    bind (bind m f) g = bind m (λx, bind (f x) g) :=
  begin
    cases m,
    apply rfl,
    apply rfl
  end
end maybe

definition Maybe [instance] {A : Type} : Monad option :=
Monad.mk (@maybe.return) (@maybe.bind)
  (@maybe.left_identity) (@maybe.right_identity)
  (@maybe.associativity)