Library rt.util.sorting

Require Import rt.util.tactics rt.util.induction rt.util.list.

(* Lemmas about sorted lists. *)
Section Sorting.

  Lemma prev_le_next :
    ∀ (T: Type) (F: T→nat) r (x0: T) i k,
      (∀ i, i < (size r).-1 → F (nth x0 r i) ≤ F (nth x0 r i.+1)) →
      (i + k ≤ (size r).-1) →
      F (nth x0 r i) ≤ F (nth x0 r (i+k)).

  Lemma sort_ordered:
    ∀ {T: eqType} (leT: rel T) (s: seq T) x0 idx,
      sorted leT s →
      idx < (size s).-1 →
      leT (nth x0 s idx) (nth x0 s idx.+1).

  Lemma sorted_rcons_prefix :
    ∀ {T: eqType} (leT: rel T) s x,
      sorted leT (rcons s x) →
      sorted leT s.

  Lemma order_sorted_rcons :
    ∀ {T: eqType} (leT: rel T) (s: seq T) (x last: T),
      transitive leT →
      sorted leT (rcons s last) →
      x \in s →
      leT x last.

  Lemma sorted_lt_idx_implies_rel :
    ∀ {T: eqType} (leT: rel T) (s: seq T) x0 i1 i2,
      transitive leT →
      sorted leT s →
      i1 < i2 →
      i2 < size s →
      leT (nth x0 s i1) (nth x0 s i2).

  Lemma sorted_rel_implies_le_idx :
    ∀ {T: eqType} (leT: rel T) (s: seq T) x0 i1 i2,
      uniq s →
      antisymmetric_over_list leT s →
      transitive leT →
      sorted leT s →
      leT (nth x0 s i1) (nth x0 s i2) →
      i1 < size s →
      i2 < size s →
      i1 ≤ i2.

End Sorting.