Require Import prosa.classic.util.tactics prosa.classic.util.induction prosa.classic.util.list.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.

Section Sorting.

  Section SortedImplLeIdx.

    Variable T: eqType.

    Variable leT: rel T.
    Notation "x ≺ y" := (leT x y) (at level 30).
    Let sorted xs := sorted leT xs.

    Variable xs: seq T.

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

    Notation "xs [| n |]" := (nth xs n) (at level 10).

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

    Lemma sorted_rcons_prefix:
      ∀ x,
        sorted (rcons xs x) →
        sorted xs.

    Hypothesis H_leT_is_transitive: transitive leT.

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

    Lemma sorted_lt_idx_implies_rel:
      ∀ i1 i2,
        sorted xs →
        i1 < i2 →
        i2 < size xs →
        xs[|i1|] ≺ xs [|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.

  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.