3

我正在尝试在 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

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

未能证明递归应用正在减少，有根据的关系 

@has_well_founded.r (list ℕ)
(@has_well_founded_of_has_sizeof (list ℕ) (@list.has_sizeof ℕ nat.has_sizeof))

可能的解决方案：

  • 在定义的末尾使用using_well_founded关键字来指定合成有根据的关系和减少证明的策略。

  • 默认的递减策略使用“假设”策略，因此可以使用“有”表达式提供提示（也称为本地证明）。嵌套异常包含递减策略的失败状态。

谁能帮我证明归并排序正在减少？

4

1 回答 1

4

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

使用(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))

所以用证明替换那些sorrys，你就可以开始了。你可能想证明类似的东西

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.

于 2019-01-04T14:22:09.007 回答