休憩：命題・証明・リストの添え字アクセス

多くの言語と同様に、Leanは角括弧を配列とリストへの添え字アクセスに使います。例えば、woodlandCitters が以下のように定義されているとします：

def woodlandCritters : List String :=
  ["hedgehog", "deer", "snail"]

ここで、各要素は次のようにして展開することができます：

def hedgehog := woodlandCritters[0]
def deer := woodlandCritters[1]
def snail := woodlandCritters[2]

しかし、4番目の要素を取り出そうとすると、実行時エラーではなくコンパイル時エラーとなります：

def oops := woodlandCritters[3]

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
⊢ 3 < List.length woodlandCritters

このエラーメッセージは、Leanが 3 < List.length woodlandCritters を自動で数学的に証明しようとして（これはルックアップが安全であることを意味します）、それができなかったというものです。リストの範囲外エラーはごくありふれたバグであり、Leanはプログラミング言語と定理証明器の2つの性質を利用して、できるだけ多くのエラーを除外します。

この仕組みを理解するには、命題・証明・タクティクという3つの重要な考え方を理解する必要があります。

命題と証明

命題 （proposition）とは、真にも偽にもなりうる文のことです。以下はすべて命題です：

• 1 + 1 = 2
• 足し算は可換である
• 素数は無限に存在する
• 1 + 1 = 15
• パリはフランスの首都である
• ブエノスアイレスは韓国の首都である
• すべての鳥は飛ぶことができる

一方で、無意味な文は命題ではありません。以下はどれも命題ではありません：

• 1 + 緑 = アイスクリーム
• すべての首都は素数である
• 少なくとも1つのホゲはフガである

命題は2つに分類されます：純粋に数学的なもので、私たちの概念の定義にのみ依存するものと、世界に関する事実であるものです。Leanのような定理証明器は前者のカテゴリを扱っており、ペンギンの飛行能力や都市の法的地位について語ることはありません。

証明 （proof）とは、ある命題が真であることを説得させる論証のことです。数学的命題の場合、これらの論証はそれに関連する概念の定義と論理的論証の規則を利用します。ほとんどの証明は人々が理解できるように書かれており、多くの面倒な詳細は省かれています。Leanのような計算機による定理証明支援器は、数学者が多くの詳細を省きながら証明を書けるように設計されており、欠落している明白なステップを埋めるのはソフトウェアの責任です。これにより見落としや間違いの可能性を減らすことができます。

Leanでは、プログラムの型はそのプログラムがほかのプログラムとどのように相互作用できるかを記述したものです。例えば、Nat → List String という型のプログラムは、引数 Nat を受け取り、文字列のリストを生成する関数です。言い換えると、それぞれの型はその型を持つプログラムとしての大事なポイントを指定したものです。

実はLeanにおいて、命題は型です。命題はその文が真であることの根拠としての大事なポイントを指定します。この根拠を提示することで、命題が証明されます。一方で、命題が偽であれば、証明を構築することは不可能です。

例えば、「1 + 1 = 2」という命題はLeanでそのまま記述することができます。この命題の根拠はコンストラクタ rfl で、この名称は 反射性 （reflexivity）の略です：

def onePlusOneIsTwo : 1 + 1 = 2 := rfl

一方で、rfl は偽の命題「1 + 1 = 15」を証明しません：

def onePlusOneIsFifteen : 1 + 1 = 15 := rfl

type mismatch
  rfl
has type
  1 + 1 = 1 + 1 : Prop
but is expected to have type
  1 + 1 = 15 : Prop

このエラーメッセージから、rfl は等号についての文の両辺がすでに同じ数値である場合に2つの式が等しいことを証明できることがわかります。1 + 1 は 2 に直接評価されるので両者は同じとみなされ、 onePlusOneIsTwo がLeanに受け入れられます。Type が Nat や String、List (Nat × String × (Int → Float)) などのデータ構造や関数を表す型を記述するように、Prop は命題を記述します。

証明されると命題は 定理 （theorem）と呼ばれます。Leanでは定理を宣言するときには def の代わりに theorem キーワードを使うのが一般的です。これにより、読者はどの宣言が数学的な証明であり、どの宣言が定義であるかがわかりやすくなります。一般論として、証明で重要なことは命題が真であるという根拠が存在するということであり、 どの 根拠が提示されたかということは特に重要ではありません。一方で、定義の場合、どの特定の値が選択されるかということは非常に重要です。なにしろ、足し算の定義として常に 0 を返すものは明らかに間違っているからです。

前者の例は以下のように書くこともできます:

def OnePlusOneIsTwo : Prop := 1 + 1 = 2

theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl

タクティク

Leanにおける証明は通常、根拠を直接示すのではなく タクティク （tactic）を用いて記述されます。タクティクは命題の根拠を構築する小さなプログラムのことです。これらのプログラムは証明したい文（ ゴール （goal）とよばれます）と利用可能な仮定を用いて証明していく過程である 証明状態 （proof state）の中で実行されます。ゴールに対してタクティクを実行すると、新しいゴールを含む新しい証明状態が生まれます。すべてのゴールが証明されたとき、証明が完了します。

タクティクを使って証明を書くには、定義を by で始めます。by と書くことでこれに続くインデントされたブロックが終わるところまでLeanがタクティクモードになります。タクティクモードでは、Leanは現在の証明状態について継続的なフィードバックを提供します。タクティクを用いた onePlusOneIsTwo もかなり短いものになります：

theorem onePlusOneIsTwo : 1 + 1 = 2 := by
  simp

simp タクティクは「簡約(simplify)」の略で、Leanでの証明の主戦力です。これはゴールをできるだけ単純な形に書き直し、またこの工程の記述を十分小さいものにしてくれます。特に、単純な等号についての文を証明します。その裏では、詳細な形式的証明が構築されますが、simp を使うことでこの複雑さを隠すことができます。

タクティクは多くの理由から便利です：

1. 多くの証明は細部に至るまで書き出すと複雑で面倒になりますが、タクティクはこうした面白くない部分を自動化してくれます。
2. タクティクで書かれた証明は柔軟な自動化によって定義の小さな変更を吸収することができるため、長期にわたるメンテナンスが容易です。
3. 1つのタクティクで多くの異なる定理を証明することができるため、Leanが裏でタクティクを使うことでユーザが手で証明を書く手間を省くことができます。例えば、配列のルックアップにはインデックスが添え字の上限内にあることの証明が必要ですが、タクティクは通常ユーザの気を煩わすことなくその証明を構築することができます。

裏側では、添え字アクセスの表記はユーザのルックアップ操作が安全であることを証明するためにタクティクを使用します。このタクティクは simp であり、ある種の算術的同一性を考慮するように設定されています。

論理結合子

論理の基本的な構成要素である「かつ」・「または」・「真」・「偽」・「～ではない」は 論理結合子 （logical connectives）と呼ばれます。各結合子は、何がその真理の根拠となるかを定義します。例えば、「 A かつ B 」という文を証明するには、 A と B の両方を証明しなければなりません。つまり、「 A かつ B 」の根拠とは、 A の根拠と B の根拠の両方を含むペアのことです。同様に、「 A または B 」の根拠は、 A の根拠と B の根拠のどちらか一方からなります。

特に、これらの結合子のほとんどはデータ型のように定義され、コンストラクタを持ちます。 A と B が命題である場合、「 A かつ B 」（ A ∧ B と書かれます）は命題です。A ∧ B の根拠はコンストラクタ And.intro で構成され、これは A → B → A ∧ B という型を持ちます。A と B を具体的な命題に置き換えれば、1 + 1 = 2 ∧ "Str".append "ing" = "String" を And.intro rfl rfl で証明することができます。もちろん、simp はやはり十分強力であるので以下のように証明してくれます：

theorem addAndAppend : 1 + 1 = 2 ∧ "Str".append "ing" = "String" := by simp

同様に、「 A または B 」（ A ∨ B と書かれます）には2つのコンストラクタがあります。なぜなら、「 A または B 」の証明には、2つの命題のうちどちらか1つが真であることしか要求していないからです。このコンストラクタは A → A ∨ B 型の Or.inl と、B → A ∨ B 型の Or.inr の2つです。

含意（もし A ならば B である）は関数を用いて表現されます。特に、 A の根拠を B の根拠に変換する関数は、それ自体が A ならば B の根拠となります。また、A → B が ¬A ∨ B の省略形です。これは通常の含意の記述とは異なりますが、2つの定式化は等価です。

「かつ」の根拠はコンストラクタであるため、パターンマッチに使用することができます。例えば、「 A かつ B ならば A または B 」の証明は、 A かつ B の根拠から A （もしくは B ）の根拠を取り出し、これを使って A または B の根拠を生成する関数です：

theorem andImpliesOr : A ∧ B → A ∨ B :=
  fun andEvidence =>
    match andEvidence with
    | And.intro a b => Or.inl a

simp タクティクはこれらの結合子を使った定理を証明することができます。例えば以下のように使うことができます：

theorem onePlusOneAndLessThan : 1 + 1 = 2 ∨ 3 < 5 := by simp
theorem notTwoEqualFive : ¬(1 + 1 = 5) := by simp
theorem trueIsTrue : True := True.intro
theorem trueOrFalse : True ∨ False := by simp
theorem falseImpliesTrue : False → True := by simp

引数に現れる根拠

simp はある種の数の等式や不等式を含む命題の証明は得意ですが、変数を含む文の証明は苦手です。例えば、simp は 4 < 15 を証明できますが、x < 4 であるからといって x < 15 も真であるということは simp にとっては簡単にはわかりません。インデックス記法は、配列へのアクセスが安全であることを証明するために裏で simp を使っているので、simp にちょっと手助けする必要があります。

インデックス記法をうまく機能させる最も簡単な方法のひとつは、データ構造へのルックアップを実行する関数に、必要な安全性の根拠を引数として取らせることです。例えば、リストの3番目の要素を返す関数は一般的には安全とは言えません。なぜなら要素の数が0、1または2個であるかもしれないからです：

def third (xs : List α) : α := xs[2]

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is perfomed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.3908
xs : List α
⊢ 2 < List.length xs

しかし、インデックス操作が安全であるという証拠からなる引数を追加することで、リストが少なくとも3つの要素を持たなければならないという制約を呼び出し側に課すことができます：

def third (xs : List α) (ok : xs.length > 2) : α := xs[2]

この例では、xs.length > 2 は xs が2つ以上の要素を 持つかどうか をチェックするプログラムではありません。これは真でも偽でもありうる命題であり、引数 ok はそれが真であることの証拠でなければなりません。

この関数が具体的なリストで呼ばれた場合、その長さはその時点で既知です。この場合、by simp は自動的にエビデンスを構築することができます：

#eval third woodlandCritters (by simp)

"snail"

根拠なしの添え字アクセス

インデックス操作がリストの範囲内であることを証明することが現実的でない場合には、ほかの方法があります。はてなマークを付けると戻り値の型が Option となり、インデックスが範囲内にあれば some 、そうでなければ none となります。例えば以下のようにふるまいます：

def thirdOption (xs : List α) : Option α := xs[2]?

#eval thirdOption woodlandCritters

some "snail"

#eval thirdOption ["only", "two"]

none

また、インデックスが範囲外になったときに Option を返すのではなく、プログラムをクラッシュさせるバージョンも存在します：

#eval woodlandCritters[1]!

"deer"

注意！#eval で実行されるコードはLeanのコンパイラのコンテキストで実行されるため、間違ったインデックスを選択するとIDEがクラッシュする可能性があります。

見るかもしれないメッセージ

Leanがインデックス操作の安全性の根拠をコンパイル時に見つけることができない場合に発生するエラーに加えて、安全でないインデックス操作を使用する多相関数は次のようなメッセージを生成することがあります:

def unsafeThird (xs : List α) : α := xs[2]!

failed to synthesize instance
  Inhabited α

これは、Leanを定理を証明するための論理としてもプログラミング言語としても使えるようにするための技術的な制限によるものです。特に、少なくとも1つは値を持つような型のプログラムだけがクラッシュすることが許可されています。これは、Leanにおける命題がその真理の根拠を分類する型の一種であるためです。偽の命題にはこのような根拠はありません。もし空である型を持つプログラムがクラッシュするとしたら、そのクラッシュしたプログラムは偽の命題のための偽の根拠の一種として使われている可能性があります。

内部的には、Leanは少なくとも1つは値を持つことが知られている型のテーブルを保持しています。このエラーはある任意の型 α がその表にあるとは限らないと言っているのです。この表に追加する方法と、unsafeThird のような関数をうまく書く方法については次の章で説明します。

リストのルックアップに使われる括弧の間にスペースを入れると、別のメッセージが表示されることがあります。

#eval woodlandCritters [1]

function expected at
  woodlandCritters
term has type
  List String

スペースを追加すると、Leanは式を関数適用として扱い、インデックスを1つの数値からなるリストとして扱います。このエラーメッセージは、Leanが woodlandCritters を関数として扱おうとした結果です。

演習問題

• 次の定理を rfl を使って証明してください。また 5 < 18 に適用したら何が起きるでしょうか？そしてそれは何故でしょうか？
  • 2 + 3 = 5
  • 15 - 8 = 7
  • "Hello, ".append "world" = "Hello, world"
• 次の定理を by simp で証明してください。
  • 2 + 3 = 5
  • 15 - 8 = 7
  • "Hello, ".append "world" = "Hello, world"
  • 5 < 18
• リストの5番目の要素をルックアップする関数を書いてください。この関数の引数にはルックアップが安全であるという根拠を渡すようにしてください。