証明支援システムLeanに入門する #2
ここからはLeanを記述する際の実際の動きを確認していきます.
Natural number gameというものの存在は知っていたのですが,今回はプログラミング言語という側面からLeanを知っていきたいと思ったので,純粋なリファレンスを読み進めていこうと思います.
Lean4のリファレンスはWork in Progressだとありましたが,入門には問題なさそうなので公式のWebサイトに用意されている Lean Manual を読んでいきます.簡単な和訳をしながら,自分の思ったことを記述していくような記事になる予定です.Leanに関して無知な人間が思ったことを雑に書いていく記事なので,嘘や根拠のない予想が多く含まれます.この記事に書かれていることを鵜呑みにしないように注意をお願いします.
1. What is Lean
Leanがプログラミング言語であることから始まり,Leanの特徴が書かれています.文法に関する簡単な紹介もあります.
-- Defines a function that takes a name and produces a greeting.
def getGreeting (name : String) := s!"Hello, {name}! Isn't Lean great?"
関数の定義はdef
キーワードを用いて行い,引数は(name: Type)
と取るようです.詳細は後の章に任せて読み流していきます.
その下にはLeanが持つ機能についての記述があり,
- 型推論
- 一階関数
- 強力なデータ型
- パターンマッチング
- 型クラス
- モナド
- 文法拡張
- 健全なマクロ
- 依存型
- メタプログラミング
- マルチスレッド
- 証明
と,様々な機能を持つことが書かれています.Haskellをよく書く私としてはワクワクする言葉が並びます.
2. Tour of Lean
この章では具体的なコードを読み書きしながらLeanの主な機能を学ぶようです.Leanには 関数,型 という2つの重要な概念が存在するとも書かれています.
Function and Namespaces
Leanのプログラムの最も基本的な部分は,名前空間に属する関数だといいます.様々な働きをする関数たちをグループ分けする最も基礎的な方法として名前空間が用意されています.
namespace Besic Functions
これが名前空間の定義です.
def sampleFunction1 x := x*x + 3
def result1 := sampleFunction1 4573
先に確認したようにLeanは関数型の言語ですので,定数も関数と同じ文法で同じように定義します.(定数は引数を持たない定数関数と解釈されます.)
ここでは
#eval 2 + 2 -- 4が出力される
#eval println! "The result of squaring the integer 4573 and adding 3 is {result1}"
Leanでは文字列中に{}
を入れることで文字列の埋め込みができるようです.{}
の中に文字列でないものが入ってもきちんとキャストされています.型クラスの概念が用意されていると書いていたので,恐らくHaskellのShow
に対応するような型クラスがあるのだと思います.
#eval
コマンドは,与えられた式を解釈して標準出力に出力するコマンドみたいです.
println!
はそれ自身が標準出力に出力しているような気がするのですが,具体的にどういう動作をしているのかは今は考えないことにしておきます.println!
は返り値のないマクロで,#eval
にマクロが与えられたときは式の解釈のみをするのかなぁと予想をして次に進みます.
def sampleFunction2 (x : Nat) := 2*x*x - x + 3
def result2 := sampleFucntion2 (7 + 4)
Leanには型推論が用意されているとのことでしたが,当然必要ならば型を明示することもできるみたいです.Nat
はNatural numberで自然数の意味です.
簡単な条件分岐も出てきました.
def sampleFunction3 (x : Int) :=
if x > 100 then
2*x*x - x + 3
else
2*x*x + x - 37
非常に完結でわかりやすい文法です.プログラミングの経験が少しでもある方にはもはや説明することもほぼありません.
if expression then
trueのときの処理
else
falseのときの処理
という文法を持つようです.if
文全体が式として処理され,関数の返り値を与えているのもポイントです.
end BasicFunctions
名前空間が閉じられました.
def twice (f : Nat → Nat) (a : Nat) :=
f (f a)
さて,関数を引数に持つ関数が現れました.f
は自然数から自然数への関数であり,a
は自然数です.twice
はa
に対してf
を二回適用する関数だと読み取れます.
#eval twice (fun x => x + 2) 10
fun
キーワードは無名関数の宣言に使われています.シンプルで良いです.
theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 :=
rfl
早速他の言語にはあまりない予約語が登場しました.どうやら,theorem
というキーワードで定理を宣言できるようです.今回の定理はfun x => x + 2
を二回適用するとfun x => x + 4
になるという主張です.では証明を,と思ったのですが,rfl
の一言で閉じられています.Leanには強力な自動証明系が備わっており,記号的な操作で証明が完了してしまうような命題については自動で証明してくれるようです.強い.
#eval twice (· + 2) 10
・ + 2
はfun x => x + 2
の糖衣構文だと書かれています.数学でも偶に書くプレースホルダが使えるようです.わかりやすくて嬉しいです.
inductive Weekday where
| sunday : Weekday
| monday : Weekday
| tuesday : Weekday
| wednesday : Weekday
| thursday : Weekday
| friday : Weekday
| saturday : Weekday
「列挙型はinductive
の特別なパターンです」とありますが.inductive
をまだ知らないのでよくわかりません.とりあえず列挙型に固有のデータ型が与えられているわけではなく,より一般的な型が存在するのだと思っておくことにします.(Weekday
って8回も書くのマジ?となっています)
こう書くことで,Weekday
名前空間の中にsunday
〜saturday
のコンストラクタが定義されるようです.
#check Weekday.sunday
#check Weekday.monday
#check
コマンドは与えられた引数の型を表示してくれます.この例ではこのように出力されました.
当然,Weekday
の型はType
となりました.
open Weekday
#check sunday
#check tuesday
open
コマンドを使うことで名前空間を展開でき,名前空間の指示なしに中身を参照できるようになります.
def natOfWeekday (d : Weekday) : Nat :=
match d with
| sunday => 1
| monday => 2
| tuesday => 3
| wednesday => 4
| thursday => 5
| friday => 6
| saturday => 7
この関数はパターンマッチングを用いてWeekday
からNat
への変換を行います.
def isMonday : Weekday → Bool :=
fun
| monday => true
| _ => false
こちらの関数は少々難解です.コメントによればこれは
fun d => match d with
| monday => true
| _ => false
の糖衣構文だということです.無名関数の引数をそのままパターンマッチングの引数に流す操作をシンプルにかけるようになっています.また,関数の本体が無名関数になっていることで,isMonday
自身には引数がないように見えているのもポイントです.
eval toString 10
#eval toString (10, 20)
文字列へキャストする関数はtoString
で提供されているようです.
文字列へキャストできる型クラスはToString
で定義されていました.
ToString
のインスタンスの実装も簡単に行なえます.
instance : ToString Weekday where
toString (d : Weekday) : String :=
match d with
| sunday => "Sunday"
| monday => "Monday"
| tuesday => "Tuesday"
| wednesday => "Wednesday"
| thursday => "Thursday"
| friday => "Friday"
| saturday => "Saturday"
やはりパターンマッチングを使用しています.
def Weekday.next (d : Weekday) : Weekday :=
match d with
| sunday => monday
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => saturday
| saturday => sunday
Weekday
という名前空間にnext
関数を定義しています.
#eval Weekday.next Weekday.wednesday
#eval next wednesday
先にWeekday
名前空間をopen
したので,指定がなくとも参照できていることがわかります.
def Weekday.previous : Weekday -> Weekday
| sunday => saturday
| monday => sunday
| tuesday => monday
| wednesday => tuesday
| thursday => wednesday
| friday => thursday
| saturday => friday
theorem Weekday.nextOfPrevious (d : Weekday) : next (previous d) = d :=
match d with
| sunday => rfl
| monday => rfl
| tuesday => rfl
| wednesday => rfl
| thursday => rfl
| friday => rfl
| saturday => rfl
この定理は「ある日の次の日の前の日」がある日と一致することを述べていますが,やはり記号的操作で完結するので自動的に証明が完了します.
また,
theorem Weekday.nextOfPrevious' (d : Weekday) : next (previous d) = d := by
cases d
all_goals rfl
とすればパターンマッチングを記述することなく証明が完了します.実際にLean Infoview
で確認したところ,cases
により全てのパターンが展開され,各々がゴールに設定され,all_goals
は全てのゴールに対して同じ操作を,今回であればrfl
を適用して証明終了,という流れでした.
さて,大まかな流れは掴めてきたので,次回は 4. Theorem Proving in Lean の指示に従ってTheorem Proving in Lean 4を読み進めようと思います.
Discussion
Theorem proving in lean4 は日本語訳もありますよ。https://aconite-ac.github.io/theorem_proving_in_lean4_ja/title_page.html
なんと,そうだったのですね.ありがとうございます.