首先,请注意您的定义存在多个问题
mergesort
。一,参数
a
是不必要的,从未使用过。 (该
a
你在第二行匹配的是新鲜的。)二,在
x::xs
如果你忘记了
x
完全。要查看您的功能实际在做什么,您可以添加关键字
meta
,如在
meta def mergesort
。这会禁用终止检查,因此您可以
#eval mergesort 2 [1, 3, 2]
</code>
并且看到你没有得到你想要的东西。你写完之后我会继续回答这个问题。
有一个默认的有根据的关系,证明它的默认方法是在本地上下文中查找证明。您可以通过查看定义中的错误消息来查看Lean期望的证据:它需要证明
list.sizeof (fhalf xs) < x + (1 + list.sizeof xs)
和
list.sizeof (sndhalf xs) < x + (1 + list.sizeof xs)
。所以通过添加线条
def mergesort (a : ?): list ? �� list ?
| [] := []
| [a] := [a]
| (x::xs) :=
have list.sizeof (fhalf xs) < x + (1 + list.sizeof xs), from sorry,
have list.sizeof (sndhalf xs) < x + (1 + list.sizeof xs), from sorry,
merge (mergesort (fhalf xs)) (mergesort (sndhalf xs))
</code>
这个策略会成功。你需要填写那些
sorry
秒。
使用
linarith
战术可用
mathlib
(通过
import tactic.linarith
你可以跳过一些算术:
def mergesort (a : ?): list ? �� list ?
| [] := []
| [a] := [a]
| (x::xs) :=
have list.sizeof (fhalf xs) �� list.sizeof xs, from sorry,
have list.sizeof (sndhalf xs) �� list.sizeof xs, from sorry,
have list.sizeof (fhalf xs) < x + (1 + list.sizeof xs), by linarith,
have list.sizeof (sndhalf xs) < x + (1 + list.sizeof xs), by linarith,
merge (mergesort (fhalf xs)) (mergesort (sndhalf xs))
</code>
所以取代那些
sorry
有证据,你很高兴。你可能想要证明这样的东西
lemma sizeof_take_le {��} [h : has_sizeof ��] : ? n (xs : list ��),
list.sizeof (list.take n xs) �� list.sizeof xs
</code>
当你更正你的定义时,细节会有所改变
mergesort
。
另一种方法是改变有根据的关系和决策策略,如同在
mathlib
定义:
https://github.com/leanprover/mathlib/blob/master/data/list/sort.lean#L174
不幸的是,这样做的界面相当低级,我不知道它是否记录在哪里或在哪里记录。
无需改变关系
using_well_founded
,您可以添加一个要使用的本地实例
list.length
代替
list.sizeof
:
def new_list_sizeof : has_sizeof (list ?) := ?list.length?
local attribute [instance, priority 100000] new_list_sizeof
</code>
这些目标产生的目标比使用者更容易证明
sizeof
。