はじめに
ある晩、古いノートを偶然見つけました。そこには、誰かがあるアイデアを執拗に追い求めていたかのような、謎めいた走り書きがびっしりと書かれていました。
あるページには、一つの問いが目を引きました。すべての数は1にたどり着けるのか？
それはコラッツ予想と呼ばれるものに関係していました。何十年もの間、人々を悩ませ続けてきたパズルです。
そのルールは、見かけによらず単純でした。
好きな正の整数を一つ選びます。
- 偶数なら2で割ります。
- 奇数なら3を掛けて1を足します。
そして、その結果に対して同じ手順を繰り返します。これはいつまでも続きます。
興味をひかれて、試しに12を選び、その旅を始めました。
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
2番目の数（6）から数えて、1にたどり着くまでに9ステップかかりました。ルールを繰り返すたびに、数は変わり続けます。
最初のうちは、この数列は予測できないように思えました。上がったり下がったり、あちこちに飛び回るのです。
しかし、この予想はこう主張しています。どんな数から始めても、必ず最後は1にたどり着く、と。
それは魅力的であると同時に、当惑させるものでもありました。
なぜ、いつもこううまくいくように見えるのでしょうか？
この過程が壊れてしまい、永遠にループしたり無限のかなたへ逃げていったりするような数は存在するのでしょうか？
ノートには、これを解けば何か深遠なことが明らかになるかもしれない、と示唆されていました。そしてそれを成し遂げた者には、名声と富、そして歴史に名を刻む場所が待っているのです。
説明
正の整数が与えられたとき、コラッツ予想の規則に従って1に到達するまでにかかるステップ数を返してください。
Subtype
この演習では、0より大きいすべての自然数を表すPositiveというSubtypeを定義します。
Subtypeは、⟨x, h⟩というペアと考えることができます。ここでxは値であり、hはその値が妥当であることの証明です。
Subtypeの中の値（ここではx）には、.valを使ってアクセスできます。たとえばx.valです。
その証明には.propertyを使ってアクセスできます。たとえばx.propertyです。
どちらも、いつもどおりパターンマッチングでアクセスすることもできます。
Subtypeの値を作るには、その値が妥当であること、この場合はその数が0より大きいことを証明する必要があります。
Leanには、この証明の出発点として使える補題や定理がたくさんあります。
たとえば、Nat.zero_lt_succは、任意の自然数nについて0 < n + 1が成り立つことを主張する補題です。
Leanでの定理証明のよい参考資料は、コアドキュメントにあります。
停止性の証明
Leanでは、再帰関数はその停止性を証明しなければなりません。
この証明が簡単なこともあり、その場合は関数の構造から暗黙のうちに導かれます。
そうでない場合は、明示的に示す必要があります。
この演習では、関数の停止性はまさにcollatz conjectureそのものであり、これは未解決の数学の問題です。
次の選択肢のいずれかを使ってみましょう。
- 関数の宣言の前に
partialキーワードを付けると、停止性チェックが無効になり、（安全とは限らない）再帰呼び出しが可能になります。
- モナドのコードで使える命令型の構文（たとえば
while）は、内部では部分再帰を使って実装されているので、停止性が要求されないときはいつでも使えます。
Idモナドを使うと、それ以外は純粋に見えるコードで、余分な効果を持ち込むことなく、こうした構文を手軽に有効にできます。
- 再帰呼び出しの最大回数を表す追加の引数を持つヘルパーを定義すれば、停止性が保証されます。
