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: Tnat) 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 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 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.