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.tactics.
Require Export prosa.util.list.

Non-Decreasing Sequence and Distances

In this file we prove properties of sorted sequences and the distances between consecutive elements.

TODO: All lemmas in this file unrelated to distances are being contributed to MathComp. With the next MathComp release containing these results, replace their uses with upstream lemmas, delete the local lemmas, and rename this file to distances.v.

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

A sequence is non-decreasing if its elements are sorted with leq.

Definition nondecreasing_sequence (xs : seq nat) := sorted leq xs.

The distances between neighboring elements are their natural-number differences. pairmap applies subtraction to each consecutive pair, starting with the first element and the tail of the sequence. For example, distances [:: 1; 10; 10; 17; 20; 41] yields [:: 9; 0; 7; 3; 21]. Empty and singleton sequences have no distances.

Definition distances (xs : seq nat) :=
pairmap (fun x y ⇒ y - x) (head 0 xs) (behead xs).

Properties of Non-Decreasing Sequence

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

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

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 ≤ last 0 xs.

Properties of Undup of Non-Decreasing Sequence

We compare elements of a non-decreasing sequence before and after undup.

Counting from the end, each element of undup xs is bounded by the corresponding element of the non-decreasing sequence xs. Here n = 0 selects the last element; indices past the beginning saturate at zero.

  Lemma undup_nth_le :
    ∀ xs n,
      nondecreasing_sequence xs →
      undup xs [| size (undup xs) - n .+1 |]
        ≤ xs [| size xs - n .+1 |].

Properties of Distances

In this section we prove a few lemmas about function 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).

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

The sequence of distances has length (size xs).-1, including when xs is empty.

  Lemma size_of_seq_of_distances :
    ∀ (xs : seq nat),
      size (distances xs) = (size xs ).-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_(x <- distances xs ) x ).

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 = ε.

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 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 < (\max_(x <- distances xs ) x ).

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 →
      last 0 xs - last 0 (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 →
      (\max_(x <- distances xs ) x ) ≤ last 0 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 sequences xs and ys of equal length, with ys non-decreasing. If the first element and all neighboring differences of xs are bounded by those of ys, then xs is dominated by ys.

  Lemma domination_of_distances_implies_domination_of_seq :
    ∀ (xs ys : seq nat),
      head 0 xs ≤ head 0 ys →
      size xs = size ys →
      nondecreasing_sequence ys →
      (∀ n, (distances xs )[|n |] ≤ (distances ys )[|n |]) →
      (∀ n, xs [|n |] ≤ ys [|n |]).

End NondecreasingSequence.