PROSAGA码农传奇-精益-精益Mergesort使用日益完善的关系

我试图在精益中创建mergesort定义，并创建了以下代码：
<pre><code>def mergesort (a: ℕ): list ℕ → list ℕ 
 | [] := [] 
 | [a] := [a] 
 | (x::xs) := merge (mergesort (fhalf xs)) (mergesort (sndhalf xs))
</code></pre>使用合并定义
<pre><code>def merge : list ℕ → list ℕ → list ℕ 
 | xs [] := xs 
 | [] ys := ys
 | (x :: xs) (y :: ys) := if x < y then x :: (merge xs ( y :: ys)) 
 else y :: (merge (x :: xs) ys)
</code></pre>和half / sndhalf定义：
<pre><code> def fhalf {α: Type} (xs: list α): list α := 
 list.take (list.length xs/2) xs

def sndhalf {α: Type} (xs: list α): list α :=
 list.drop (list.length xs/2) xs
</code></pre>但是，我收到以下错误消息：无法证明递归应用程序在减少，建立良好的关系
<pre><code>@has_well_founded.r (list ℕ)
(@has_well_founded_of_has_sizeof (list ℕ) (@list.has_sizeof ℕ nat.has_sizeof))
</code></pre>可能的解决方案：using_well_founded在定义的末尾使用关键字来指定用于综合良好关系和减少证明的策略。默认的递减策略使用“假设”策略，因此可以使用“ have”表达式提供提示（aka局部证明）。嵌套异常包含递减策略的失败状态。谁能帮助我证明mergesort正在减少？

首先，请注意，您对的定义存在多个问题mergesort。一，该参数a是不必要的，永远不会使用。（a在第二行中匹配的内容是新鲜的。）在这种x::xs情况下，您将x完全忘记了。要查看函数的实际作用，可以添加关键字meta，如中所示meta def mergesort。这将禁用终止检查，因此您可以#eval mergesort 2 [1, 3, 2]看到自己没有得到想要的东西。在您撰写本文时，我将继续回答。

有一个默认的有根据的关系，证明它的默认方法是在本地上下文中查找证明。通过查看定义中的错误消息，您可以看到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))
```

这个策略将会成功。您需要填写那些sorry。

使用（via ）中linarith可用的策略，您可以跳过一些算法：mathlibimport 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))
```

因此，sorry用证明替换那些，那么您就很好了。您可能想证明类似

```
lemma sizeof_take_le {α} [h : has_sizeof α] : ∀ n (xs : list α), 
  list.sizeof (list.take n xs) ≤ list.sizeof xs
```

当您更正的定义时，详细信息将有所更改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
```
与使用产生的目标相比，产生的目标将使您更容易证明sizeof。