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.

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

    Lemma iota_is_increasing_sequence :
      ∀ a b P,
        increasing_sequence [seq x <- index_iota a b | P x ].

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.

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.

    Lemma nondec_seq_zero_first :
      ∀ xs,
        (0 \in xs ) →
        nondecreasing_sequence xs →
        first0 xs = 0.

If x1::x2::xs is a non-decreasing sequence, then either x1 = x2 or x1 < x2.

    Lemma nondecreasing_sequence_2cons_leVeq :
      ∀ x1 x2 xs,
        nondecreasing_sequence (x1 :: x2 :: xs) →
        x1 = x2 ∨ x1 < x2.

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

    Lemma nondecreasing_sequence_cons :
      ∀ 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).

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

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

    Lemma nondecreasing_sequence_cons_min :
      ∀ 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 ).

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

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.

    Lemma nodup_sort_2cons_lt :
      ∀ 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.

    Lemma last0_undup :
      ∀ xs,
        nondecreasing_sequence xs →
        last0 (undup xs) = last0 xs.

Non-decreasing sequence remains non-decreasing after application of undup.

    Lemma nondecreasing_sequence_undup :
      ∀ 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.

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.

    Lemma distances_unfold_2cons :
      ∀ x0 x1 xs,
        distances (x0 ::x1 ::xs) = (x1 - x0 ) :: distances (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 ].

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

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

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

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.

Section DistancesOfNonDecreasingSequence.

First we show that the max distance between elements of any nontrivial sequence (i.e., a sequence that contains at least 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).

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

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.

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

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

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.