2

我正在写一篇关于使用 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.

我知道要证明有效，我们需要引理或定理，但是我不确定在那之后从哪里开始。谢谢您的帮助 ：）

4

2 回答 2

3

将您的问题视为“符号测试”的问题。编写一个函数来测试您的输出是否正确，然后显示您的初始代码和测试函数的所有组合都按预期工作。

这是我最喜欢的数据类型排序算法测试功能。

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-09T09:17:19.637 回答
3

你可以证明你的代码有很多很好的定理。

  • 定义一个函数 pos，它将一个数字和一个列表映射到列表中数字的索引。

  • Th 1：对于所有列表 S，以及 S 中的 a、b，(a <= b) <-> (pos a (sort S)) <= (pos b (sort S))。这将是排序函数的正确性定理。

  • Th 2：（排序（排序 S））=排序 S

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

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

  • Th 4：有序列表的倒数最大元素的pos为0。

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

  • 第 5 题：证明 (sort <= S) = (reverse (sort >= S))

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

于 2012-04-10T16:46:15.110 回答