sorting - 使用 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 中的 a、b，(a <= b) <-> (pos a (sort S)) <= (pos b (sort S))。这将是排序函数的正确性定理。

• Th 2: (sort (sort S)) = sort S

• 定义函数 min 和 max 以查找列表 S 的最小和最大元素。

• Th 3: 排序列表的最小元素的pos为0。

• 第4:排序后的链表的倒序最大元素的pos为0。

从您的排序例程中抽象出一个谓词，以便您可以将其作为参数传递。

• 第 5 次:证明 (sort <= S) = (reverse (sort >= S))

等你可以无限地继续这个广告。这很有趣。 :-)