Skip to content
Snippets Groups Projects
Commit fcde91ef authored by Sergey Bozhko's avatar Sergey Bozhko :eyes: Committed by Björn Brandenburg
Browse files

clean up in util/nondecreasing.v

parent 1b778299
No related branches found
No related tags found
1 merge request!148clean up in util/nondecreasing.v
Pipeline #53956 passed with warnings
Stage: build
Stage: process
Hide whitespace changes
Inline Side-by-side
Showing
with 169 additions and 218 deletions
util/nondecreasing.v
+ 169
− 218
View file @ fcde91ef
......@@ -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.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment