首先，请注意您的定义存在多个问题
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
。