Coq 对列表进行排序的策略？

Question

为了证明，我想使用以下事实：对于任何整数列表，都存在该列表的排序版本。这对我来说似乎很明显，但我找不到做类似事情的策略。我试图创建自己的（下），但我被卡住了，所以这个事实可能不像我想象的那么明显（或者它甚至不是真的？）

Definition sorted := (StronglySorted (λ x y, x ≤ y)).
Lemma exists_sorted:  ∀ (L : list Z) (a : Z), ∃ L0 : list Z, sorted L0 ∧ (List.In a L ⇔ List.In a L0).
Proof.
  induction L.
  - intros.
    exists nil.
    split.
    + apply SSorted_nil.
    + tauto.
  - intros.
    pose proof (IHL a).
    destruct H as [L0 [H H0]].

从那里我的想法似乎有点循环。有什么建议吗？

Answer 1

总结：

Require Import Orders Sorting ZArith.

Module ZOrder <: TotalLeBool.
Definition t := Z.
Definition leb := Z.leb.
Lemma leb_total : forall x y : t, leb x y = true \/ leb y x = true.
Proof.
intros x y; case (Zle_bool_total x y); auto.
Qed.

End ZOrder.

Module ZSort := Sort ZOrder.

Lemma Transitive_Zle_bool : Transitive (fun x y => is_true (x <=? y)%Z).
Proof.
intros x y z; unfold is_true; rewrite <- 3!Zle_is_le_bool; apply Z.le_trans.
Qed.

Lemma exists_sorted:  forall (L : list Z), exists L0 : list Z, 
 StronglySorted (fun x y => is_true (x <=? y)%Z) L0 /\ 
 (forall a: Z, List.In a L <-> List.In a L0).
Proof.
intros l; exists (ZSort.sort l).
split;[apply ZSort.StronglySorted_sort; apply Transitive_Zle_bool | ].
intros a; split; apply Permutation.Permutation_in.
  apply ZSort.Permuted_sort.
apply Permutation.Permutation_sym; apply ZSort.Permuted_sort.
Qed.

这是浏览 Coq 库的问题。我不知道你是怎么想到 StronglySorted 这个概念的，但它确实存在于 Coq 系统附带的库中。

如果您只键入以下内容

Require Import Sorted ZArith.

那么你只会得到对列表进行排序意味着什么的定义，而不是排序函数的定义。你看到这个是因为命令

Search StronglySorted.

只返回半打定理，这些定理大多与StronglySorted 和Sorted 之间的关系以及StronglySorted 的归纳原理有关。

通过在 Coq 发行版的源代码上使用 git grep，我发现 StronglySorted 的概念在两个库中使用，第二个名为 Mergesort。啊哈！ 合并排序是算法的名称，所以它可能会构造一个排序列表 为我们。现在MergesortSorted 都包含在Sorting 中，这就是我们的库 会用。

Require Import Sorting ZArith.

现在，如果我输入Search StronglySorted.，我看到结果中添加了一个新定理，名称为NatSort.StronglySorted_sort。情节变厚了。这个定理的陈述很长，但它基本上表达了如果函数Nat.leb计算的关系是传递的，那么函数NatSort.sort确实返回一个排序列表。

好吧，我们不想要一个对自然数的排序函数，而是一个对Z 类型的整数的排序函数。但是，如果您研究文件 Mergesort.v，您会发现 NatSort 是 functor 在结构上的实例化，该结构描述自然数的比较函数，并证明该比较是 total 在某种意义上。所以我们只需要为整数创建同一种结构。

请注意，我为引理 exists_sorted 证明的陈述与您使用的不同。重要的修改是存在陈述和全称量化的顺序不同。使用您的陈述，可以通过仅提供包含 a 或不包含 a 的列表来证明该陈述，具体取决于 a 是否在 L 中。

现在，这只是一个部分令人满意的答案，因为StronglySorted (fun x y => (x <=? y)%Z) 与您的sorted 不同。这向我们表明，当 R1 和 R2 等价时，表示 StronglySorted R1 <-> StronglySorted R2 的库中缺少一个引理。

补充：要在StronglySorted 中拥有正确关系的陈述，您需要接近以下证明的东西。在我看来，引理StronglySorted_impl 也应该在模块Sorted 中提供。

Lemma StronglySorted_impl {A : Type} (R1 R2 : A -> A -> Prop) (l : list A) :
  (forall x y, List.In x l -> List.In y l -> R1 x y -> R2 x y) ->
  StronglySorted R1 l -> StronglySorted R2 l.
Proof.
intros imp sl; revert imp; induction sl as [ | a l sl IHsl Fl];
  intros imp; constructor.
  now apply IHsl; intros x y xin yin; apply imp; simpl; right.
clear IHsl sl; revert imp; induction Fl; auto.
constructor;[now apply imp; simpl; auto | ].
apply IHFl.
intros y z yin zin; apply imp; simpl in yin, zin.
  now destruct yin as [ ya | yin]; simpl; auto.
now destruct zin as [za | zin]; simpl; auto.
Qed.

Lemma exists_sorted':  forall (L : list Z), exists L0 : list Z, 
 StronglySorted (fun x y => (x <= y)%Z) L0 /\ 
 (forall a: Z, List.In a L <-> List.In a L0).
Proof.
intros L; destruct (exists_sorted L) as [L' [sl permP]].
exists L'; split; [ | exact permP].
apply (StronglySorted_impl (fun x y => is_true (x <=? y)%Z)); auto.
now intros x y _ _; apply Zle_bool_imp_le.
Qed.

Answer 2

如果您允许Z 是任何类型，那么在构造类型理论中实际上选择顺序并不是那么简单。我建议您看一下 Cyril 的 Cohen（和其他人）finmap library，特别是给定具有选择原则和可判定相等性的类型 T，它完全符合您的要求，也就是说，导出规范排序对于T 的任何列表。

具体看排序功能here

Definition f (s : seq K) := choose (perm_eq (undup s)) (undup s).

在哪里

choose : forall T : choiceType, pred T -> T -> T

是选择原则，undup去除重复，perm_eq相等直到排列。

编辑对于已经具有等式关系的类型的情况，只要您具有排序函数及其理论，证明应该是微不足道的。示例：

From mathcomp Require Import all_ssreflect all_algebra.

Open Scope ring_scope.
Import Num.Theory.

Lemma exists_sorted (N : realDomainType) (l : seq N) :
  exists l_sorted, sorted <=%R l_sorted /\ perm_eq l_sorted l.
Proof.
exists (sort <=%R l).
by split; [apply: (sort_sorted (@ler_total _))|apply/perm_eqlP/perm_sort].
Qed.

Definition exists_sorted_int := exists_sorted [realDomainType of int].

事实上，整个定理是多余的，因为你最好使用原始理论。