# Library prosa.util.nondecreasing

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Require Export prosa.util.epsilon.
Require Export prosa.util.nat.
Require Export prosa.util.list.

# Non-Decreasing Sequence and Distances

In this file we introduce the notion of a non-decreasing sequence.
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-decreasing iff for any two indices n1 and n2 such that n1 n2 < size [xs] condition [xs][n1] [xs][n2] holds.
Definition nondecreasing_sequence (xs : seq nat) :=
n1 n2,
n1 n2 < size xs
xs[|n1|] xs[|n2|].

Similarly, we define an increasing sequence.
Definition increasing_sequence (xs : seq nat) :=
n1 n2,
n1 < n2 < size xs
xs[|n1|] < 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)).

End Definitions.

# Properties of Increasing Sequence

In this section we prove a few lemmas about increasing sequences.
Section IncreasingSequence.

Note that a filtered iota sequence is an increasing sequence.
We prove that any increasing sequence is also a non-decreasing sequence.

# Properties of Non-Decreasing Sequence

In this section we prove a few lemmas about non-decreasing sequences.
Section NonDecreasingSequence.

First we prove that if 0 xs, then 0 is the first element of xs.
If x1::x2::xs is a non-decreasing sequence, then either x1 = x2 or x1 < x2.
We prove that if x::xs is a non-decreasing sequence, then xs also is a non-decreasing sequence.
Let xs be a non-decreasing sequence, then for x s.t. y xs, x y x::xs is a non-decreasing sequence.
We prove that if x::xs is a non-decreasing sequence, then x::x::xs also is a non-decreasing sequence.
We prove that if x::xs is a non-decreasing sequence, then x is a minimal element of xs.
We also prove a similar lemma for strict minimum.
Next, we prove that no element can lie strictly between two neighboring elements and still belong to the list.
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].
Note that the last element of a non-decreasing sequence is the max element.

# Properties of Undup of Non-Decreasing Sequence

In this section we prove a few lemmas about undup of non-decreasing sequences.
Section Undup.

First we prove that undup x::x::xs is equal to undup x::xs.
Remark nodup_sort_2cons_eq:
{X : eqType} (x : X) (xs : seq X),
undup (x::x::xs) = undup (x::xs).

For non-decreasing sequences we show that the fact that x1 < x2 implies that undup x1::x2::xs = x1::undup x2::xs.
Next we show that function undup doesn't change the last element of a sequence.
Non-decreasing sequence remains non-decreasing after application of undup.
We also show that the penultimate element of a sequence undup xs is bounded by the penultimate element of sequence xs.

# Properties of Distances

In this section we prove a few lemmas about function distances.
Section Distances.

We begin with a simple lemma that helps us unfold distances of lists with two consecutive cons x0::x1::xs.
Similarly, we prove a lemma stating that two consecutive appends to a sequence in distances function ( ++ [:: a; b])) can be rewritten as ++ [:: a]) ++ [:: b - a].
We also prove a lemma stating that one append to a sequence in the distances function (i.e., ++ [:: x])) can be rewritten as distances xs ++ [:: x - last0 xs].
We prove that the difference between any two neighboring elements is bounded by the max element of the distances-sequence.
Note that the distances-function has the expected behavior indeed. I.e. an element on the position n of the distance-sequence is equal to the difference between elements on positions n+1 and 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.

We prove that index_iota 0 n produces a sequence of numbers which are always one unit apart from each other.
Lemma distances_of_iota_ε:
n x, x \in distances (index_iota 0 n) x = ε.

End Distances.

# Properties of Distances of Non-Decreasing Sequence

In this section, we prove a few basic lemmas about distances of non-decreasing sequences.
First we show that the max distance between elements of any nontrivial sequence (i.e. a sequence that contains at leas two distinct elements) is positive.
Given a non-decreasing 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 xs[n-2].
The max element of the distances-sequence of a sequence xs is bounded by the last element of xs. Since all elements of xs are non-negative, they all lie within the interval 0, last xs.
Let xs be a non-decreasing sequence. We prove that distances of sequence [seq ρ <- index_iota 0 k.+1 | ρ \in xs] coincide with sequence [seq x <- distances xs | 0 < x]].
Let xs again be a non-decreasing sequence. We prove that distances of sequence undup xs coincide with sequence of positive distances of xs.
Consider two non-decreasing 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.