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

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; move ⇒ /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; 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.

∀ 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; move ⇒ /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; 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.

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

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

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.

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

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.

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

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

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

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.

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

∀ 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; move ⇒ 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; 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.

∀ (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; move ⇒ 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; 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.

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.

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

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.

End NonDecreasingSequence.

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

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.

End NonDecreasingSequence.

# Properties of Undup of Non-Decreasing Sequence

In this section we prove a few lemmas about undup of non-decreasing sequences.
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.

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

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

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 move/undup_nil.

Qed.

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

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 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; 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 //.

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.

∀ 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; 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 //.

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; 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 as [ |? xs].

++ by exfalso.

++ by destruct xs.

Qed.

End Undup.

∀ 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; 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 as [ |? xs].

++ by exfalso.

++ by destruct xs.

Qed.

End Undup.

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.

∀ 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; move ⇒ /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.

∀ (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; move ⇒ /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; 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.

by rewrite IHn // ?LEN // /last0 last_cat.

Qed.

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

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

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

elim: len ⇒ [ |len IHlen] xs LE n.

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

∀ (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; 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 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; 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/eqP; rewrite eqn_add2r; apply/eqP.

apply IHlen; last by done.

by move: EQ ⇒ /eqP; rewrite //= eqSS ⇒ /eqP <-.

}

Qed.

∀ (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; 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/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;

move ⇒ /orP [/eqP EQ|F]; subst.

Qed.

End Distances.

∀ 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;

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.

move ⇒ xs 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.

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; move ⇒ /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.

}

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.

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

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; move ⇒ /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.

}

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.

∀ (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; move ⇒ /orP [/eqP KK|KK].

move: EQ; rewrite /last0 -nth_last -{1}KK -[_.+2.-1]pred_Sn; move ⇒ /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; move ⇒ /eqP.

apply/andP; split; first by done.

by apply ltn_trans with idx.+2.

}

Qed.

∀ (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; move ⇒ /orP [/eqP KK|KK].

move: EQ; rewrite /last0 -nth_last -{1}KK -[_.+2.-1]pred_Sn; move ⇒ /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; 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].

elim: n xs BO ⇒ [ |n IHn] xs 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 : 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.

∀ 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; 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 : 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.

∀ 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; move ⇒ /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 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|]).

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; move ⇒ /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 DistancesOfNonDecreasingSequence.

End NondecreasingSequence.