# 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.
Lemma iota_is_increasing_sequence:
a b P,
increasing_sequence [seq x <- index_iota a b | P x].
Proof.
clear; intros ? ? ?.
have EX : k, b - a k.
{ by (b-a). } destruct EX as [k BO].
revert a b P BO; induction k.
{ movea b P BO n1 n2.
move: BO; rewrite leqn0; move ⇒ /eqP BO.
rewrite /index_iota BO; simpl.
by move ⇒ /andP [_ F].
}
{ movea b P BO n1 n2 /andP [GE LT].
case: (leqP b a) ⇒ [N|N].
- move: N; rewrite -subn_eq0; move ⇒ /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; rewrite leq_eqVlt; move ⇒ [/orP [/eqP EQ| LT1] LT2].
- by subst.
- by apply ltnW; apply INC; apply/andP; split.
Qed.

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.
Proof.
destruct xs as [ | x xs]; first by done.
destruct x as [ | x]; first by done.
rewrite in_cons; move ⇒ /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.
intros ? ? ? 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.
moven1 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.
x xs,
( y, y \in xs x y)
nondecreasing_sequence xs
nondecreasing_sequence (x :: xs).
Proof.
intros x xs MIN ND [ |n1] [ | n2]; try done.
- 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.
+ apply ND; apply/andP; split; auto.
- by rewrite //= !ltnS; apply ND.
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 ? ? ND ? 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.
intros ? ? ? STR ?; apply/negP; intros ?.
move: H0 ⇒ /nthP. intros GG.
specialize (GG 0).
move: GG ⇒ [ind LE HHH].
subst x; rename ind into x.
destruct (n.+1 < size xs) eqn:Bt; last first.
{ move: Bt ⇒ /negP /negP; rewrite -leqNgt; moveBt.
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; move ⇒ /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; move ⇒ /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; move ⇒ /negP STR; apply: STR.
}
by move: LT; rewrite ltnNge; move ⇒ /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.
intros ? ? SIZE LAST.
have EX: n, size xs n by (size xs). move: EX ⇒ [n LE].
destruct n; first by destruct xs.
destruct n; first by destruct xs; last destruct xs.
generalize dependent xs.
induction n; intros.
{ by destruct xs; [ | destruct xs; [ | destruct xs; [ 0 | ] ] ]. }
{ destruct xs; [ | destruct xs; [ | ]]; try by done.
destruct 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.
}
move: IHn ⇒ [idx [SI /andP [G L]]].
idx.+1; split.
- 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.
intros ? ? STR IN.
have NEQ: x y, x = y x != y.
{ clear; intros.
destruct (x == y) eqn:EQ.
- by left; apply/eqP.
- by right.
}
move: (NEQ _ x (last0 xs)); clear NEQ; move ⇒ [EQ|NEQ].
{ by subst x. }
{ move: IN ⇒ /nthP EX.
specialize (EX 0).
move: EX ⇒ [id SIZE EQ].
rewrite /last0 -nth_last -EQ; subst x.
apply STR; apply/andP.
have POS: 0 < size xs.
{ by apply leq_trans with (id + 1); first rewrite addn1. }
split.
- by rewrite prednK.
}
Qed.

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).
Proof.
intros; 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.
intros; 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.
induction xs as [ | x1 xs]; first by done.
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.
rewrite [in X in _ = X]last0_cons //.
by eapply nondecreasing_sequence_cons; eauto 2.
+ rewrite nodup_sort_2cons_lt // last0_cons.
rewrite IHxs //; eauto using nondecreasing_sequence_cons.
by intros ?; apply undup_nil in H.
Qed.

Non-decreasing sequence remains non-decreasing after application of undup.
Lemma nondecreasing_sequence_undup:
xs,
nondecreasing_sequence xs
nondecreasing_sequence (undup xs).
Proof.
intros ?.
have EX: len, size xs len.
{ by (size xs). } destruct EX as [n BO].
revert xs BO; induction n.
- by intros xs; rewrite leqn0 size_eq0; move ⇒ /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 //.
intros ? ?.
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.
intros ?.
have EX: len, size xs len by ( (size xs)).
destruct EX as [n BO].
revert xs BO; induction n.
- by intros xs; rewrite leqn0 size_eq0; move ⇒ /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. by done. 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.
destruct xs.
++ by exfalso.
++ destruct xs; simpl in *; auto.
Qed.

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

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].
Lemma distances_unfold_2app_last:
(a b : nat) (xs : seq nat),
distances (xs ++ [:: a; b])
= distances (xs ++ [:: a]) ++ [:: b - a].
Proof.
intros.
have EX: n, size xs n by ( (size xs)).
destruct EX as [n LE].
revert xs LE; induction n; intros.
- by move: LE; rewrite leqn0 size_eq0; move ⇒ /eqP LE; subst.
- destruct xs as [ | x0]; first by unfold distances.
destruct xs as [ | x1]; first by unfold distances.
have → : distances ([:: x0, x1 & xs] ++ [:: a; b]) = x1 - x0 :: distances ((x1 :: xs) ++ [:: a; b]).
{ by simpl; rewrite distances_unfold_2cons. }
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., ++ [:: 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].
revert x xs LE POS; induction n; intros.
- by move: LE; rewrite leqn0 size_eq0; move ⇒ /eqP LE; subst.
- move: LE; rewrite leq_eqVlt; move ⇒ /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.
rewrite IHn.
× by rewrite /last0 last_cat.
× by rewrite LEN.
× by done.
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.
induction n; intros.
{ move: LE; rewrite leqn0 size_eq0; move ⇒ /eqP EQ; subst.
by rewrite !nth_default.
}
{ move: LE; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ|LT]; last first.
{ by apply IHn; rewrite ltnS in LT. }
destruct xs; first by done.
destruct 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; induction xs; intros ? IN; first by done.
rewrite max0_cons leq_max; apply/orP.
move: IN; rewrite in_cons; move ⇒ /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.
induction len; intros.
{ by move: LE; rewrite leqn0 size_eq0; move ⇒ /eqP EQ; subst; destruct n. }
move: LE; rewrite leq_eqVlt; move ⇒ /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; 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.
induction len; intros × LE SIZE.
{ by move: LE; rewrite leqn0 size_eq0; move ⇒ /eqP EQ; subst. }
{ move: LE; rewrite leq_eqVlt; move ⇒ /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 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.
intros n x IN; induction n.
- by unfold index_iota, distances in IN.
- destruct n; first by unfold distances, index_iota in IN.
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;
move ⇒ /orP [/eqP EQ|F]; subst.
Qed.

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.
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.
movexs SIZE [x [y [INx [INy NEQ]]]].
move: INx INy ⇒ /nthP INx /nthP INy; specialize (INx 0); specialize (INy 0).
move: INx INy ⇒ [indx SIZEx EQx] [indy SIZEy EQy].
have 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).
{ 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; move ⇒ /negP T; apply: T.
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.
induction Δ; intros; 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 SIZE; apply/andP; split; first by done.
rewrite ltnNge; apply/negP; intros CONTR.
move: LT; rewrite ltnNge; move ⇒ /negP LT; apply: LT.
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.
- (indx + Δ); split; last by 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.
}
move: NEQ ⇒ /eqP; rewrite neq_ltn; move ⇒ /orP [LT|LT].
- by eapply L with (indx := indx) (x := x) (y := y); eauto.
- by eapply L with (indx := indy) (indy := indx) (x := y) (y := x); eauto.
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.
intros.
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; 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; intros.
induction xs; first by done.
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: Fd 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.
move: IN; rewrite leq_eqVlt; move ⇒ /orP [/eqP KK|KK].
move: EQ; rewrite /last0 -nth_last -{1}KK -[_.+2.-1]pred_Sn; move ⇒ /eqP; by done.
+ by apply ltn_trans with idx.+2.
+ by apply ltnW.
+ 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.
destruct idx; first by move: EQ; rewrite /first0 -nth0; move ⇒ /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].
revert xs BO; induction n; intros ? Len k Bound NonDec.
{ move: Len; rewrite leqn0 size_eq0; move ⇒ /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 : natleq (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 : natleq (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.
intros ? 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].
revert xs NonDec BO; induction n.
- 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.
induction len.
{ by intros; move: LE1 LE2; rewrite !leqn0 !size_eq0 ⇒ /eqP → /eqP →. }
{ intros ? LycSIZE ? 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; move ⇒ /negP LE; apply: LE.
- 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; [ | destruct n]. }
destruct n; first by done.
simpl; apply IHlen; try done.
- movem1 m2 /andP [B1 B2].
apply (STRxs m1.+1 m2.+1); apply/andP; split.
+ by rewrite ltnS.