反转数组

说明

你的任务是证明自定义的列表反转函数与内置的List.reverse相等。

由于本练习的性质，我们不依赖传统的运行时测试，而是通过定理check来检查证明。 如果这个定理能通过类型检查，你就可以认为测试通过了。

如果你在本地或 Lean 的在线演练场中工作，就能通过 Lean InfoView 立即得到反馈，了解某个定理是成功还是失败，以及失败的原因。 它是一个非常宝贵的工具，能显示你的证明中用到的所有局部值，以及你当前的目标。

在 Lean 中证明定理

定理证明是 Lean 不可分割的一部分。 它让程序员能够证明自己程序的属性，对程序的行为进行推理，并在类型层面编码约束和规范。

这一章很好地介绍了 Lean 中的定理证明。 如果想更深入地学习，Lean 官网把这本书列为官方资源。

Lean 提供了许多策略，可以自动完成证明，或者证明的一部分。 你也许想查阅一下语言参考。

@[csimp]
theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
    ... -- proof here

-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.