From fcde91efbdef1762165d0ca91242025a474fd184 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 20 Sep 2021 10:50:35 +0200
Subject: [PATCH] clean up in util/nondecreasing.v
---
util/nondecreasing.v | 387 +++++++++++++++++++------------------------
1 file changed, 169 insertions(+), 218 deletions(-)
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 722f172ce..1462134ca 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -14,7 +14,7 @@ Section NondecreasingSequence.
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. *)
+ such that [n1 <= n2 < size [xs]] condition [[xs][n1] <= [xs][n2]] holds. *)
Definition nondecreasing_sequence (xs : seq nat) :=
forall n1 n2,
n1 <= n2 < size xs ->
@@ -49,29 +49,29 @@ Section NondecreasingSequence.
Proof.
clear; intros ? ? ?.
have EX : exists k, b - a <= k.
- { exists (b-a); now simpl. } destruct EX as [k BO].
+ { by exists (b-a). } destruct EX as [k BO].
revert a b P BO; induction k.
{ move => a b P BO n1 n2.
move: BO; rewrite leqn0; move => /eqP BO.
rewrite /index_iota BO; simpl.
- by move => /andP [_ F].
+ 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.
- rewrite /index_iota EQ //= in LT.
+ 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.
- rewrite index_iota_lt_step // //= PA //= in LT.
+ by rewrite index_iota_lt_step // //= PA //= in LT.
* apply IHk; try ssrlia.
apply/andP; split; first by done.
- rewrite index_iota_lt_step // //= PA //= in LT.
+ by rewrite index_iota_lt_step // //= PA //= in LT.
+ apply IHk; try ssrlia.
apply/andP; split; first by done.
- rewrite index_iota_lt_step // //= PA //= in LT.
- }
+ by rewrite index_iota_lt_step // //= PA //= in LT.
+ }
Qed.
(** We prove that any increasing sequence is also a non-decreasing
@@ -81,8 +81,7 @@ Section NondecreasingSequence.
increasing_sequence xs ->
nondecreasing_sequence xs.
Proof.
- intros ? INC.
- intros n1 n2.
+ 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.
@@ -111,7 +110,7 @@ Section NondecreasingSequence.
feed ND.
{ apply/andP; split; first by done.
by simpl; rewrite ltnS index_mem. }
- by simpl in ND; rewrite NTH in ND.
+ by simpl in ND; rewrite NTH in ND.
Qed.
(** If [x1::x2::xs] is a non-decreasing sequence, then either
@@ -124,7 +123,7 @@ Section NondecreasingSequence.
intros ? ? ? ND.
destruct (ltngtP x1 x2) as [LT | GT | EQ]; auto.
move_neq_down GT.
- by specialize (ND 0 1); apply ND.
+ by specialize (ND 0 1); apply ND.
Qed.
(** We prove that if [x::xs] is a non-decreasing sequence,
@@ -153,14 +152,13 @@ Section NondecreasingSequence.
nondecreasing_sequence (x :: xs).
Proof.
intros x xs MIN ND [ |n1] [ | n2]; try done.
- - move => /andP [_ S]; simpl.
+ - 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.
+ simpl in *; rewrite ltnS in S.
+ by apply leq_ltn_trans with n2.
+ apply ND; apply/andP; split; auto.
- - simpl; rewrite !ltnS.
- by apply ND.
+ - by rewrite //= !ltnS; apply ND.
Qed.
(** We prove that if [x::xs] is a non-decreasing sequence,
@@ -172,13 +170,12 @@ Section NondecreasingSequence.
Proof.
intros ? ? ND.
move => [ | n1] [ | n2] /andP [LT1 LT2]; try done.
- - specialize (ND 0 n2); simpl in ND.
- apply ND.
- by simpl in LT2; rewrite ltnS in LT2.
+ - specialize (ND 0 n2).
+ by apply ND; rewrite //= ltnS in LT2.
- apply ND.
apply/andP; split.
+ by rewrite ltnS in LT1.
- + by simpl in LT2; rewrite ltnS in LT2.
+ + by rewrite //= ltnS in LT2.
Qed.
(** We prove that if [x::xs] is a non-decreasing sequence,
@@ -193,11 +190,9 @@ Section NondecreasingSequence.
specialize (ND 0 (index y xs).+1).
move: (IN) => IDL; rewrite -index_mem in IDL.
feed ND.
- { apply/andP; split; first by done.
- by simpl; rewrite ltnS.
- }
+ { by apply/andP; split; last rewrite //= ltnS. }
eapply leq_trans; first by apply ND.
- by simpl; rewrite IDX.
+ by rewrite //= IDX.
Qed.
(** We also prove a similar lemma for strict minimum. *)
@@ -211,7 +206,7 @@ Section NondecreasingSequence.
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.
+ by apply nondecreasing_sequence_cons_double.
Qed.
(** Next, we prove that no element can lie strictly between two
@@ -230,32 +225,34 @@ Section NondecreasingSequence.
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.
- rewrite Bt in H; by move: H => /andP [_ T]. }
+ 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.
+ 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; [ apply ltnW | done].
+ - 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.
+ 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]]. *)
+ (** 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:
forall (xs : seq nat) (x : nat),
2 <= size xs ->
@@ -272,17 +269,17 @@ Section NondecreasingSequence.
induction n; intros.
{ by destruct xs; [ | destruct xs; [ | destruct xs; [exists 0 | ] ] ]. }
{ destruct xs; [ | destruct xs; [ | ]]; try by done.
- destruct xs.
- { by exists 0; simpl in *. }
+ destruct xs; first by (exists 0).
destruct (leqP n1 x) as [NEQ|NEQ]; last first.
- { exists 0; split; auto. move: LAST => /andP [LAST _]. by apply/andP; split. }
+ { exists 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 /last0 !last_cons.
}
{ by rewrite -(ltn_add2r 1) !addn1. }
move: IHn => [idx [SI /andP [G L]]].
@@ -300,26 +297,27 @@ Section NondecreasingSequence.
(x \in xs) ->
x <= last0 xs.
Proof.
- clear; intros ? ? STR IN.
+ intros ? ? STR IN.
have NEQ: forall x y, x = y \/ x != y.
- { clear. intros.
+ { 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.
- rewrite -addn1 in SIZE.
- apply STR; apply/andP.
- have POS: 0 < size xs.
- { by apply leq_trans with (id + 1); [rewrite addn1| done]. }
- split.
- - by rewrite -(leq_add2r 1) !addn1 prednK // -addn1.
- - by rewrite prednK.
+ { 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.
@@ -327,7 +325,7 @@ Section 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:
forall {X : eqType} (x : X) (xs : seq X),
@@ -335,7 +333,7 @@ Section NondecreasingSequence.
Proof.
intros; rewrite {2 3}[cons] lock //= -lock.
rewrite in_cons eq_refl; simpl.
- by destruct (x \in xs).
+ by destruct (x \in xs).
Qed.
(** For non-decreasing sequences we show that the fact that
@@ -355,8 +353,7 @@ Section NondecreasingSequence.
apply/eqP; rewrite eqbF_neg.
apply nondecreasing_sequence_cons in H0.
apply/negP; intros ?; eauto 2.
- eapply nondecreasing_sequence_cons_min in H0; eauto 2.
- by move_neq_down H.
+ by eapply nondecreasing_sequence_cons_min in H0; eauto 2; ssrlia.
Qed.
(** Next we show that function [undup] doesn't change
@@ -372,10 +369,10 @@ Section NondecreasingSequence.
+ subst; rename x2 into x.
rewrite nodup_sort_2cons_eq IHxs.
rewrite [in X in _ = X]last0_cons //.
- eapply nondecreasing_sequence_cons; eauto 2.
+ 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.
+ by intros ?; apply undup_nil in H.
Qed.
(** Non-decreasing sequence remains non-decreasing after application of [undup]. *)
@@ -386,20 +383,19 @@ Section NondecreasingSequence.
Proof.
intros ?.
have EX: exists len, size xs <= len.
- { exists (size xs); now simpl. } destruct EX as [n BO].
+ { by exists (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]]; try done.
- intros Size NonDec.
+ - 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 //.
+ + 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.
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.
+ by apply IHn; eauto using nondecreasing_sequence_cons.
Qed.
(** We also show that the penultimate element of a sequence [undup xs]
@@ -411,34 +407,31 @@ Section NondecreasingSequence.
Proof.
Opaque undup.
intros ?.
- have EX: exists len, size xs <= len.
- { exists (size xs); now simpl. } destruct EX as [n BO].
+ have EX: exists len, size xs <= len by (exists (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]]; try done.
- intros Size NonDec.
+ - 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 //.
+ 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.
+ 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.
- Transparent undup.
Qed.
End Undup.
-
(** * Properties of Distances *)
(** In this section we prove a few lemmas about function [distances]. *)
Section Distances.
@@ -448,7 +441,7 @@ Section NondecreasingSequence.
Lemma distances_unfold_2cons:
forall x0 x1 xs,
distances (x0::x1::xs) = (x1 - x0) :: distances (x1::xs).
- Proof. by intros; unfold distances; simpl; rewrite drop0. Qed.
+ 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
@@ -459,8 +452,9 @@ Section NondecreasingSequence.
distances (xs ++ [:: a; b])
= distances (xs ++ [:: a]) ++ [:: b - a].
Proof.
- clear; intros.
- have EX: exists n, size xs <= n. exists (size xs); by done. destruct EX as [n LE].
+ intros.
+ have EX: exists n, size xs <= n by (exists (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.
@@ -468,21 +462,21 @@ Section NondecreasingSequence.
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]).
- { by simpl; rewrite distances_unfold_2cons. }
- by done.
+ 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 ([distances(xs ++ [:: x])]) can
- be rewritten as [distances xs ++ [:: x - last0 xs]]. *)
+ in the [distances] function (i.e., [distances(xs ++ [:: x])])
+ can be rewritten as [distances xs ++ [:: x - last0 xs]]. *)
Lemma distances_unfold_1app_last:
forall x xs,
size xs >= 1 ->
distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs].
Proof.
- clear. intros x xs POS.
- have EX: exists n, size xs <= n. exists (size xs); by done. destruct EX as [n LE].
+ intros x xs POS.
+ have EX: exists n, size xs <= n by (exists (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.
@@ -499,131 +493,104 @@ Section NondecreasingSequence.
Qed.
(** We prove that the difference between any two neighboring elements is
- bounded by the max element of the distances-sequence. *)
+ bounded by the max element of the distances-sequence. *)
Lemma distance_between_neighboring_elements_le_max_distance_in_seq:
forall (xs : seq nat) (n : nat),
xs[|n.+1|] - xs[|n|] <= max0 (distances xs).
Proof.
- clear; intros xs id.
+ intros xs id.
apply leq_trans with (distances xs [| id |]).
rewrite leq_eqVlt; apply/orP; left; apply/eqP.
- have EX: exists n, size xs <= n. { by exists (size xs). } move: EX => [n LE].
- generalize dependent xs; generalize dependent id.
- induction n.
- { intros.
- move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst.
- by rewrite !nth_default.
+ have EX: exists n, size xs <= n by (exists (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.
}
- { intros.
- move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT]; last first.
+ { 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 Fact: distances [:: n0, n1 & xs] = (n1 - n0) :: distances [:: n1 & xs].
- { by rewrite /distances; simpl; rewrite drop0. }
- rewrite Fact; clear Fact.
+ have ->: distances [:: n0, n1 & xs] = (n1 - n0) :: distances [:: n1 & xs].
+ { by rewrite /distances //= drop0. }
destruct id; first by done.
- simpl.
- rewrite -IHn. simpl. by done.
- by move: EQ => /eqP; simpl; rewrite eqSS; move => /eqP EQ; rewrite -EQ.
+ rewrite //= -IHn //=.
+ by move: EQ => /eqP; rewrite //= eqSS => /eqP EQ; rewrite -EQ.
}
- { have Lem: forall x xs, x \in xs -> x <= max0 xs.
- { clear; intros.
- generalize dependent x.
- induction xs; first by done.
- intros ? IN; rewrite max0_cons leq_max; apply/orP.
+ { have Lem: forall 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 //.
+ - by rewrite nth_default.
+ - apply Lem; rewrite mem_nth //.
move: SIZE => /negP /negP.
- by rewrite ltnNge.
- }
+ 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]. *)
+ 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:
forall (xs : seq nat) (n : nat),
(distances xs)[|n|] = xs[|n.+1|] - xs[|n|].
Proof.
intros xs.
- have EX: exists len, size xs <= len.
- { by exists (size xs). } move: EX => [len LE].
- generalize dependent xs.
+ have EX: exists len, size xs <= len by (exists (size xs)).
+ move: EX => [len LE]; move: xs LE.
induction len; intros.
- { move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst.
- unfold distances. simpl.
- by destruct n; simpl.
- }
+ { 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].
- { by destruct n as [ | [ | ]]. }
+ destruct xs as [ | x2 xs]; first by destruct n as [ | [ | ]].
destruct n; first by done.
- have F: distances [:: x1, x2 & xs] [|n.+1|] = distances [::x2 & xs] [| n |].
- { have EQ': distances [:: x1, x2 & xs] = (x2 - x1) :: distances [::x2 & xs].
- { by unfold distances; simpl; rewrite drop0. }
- by rewrite EQ'.
+ 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 F2: [:: x1, x2 & xs] [|n.+2|] - [:: x1, x2 & xs] [|n.+1|] = [:: x2 & xs] [|n.+1|] - [:: x2 & xs] [|n|]; first by done.
- rewrite F F2.
+ have ->: [:: x1, x2 & xs] [|n.+2|] - [:: x1, x2 & xs] [|n.+1|] = [:: x2 & xs] [|n.+1|] - [:: x2 & xs] [|n|] by done.
apply IHlen.
- move: EQ => /eqP; simpl; rewrite eqSS; move => /eqP EQ.
- by rewrite -EQ.
+ 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. *)
+ than the size of the original sequence. *)
Lemma size_of_seq_of_distances:
forall (xs : seq nat),
2 <= size xs ->
size xs = size (distances xs) + 1.
Proof.
- clear.
intros xs.
- have EX: exists len, size xs <= len.
- { exists (size xs). by done. }
- move: EX => [len LE].
- generalize dependent xs.
- induction len.
- { intros.
- move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst.
- by done.
+ have EX: exists len, size xs <= len by (exists (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/eqP; rewrite eqn_add2r; apply/eqP.
+ apply IHlen; last by done.
+ by move: EQ => /eqP; rewrite //= eqSS => /eqP <-.
}
- intros ? ? SIZE.
- move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last first.
- { 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 F1: size [:: x1, x2, x3 & xs] = size [:: x2, x3 & xs] + 1.
- { by rewrite addn1. }
- have F2: size (distances [:: x1, x2, x3 & xs]) = size (distances [:: x2, x3 & xs]) + 1.
- { by rewrite addn1. }
- rewrite F1 F2; clear F1 F2.
- apply/eqP; rewrite eqn_add2r; apply/eqP.
- apply IHlen; last by done.
- move: EQ => /eqP. simpl. rewrite eqSS; move => /eqP EQ.
- by rewrite -EQ.
Qed.
(** We prove that [index_iota 0 n] produces a sequence of numbers
- with which are always one unit apart each other. *)
+ which are always one unit apart each other. *)
Lemma distances_of_iota_ε:
forall n x, x \in distances (index_iota 0 n) -> x = ε.
Proof.
- clear; intros n x IN.
- induction n.
+ intros n x IN; induction n.
- by unfold index_iota, distances in IN.
- destruct n; first by unfold distances, index_iota in IN.
- rewrite -addn1 /index_iota subn0 iota_add in IN .
+ rewrite -addn1 /index_iota subn0 iota_add in IN.
rewrite add0n in IN.
rewrite distances_unfold_1app_last in IN; last by rewrite size_iota.
move: IN; rewrite mem_cat; move => /orP [IN|IN].
@@ -647,8 +614,8 @@ Section NondecreasingSequence.
(exists x y, x \in xs /\ y \in xs /\ x <> y) ->
0 < max0 (distances xs).
Proof.
- move => xs SIZE SMI. move: SMI => [x [y [INx [INy NEQ]]]].
- move: INx INy => /nthP INx /nthP INy. specialize (INx 0); specialize (INy 0).
+ 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: forall (x y indx indy : nat),
indx < size xs -> indy < size xs ->
@@ -659,8 +626,8 @@ Section NondecreasingSequence.
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: exists Δ, indy = indx + Δ. exists (indy - indx); ssrlia. move: EQ => [Δ EQ]; subst indy.
+ by apply SIZE; apply/andP. }
+ have EQ: exists Δ, indy = indx + Δ; [by exists (indy - indx); ssrlia | move: EQ => [Δ EQ]; subst indy].
have F: exists 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 ssrlia.
@@ -671,56 +638,47 @@ Section NondecreasingSequence.
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. }
+ by rewrite nth_default ?addnS. }
move: ALT => [/eqP EQ|LT'].
- edestruct (IHΔ) as [ind [B UP]]; eauto 5 using addn1, leq_add2l.
exists ind; split; last by done.
move: B => /andP [B1 B2]; apply/andP; split; first by done.
- by rewrite addnS ltnS ltnW.
+ by rewrite addnS ltnS ltnW.
- exists (indx + Δ); split; last by rewrite -addnS.
- by apply/andP; split; [rewrite leq_addr | 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].
- - eapply L with (indx := indx) (x := x) (y := y); eauto.
- - eapply L with (indx := indy) (indy := indx) (x := y) (y := x); eauto.
+ - 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]]. *)
+ (** 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:
forall (xs : seq nat),
nondecreasing_sequence xs ->
last0 xs - last0 (distances xs) = xs [| (size xs).-2 |].
Proof.
- clear.
+ unfold nondecreasing_sequence in *.
intros xs SIS.
- destruct xs as [ | x1 xs]. by done.
- destruct xs as [ | x2 xs]. by rewrite subn0.
- rewrite {2}/last0 -[in X in _ - X]nth_last function_of_distances_is_correct prednK;
- last by done.
+ 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.
- rewrite size_of_seq_of_distances; last by done.
- rewrite !addn1.
- rewrite -pred_Sn.
- rewrite subKn; first by done.
- unfold X.
- unfold nondecreasing_sequence in *.
- apply SIS.
- apply/andP; split.
- simpl; by done.
- rewrite [in X in _ < X]size_of_seq_of_distances; last by done.
- by rewrite addn1.
+ 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]. Note that all elements of [xs] are positive.
- Thus they all lie within the interval [0, last xs]. *)
+ (** 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:
forall (xs : seq nat),
nondecreasing_sequence xs ->
@@ -739,11 +697,10 @@ Section NondecreasingSequence.
+ by apply H; rewrite in_cons; apply/orP; left.
+ by apply IHxs; intros; apply H; rewrite in_cons; apply/orP; right.
}
- apply F; clear F; intros d IN.
+ 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.
- rewrite leq_sub //.
+ 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.
@@ -761,7 +718,7 @@ Section NondecreasingSequence.
rewrite -(ltn_add2r 1) addn1 -size_of_seq_of_distances in IN; last by done.
destruct idx; first by move: EQ; rewrite /first0 -nth0; move => /eqP.
apply/andP; split; first by done.
- by apply ltn_trans with idx.+2.
+ by apply ltn_trans with idx.+2.
}
Qed.
@@ -775,23 +732,20 @@ Section NondecreasingSequence.
distances [seq Ï <- index_iota 0 k.+1 | Ï \in xs] = [seq x <- distances xs | 0 < x].
Proof.
intros xs.
- have EX: exists len, size xs <= len.
- { exists (size xs); now simpl. } 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.
+ have EX: exists len, size xs <= len by (exists (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.
}
- { intros ? Len k Bound NonDec.
- destruct xs as [ |x1 [ |x2 xs]].
+ { 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: forall y : nat, y \in x2 :: xs -> x1 <= y. by apply nondecreasing_sequence_cons_min.
have M2: forall x : nat, x \in x2 :: xs -> x <= k. by intros; apply Bound; rewrite in_cons; apply/orP; right.
- have M3: forall y : nat, y \in xs -> x2 <= y
- by apply nondecreasing_sequence_cons in NonDec; apply nondecreasing_sequence_cons_min.
+ have M3: forall 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)))))
@@ -806,7 +760,7 @@ Section NondecreasingSequence.
{ 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.
- rewrite {1}range_iota_filter_step //. rewrite distances_unfold_2cons. rewrite {1}range_iota_filter_step //.
+ by rewrite {1}range_iota_filter_step // distances_unfold_2cons {1}range_iota_filter_step //.
}
Qed.
@@ -824,8 +778,7 @@ Section NondecreasingSequence.
have EX: exists len, size xs <= len.
{ exists (size xs); now simpl. } destruct EX as [n BO].
revert xs NonDec BO; induction n.
- - intros xs _; rewrite leqn0 size_eq0; move => /eqP EQ; subst xs.
- by rewrite filter_pred0.
+ - 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].
@@ -833,23 +786,23 @@ Section NondecreasingSequence.
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].
+ 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.
+ by rewrite in_cons eq_refl.
}
rewrite rem_lt_id //; last by apply nondecreasing_sequence_cons_smin.
- rewrite IHn //; eauto using nondecreasing_sequence_cons.
+ 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]. *)
+ (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:
forall (xs ys : seq nat),
first0 xs <= first0 ys ->
@@ -864,13 +817,11 @@ Section NondecreasingSequence.
intros xs ys.
have EX: exists len, size xs <= len /\ size ys <= len.
{ exists (maxn (size xs) (size ys)).
- by split; rewrite leq_max; apply/orP; [left | right].
+ by split; rewrite leq_max; apply/orP; [left | right].
} move: EX => [len [LE1 LE2]].
generalize dependent xs; generalize dependent ys.
induction len.
- { intros; move: LE1 LE2; rewrite !leqn0 !size_eq0; move => /eqP E1 /eqP E2.
- by subst.
- }
+ { 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.
@@ -897,7 +848,7 @@ Section NondecreasingSequence.
apply (STRys m1.+1 m2.+1); apply/andP; split.
+ by rewrite ltnS.
+ by rewrite -(ltn_add2r 1) !addn1 in B2.
- - intros. specialize (LE n0.+1). simpl in LE. by done.
+ - by intros; specialize (LE n0.+1); simpl in LE.
}
Qed.
--
GitLab