Coq tactic to sort a list?

Question

For a proof, I want to use the fact that for any list of integers, there exists a sorted version of that list. This seems obvious to me, but I couldn't find a tactic that does something like that. I tried to create my own (below), but I got stuck, so maybe this fact isn't as obvious as I thought it was (or maybe it isn't even true?)

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]].

and from there my idea seems a bit circular. Any advice?

Answer 1

Summary:

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.

This is a matter of navigating the Coq libraries. I don't know how you came by the concept StronglySorted, but it is indeed present in the libraries shipped with the Coq system.

If you only type the following

Require Import Sorted ZArith.

Then you only get a definition of what it means for a list to be sorted, but not the definition of a sorting function. You see this because the command

Search StronglySorted.

only returns half a dozen theorems that are mostly linked with the relation between StronglySorted and Sorted and the induction principle for StronglySorted.

By using git grep on the sources of the Coq distribution, I figured out that the concept StronglySorted was used in two libraries, the second one is named Mergesort. Aha! merge sort is the name of an algorithm, so it will probably constructed a sorted list for us. Now both Mergesort Sorted are included in Sorting so that is the library we will use.

Require Import Sorting ZArith.

Now if I type Search StronglySorted. I see there is a new theorem added to the results, with the name NatSort.StronglySorted_sort. The plot thickens. The statement of this theorem is long, but it basically expresses that if the relation computed by the function Nat.leb is transitive, then the function NatSort.sort indeed returns a sorted list.

Well, we do not want a sorting function on natural numbers, but a sorting function on integers of type Z. But if you study the file Mergesort.v you see that NatSort is an instantiation of a functor on a structure that describes the comparison function for natural numbers and the proof that this comparison is total in a certain senses. So we only need to create the same kind of structure for integers.

Please note that the statement I proved for the lemma exists_sorted is not the same as the one you used. The important modification is that the order of existential statements and universal quantifications are not the same. With your statement, one could prove the statement by providing only a list containing a or not, depending on whether a is in L or not.

Now, this is only a partially satisfactory answer, because StronglySorted (fun x y => (x <=? y)%Z) is not the same as your sorted. This shows us that there is a missing lemma in the library expressing StronglySorted R1 <-> StronglySorted R2 when R1 and R2 are equivalent.

Complement: to have the statement with the right relation in StronglySorted you would need something close to the following proof. Lemma StronglySorted_impl should be provided in module Sorted too, in my opinion.

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

Actually picking the order is not so trivial in constructive type theory, if you allow Z to be any type. I recommend you have a look to Cyril's Cohen (and others) finmap library , in particular, given a type T with a choice principle and decidable equality it exactly does what you want, that is to say, to derive a canonical ordering for any list of T.

In particular, see the sorting function here

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

where

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

is the choice principle, undup removes duplicates, and perm_eq equality up to permutation.

Edit for the case of a type that already has an equality relation the proof should be trivial provided you have a sort function and its theory of course. Example:

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].

In fact, the whole theorem is redundant as you are better off with the primitive theory.