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