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

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

Properties of Increasing Sequence

In this section we prove a few lemmas about increasing sequences.
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].
  Proof.
    clear⇒ a b P.
    have EX : ∃ k, b - a ≤ k.
    { by ∃ (b-a). } destruct EX as [k BO].
    revert a b P BO; elim: k ⇒ [ |k IHk].
    { move ⇒ a b P BO n1 n2.
      move: BO; rewrite leqn0 ⇒ /eqP BO.
      rewrite /index_iota BO; simpl.
      by move ⇒ /andP [_ F].
    }
    { move ⇒ a b P BO n1 n2 /andP [GE LT].
      case: (leqP b a) ⇒ [N|N].
      - move: N; rewrite -subn_eq0 ⇒ /eqP EQ.
        by rewrite /index_iota EQ //= in LT.
      - rewrite index_iota_lt_step; last by done.
        simpl; destruct (P a) eqn:PA.
        + destruct n1, n2; try done; simpl.
          × apply iota_filter_gt; first by done.
            by rewrite index_iota_lt_step // //= PA //= in LT.
          × apply IHk; try lia.
            apply/andP; split; first by done.
            by rewrite index_iota_lt_step // //= PA //= in LT.
        + apply IHk; try lia.
          apply/andP; split; first by done.
          by rewrite index_iota_lt_step // //= PA //= in LT.
    }
  Qed.

We prove that any increasing sequence is also a non-decreasing sequence.
  Lemma increasing_implies_nondecreasing :
    ∀ xs,
      increasing_sequence xs →
      nondecreasing_sequence xs.
  Proof.
    intros ? INC n1 n2.
    move ⇒ /andP [+ LT2]; rewrite leq_eqVlt ⇒ /orP [/eqP → //| LT1].
    by apply: ltnW; apply: INC; apply/andP.
  Qed.

Properties of Non-Decreasing Sequence

In this section we prove a few lemmas about non-decreasing sequences.
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.
  Proof.
    move⇒ xs.
    destruct xs as [ | x xs]; first by done.
    destruct x as [ | x]; first by done.
    rewrite in_cons ⇒ /orP [/eqP EQ | IN] ND; first by done.
    exfalso.
    have NTH := nth_index 0 IN.
    specialize (ND 0 (index 0 xs).+1).
    feed ND.
    { apply/andP; split; first by done.
        by simpl; rewrite ltnS index_mem. }
    by simpl in ND; rewrite NTH in ND.
  Qed.

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.
  Proof.
    move⇒ x1 x2 xs ND.
    destruct (ltngtP x1 x2) as [LT | GT | EQ]; auto.
    move_neq_down GT.
    by specialize (ND 0 1); apply ND.
  Qed.

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.
  Proof.
    intros ? ? ND.
    move ⇒ n1 n2 /andP [LT1 LT2].
    specialize (ND n1.+1 n2.+1).
    apply ND.
    apply/andP; split.
    - by rewrite ltnS.
    - by simpl; rewrite ltnS.
  Qed.

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).
  Proof.
    move⇒ x xs MIN ND [ |n1] [ | n2] //.
    move⇒ /andP [_ S] //=.
    apply leq_trans with (xs [| 0 |]).
    - apply MIN; apply mem_nth.
      simpl in *; rewrite ltnS in S.
      by apply leq_ltn_trans with n2.
    - by apply ND; apply/andP; split.
  Qed.

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).
  Proof.
    intros ? ? ND.
    move ⇒ [ | n1] [ | n2] /andP [LT1 LT2]; try done.
    - specialize (ND 0 n2).
      by apply ND; rewrite //= ltnS in LT2.
    - apply ND.
      apply/andP; split.
      + by rewrite ltnS in LT1.
      + by rewrite //= ltnS in LT2.
  Qed.

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).
  Proof.
    intros x xs ND y IN.
    have IDX := nth_index 0 IN.
    specialize (ND 0 (index y xs).+1).
    move: (IN) ⇒ IDL; rewrite -index_mem in IDL.
    feed ND.
    { by apply/andP; split; last rewrite //= ltnS. }
    eapply leq_trans; first by apply ND.
    by rewrite //= IDX.
  Qed.

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).
  Proof.
    intros ? ? ? LT ND ? IN.
    eapply leq_trans; first by apply LT.
    apply nondecreasing_sequence_cons in ND.
    eapply nondecreasing_sequence_cons_min; last by apply IN.
    by apply nondecreasing_sequence_cons_double.
  Qed.

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).
  Proof.
    move⇒ xs x n STR H; apply/negP ⇒ /nthP ⇒ /(_ 0) [ind LE HHH].
    subst x; rename ind into x.
    destruct (n.+1 < size xs) eqn:Bt; last first.
    { move: Bt ⇒ /negP /negP; rewrite -leqNgt ⇒ Bt.
      apply nth_default with (x0 := 0) in Bt.
      by rewrite Bt in H; move: H ⇒ /andP [_ T]. }
    have B1: n.+1 < size xs; first by done. clear Bt.
    have B2: n < size xs; first by apply leq_ltn_trans with n.+1.
    have GT: n < x.
    { move: H ⇒ /andP [T _].
      rewrite ltnNge; apply/negP; intros CONTR.
      specialize (STR x n).
      feed STR.
      { by apply/andP; split. }
      by move: STR; rewrite leqNgt ⇒ /negP STR; apply: STR.
    }
    have LT: x < n.+1.
    { clear GT.
      move: H ⇒ /andP [_ T].
      rewrite ltnNge; apply/negP; intros CONTR.
      move: CONTR; rewrite leq_eqVlt ⇒ /orP [/eqP EQ | CONTR].
      - by subst; rewrite ltnn in T.
      - specialize (STR n.+1 x).
        feed STR.
        { by apply/andP; split; first apply ltnW. }
        by move: STR; rewrite leqNgt ⇒ /negP STR; apply: STR.
    }
    by move: LT; rewrite ltnNge ⇒ /negP LT; apply: LT.
  Qed.

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|].
  Proof.
    move⇒ xs x SIZE LAST.
    have EX: ∃ n, size xs ≤ n by ∃ (size xs). move: EX ⇒ [n LE].
    destruct n as [ |n]; first by destruct xs.
    destruct n as [ |n]; first by destruct xs as [ |? xs]; last destruct xs.
    generalize dependent xs.
    elim: n ⇒ [ |n IHn] xs SIZE LAST LE.
    { by destruct xs as [ |? xs]; [ | destruct xs as [ |? xs]; [ | destruct xs; [∃ 0 | ] ] ]. }
    { destruct xs as [ |n0 xs]; [ | destruct xs as [ |n1 xs]; [ | ]]; try by done.
      destruct xs as [ |n2 xs]; first by (∃ 0).
      destruct (leqP n1 x) as [NEQ|NEQ]; last first.
      { ∃ 0; split; auto. move: LAST ⇒ /andP [LAST _].
        by apply/andP; split. }
      { specialize (IHn [:: n1, n2 & xs]).
        feed_n 3 IHn.
        { by done. }
        { move: LAST ⇒ /andP [LAST1 LAST2].
          apply/andP; split; first by done.
          apply leq_trans with (last0 [:: n0, n1, n2 & xs]); first by done.
          by rewrite /last0 !last_cons.
        }
        { by rewrite -(ltn_add2r 1) !addn1. }
        move: IHn ⇒ [idx [SI /andP [G L]]].
        ∃ idx.+1; split.
        - by simpl in *; rewrite -addn1 -[in X in _ ≤ X]addn1 leq_add2r.
        - by apply/andP; split.
      }
    }
  Qed.

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.
  Proof.
    move⇒ xs x STR IN.
    have NEQ: ∀ x y, x = y ∨ x != y.
    { clear⇒ t x y.
      destruct (x == y) eqn:EQ.
      - by left; apply/eqP.
      - by right.
    }
    move: {NEQ} (NEQ _ x (last0 xs)) ⇒ [EQ|NEQ].
    { by subst x. }
    { move: IN ⇒ /nthP EX.
      specialize (EX 0).
      move: EX ⇒ [id SIZE EQ].
      rewrite /last0 -nth_last -EQ; subst x.
      rewrite -addn1 in SIZE.
      apply STR; apply/andP.
      have POS: 0 < size xs.
      { by apply leq_trans with (id + 1); first rewrite addn1. }
      split.
      - by rewrite -(leq_add2r 1) !addn1 prednK // -addn1.
      - by rewrite prednK.
    }
  Qed.

Properties of Undup of Non-Decreasing Sequence

In this section we prove a few lemmas about undup of non-decreasing sequences.
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).
  Proof.
    move⇒ X x xs; rewrite {2 3}[cons] lock //= -lock.
    rewrite in_cons eq_refl; simpl.
    by destruct (x \in xs).
  Qed.

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).
  Proof.
    move⇒ x1 x2 xs H H0; rewrite {2 3 4}[cons] lock //= -lock.
    rewrite in_cons.
    have → : (x1 == x2) = false.
    { by apply/eqP/eqP; rewrite neq_ltn; rewrite H. }
    rewrite [cons]lock //= -lock.
    have → : (x1 \in xs) = false; last by done.
    apply/eqP; rewrite eqbF_neg.
    apply nondecreasing_sequence_cons in H0.
    apply/negP; intros ?; eauto 2.
    by eapply nondecreasing_sequence_cons_min in H0; eauto 2; lia.
  Qed.

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.
  Proof.
    elim⇒ [//|x1 xs IHxs].
    intros ND; destruct xs as [ |x2 xs]; first by done.
    destruct (nondecreasing_sequence_2cons_leVeq _ _ _ ND) as [EQ|LT].
    - subst; rename x2 into x.
      rewrite nodup_sort_2cons_eq IHxs //=.
      by eapply nondecreasing_sequence_cons; eauto 2.
    - rewrite nodup_sort_2cons_lt // last0_cons.
      + rewrite IHxs //; eauto using nondecreasing_sequence_cons.
      + by move/undup_nil.
  Qed.

Non-decreasing sequence remains non-decreasing after application of undup.
  Lemma nondecreasing_sequence_undup :
    ∀ xs,
      nondecreasing_sequence xs →
      nondecreasing_sequence (undup xs).
  Proof.
    move⇒ xs.
    have EX: ∃ len, size xs ≤ len.
    { by ∃ (size xs). } destruct EX as [n BO].
    revert xs BO; elim: n ⇒ [ |n IHn].
    - by intros xs; rewrite leqn0 size_eq0 ⇒ /eqP EQ; subst xs.
    - intros [ |x1 [ | x2 xs]] Size NonDec; try done.
      destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec) as [EQ|LT].
      + subst; rename x2 into x.
        by rewrite nodup_sort_2cons_eq; apply IHn; eauto using nondecreasing_sequence_cons.
      + rewrite nodup_sort_2cons_lt //.
        apply nondecreasing_sequence_add_min.
        × move⇒ y H.
        eapply nondecreasing_sequence_cons_min with (y := y) in NonDec; auto.
        rewrite -mem_undup; eauto using nondecreasing_sequence_cons.
        × by apply IHn; eauto using nondecreasing_sequence_cons.
  Qed.

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 |].
  Proof.
    Opaque undup.
    move⇒ xs.
    have EX: ∃ len, size xs ≤ len by (∃ (size xs)).
    destruct EX as [n BO].
    revert xs BO; elim: n ⇒ [ |n IHn].
    - by intros xs; rewrite leqn0 size_eq0 ⇒ /eqP EQ; subst xs.
    - intros [ |x1 [ | x2 xs]] Size NonDec; try done.
      destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec) as [EQ|LT].
      × subst; rename x2 into x.
        rewrite nodup_sort_2cons_eq //.
        eapply leq_trans.
        ** apply IHn; first by done.
           by eapply nondecreasing_sequence_cons; eauto.
        ** destruct xs as [ | x1 xs]; first by done.
           by rewrite [in X in _ ≤ X]nth0_cons //.
      × rewrite nodup_sort_2cons_lt //; simpl.
        case (posnP (size (undup (x2 :: xs))).-1) as [Z|POS].
        ** rewrite Z; simpl.
           apply leq_trans with ([:: x1, x2 & xs] [|0|]); first by done.
           by apply NonDec; apply/andP; split; simpl.
        ** rewrite nth0_cons //.
           eapply leq_trans; first apply IHn; eauto using nondecreasing_sequence_cons.
           by destruct xs as [ |? xs]; [exfalso| destruct xs].
  Qed.

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).
  Proof. by intros; rewrite /distances //= drop0. Qed.

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].
  Proof.
    move⇒ a b xs.
    have EX: ∃ n, size xs ≤ n by (∃ (size xs)).
    destruct EX as [n LE].
    elim: n xs LE ⇒ [ |n IHn] xs LE.
    - by move: LE; rewrite leqn0 size_eq0 ⇒ /eqP LE; subst.
    - destruct xs as [ | x0 xs]; first by unfold distances.
      destruct xs as [ | x1 xs]; first by unfold distances.
      have → : distances ([:: x0, x1 & xs] ++ [:: a; b]) = x1 - x0 :: distances ((x1 :: xs) ++ [:: a; b]).
      { by simpl; rewrite distances_unfold_2cons. }
      rewrite IHn; last by simpl in *; rewrite -(leq_add2r 1) !addn1.
      have → : distances ([:: x0, x1 & xs] ++ [:: a]) = x1 - x0 :: distances ((x1 :: xs) ++ [:: a]); last by done.
      by rewrite //= distances_unfold_2cons.
  Qed.

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].
  Proof.
    intros x xs POS.
    have EX: ∃ n, size xs ≤ n by (∃ (size xs)).
    destruct EX as [n LE].
    elim: n x xs LE POS ⇒ [ |n IHn] x xs LE POS.
    - by move: LE; rewrite leqn0 size_eq0 ⇒ /eqP LE; subst.
    - move: LE; rewrite leq_eqVlt ⇒ /orP [/eqP LEN' | LE]; last first.
      + by rewrite ltnS in LE; apply IHn.
      + destruct (seq_elim_last _ _ LEN') as [x__new [xs__l [EQ2 LEN]]].
        subst xs; clear LEN' POS; rename xs__l into xs.
        rewrite -catA.
        rewrite distances_unfold_2app_last.
        destruct xs; first by done.
        by rewrite IHn // ?LEN // /last0 last_cat.
  Qed.

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).
  Proof.
    intros xs id.
    apply leq_trans with (distances xs [| id |]).
    - rewrite leq_eqVlt; apply/orP; left; apply/eqP.
      have EX: ∃ n, size xs ≤ n by (∃ (size xs)).
      move: EX ⇒ [n LE]; move: xs id LE.
      elim: n ⇒ [ |n IHn] xs id LE.
      { move: LE; rewrite leqn0 size_eq0 ⇒ /eqP EQ; subst.
        by rewrite !nth_default.
      }
      { move: LE; rewrite leq_eqVlt ⇒ /orP [/eqP EQ|LT]; last first.
        { by apply IHn; rewrite ltnS in LT. }
        destruct xs as [ | n0 xs]; first by done.
        destruct xs as [ | n1 xs]; first by destruct id; [simpl |rewrite !nth_default].
        have ->: distances [:: n0, n1 & xs] = (n1 - n0) :: distances [:: n1 & xs].
        { by rewrite /distances //= drop0. }
        destruct id; first by done.
        rewrite //= -IHn //=.
        by move: EQ ⇒ /eqP; rewrite //= eqSS ⇒ /eqP EQ; rewrite -EQ.
      }
    - have Lem: ∀ xs x, x \in xs → x ≤ max0 xs.
      { clear; elim⇒ [//|a xs IHxs] x IN.
        rewrite max0_cons leq_max; apply/orP.
        move: IN; rewrite in_cons ⇒ /orP [/eqP EQ| IN].
        + by left; subst.
        + by right; apply IHxs.
      }
      destruct (size (distances xs) ≤ id) eqn:SIZE.
      + by rewrite nth_default.
      + apply Lem; rewrite mem_nth //.
        move: SIZE ⇒ /negP /negP.
        by rewrite ltnNge.
  Qed.

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|].
  Proof.
    intros xs.
    have EX: ∃ len, size xs ≤ len by (∃ (size xs)).
    move: EX ⇒ [len LE]; move: xs LE.
    elim: len ⇒ [ |len IHlen] xs LE n.
    { by move: LE; rewrite leqn0 size_eq0 ⇒ /eqP EQ; subst; destruct n. }
    move: LE; rewrite leq_eqVlt ⇒ /orP [/eqP EQ| LE]; last by apply IHlen.
    destruct xs as [ | x1 xs]; first by done.
    destruct xs as [ | x2 xs]; first by destruct n as [ | [ | ]].
    destruct n as [ |n]; first by done.
    have ->: distances [:: x1, x2 & xs] [|n.+1|] = distances [::x2 & xs] [| n |].
    { have ->: distances [:: x1, x2 & xs] = (x2 - x1) :: distances [::x2 & xs]; last by done.
      { by rewrite /distances //= drop0. }
    }
    have ->: [:: x1, x2 & xs] [|n.+2|] - [:: x1, x2 & xs] [|n.+1|] = [:: x2 & xs] [|n.+1|] - [:: x2 & xs] [|n|] by done.
    apply IHlen.
    by move: EQ ⇒ /eqP; rewrite //= eqSS ⇒ /eqP <-.
  Qed.

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.
  Proof.
    intros xs.
    have EX: ∃ len, size xs ≤ len by (∃ (size xs)).
    move: EX ⇒ [len LE]; move: xs LE.
    elim: len ⇒ [ |len IHlen] xs LE SIZE.
    { by move: LE; rewrite leqn0 size_eq0 ⇒ /eqP EQ; subst. }
    { move: LE; rewrite leq_eqVlt ⇒ /orP [/eqP EQ| LE]; last by apply IHlen.
      destruct xs as [ | x1 xs]; first by inversion EQ.
      destruct xs as [ | x2 xs]; first by inversion SIZE.
      destruct xs as [ | x3 xs]; first by done.
      clear SIZE.
      have ->: size [:: x1, x2, x3 & xs] = size [:: x2, x3 & xs] + 1 by rewrite addn1.
      have ->: size (distances [:: x1, x2, x3 & xs]) = size (distances [:: x2, x3 & xs]) + 1 by rewrite addn1.
      apply/eqP; rewrite eqn_add2r; apply/eqP.
      apply IHlen; last by done.
      by move: EQ ⇒ /eqP; rewrite //= eqSS ⇒ /eqP <-.
    }
  Qed.

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 = ε.
  Proof.
    move⇒ n x; elim: n ⇒ [ |n IHn] IN.
    - by unfold index_iota, distances in IN.
    - destruct n; first by unfold distances, index_iota in IN.
      move: IN; rewrite -addn1 /index_iota subn0 iotaD add0n.
      rewrite distances_unfold_1app_last; last by rewrite size_iota.
      rewrite mem_cat ⇒ /orP [IN|IN].
      + by apply IHn; rewrite /index_iota subn0; simpl.
      + by move: IN;
          rewrite -addn1 iotaD /last0 last_cat add0n addn1 // subSnn in_cons ⇒ /orP [/eqP EQ|F]; subst.
  Qed.

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 < max0 (distances xs).
  Proof.
    move ⇒ xs SIZE [x [y [/nthP INx [/nthP INy /eqP NEQ]]]].
    move: (INx 0) (INy 0) ⇒ [indx SIZEx EQx] [indy SIZEy EQy].
    suff L:
      ∀ (x y indx indy : nat),
        indx < size xs → indy < size xs →
        nondecreasing_sequence xs →
        x < y → xs [|indx|] = x → xs [|indy|] = y →
        0 < max0 (distances xs).
    { move: NEQ; rewrite neq_ltn ⇒ /orP [LT|LT].
       - by apply: (L x y indx indy).
       - by apply: (L y x indy indx). }
    clear; intros x y indx indy SIZEx SIZEy SIZE LT EQx EQy.
    have LTind: indx < indy.
    { rewrite ltnNge; apply/negP; intros CONTR.
      subst x y; move: LT; rewrite ltnNge ⇒ /negP; apply.
      by apply SIZE; apply/andP. }
    have EQ: ∃ Δ, indy = indx + Δ; [by ∃ (indy - indx); lia | move: EQ ⇒ [Δ EQ]; subst indy].
    have F: ∃ ind, indx ≤ ind < indx + Δ ∧ xs[|ind|] < xs[|ind.+1|].
    { subst x y; clear SIZEx SIZEy; revert xs indx LTind SIZE LT.
      elim: Δ ⇒ [ |Δ IHΔ] xs indx LTind SIZE LT; first by lia.
      destruct (posnP Δ) as [ZERO|POS].
      { by subst Δ; ∃ indx; split; [rewrite addn1; apply/andP | rewrite addn1 in LT]; auto. }
      have ALT: xs[|indx + Δ|] == xs[|indx + Δ.+1|] ∨ xs[|indx + Δ|] < xs[|indx + Δ.+1|].
      { apply/orP; rewrite -leq_eqVlt addnS.
        apply SIZE; apply/andP; split; first by done.
        rewrite ltnNge; apply/negP; intros CONTR.
        move: LT; rewrite ltnNge ⇒ /negP LT; apply: LT.
        by rewrite nth_default ?addnS. }
      move: ALT ⇒ [/eqP EQ|LT'].
      - edestruct (IHΔ) as [ind [B UP]]; eauto 5 using addn1, leq_add2l.
        ∃ ind; split; last by done.
        move: B ⇒ /andP [B1 B2]; apply/andP; split; first by done.
        by rewrite addnS ltnS ltnW.
      - ∃ (indx + Δ); split; last by rewrite -addnS.
        by apply/andP; split; [rewrite leq_addr | rewrite addnS]. }
    move: F ⇒ [ind [/andP [B1 B2] UP]].
    apply leq_trans with (xs [|ind.+1|] - xs [|ind|]).
    - by rewrite subn_gt0.
    - by apply distance_between_neighboring_elements_le_max_distance_in_seq.
  Qed.

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 |].
  Proof.
    unfold nondecreasing_sequence in ×.
    intros xs SIS.
    destruct xs as [ | x1 xs]; first by done.
    destruct xs as [ | x2 xs]; first by rewrite subn0.
    rewrite {2}/last0 -[in X in _ - X]nth_last function_of_distances_is_correct prednK; last by done.
    set [:: x1, x2 & xs] as X.
    rewrite /last0 -nth_last size_of_seq_of_distances; last by done.
    rewrite !addn1 -pred_Sn subKn; first by done.
    rewrite /X; apply SIS; apply/andP; split; first by simpl.
    by rewrite [in X in _ < X]size_of_seq_of_distances; first rewrite addn1.
  Qed.

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.
  Proof.
    move⇒ xs H.
    have SIZE: size xs < 2 ∨ 2 ≤ size xs.
    { by destruct (size xs) as [ | n]; last destruct n; auto. }
    move: SIZE ⇒ [LT | SIZE2].
    { by destruct xs as [ |? xs]; last destruct xs. }
    apply leq_trans with (last0 xs - first0 xs); last by apply leq_subr.
    have F: ∀ xs c, (∀ x, x \in xs → x ≤ c) → max0 xs ≤ c.
    { clear; move⇒ xs c H.
      elim: xs H ⇒ [//|a xs IHxs] H.
      rewrite max0_cons geq_max; apply/andP; split.
      + by apply H; rewrite in_cons; apply/orP; left.
      + by apply IHxs; intros; apply H; rewrite in_cons; apply/orP; right.
    }
    apply: F ⇒ d IN.
    move: IN ⇒ /nthP T; specialize (T 0); move: T ⇒ [idx IN DIST].
    rewrite function_of_distances_is_correct in DIST.
    rewrite -DIST leq_sub //.
    { destruct (xs [|idx.+1|] == last0 xs) eqn:EQ.
      - by rewrite leq_eqVlt; apply/orP; left.
      - rewrite /last0 -nth_last. apply H.
        rewrite -(ltn_add2r 1) addn1 -size_of_seq_of_distances in IN; last by done.
        move: IN; rewrite leq_eqVlt ⇒ /orP [/eqP KK|KK].
        + move: EQ; rewrite /last0 -nth_last -{1}KK -[_.+2.-1]pred_Sn ⇒ /eqP; by done.
        + apply/andP; split; first rewrite -(ltn_add2r 1) !addn1 prednK //.
        by rewrite prednK //; apply ltn_trans with idx.+2.
    }
    { destruct (first0 xs == xs [|idx|]) eqn:EQ.
      - by rewrite leq_eqVlt; apply/orP; left.
      - rewrite /first0 -nth0. apply H.
        rewrite -(ltn_add2r 1) addn1 -size_of_seq_of_distances in IN; last by done.
        destruct idx as [ |idx]; first by move: EQ; rewrite /first0 -nth0 ⇒ /eqP.
        apply/andP; split; first by done.
        by apply ltn_trans with idx.+2.
    }
  Qed.

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].
  Proof.
    intros xs.
    have EX: ∃ len, size xs ≤ len by (∃ (size xs)).
    destruct EX as [n BO].
    elim: n xs BO ⇒ [ |n IHn] xs Len k Bound NonDec.
    { move: Len; rewrite leqn0 size_eq0 ⇒ /eqP T; subst.
      by rewrite filter_pred0.
    }
    { destruct xs as [ |x1 [ |x2 xs]].
      - by rewrite filter_pred0.
      - by rewrite index_iota_filter_singl; last (rewrite ltnS; apply Bound; rewrite in_cons; apply/orP; left).
      - have LEx1: x1 ≤ k by apply Bound; rewrite in_cons eq_refl.
        have LEx2: x2 ≤ k by apply Bound; rewrite !in_cons eq_refl orbT.
        have M1: ∀ y : nat, y \in x2 :: xs → x1 ≤ y by apply nondecreasing_sequence_cons_min.
        have M2: ∀ x : nat, x \in x2 :: xs → x ≤ k by intros; apply Bound; rewrite in_cons; apply/orP; right.
        have M3: ∀ y : nat, y \in xs → x2 ≤ y by apply nondecreasing_sequence_cons in NonDec; apply nondecreasing_sequence_cons_min.
        destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec).
        + subst; rewrite distances_unfold_2cons.
          replace ((@filter nat (fun x : nat ⇒ leq (S O) x) (@cons nat (subn x2 x2) (distances (@cons nat x2 xs)))))
            with ([seq x <- distances (x2 :: xs) | 0 < x]); last by rewrite subnn.
          rewrite range_filter_2cons.
            by apply IHn; eauto 2 using nondecreasing_sequence_cons.
        + have M4: ∀ y : nat, y \in x2 :: xs → x1 < y by apply nondecreasing_sequence_cons_smin.
          rewrite distances_unfold_2cons.
          rewrite range_iota_filter_step // rem_lt_id //.
          replace ((@filter nat (fun x : nat ⇒ leq (S O) x) (@cons nat (subn x2 x1) (distances (@cons nat x2 xs)))))
            with (x2 - x1 :: [seq x <- distances (x2 :: xs) | 0 < x]); last first.
          { simpl; replace (0 < x2 - x1) with true; first by done.
              by apply/eqP; rewrite eq_sym; rewrite eqb_id subn_gt0. }
          rewrite -(IHn _ _ k) //; last eapply nondecreasing_sequence_cons; eauto 2.
          by rewrite {1}range_iota_filter_step // distances_unfold_2cons {1}range_iota_filter_step //.
    }
  Qed.

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).
  Proof.
    move⇒ xs NonDec.
    rewrite -(distances_iota_filtered _ (max0 xs)); [ | by apply in_max0_le | by done].
    enough ([seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = (undup xs)) as IN; first by rewrite IN.
    have EX: ∃ len, size xs ≤ len.
    { ∃ (size xs); now simpl. } destruct EX as [n BO].
    elim: n xs NonDec BO ⇒ [ |n IHn].
    - by intros xs _; rewrite leqn0 size_eq0 ⇒ /eqP ->; rewrite filter_pred0.
    - intros [ |x1 [ | x2 xs]].
      + by rewrite filter_pred0.
      + by rewrite index_iota_filter_singl ?L02 //; apply/andP; split; [ done | destruct x1].
      + intros NonDec Size.
        destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec) as [EQ|LT].
        × subst; rename x2 into x.
          rewrite nodup_sort_2cons_eq range_filter_2cons max0_2cons_eq.
          by apply IHn; [ eapply nondecreasing_sequence_cons; eauto | by done].
        × rewrite nodup_sort_2cons_lt // max0_2cons_le; last by rewrite ltnW.
          rewrite index_iota_filter_step; [ | | by apply nondecreasing_sequence_cons_min]; last first.
          { apply/andP; split; first by done.
            eapply leq_trans; first by eassumption.
            rewrite ltnW // ltnS; apply in_max0_le.
            by rewrite in_cons eq_refl.
          }
          rewrite rem_lt_id //; last by apply nondecreasing_sequence_cons_smin.
          by rewrite IHn //; eauto using nondecreasing_sequence_cons.
  Qed.

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|]).
  Proof.
    intros xs ys.
    have EX: ∃ len, size xs ≤ len ∧ size ys ≤ len.
    { ∃ (maxn (size xs) (size ys)).
      by split; rewrite leq_max; apply/orP; [left | right].
    } move: EX ⇒ [len [LE1 LE2]].
    generalize dependent xs; generalize dependent ys.
    elim: len ⇒ [ |len IHlen].
    { move⇒ ys + xs + H H0 h1 H2 H3 H4 H5 n.
      by rewrite !leqn0 !size_eq0 ⇒ /eqP → /eqP →. }
    { intros ys LycSIZE xs LxSIZE FLE Sxs Sys SIZEEQ STRxs STRys LE n.
      destruct xs as [ | x1 xs], ys as [ | y1 ys]; try by done.
      destruct xs as [ | x2 xs], ys as [ | y2 ys]; try by done.
      have F: x2 ≤ y2.
      { specialize (STRxs 0 1); feed STRxs; first by done.
        specialize (STRys 0 1); feed STRys; first by done.
        specialize (LE 0); simpl in LE, FLE.
        rewrite leqNgt; apply/negP; intros NEQ.
        move: LE; rewrite leqNgt ⇒ /negP LE; apply: LE.
        rewrite -(ltn_add2r x1) subnK // addnBAC // -(ltn_add2r y1) subnK.
        - by eapply leq_ltn_trans; [erewrite leq_add2l | erewrite ltn_add2r].
        - by apply leq_trans with y2; auto using leq_addr.
      }
      destruct xs as [ | x3 xs], ys as [ | y3 ys]; try by done.
      { by destruct n as [ |n]; [ | destruct n]. }
      destruct n ⇒ //.
      simpl; apply: IHlen ⇒ //.
      - move ⇒ m1 m2 /andP [B1 B2].
        apply (STRxs m1.+1 m2.+1); apply/andP; split.
        + by rewrite ltnS.
        + by rewrite -(ltn_add2r 1) !addn1 in B2.
      - move ⇒ m1 m2 /andP [B1 B2].
        apply (STRys m1.+1 m2.+1); apply/andP; split.
        + by rewrite ltnS.
        + by rewrite -(ltn_add2r 1) !addn1 in B2.
      - by move⇒ n0; specialize (LE n0.+1); simpl in LE.
    }
  Qed.

End NondecreasingSequence.