Coqを使ったクイックソート証明

Question

私は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. 

たちは補題や定理を必要とするが、その後、私はそれ以降開始する場所を確認していない動作するように。助けを感謝します。

Answer 1

あなたのコードについて証明できる多くの素晴らしい定理があります。

• 番号とリストをリスト内の番号のインデックスにマップする関数posを定義します。

• のTh 1：すべてのリストS、及び、SでB、（< = B）<について - >（POS（ソートS））< =（POSのB（ソートS））。これはソート関数の正しさの定理になります。

• のTh 2：（ソート（並べ替えS））は=ソート

• リストの最小および最大の要素を見つけるために、関数minおよびmaxを定義S S.

• Thを3：ソートされたリストの最小要素のPOS 0

• のTh 4：ソートされたリストの逆の最大要素のposが0

あります

要約ソートルーチンからの述語を引数として渡すことができるようにします。

• のTh 5：あなたは、この無限に続けることができます（ソート< = S）=（> = S（ソート）をリバース）

などすることを示しています。それはたくさんの楽しみです。 :-)

Answer 2

"シンボリックテスト"の問題として問題を表示します。出力が正しいことをテストする関数を記述し、初期コードとテスト関数のすべての組み合わせが意図した通りに動作することを示します。

あなたのデータ型のソートアルゴリズムのための私のお気に入りのテスト関数です。

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

をしかし、あなたはメインの1を証明するに取得する前に多くの中間補題を証明する必要があります。

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. 

あなたは次のように証拠を開始することができます。したがって、正式な証明は、テストの完全な範囲を保証することを除いて、実際にテストに似ています。