使用Coq快速排除

我正在編寫一個關於使用Coq系統的快速排列算法的程序驗證的論文。我已經在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.

我知道一個證明的工作，我們需要一個引理或者定理但當時我不知道在哪裏後啓動的。感謝您的幫助:)

來源

2012-04-07 user1319321

有許多很好的定理可以證明您的代碼。

定義一個函數pos，它將數字和列表映射到列表中數字的索引。
度Th 1：對於所有列出S，以及a，b在S，（一個< = b）的< - >（POS一個（排序S））< =（POS B（排序S））。這將是一個排序函數的正確性定理。
的Th 2：（排序（排序S））=排序š
定義函數的最小值和最大值，以找到最小和列表的最大元素S.
釷3：排序列表的最小元件的pos是0
的Th 4：排序列表的反向的最大元素的pos是0

從您的排序例程中抽象出一個謂詞，以便您可以將它作爲參數傳遞。

釷5：證明（排序< = S）=（反向（排序> = S））

等，你可以繼續這種循環往復。這很有趣。 :-)

來源

2012-04-10 16:46:15

將您的問題視爲「符號測試」的問題。編寫一個測試你的輸出是否正確的函數，然後顯示你的初始代碼和你的測試函數的所有組合都按預期工作。

這是我最喜歡的數據類型排序算法測試函數。

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.

但你必須要得到證明主要的一個前證明許多中間引理。所以形式化證明就像測試一樣，除了你確保全面覆蓋測試。

來源

2012-11-09 09:17:19 Yves

使用Coq快速排除

回答

相關問題