Library rt.util.sorting
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
[forall 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.
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
[forall 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.