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 的 Subtype，用于表示所有大于 0 的自然数。可以把 Subtype 看作一对 ⟨x, h⟩，其中 x 是值，h 是它有效性的证明。

Subtype 里的值（这里是 x）可以用 .val 访问，例如 x.val。它的证明可以用 .property 访问，例如 x.property。和往常一样，这两者也可以通过模式匹配访问。

要为 Subtype 构造一个值，必须证明它的有效性，在这里就是要证明这个数大于 0。

Lean 里有很多引理和定理可以作为这个证明的起点。例如，Nat.zero_lt_succ 是一个引理，它断言对于任意自然数 n：0 < n + 1。

Advanced

关于在 Lean 中进行定理证明，一个好的参考资料是核心文档。

在 Lean 中，递归函数必须证明自己的终止性。这个证明有时很直接，会隐含地由函数的结构得出。另一些情况下，则必须把它显式地写出来。

在本练习中，函数的终止性恰恰就是 collatz conjecture，这是一个尚未解决的数学问题。

可以考虑使用下面几种方法之一：

在函数声明前加上 partial 关键字，会关闭终止性检查，并允许（可能不安全的）递归调用。
单子代码中允许使用的命令式结构，比如 while，底层是用部分递归实现的，所以只要不强制要求终止性，就可以使用它们。使用 Id 单子，是在原本看起来纯粹的代码中启用这些结构的一种便捷方式，而且不会引入额外的效果。
定义一个辅助函数，并给它加一个表示最大递归调用次数的额外参数，就能确保终止。