休憩：タクティク・帰納法・証明

証明とユーザインタフェースについての注意

本書では証明の書き方について、あたかも一度に書いてLeanに提出し、Leanがエラーメッセージを返して残りの作業を説明するものであるかのように紹介しました。Leanとのやりとりは実際にはもっと楽しいものです。Leanはカーソルが移動するたびに証明に関する情報を提供し、証明を簡単にする対話的な機能も多数存在します。詳細についてはLean開発環境のドキュメントを参照してください。

本書での、証明の段階的な構築とその結果得られるメッセージの表示に焦点を当てたアプローチは、Leanのエキスパートが使う手順よりはるかに遅いとはいえ、証明を書いている最中にLeanが提供してくれる種類の対話的なフィードバックを示しています。同時に、不完全な証明が完全なものへと進化していく過程を見ることは、証明する上で有益な視点となります。証明を書くスキルが上がるにつれて、Leanのフィードバックはエラーではなく、読者自身の思考プロセスをサポートするものであると感じられるようになるでしょう。対話的なアプローチを学ぶことはとても重要です。

再帰と帰納法

前章の関数 plusR_succ_left と plusR_zero_left は2つの観点から見ることができます。一方からは、他の再帰関数がリストや文字列などのデータ構造を構築するのと同じように、命題の根拠を構築する再帰関数となります。他方からは、これは 数学的帰納法 （mathematical induction）による証明でもあります。

数学的帰納法はある文が以下の2つのステップによって すべての 自然数について証明されるという証明技法です：

1. その文が \( 0 \) について成り立つことを示す。これは 基本ケース （base case）と呼ばれます。
2. その文がとある任意に選ばれた整数 \( n \) について成り立つという仮定の下で \( n + 1 \) について成り立つことを示す。これは 帰納法のステップ （induction step）と呼ばれます。その文が \( n \) について成り立つという仮定は 帰納法の仮定 （induction hypothesis）と呼ばれます。

ある文を すべての 自然数についてチェックすることは不可能であるため、帰納法は原理的にはどのような自然数にも拡張できる証明を書く手段を提供します。例えば、3という値について具体的な証明が必要な場合、まず基本ケースを使い、次に帰納法のステップを3回使うことで、0・1・2、そして最後に3について証明することができます。こうして、すべての自然数についての証明ができます。

帰納法のタクティク

congrArg のような補助関数を使用する再帰関数として帰納法による証明を書くことは、証明の背後にある意図を表現するにあたっては必ずしも良い仕事ではありません。再帰関数は確かに帰納法の構造を持っていますが、これは証明を エンコード したものと見なすべきでしょう。さらに、Leanのタクティクシステムは、再帰関数を明示的に記述する時には利用できない、証明の構築を自動化する多くの機会を提供します。Leanは1つのタクティクブロックで帰納法による証明全体を実行できる帰納法用の タクティク を提供しています。裏では、Leanは帰納法の使用に対応する再帰関数を構築しています。

帰納法のタクティクで plusR_zero_left を証明するには、まずそのシグネチャを書くことから始めます（これは正真正銘の証明であるため、theorem を使います）。続いて、by induction k を定義の本体として使います：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k

出力されるメッセージでは2つのゴールが示されます：

unsolved goals
case zero
⊢ Nat.zero = Nat.plusR 0 Nat.zero

case succ
n✝ : Nat
n_ih✝ : n✝ = Nat.plusR 0 n✝
⊢ Nat.succ n✝ = Nat.plusR 0 (Nat.succ n✝)

タクティクブロックはLeanの型チェッカがファイルを処理する間に実行されるプログラムであり、C言語のプリプロセッサマクロをより強力にしたようなものです。これらのタクティクは実際のプログラムを生成します。

タクティク言語ではゴールは複数になることがあります。それぞれのゴールは型といくつかの仮定から構成されます。これらはアンダースコアをプレースホルダとして使った場合と似ています。すなわち、ゴールの型は証明されるものを、仮定はスコープ内で使用できるものをそれぞれ表します。ゴール case zero の場合、仮定は無く、型は Nat.zero = Nat.plusR 0 Nat.zero となり、これは定理の k を 0 に置き換えた文です。ゴール case succ では、n✝ と n_ih✝ という2つの仮定があります。裏では、induction タクティクによって全体の型を絞り込む依存パターンマッチが作成され、n✝ はそのパターンにおける Nat.succ の引数を表しています。仮定 n_ih✝ は生成された関数を n✝ に対して再帰的に呼び出した結果を表します。その型は定理の全体的な型に対して、ただ k の代わりに n✝ にしただけのものです。ゴール case succ の一部として満たされる型は、定理全体の型に対して、k の代わりに Nat.succ n✝ にしたものです。

induction タクティクを使用した結果得られた2つのゴールは数学的帰納法の説明における基本ケースと帰納法のステップに相当します。基本ケースは case zero です。case succ では、n_ih✝ が帰納法の仮定に、case succ の全体が帰納法のステップにそれぞれ相当します。

この証明の記述にあたっての次のステップは2つのゴールに対して順番に焦点を当てることです。do ブロックにおいて pure () を使うことで「何もしない」ことを示すことができるように、タクティク言語には skip という文があり、これも何もしません、これはLeanの構文がタクティクを要求しているものの、まだどれを使うべきか明確でない場合に使うことができます。with を induction 文の最後に追加すると、パターンマッチに似た構文になります：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => skip
  | succ n ih => skip

2つの skip 文にはそれぞれメッセージが関連付けられます。1つ目は基本ケースについて示しています：

unsolved goals
case zero
⊢ Nat.zero = Nat.plusR 0 Nat.zero

2つ目は帰納法のステップについて示しています：

unsolved goals
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 (Nat.succ n)

帰納法のステップにて、ダガーが付いたアクセスできない名前は succ の後に置いた名前、すなわち n と ih によって置き換えられています。

induction ... with の後にあるこれらのケースはパターンではありません：これらは0個以上の名前を伴うゴールの名前です。この名前はゴールで導入される仮定に使われます；ゴールが導入する以上の名前を指定するとエラーになります：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => skip
  | succ n ih lots of names => skip

too many variable names provided at alternative 'succ', #5 provided, but #2 expected

基本ケースに焦点を当てると、再帰関数の中での場合と同じように、rfl タクティクが induction タクティクの中でもうまく機能します：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => rfl
  | succ n ih => skip

この証明の再帰関数によるものでは、型注釈によって期待される型が理解しやすいものになっていました。タクティク言語ではゴールを解きやすくするための具体的な変換方法がいくつもあります。unfold タクティクは定義された名前をその定義に置き換えます：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => rfl
  | succ n ih =>
    unfold Nat.plusR

これで、ゴールの等式の右辺は Nat.plusR 0 (Nat.succ n) ではなく Nat.plusR 0 n + 1 になりました：

unsolved goals
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ n = Nat.plusR 0 n + 1

congrArg のような関数や ▸ のような演算子に訴える代わりに、証明のゴールを等号の証明によって変換することができるタクティクがあります。最も重要なものの1つが rw で、これは等号の証明のリストを受け取り、各等式の左辺に対応するゴールの式を右辺で置き換えます。これは plusR_zero_left にてほとんど正しく機能します：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => rfl
  | succ n ih =>
    unfold Nat.plusR
    rw [ih]

しかし、書き換えの方向性が誤っていました。n を Nat.plusR 0 n に置き換えたことでゴールの複雑性は減るどころかむしろ増えました：

unsolved goals
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ Nat.succ (Nat.plusR 0 n) = Nat.plusR 0 (Nat.plusR 0 n) + 1

これは rewrite の呼び出しで ih の前に左向き矢印を置くことで改善されます。これは等式の右辺を左辺で置き換えるよう指示します：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => rfl
  | succ n ih =>
    unfold Nat.plusR
    rw [←ih]

この書き換えによって等式の両辺が同一になり、Leanはこれをもって rfl を処理します。これで証明は完了です。

タクティクゴルフ

ここまでのところ、タクティク言語はその真価をまだ発揮していません。上記の証明は再帰関数より短くありません；これは完全なLeanの言語ではなく、ドメイン固有の言語で書かれているに過ぎません。しかし、タクティクを使った証明はより短く、より簡単で、より保守しやすいものになります。ゴルフでスコアが低い方が良いように、タクティクゴルフでは証明が短い方が良いです。

plusR_zero_left の帰納法のステップは単純化のためのタクティク simp を使って証明することができます。simp を単独で使っても役に立ちません：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => rfl
  | succ n ih =>
    simp

simp made no progress

しかし、simp は定義の集まりを使用するように設定することができます。rw と同様に、これらの引数はリストで提供します。simp に Nat.plusR の定義を考慮するよう依頼すると、よりシンプルなゴールにたどり着きます：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => rfl
  | succ n ih =>
    simp [Nat.plusR]

unsolved goals
case succ
n : Nat
ih : n = Nat.plusR 0 n
⊢ n = Nat.plusR 0 n

特に、このゴールは帰納法の仮定と同じものになりました。単純な等式を自動的に証明するだけでなく、単純化は Nat.succ A = Nat.succ B のようなゴールを A = B に自動的に置き換えます。帰納法の仮定 ih はまさに（exactly）正しい型を持っているため、exact タクティクによってその仮定を使うべきであることを示すことができます：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => rfl
  | succ n ih =>
    simp [Nat.plusR]
    exact ih

しかし、exact の使用はやや脆弱です。証明を「ゴルフ」している最中に帰納法の仮定の名前の変更があり得るため、この証明が機能しなくなる原因になります。assumption タクティクは仮定のうちの どれか がゴールにマッチすれば、それによって現在のゴールを解決します：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k with
  | zero => rfl
  | succ n ih =>
    simp [Nat.plusR]
    assumption

この証明は展開と明示的な書き換えを行った以前の証明よりも短くありません。しかし、simp が多くの種類のゴールを解決できるという事実を利用して、一連の変換を変換をより短くすることができます。最初のステップは induction の後ろの with を削除することです。構造化された読みやすい証明のためには、with 構文は便利です。ケースが欠けていれば文句を言い、帰納法の構造を明確に示すことができます。しかし、証明を短くするには、もっと自由なアプローチが必要になることがよくあります。

with 無しの induction を使用すると証明の状態は単純に2つのゴールを持ったものになります。induction ... with タクティクの分岐と同じように、case タクティクをそのどちらかのゴールを選択するために使うことができます。言い換えると、次の証明は前の証明と等価です：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k
  case zero => rfl
  case succ n ih =>
    simp [Nat.plusR]
    assumption

ゴールを1つ持つコンテキスト（つまり k = Nat.plusR 0 k ）では、induction k タクティクは2つのゴールを生成します。一般的には、タクティクはエラーで失敗するかあるゴールを0個以上の新しいゴールに変換します。それぞれの新しいゴールは証明すべきことが残っていることを表します。もしその結果ゴールが0個になれば、そのタクティクは成功であり、その部分の証明は終わったことになります。

<;> 演算子は2つのタクティクを引数に取り、新しいタクティクを生成します。T1 <;> T2 は T1 を現在のゴールに適用し、続いて T2 を T1 が作成した すべての ゴールに適用します。言い換えると、<;> は多くの種類のゴールを解決することができる一般的なタクティクを、一度に複数のゴールに使用することを可能にします。そのような一般的なタクティクの1つが simp です。

simp はこの証明の基本ケースの完成と帰納法のステップを進めることの両方を行うことができるため、induction と <;> と一緒に使うことで証明を短縮することができます：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k <;> simp [Nat.plusR]

この結果、ゴールはただ1つ、変換された帰納法のステップだけとなります：

unsolved goals
case succ
n✝ : Nat
n_ih✝ : n✝ = Nat.plusR 0 n✝
⊢ n✝ = Nat.plusR 0 n✝

このゴールで assumption を実行すれば証明が完了します：

theorem plusR_zero_left (k : Nat) : k = Nat.plusR 0 k := by
  induction k <;> simp [Nat.plusR] <;> assumption

ここで ih が明示的に名付けられていないため、exact は使えないでしょう。

初心者にとって、この証明は読みやすくはありません。しかし、熟練したユーザにとって simp のような強力なタクティクで多くの単純なケースを処理し、証明のテキストを興味深いケースに集中させることはよくあるパターンです。さらに、このような証明は、証明に関係する関数やデータ型の小さな変更に対して頑強である傾向があります。タクティクゴルフゲームは、証明を書く時のセンスとスタイルを磨くことに役立ちます。

他のデータ型への帰納法

数学的帰納法は Nat.zero の基本ケースと Nat.succ の帰納法のステップを提供することで自然数についての文を証明します。帰納法の原理はほかのデータ型でも有効です。再帰引数を持たないコンストラクタが基本ケースを形成し、再帰引数を持つコンストラクタが帰納法のステップを形成します。帰納法によって証明を実行できるこの能力がまさにこれらのデータ型を 帰納的 データ型と呼ぶ所以です。

その一例が二分木に対する帰納法です。二分木に対する帰納法は、ある文が以下の2つのステップによって すべての 二分木について証明されるという証明技法です：

1. その文が BinTree.leaf について成り立つことを示す。これは基本ケースと呼ばれます。
2. その文がとある任意に選ばれた木 l と r について成り立つという仮定の下で BinTree.branch l x r について成り立つことを示す。ここで x は任意に選ばれた新しいデータの点です。これは 帰納法のステップ と呼ばれます。その文が l と r について成り立つという仮定は 帰納法の仮定 と呼ばれます。

BinTree.count は木にある枝の数を数えます：

def BinTree.count : BinTree α → Nat
  | .leaf => 0
  | .branch l _ r =>
    1 + l.count + r.count

木のコピー は木の枝の数を変えません。これは木に対する帰納法を使って証明できます。最初のステップは定義を述べて induction を呼び出すことです：

theorem BinTree.mirror_count (t : BinTree α) : t.mirror.count = t.count := by
  induction t with
  | leaf => skip
  | branch l x r ihl ihr => skip

基本ケースは葉のコピーの数の計上は、もとの葉の数の計上と同じということを述べています：

unsolved goals
case leaf
α : Type
⊢ count (mirror leaf) = count leaf

帰納法のステップでは、左と右の部分木のコピーをしても枝の数に影響がないという仮定を許し、これらの部分木を含んだ木をコピーしても全体の枝の数が保たれるという証明を要求します：

unsolved goals
case branch
α : Type
l : BinTree α
x : α
r : BinTree α
ihl : count (mirror l) = count l
ihr : count (mirror r) = count r
⊢ count (mirror (branch l x r)) = count (branch l x r)

基本ケースは真です。というのも leaf をコピーすると leaf になり、式の左右は定義上同値になるからです。これは simp を使って BinTree.mirror を展開する命令で表現できます：

theorem BinTree.mirror_count (t : BinTree α) : t.mirror.count = t.count := by
  induction t with
  | leaf => simp [BinTree.mirror]
  | branch l x r ihl ihr => skip

帰納法のステップでは、ゴールの中に帰納法の仮定とすぐに一致するものはありません。BinTree.count と BinTree.mirror の定義を使って単純化すると、関係性が明らかになります：

theorem BinTree.mirror_count (t : BinTree α) : t.mirror.count = t.count := by
  induction t with
  | leaf => simp [BinTree.mirror]
  | branch l x r ihl ihr =>
    simp [BinTree.mirror, BinTree.count]

unsolved goals
case branch
α : Type
l : BinTree α
x : α
r : BinTree α
ihl : count (mirror l) = count l
ihr : count (mirror r) = count r
⊢ 1 + count (mirror r) + count (mirror l) = 1 + count l + count r

帰納法の仮定がどちらもゴールの左辺を右辺の近いものに書き換えるために使うことができます：

theorem BinTree.mirror_count (t : BinTree α) : t.mirror.count = t.count := by
  induction t with
  | leaf => simp [BinTree.mirror]
  | branch l x r ihl ihr =>
    simp [BinTree.mirror, BinTree.count]
    rw [ihl, ihr]

unsolved goals
case branch
α : Type
l : BinTree α
x : α
r : BinTree α
ihl : count (mirror l) = count l
ihr : count (mirror r) = count r
⊢ 1 + count r + count l = 1 + count l + count r

simp_arith タクティクは simp に追加で算術的な等式を使用できるようにしたもので、この目標を証明するにあたって十分であり、以下を出力します：

theorem BinTree.mirror_count (t : BinTree α) : t.mirror.count = t.count := by
  induction t with
  | leaf => simp [BinTree.mirror]
  | branch l x r ihl ihr =>
    simp [BinTree.mirror, BinTree.count]
    rw [ihl, ihr]
    simp_arith

展開される定義に加えて、単純化器は証明ゴールを単純化する間に書き換えとして使用する等式証明の名前を渡すこともできます。BinTree.mirror_count は以下のように書くこともできます：

theorem BinTree.mirror_count (t : BinTree α) : t.mirror.count = t.count := by
  induction t with
  | leaf => simp [BinTree.mirror]
  | branch l x r ihl ihr =>
    simp_arith [BinTree.mirror, BinTree.count, ihl, ihr]

証明が複雑になると、手作業で仮定を列挙することは面倒になります。さらに、手作業で仮定の名前を書くと複数のサブゴールの証明ステップでの再利用が難しくなります。simp や simp_arith に * という引数を与えることで、ゴールを単純化したり解いたりする際に、全ての 仮定を使用するように指示することができます。つまり、証明は以下のようにも書けます：

theorem BinTree.mirror_count (t : BinTree α) : t.mirror.count = t.count := by
  induction t with
  | leaf => simp [BinTree.mirror]
  | branch l x r ihl ihr =>
    simp_arith [BinTree.mirror, BinTree.count, *]

どちらの分岐も単純化器を使用しているため、証明は以下のように簡約されます：

theorem BinTree.mirror_count (t : BinTree α) : t.mirror.count = t.count := by
  induction t <;> simp_arith [BinTree.mirror, BinTree.count, *]

演習問題

• induction ... with タクティクを使って plusR_succ_left を証明してください。
• plus_succ_left の証明を <;> を使って一行になるよう書き換えてください。
• リストについての帰納法を使って、リストの連結が結合的であることを証明してください：theorem List.append_assoc (xs ys zs : List α) : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs