Ready to put your newfound language skills into use? Get 40% off CodeCrafter's real-world proficiency projects!

考拉茲猜想

中等

簡介

某天晚上，你偶然發現了一本舊筆記本，裡頭寫滿了神祕難解的潦草字跡，彷彿有人正執著地追逐著某個念頭。其中一頁上，有個問題格外醒目：每個數字都能找到通往 1 的路嗎？ 它與一個叫做Collatz Conjecture的東西有關，這道謎題困擾了無數思想家數十年。

規則看似簡單，實則不然。隨便挑一個正整數。

接著，對得到的結果重複這些步驟，就這樣無限循環下去。

出於好奇，你挑了數字 12 來測試，就此展開這段旅程：

12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1

從第二個數字（6）開始算起，一共花了 9 步才抵達 1，而且每套用一次規則，數字就持續變化。起初，這個數列看起來毫無規律，忽上忽下，變幻莫測。然而，這個猜想主張，無論起始數字是什麼，最後都一定會抵達 1。

這既迷人，又令人費解。為什麼這似乎總是行得通？會不會有某個數字，會讓這個過程崩解，永遠循環下去，或是一路奔向無窮？筆記本暗示，解開這個謎題或許能揭露出某些深奧的道理，而伴隨而來的是名聲、財富，以及名留青史，這些都等著能解開它祕密的人。

說明

給定一個正整數，請依照考拉茲猜想的規則，回傳它達到 1 所需的步數。

這個練習定義了一個叫做 Positive 的子型別，代表所有大於 0 的自然數。子型別可以想成是一對 ⟨x, h⟩，其中 x 是值，h 則是它有效性的證明。

子型別裡的值（在這裡是 x）可以用 .val 存取，例如 x.val。它的證明則可以用 .property 存取，例如 x.property。兩者也可以照慣例用模式比對存取。

要建構一個子型別的值，就必須證明它有效，在這裡就是要證明那個數字大於 0。

Lean 裡有不少引理和定理，可以作為這個證明的起點。例如，Nat.zero_lt_succ 是一個引理，它斷言對任何自然數 n 而言：0 < n + 1。

Advanced

想找 Lean 定理證明的優良參考資料，可以看核心文件。

在 Lean 裡，遞迴函式必須證明自己會終止。這個證明有時很直接，可以從函式的結構隱含地得出。其他情況下，則必須明白寫出來。

在這個練習裡，函式的終止性正是 collatz conjecture，這是一個尚未解決的數學問題。

不妨考慮以下其中一種做法：

在函式宣告前加上 partial 關鍵字，會停用終止檢查，並允許（可能不安全的）遞迴呼叫。
單子程式碼允許的命令式結構（例如 while）在底層是用部分遞迴實作的，所以只要不強制要求終止，就可以使用它們。使用 Id 單子是在外觀看似純粹的程式碼中啟用這些結構的便利做法，而且不會引入額外的效應。
定義一個帶有額外參數的輔助函式，用這個參數記錄遞迴呼叫次數的上限，就能確保終止。