Lean Mergesort, используя возрастающее обоснованное отношение - PullRequest
Новая
       16

Lean Mergesort, используя возрастающее обоснованное отношение

0 голосов
/ 30 декабря 2018

Я пытаюсь создать определение слияния в 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 в конце вашего определения, чтобы указать тактику для синтеза обоснованных отношений и уменьшения доказательств.

  • Используется стандартная тактика уменьшениятактика «предположения», таким образом, подсказки (или локальные доказательства) могут быть предоставлены с использованием выражений «иметь».Вложенное исключение содержит состояние отказа для тактики уменьшения.

Может ли кто-нибудь помочь мне доказать, что сортировка слиянием уменьшается?

1 Ответ

0 голосов
/ 04 января 2019

Во-первых, обратите внимание, что в вашем определении mergesort есть несколько проблем.Во-первых, параметр a не нужен и никогда не используется.(a, который вы соответствуете во второй строке, является новым.) Два, в случае x::xs, вы полностью забываете о x.Чтобы увидеть, что на самом деле делает ваша функция, вы можете добавить ключевое слово meta, как в meta def mergesort.Это отключает проверку завершения, поэтому вы можете #eval mergesort 2 [1, 3, 2] и увидеть, что вы не получаете то, что хотите.Я продолжу отвечать на это так, как вы написали.

Существует обоснованное отношение по умолчанию, и метод доказательства по умолчанию - это поиск доказательств в локальном контексте.Вы можете увидеть, какие доказательства ожидает Лин, посмотрев на сообщения об ошибках в вашем определении: ему нужны доказательства 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 s.

Используя тактику 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 К сожалению, интерфейс для этого довольно низкоуровневый, и я не знаю, документирован ли он или где.

Изменитьотношение без 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.

...