# Sorting

In this modeule we prove a few lemmas about sorted sequences.
Section Sorting.

Section SortedImplLeIdx.

(* Consider an arbitrary type T... *)
Variable T: eqType.

(* ... and some binary relation leT (≺) on it. *)
Variable leT: rel T.
Notation "x ≺ y" := (leT x y) (at level 30).
Let sorted xs := sorted leT xs.

(* Next, let xs be a sequence of elements of type T. *)
Variable xs: seq T.

(* Since Coq requires all functions to be total, we
need to specify a default value for cases when
an index exceeds the size of the sequence. *)

Variable default: T.
Let nth := nth default.

(* Next, let's introduce a notation for the nth element of a sequence. *)
Notation "xs [| n |]" := (nth xs n) (at level 10).

(* We prove that, given the fact that sequence xs is sorted,
the i'th element of xs is ≺ than the i+1'th element. *)

Lemma sort_ordered:
(idx: nat),
sorted xs
idx < (size xs).-1
xs[|idx|] xs[|idx.+1|].

(* Next we prove that the prefix of a sorted sequence is also sorted. *)
Lemma sorted_rcons_prefix:
x,
sorted (rcons xs x)
sorted xs.

(* Let's assume that relation leT (≺) is transitive. *)
Hypothesis H_leT_is_transitive: transitive leT.

(* Given the fact that sequence xs is sorted, we prove that
the last elements of the sequence is the max. element. *)

Lemma order_sorted_rcons:
(x lst: T),
sorted (rcons xs lst)
x \in xs
x lst.

(* Next, we prove that for sorted sequence xs and for any
two indices i1 and i2, i1 < i2 implies xs|i1| ≺ xs|i2|. *)

Lemma sorted_lt_idx_implies_rel:
i1 i2,
sorted xs
i1 < i2
i2 < size xs
xs[|i1|] xs [|i2|].

(* Finally, assuming that (1) xs is sorted and contains
no duplicates, (2) ≺ is antisymmetric and transitive,
we prove that x|i1| ≺ x|i2| implies i1 ≤ i2. *)

Lemma sorted_rel_implies_le_idx:
i1 i2,
uniq xs
antisymmetric_over_list leT xs
sorted xs
xs[|i1|] xs[|i2|]
i1 < size xs
i2 < size xs
i1 i2.

End SortedImplLeIdx.

(* Let F be a function from some type to natural numbers. Then for a
sequence xs, the fact that  i: F(xs[i]) F(xs[i+1]) implies that
i k: F(xs[i]) F(xs[i + k]). *)

Lemma prev_le_next:
{T: Type} (F: T nat) (xs: seq T) (def: T) (i k: nat),
( i, i < (size xs).-1 F (nth def xs i) F (nth def xs i.+1))
(i + k (size xs).-1)
F (nth def xs i) F (nth def xs (i+k)).

End Sorting.