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 的归纳原理.

通过使用 git grep根据 Coq 发行版的来源，我发现了这个概念 StronglySorted用于两个库，第二个库名为 Mergesort 。啊哈! merge sort是一个算法的名称，所以它可能会构造一个排序列表为了我们。现在都是Mergesort Sorted包含在Sorting中这就是我们的图书馆会用。

Require Import Sorting ZArith.

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

好吧，我们不需要自然数的排序函数，而是 Z 类型的整数的排序函数。 。但是如果你研究文件Mergesort.v你看到NatSort是一个结构上仿函数的实例，描述自然数的比较函数，并证明该比较在某种意义上是总体。所以我们只需要为整数创建相同类型的结构即可。

请注意我证明的引理 exists_sorted 的陈述和你用的不一样。重要的修改是存在陈述和普遍量化的顺序不同。根据你的陈述，人们可以通过仅提供包含或不包含 a 的列表来证明该陈述，具体取决于 a 是否在 L 中。

现在，这只是一个部分令人满意的答案，因为 StronglySorted (fun x y => (x <=? y)%Z)与您的 sorted 不一样。这表明库中缺少一个引理，表示 StronglySorted R1 <-> StronglySorted R2当R1和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.