From 8eae5c44150e2b55d7acca5f1b087b556ac493fc Mon Sep 17 00:00:00 2001 From: s-taiga <56785231+s-taiga@users.noreply.github.com> Date: Sun, 1 Sep 2024 00:28:15 +0900 Subject: [PATCH] =?UTF-8?q?10.2=E7=AB=A0=20tail-recursion-proofs=20(#80)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 翻訳開始 * 翻訳完了 * セルフレビュー --- functional-programming-lean/src/SUMMARY.md | 2 +- .../programs-proofs/tail-recursion-proofs.md | 241 ++++++++++++++++++ 2 files changed, 242 insertions(+), 1 deletion(-) diff --git a/functional-programming-lean/src/SUMMARY.md b/functional-programming-lean/src/SUMMARY.md index 69b707da..8cba8647 100644 --- a/functional-programming-lean/src/SUMMARY.md +++ b/functional-programming-lean/src/SUMMARY.md @@ -62,7 +62,7 @@ - [休憩：タクティク・帰納法・証明](./tactics-induction-proofs.md) - [プログラミング・証明・パフォーマンス](programs-proofs.md) - [末尾再帰](programs-proofs/tail-recursion.md) - - [Proving Equivalence](programs-proofs/tail-recursion-proofs.md) + - [同値の証明](programs-proofs/tail-recursion-proofs.md) - [Arrays and Termination](programs-proofs/arrays-termination.md) - [More Inequalities](programs-proofs/inequalities.md) - [Safe Array Indices](programs-proofs/fin.md) diff --git a/functional-programming-lean/src/programs-proofs/tail-recursion-proofs.md b/functional-programming-lean/src/programs-proofs/tail-recursion-proofs.md index 3e24da03..3f57bb66 100644 --- a/functional-programming-lean/src/programs-proofs/tail-recursion-proofs.md +++ b/functional-programming-lean/src/programs-proofs/tail-recursion-proofs.md @@ -1,29 +1,60 @@ + +# 同値の証明 + + + +あるプログラムを末尾再帰とアキュムレータを使うように書き直すと、元のプログラムとはかなり異なった見た目になることがあります。オリジナルの再帰関数の方が大抵理解しやすいですが、実行時にスタックを使い果たしてしまう危険性があります。両方のバージョンのプログラムをいくつかの例でテストして単純なバグを取り除いた後に、証明を使ってこれらのプログラムが同値であることをはっきりと示すことができます。 + + +## `sum` の等価の証明 + + +`sum` についてこの両方のバージョンが等しいことを証明するには、まずスタブの証明で定理の文を書き始めます： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq0}} ``` + + +想定されるようにLeanは未解決のゴールを表示します： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq0}} ``` + + +`NonTail.sum` と `Tail.sum` は定義上同値ではないため、ここでは `rfl` タクティクを使うことはできません。しかし、関数が等しいと言えるのは定義上の同値だけではありません。同じ入力に対して同じ出力を生成することを証明することで、2つの関数が等しいことを証明することも可能です。言い換えると、\\( f = g \\) はすべての可能な入力 \\( x \\) に対して \\( f(x) = g(x) \\) を示すことで証明できます。この原理は **関数の外延性** （function extensionality）と呼ばれます。関数の外延性はまさに `NonTail.sum` が `Tail.sum` と等しいことを説明します：どちらも数値のリストを合計を計算するからです。 + + +Leanのタクティク言語では、関数の外延性は `funext` を使うことで呼び出され、その後に任意の引数に使われる名前が続きます。この任意の引数はコンテキスト中に仮定として追加され、ゴールはこの引数に適用される関数が等しいことの証明を要求するものへと変化します： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq1}} ``` @@ -31,10 +62,15 @@ The arbitrary argument is added as an assumption to the context, and the goal ch {{#example_out Examples/ProgramsProofs/TCO.lean sumEq1}} ``` + + +このゴールは引数 `xs` の帰納法によって証明できます。どちらの `sum` 関数も、空のリストに適用すると基本ケースに対応する `0` を返します。入力リストの先頭に数値を追加すると、両方の関数でその数値を計算結果に加算します。これは帰納法のステップに対応します。`induction` タクティクを実行すると、2つのゴールが得られます： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq2a}} ``` @@ -45,200 +81,362 @@ Invoking the `induction` tactic results in two goals: {{#example_out Examples/ProgramsProofs/TCO.lean sumEq2b}} ``` + + +`nil` に対応する基本ケースは `rfl` を使って解決できます。というのも、どちらの関数も空のリストを渡すと `0` を返すからです： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq3}} ``` + + +帰納法のステップを解く最初のステップはゴールを単純化することで、`simp` によって `NonTail.sum` と `Tail.sum` を展開します： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq4}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq4}} ``` + + +`Tail.sum` を展開することで処理が `Tail.sumHelper` に即座に委譲されていることがわかり、これもまた単純化されるべきです： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq5}} ``` + + +これらによって、ゴールでは `sumHelper` の計算のステップが進み、アキュムレータに `y` が加算されます： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq5}} ``` + + +帰納法の仮定で書き換えを行うことで、ゴールから `NonTail.sum` のすべての言及が削除されます： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEq6}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEq6}} ``` + + +この新しいゴールは、あるリストの和にある数を加えることは、`sumHelper` の最初のアキュムレータとしてその数を使うことと同じであるということを述べています。わかりやすくするために、この新しいゴールは別の定理として証明することができます： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEqHelperBad0}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEqHelperBad0}} ``` + + +繰り返しになりますが、これは帰納法による証明であり、基本ケースは `rfl` を使っています： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEqHelperBad1}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEqHelperBad1}} ``` + + +これは帰納法のステップであるため、ゴールは帰納法の仮定 `ih` と一致するまで単純化する必要があります。`Tail.sum` と `Tail.sumHelper` の定義を使って単純化すると、以下のようになります： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean sumEqHelperBad2}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean sumEqHelperBad2}} ``` + +理想的には、帰納法の仮定を使って `Tail.sumHelper (y + n) ys` を置き換えることができますが、両者は一致しません。この帰納法の仮定は `Tail.sumHelper n ys` には使えますが、`Tail.sumHelper (y + n) ys` には使えません。つまり、この証明は行き詰ってしまいます。 + + + +## 再挑戦 + + +この方針でなんとか頑張る代わりに、ここで一歩引いて考えてみましょう。なぜこの関数の末尾再帰バージョンと非末尾再帰バージョンは等しいのでしょうか？根本的に言えばリストの各要素について、再帰版の結果に加算されるのと同じ量だけアキュムレータが増えます。この洞察によってエレガントな証明を書くことができます。重要なのは、帰納法による証明は帰納法の仮定を **任意の** アキュムレータ値に適用できるように設定しなければならないということです。 + + +先ほどの試みは置いておいて、上記の洞察は次の文にエンコードされます： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper0}} ``` + + +この文において、`n` がコロンの後にある型の一部であることが非常に重要です。この結果、ゴールは「全ての `n` について～」の略である `∀ (n : Nat)` で始まります。 + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper0}} ``` + + +帰納法のタクティクを用いると、この「全ての～について～」という文を含んだゴールができます： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper1a}} ``` + + +`nil` のケースでは、ゴールは次のようになります： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper1a}} ``` + + +`cons` の帰納法のステップでは、帰納法の仮定と具体的なゴールの両方に「全ての `n` について～」が含まれます： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper1b}} ``` + +言い換えると、ゴールの証明はより難しくなりましたが、これに応じて帰納法の仮定はより有用なものになったということです。 + + + +「全ての \\( x \\) について～」で始まる文の数学的な証明はある任意の \\( x \\) を仮定してその文を証明します。ここで「任意」という言葉は \\( x \\) について追加の性質を何も仮定しないことを意味し、これによって文は **どんな** \\( x \\) について成立します。Leanでは、「全ての～について～」文は依存型の関数です：これに適用されるどんな値に対しても、この命題の根拠を返します。同様に、任意の \\( x \\) を選ぶプロセスは ``fun x => ...`` を使うことと同じです。タクティク言語においては、任意の \\( x \\) を選ぶこの処理は `intro` タクティクを使って実行されます。これは裏ではタクティクのスクリプトが完成したタイミングで関数を生成します。`intro` タクティクにはこの任意の値に使用する名前を指定します。 + + +`nil` のケースで `intro` タクティクを使うことでゴールから `∀ (n : Nat),` が取り除かれ、仮定 `n : Nat` が追加されます： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper2}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper2}} ``` + + +この命題の同値の両辺は、定義上 `n` に同値であるため、`rfl` で十分です： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper3}} ``` + + +`cons` のゴールにも「全ての～について～」が含まれます： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper3}} ``` + + +このことから `intro` を使う必要があります。 + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper4}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper4}} ``` + + +これでこの証明のゴールは `NonTail.sum` と `Tail.sumHelper` の両方を `y :: ys` に適用したものとなります。単純化することで次のステップをより明確にすることができます。 + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper5}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper5}} ``` + + +このゴールは帰納法の仮定に非常に近いです。一致しない点は2つです： + + + + * この等式の左辺は `n + (y + NonTail.sum ys)` ですが、帰納法の仮定では左辺は `NonTail.sum ys` に何かしらの数値を足した数であることが求められています。言い換えれば、このゴールは `(n + y) + NonTail.sum ys` と書き直されるべきで、これは自然数の足し算が結合的であることから成り立ちます。 + * 左辺を `(n + y) + NonTail.sum ys` と書き換えた[^1]場合、右辺のアキュムレータの引数は `y + n` ではなく `n + y` とする必要があります。足し算は可換でもあるため、この書き換えも成り立ちます。 + + +足し算の結合性と可換性はLeanの標準ライブラリですでに証明されています。結合性の証明は `{{#example_in Examples/ProgramsProofs/TCO.lean NatAddAssoc}}` という名前で `{{#example_out Examples/ProgramsProofs/TCO.lean NatAddAssoc}}` という型を持ち、可換性の証明は `{{#example_in Examples/ProgramsProofs/TCO.lean NatAddComm}}` という名前で `{{#example_out Examples/ProgramsProofs/TCO.lean NatAddComm}}` という型を持ちます。通常、`rw` タクティクには型が同値である式を指定します。しかし、引数が等式を返す依存型の関数である場合、等式がゴールの何かとマッチするようにその関数の引数を見つけようとします。ここでは結合性が適用できる可能性のある個所はただ1つですが、等式 `{{#example_in Examples/ProgramsProofs/TCO.lean NatAddAssoc}}` の右辺が証明のゴールにマッチするため、書き換えの方向は逆にしなければなりません： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper6}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper6}} ``` + + +しかし、`{{#example_in Examples/ProgramsProofs/TCO.lean NatAddComm}}` で直接書き換えすると間違った結果になります。ここでの `rw` タクティクは間違った書き換え場所を推測しており、意図しないゴールに導きます： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper7}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper7}} ``` + + +これは `Nat.add_comm` の引数として `y` と `n` を明示的に提示することで解決します： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqHelper8}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqHelper8}} ``` + + +これでゴールは帰納法の仮定にマッチするようになりました。特に、帰納法の仮定の型は依存型の関数型です。`ih` を `n + y` に適用すると、期待していた型そのものになります。`exact` タクティクはその引数が正確に望みの型である場合、証明のゴールを完成させます： + ```leantac {{#example_decl Examples/ProgramsProofs/TCO.lean nonTailEqHelperDone}} ``` + + +実際の証明では、ゴールをこのような補助的な定義の型と一致させるためにはさらにほんの少しだけ追加作業が必要になります。最初のステップは、ここでも関数の外延性を呼び出すことです： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqReal0}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqReal0}} ``` + + +次のステップは `Tail.sum` を展開し、`Tail.sumHelper` を公開することです： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqReal1}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqReal1}} ``` + + + +こうすることで、型はほとんど一致します。しかし、補助定理では左辺に追加で加算を行っています。言い換えると、証明のゴールは `NonTail.sum xs = Tail.sumHelper 0 xs` ですが、`non_tail_sum_eq_helper_accum` を `xs` と `0` に適用すると `0 + NonTail.sum xs = Tail.sumHelper 0 xs` という型が得られます。ここで標準ライブラリには `{{#example_out Examples/ProgramsProofs/TCO.lean NatZeroAdd}}` という型を持つ `{{#example_in Examples/ProgramsProofs/TCO.lean NatZeroAdd}}` という証明があります。この関数を `NonTail.sum xs` に適用すると式は `{{#example_out Examples/ProgramsProofs/TCO.lean NatZeroAddApplied}}` という型になり、これで右辺から左辺への書き換えによって望みの型が得られます： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean nonTailEqReal2}} ``` ```output error {{#example_out Examples/ProgramsProofs/TCO.lean nonTailEqReal2}} ``` + + +最終的に、この補助定理によって証明が完成します： + ```leantac {{#example_decl Examples/ProgramsProofs/TCO.lean nonTailEqRealDone}} ``` + +この証明はアキュムレータを渡す版の末尾再帰関数が非末尾再帰版と等しいことを証明する時に使用できる一般的なパターンを示しています。最初のステップでは、開始時のアキュムレータの引数と最終結果の関係を発見することです。例えば、`Tail.sumHelper` を `n` のアキュムレータで開始すると、最終的な合計に `n` が加算され、`Tail.reverseHelper` を `ys` のアキュムレータで開始すると、最終的な反転されたリストが `ys` の前に追加されます。2つ目のステップは、この関係を定理として書き出し、帰納法によって証明することです。実際にはアキュムレータは常に `0` や `[]` などの中立な値で初期化されますが、開始時のアキュムレータを任意の値にすることができるこの一般的な文は、十分に強力な帰納法の仮定を得るために必要なものです。最後に、この補助定理を実際のアキュムレータの初期値で使用すると望ましい証明が得られます。例えば、`non_tail_sum_eq_tail_sum` ではアキュムレータは `0` が指定されます。この場合、中立的なアキュムレータの初期値が適切な場所で発生するようにゴールを書き換える必要があるかもしれません。 + + +## 演習問題 + +### 準備運動 + + + +`Nat.zero_add` ・`Nat.add_assoc` ・`Nat.add_comm` の証明を `induction` タクティクを使って自分で書いてみましょう。 + + + +### アキュムレータについて他の証明 + + +#### リストの反転 + + +`sum` についての証明を `NonTail.reverse` と `Tail.reverse` の証明に適用してください。最初のステップは `Tail.reverseHelper` に渡されるアキュムレータの値と非末尾再帰的な反転の間の関係を考えることです。ちょうど `Tail.sumHelper` でアキュムレータに数値を追加することが全体の合計に追加することと同じように、`Tail.reverseHelper` でアキュムレータに新しい要素を追加するために `List.cons` を使用することは全体の結果に何らかの変更を加えることと同じです。関係性がはっきりするまで、紙と鉛筆を使って3，4例の異なるアキュムレータの値を試してください。この関係を使って適切な補助定理を証明してください。それから全体の証明を書き下してください。`NonTail.reverse` と `Tail.reverse` は多相であるため、両者が等価であることを示すにはLeanが `α` にどのような型を使うべきかを考えさせないために `@` を使う必要があります。いったん `α` が通常の引数として扱われると、`funext` は `α` と `xs` の両方で呼び出されるようになります： + ```leantac {{#example_in Examples/ProgramsProofs/TCO.lean reverseEqStart}} ``` + + +これによって適切なゴールが生まれます： + ```output error {{#example_out Examples/ProgramsProofs/TCO.lean reverseEqStart}} ``` + + +#### 階乗 + + +アキュムレータと結果の関係を見つけ、適切な補助定理を証明することによって、前の節の練習問題で出てきた `NonTail.factorial` が読者の末尾再帰版の解答と等しいことを証明してください。 + +[^1]: 原文では`(y + n) + NonTail.sum ys`となっているが、おそらく`y`と`n`の位置が逆になっている \ No newline at end of file