精益合并排序使用增加的有根据的关系

Question

我正在尝试在 Lean 中创建合并排序定义并创建了以下代码：

def mergesort (a: ℕ): list ℕ → list ℕ     
    | [] := []    
    | [a] := [a]  
    | (x::xs) :=  merge (mergesort (fhalf xs)) (mergesort (sndhalf xs))

与合并定义

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)

和 fhalf / sndhalf 定义：

 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

但是，我收到以下错误消息：

failed to prove recursive application is decreasing, well founded relation
@has_well_founded.r (list ℕ)
(@has_well_founded_of_has_sizeof (list ℕ) (@list.has_sizeof ℕ nat.has_sizeof)) 
Possible solutions:

Use using_well_founded keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.

The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions. The nested exception contains the failure state for the decreasing tactic.

谁能帮我证明归并排序是递减的？

Answer 1

首先，请注意您对 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))

这个策略会成功。您需要填写那些 sorrys.

使用 mathlib 中可用的 linarith 策略（通过 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))

所以用证明替换那些 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.

相比，这产生的目标将更容易证明。

精益合并排序使用增加的有根据的关系

Lean Mergesort using increasing well founded relation

algorithm

mergesort

lean