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.

    (* 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.