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

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))

这个策略会成功。你需要填写那些 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))

所以替换那些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不幸的是，执行此操作的接口(interface)相当低级，我不知道是否或在何处记录了它。

在没有 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 相比，这产生的目标将更容易证明。 .