Require Import rt.util.all.

Module NondecreasingSequence.

  (* First, let's introduce the notion of the nth element of a sequence. *)
  Notation "xs [| n |]" := (nth 0 xs n) (at level 30).

  (* In this section we provide the notion of a non-decreasing sequence. *)
  Section Definitions.

    (* We say that a sequence xs is non-decincreasing iff for any two indices n1 and n2 
       such that [n1 <= n2 < size xs] the following condition holds: xs[n1] <= xs[n2]. *)
    Definition nondecreasing_sequence (xs: seq nat) :=
      ∀ n1 n2,
        n1 ≤ n2 < size xs →
        nth 0 xs n1 ≤ nth 0 xs n2.

    (* For a non-decreasing sequence we define the notion of 
       distances between neighboring elements of the sequence. *)
    (* Example:
       Consider the following sequence of natural numbers: xs = [:: 1; 10; 10; 17; 20; 41]. 
       Then [drop 1 xs] is equal to [:: 10; 10; 17; 20; 41].
       Then [zip xs (drop 1 xs)] is equal to [:: (1,10); (10,10); (10,17); (17,20); (20,41)]
       And after the mapping [map (fun '(x1, x2) => x2 - x1)] we end up with [:: 9; 0; 7; 3; 21]. *)
    Definition distances (xs: seq nat) :=
      map (fun '(x1, x2) ⇒ x2 - x1) (zip xs (drop 1 xs)).

    (* Next, we define some common operations on lists. 
       Namely max, first, and last. *)
    Definition max := foldl maxn 0.
    Definition first := head 0.
    Definition last := last 0.

  End Definitions.

  (* In this section, we prove a few basic lemmas about nondecreasing sequences. *)
  Section Lemmas.

    (* Next, we prove that no element can lie strictly between two 
       neighboring elements and still belong to the list. *)
    Lemma antidensity_of_nondecreasing_seq:
      ∀ (xs: seq nat) (x: nat) (n: nat),
        nondecreasing_sequence xs →
        xs [| n |] < x < xs [| n.+1 |] →
        ~~ (x \in xs).

    (* Alternatively, consider an arbitrary natural number x that is 
       bounded by the first and the last element of a sequence xs. Then 
       there is an index n such that xs[n] <= x < x[n+1]. *)
    Lemma belonging_to_segment_of_seq_is_total:
      ∀ (xs: seq nat) (x: nat),
        2 ≤ size xs →
        first xs ≤ x < last xs →
        ∃ n,
          n.+1 < size xs ∧
          xs[|n|] ≤ x < xs[|n.+1|].

    (* We prove that the difference between any two neighboring elements is
       bounded by the max element of the distances-sequence. *)
    Lemma distance_between_neighboring_elements_le_max_distance_in_seq:
      ∀ (xs: seq nat) (n: nat),
        xs[|n.+1|] - xs[|n|] ≤ max (distances xs).

    (* As a corollary, the max distance between elements of any nontrivial sequence
       (i.e. a sequence that contains at leas two distinct elements) is positive. *)
    Corollary max_distance_in_nontrivial_seq_is_positive:
      ∀ (xs: seq nat),
        nondecreasing_sequence xs →
        (∃ x y, x \in xs ∧ y \in xs ∧ x ≠ y) →
        0 < max (distances xs).

    (* Note that the distances-function has the expected behavior indeed. I.e. an element 
       on the n-th position of the distance-sequence is equal to the difference between
       n+1-th and n-th elements. *)
    Lemma function_of_distances_is_correct:
      ∀ (xs: seq nat) (n: nat),
        (distances xs)[|n|] = xs[|n.+1|] - xs[|n|].

    (* We show that the size of a distances-sequence is one less 
       than the size of the original sequence. *)
    Lemma size_of_seq_of_distances:
      ∀ (xs: seq nat),
        2 ≤ size xs →
        size xs = size (distances xs) + 1.

    (* Note that the last element of a nondecreasing sequence is the max element. *)
    Lemma last_is_max_in_nondecreasing_seq:
      ∀ (xs: seq nat) (x: nat),
        nondecreasing_sequence xs →
        (x \in xs) →
        x ≤ last xs.

    (* Given a nondecreasing sequence xs with length n, we show that the difference 
       between the last element of xs and the last element of the distances-sequence 
       of xs is equal to the (n-2)'th element of xs. *)
    Lemma last_seq_minus_last_distance_seq:
      ∀ (xs: seq nat),
        nondecreasing_sequence xs →
        last xs - last (distances xs) = xs [| (size xs).-2 |].

    (* Note that the last element is at most the max element. *)
    Lemma last_of_seq_le_max_of_seq:
      ∀ (xs: seq nat),
        last xs ≤ max xs.

    (* If any n'th element of a sequence xs is less-than-or-equal-to n'th 
       element of ys, then max of xs is less-than-or-equal-to max of ys. *)
    Lemma max_of_dominating_seq:
      ∀ (xs ys: seq nat),
        (∀ n, xs[|n|] ≤ ys[|n|]) →
        max xs ≤ max ys.

    (* The max element of the distances-sequence of a sequence xs is bounded 
       by the last element of xs. Note that all elements of xs are positive.
       Thus they all lie within the interval [0, last xs]. *)
    Lemma max_distance_in_seq_le_last_element_of_seq:
      ∀ (xs: seq nat),
        nondecreasing_sequence xs →
        max (distances xs) ≤ last xs.

    (* Consider two nondecreasing sequences xs and ys and assume that 
       (1) first element of xs is at most the first element of ys and 
       (2) distances-sequences of xs is dominated by distances-sequence of 
       ys. Then xs is dominated by ys.  *)
    Lemma domination_of_distances_implies_domination_of_seq:
      ∀ (xs ys: seq nat),
        first xs ≤ first ys →
        2 ≤ size xs →
        2 ≤ size ys →
        size xs = size ys →
        nondecreasing_sequence xs →
        nondecreasing_sequence ys →
        (∀ n, (distances xs)[|n|] ≤ (distances ys)[|n|]) →
        (∀ n, xs[|n|] ≤ ys[|n|]).

  End Lemmas.

End NondecreasingSequence.