Library prosa.classic.util.sorting


In this modeule we prove a few lemmas about sorted sequences.
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:
        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.