Быстрое доказательство с использованием Coq

Question

Я пишу диссертацию по проверке программы алгоритма быстрой сортировки с использованием системы Coq. Я определил quicksort в Coq, но мой руководитель и я не очень хорошо пишут фактическое доказательство, используя тактику. Есть ли кто-нибудь, кто может помочь в этом разделе доказательства coq? Ниже то, что мы придумали до сих пор:

Inductive nat : Type := 
    | O : nat 
    | S : nat -> nat. 

Check (S (S (S (S O)))). 

Definition isZero (n:nat) : bool := 
    match n with 
    O => true 
    |S p => false 
    end. 

Inductive List: Set := 
| nil: List 
| cons: nat -> List -> List. 

Fixpoint Concat (L R: List) : List := 
match L with 
| nil => R 
| cons l ls => cons l (Concat ls R) 
end. 

Fixpoint Less (n m:nat) := 
    match m with 
    O => false 
    |S q => match n with 
      O => true 
     |S p => Less p q 
     end 
    end.  

Fixpoint Lesseq (n m:nat) := 
    match n with 
    O => true 
    |S p => match m with 
      O => false 
      |S q => Lesseq p q 
      end 
    end. 

Fixpoint Greatereq (n m:nat) := 
    match n with 
    O => true 
    |S p => match m with 
      O => true 
      |S q => Greatereq p q 
      end 
    end. 


Fixpoint Allless (l:List) (n:nat) : List := 
    match l with 
    nil => nil 
    |cons m ls => match Less n m with 
       false => Allless ls n 
       |true => cons m (Allless ls n) 
       end 
end.    

Fixpoint Allgeq (l:List) (n:nat) : List := 
    match l with 
    nil => nil 
    |cons m ls => match Greatereq n m with 
       false => Allgeq ls n 
       |true => cons m (Allgeq ls n) 
       end 
end. 

Fixpoint qaux (n:nat) (l:List) : List := 
    match n with 
    O => nil 
|S p => match l with 
     nil => nil 
     |cons m ls => let low := Allless ls m in 
        (let high := Allgeq ls m in 
        Concat (qaux p low) (cons m (qaux p high))) 
     end 
end. 

Fixpoint length (l:List) : nat := 
match l with 
    nil => O 
|cons m ls => S (length ls) 
end. 

Fixpoint Quicksort (l:List) : List := qaux (length l) l. 

Я знаю, что для доказательства работы нам понадобится лемма или теорему, но тогда я не знаю, с чего начать после этого. Спасибо за помощь :)

Answer 1

Есть много хороших теорем, которые вы можете доказать о своем коде.

• Определите функцию pos, которая отображает число и список в индекс номера в списке.

• ЧТ 1: Для всех списков S, а, б, в S, (а < = б) < -> (Pos а (сортировки S)) < = (поз Ь (вид S)). Это была бы теорема корректности для функции сортировки.

• Th 2: (сорт (сорт S)) = S рода

• Определение функции мин и макс, чтобы найти минимальные и максимальные элементы списка S.

• ЧТ 3: Размер позы минимального элемента отсортированного списка равно 0.

• ЧТЫ 4: позы максимального элемента в обратном направлении отсортированного списка 0.

Представьте предикат из вашей процедуры сортировки, чтобы вы могли передать его в качестве аргумента.

• Th 5: Покажите, что (сортировать < = S) = (реверс (вид> = S))

и т.д. Вы можете продолжать это до бесконечности. Это очень весело. :-)

Answer 2

Рассмотрите вашу проблему как проблему «символического тестирования». Напишите функцию, которая проверяет правильность вашего вывода, а затем покажет, что все комбинации исходного кода и функции тестирования работают по назначению.

Это моя любимая функция тестирования для алгоритма сортировки по вашему типу данных.

Fixpoint sorted (l : List) : bool := 
    match l with cons a l' => 
    match l' with cons b l'' => 
     if Lesseq a b then sorted l' else false 
    | nil => true 
    end 
    | nil => true 
    end. 

, то вы можете начать доказательство следующим образом:

Lemma Quicksort_sorted : forall l, sorted (Quicksort l) = true. 

Но вам придется доказать множество промежуточных лемм перед тем, как к доказательству основной. Таким образом, формальное доказательство действительно похоже на тестирование, за исключением того, что вы обеспечиваете полное покрытие теста.