我正在写一篇关于使用 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.
我知道要证明有效，我们需要引理或定理，但之后我不确定从哪里开始。感谢您的帮助:)
最佳答案
关于您的代码，您可以证明许多不错的定理。
定义一个函数 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))
等你可以无限地继续这个广告。这很有趣。 :-)
关于sorting - 使用 Coq 的快速排序证明，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/10056782/