# 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.

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.

In this section we provide the notion of a non-decreasing sequence.

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|].

∀ n1 n2,

n1 ≤ n2 < size xs →

xs[|n1|] ≤ xs[|n2|].

Similarly, we define an increasing sequence.

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.

map (fun '(x1, x2) ⇒ x2 - x1) (zip xs (drop 1 xs)).

End Definitions.

Note that a filtered iota sequence is an increasing sequence.

We prove that any increasing sequence is also a non-decreasing
sequence.

Lemma increasing_implies_nondecreasing:

∀ xs,

increasing_sequence xs →

nondecreasing_sequence xs.

End IncreasingSequence.

∀ xs,

increasing_sequence xs →

nondecreasing_sequence xs.

End IncreasingSequence.

# Properties of Non-Decreasing Sequence

In this section we prove a few lemmas about non-decreasing sequences.
Lemma nondecreasing_sequence_2cons_leVeq:

∀ x1 x2 xs,

nondecreasing_sequence (x1 :: x2 :: xs) →

x1 = x2 ∨ x1 < x2.

∀ x1 x2 xs,

nondecreasing_sequence (x1 :: x2 :: xs) →

x1 = x2 ∨ x1 < x2.

Lemma nondecreasing_sequence_cons:

∀ x xs,

nondecreasing_sequence (x :: xs) →

nondecreasing_sequence xs.

∀ x xs,

nondecreasing_sequence (x :: xs) →

nondecreasing_sequence xs.

Let xs be a non-decreasing sequence,
then for x s.t. ∀ y ∈ xs, x ≤ y
x::xs is a non-decreasing sequence.

Lemma nondecreasing_sequence_add_min:

∀ x xs,

(∀ y, y \in xs → x ≤ y) →

nondecreasing_sequence xs →

nondecreasing_sequence (x :: xs).

∀ x xs,

(∀ y, y \in xs → x ≤ y) →

nondecreasing_sequence xs →

nondecreasing_sequence (x :: xs).

We prove that if x::xs is a non-decreasing sequence,
then x::x::xs also is a non-decreasing sequence.

Lemma nondecreasing_sequence_cons_double:

∀ x xs,

nondecreasing_sequence (x :: xs) →

nondecreasing_sequence (x :: x :: xs).

∀ x xs,

nondecreasing_sequence (x :: xs) →

nondecreasing_sequence (x :: x :: xs).

Lemma nondecreasing_sequence_cons_min:

∀ x xs,

nondecreasing_sequence (x :: xs) →

(∀ y, y \in xs → x ≤ y).

∀ x xs,

nondecreasing_sequence (x :: xs) →

(∀ y, y \in xs → x ≤ y).

We also prove a similar lemma for strict minimum.

Corollary nondecreasing_sequence_cons_smin:

∀ x1 x2 xs,

x1 < x2 →

nondecreasing_sequence (x1 :: x2 :: xs) →

(∀ y, y \in x2 :: xs → x1 < y).

∀ x1 x2 xs,

x1 < x2 →

nondecreasing_sequence (x1 :: x2 :: xs) →

(∀ y, y \in x2 :: xs → x1 < y).

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).

∀ (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 →

first0 xs ≤ x < last0 xs →

∃ n,

n.+1 < size xs ∧

xs[|n|] ≤ x < xs[|n.+1|].

∀ (xs : seq nat) (x : nat),

2 ≤ size xs →

first0 xs ≤ x < last0 xs →

∃ n,

n.+1 < size xs ∧

xs[|n|] ≤ x < xs[|n.+1|].

Note that the last element of a non-decreasing sequence is the max element.

Lemma last_is_max_in_nondecreasing_seq:

∀ (xs : seq nat) (x : nat),

nondecreasing_sequence xs →

(x \in xs) →

x ≤ last0 xs.

End NonDecreasingSequence.

∀ (xs : seq nat) (x : nat),

nondecreasing_sequence xs →

(x \in xs) →

x ≤ last0 xs.

End NonDecreasingSequence.

# Properties of Undup of Non-Decreasing Sequence

In this section we prove a few lemmas about undup of non-decreasing sequences.
For non-decreasing sequences we show that the fact that
x1 < x2 implies that undup x1::x2::xs = x1::undup x2::xs.

Lemma nodup_sort_2cons_lt:

∀ x1 x2 xs,

x1 < x2 →

nondecreasing_sequence (x1::x2::xs) →

undup (x1::x2::xs) = x1 :: undup (x2::xs).

∀ x1 x2 xs,

x1 < x2 →

nondecreasing_sequence (x1::x2::xs) →

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.

Lemma nondecreasing_sequence_undup:

∀ xs,

nondecreasing_sequence xs →

nondecreasing_sequence (undup xs).

∀ xs,

nondecreasing_sequence xs →

nondecreasing_sequence (undup xs).

We also show that the penultimate element of a sequence undup xs
is bounded by the penultimate element of sequence xs.

Lemma undup_nth_le:

∀ xs,

nondecreasing_sequence xs →

undup xs [| (size (undup xs)).-2 |] ≤ xs [| (size xs).-2 |].

Opaque undup.

End Undup.

∀ xs,

nondecreasing_sequence xs →

undup xs [| (size (undup xs)).-2 |] ≤ xs [| (size xs).-2 |].

Opaque undup.

End Undup.

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 (distances(xs
++ [:: a; b])) can be rewritten as distances(xs ++ [:: a])
++ [:: b - a].

Lemma distances_unfold_2app_last:

∀ (a b : nat) (xs : seq nat),

distances (xs ++ [:: a; b])

= distances (xs ++ [:: a]) ++ [:: b - a].

∀ (a b : nat) (xs : seq nat),

distances (xs ++ [:: a; b])

= distances (xs ++ [:: a]) ++ [:: b - a].

We also prove a lemma stating that

*one*append to a sequence in the distances function (i.e., distances(xs ++ [:: x])) can be rewritten as distances xs ++ [:: x - last0 xs].
Lemma distances_unfold_1app_last:

∀ x xs,

size xs ≥ 1 →

distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs].

∀ x xs,

size xs ≥ 1 →

distances (xs ++ [:: x]) = 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.

Lemma distance_between_neighboring_elements_le_max_distance_in_seq:

∀ (xs : seq nat) (n : nat),

xs[|n.+1|] - xs[|n|] ≤ max0 (distances xs).

∀ (xs : seq nat) (n : nat),

xs[|n.+1|] - xs[|n|] ≤ max0 (distances xs).

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.

Lemma function_of_distances_is_correct:

∀ (xs : seq nat) (n : nat),

(distances xs)[|n|] = xs[|n.+1|] - xs[|n|].

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

We prove that index_iota 0 n produces a sequence of numbers
which are always one unit apart from each other.

# 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.

Lemma max_distance_in_nontrivial_seq_is_positive:

∀ (xs : seq nat),

nondecreasing_sequence xs →

(∃ x y, x \in xs ∧ y \in xs ∧ x ≠ y) →

0 < max0 (distances xs).

∀ (xs : seq nat),

nondecreasing_sequence xs →

(∃ x y, x \in xs ∧ y \in xs ∧ x ≠ y) →

0 < max0 (distances xs).

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].

Lemma last_seq_minus_last_distance_seq:

∀ (xs : seq nat),

nondecreasing_sequence xs →

last0 xs - last0 (distances xs) = xs [| (size xs).-2 |].

∀ (xs : seq nat),

nondecreasing_sequence xs →

last0 xs - last0 (distances xs) = xs [| (size xs).-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.

Lemma max_distance_in_seq_le_last_element_of_seq:

∀ (xs : seq nat),

nondecreasing_sequence xs →

max0 (distances xs) ≤ last0 xs.

∀ (xs : seq nat),

nondecreasing_sequence xs →

max0 (distances xs) ≤ last0 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]].

Lemma distances_iota_filtered:

∀ xs k,

(∀ x, x \in xs → x ≤ k) →

nondecreasing_sequence xs →

distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] = [seq x <- distances xs | 0 < x].

∀ xs k,

(∀ x, x \in xs → x ≤ k) →

nondecreasing_sequence xs →

distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] = [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.

Lemma distances_positive_undup:

∀ xs,

nondecreasing_sequence xs →

[seq d <- distances xs | 0 < d] = distances (undup xs).

∀ xs,

nondecreasing_sequence xs →

[seq d <- distances xs | 0 < d] = distances (undup 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.

Lemma domination_of_distances_implies_domination_of_seq:

∀ (xs ys : seq nat),

first0 xs ≤ first0 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 DistancesOfNonDecreasingSequence.

End NondecreasingSequence.

∀ (xs ys : seq nat),

first0 xs ≤ first0 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 DistancesOfNonDecreasingSequence.

End NondecreasingSequence.