Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.util.epsilon.
Require Export prosa.util.nat.[Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ]
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 ).
(** In this section we provide the notion of a non-decreasing sequence. *)
Section Definitions .
(** We say that a sequence [xs] is non-decreasing iff for any two indices [n1] and [n2]
such that [n1 <= n2 < size [xs]] condition [[xs][n1] <= [xs][n2]] holds. *)
Definition nondecreasing_sequence (xs : seq nat) :=
forall n1 n2 ,
n1 <= n2 < size xs ->
xs[|n1|] <= xs[|n2|].
(** Similarly, we define an increasing sequence. *)
Definition increasing_sequence (xs : seq nat) :=
forall n1 n2 ,
n1 < n2 < size xs ->
xs[|n1|] < xs[|n2|].
(** For a non-decreasing sequence we define the notion of
distances between neighboring elements of the sequence. *)
(** Example:
Consider the following sequence of natural numbers: [xs] = [:: 1; 10; 10; 17; 20; 41].
Then [drop 1 xs] is equal to [:: 10; 10; 17; 20; 41].
Then [zip xs (drop 1 xs)] is equal to [:: (1,10); (10,10); (10,17); (17,20); (20,41)]
And after the mapping [map (fun '(x1, x2) => x2 - x1)] we end up with [:: 9; 0; 7; 3; 21]. *)
Definition distances (xs : seq nat) :=
map (fun '(x1, x2) => x2 - x1) (zip xs (drop 1 xs)).
End Definitions .
(** * Properties of Increasing Sequence *)
(** In this section we prove a few lemmas about increasing sequences. *)
Section IncreasingSequence .
(** Note that a filtered iota sequence is an increasing sequence. *)
Lemma iota_is_increasing_sequence :
forall a b P ,
increasing_sequence [seq x <- index_iota a b | P x].forall (a b : nat) (P : nat -> bool),
increasing_sequence [seq x <- index_iota a b | P x]
Proof .forall (a b : nat) (P : nat -> bool),
increasing_sequence [seq x <- index_iota a b | P x]
clear => a b P.a, b : nat P : nat -> bool
increasing_sequence [seq x <- index_iota a b | P x]
have EX : exists k , b - a <= k.a, b : nat P : nat -> bool
exists k : nat, b - a <= k
{ a, b : nat P : nat -> bool
exists k : nat, b - a <= k
by exists (b -a). } a, b : nat P : nat -> bool EX : exists k : nat, b - a <= k
increasing_sequence [seq x <- index_iota a b | P x]
destruct EX as [k BO].a, b : nat P : nat -> bool k : nat BO : b - a <= k
increasing_sequence [seq x <- index_iota a b | P x]
revert a b P BO; elim : k => [ |k IHk].forall (a b : nat) (P : nat -> bool),
b - a <= 0 ->
increasing_sequence [seq x <- index_iota a b | P x]
{ forall (a b : nat) (P : nat -> bool),
b - a <= 0 ->
increasing_sequence [seq x <- index_iota a b | P x]
move => a b P BO n1 n2.a, b : nat P : nat -> bool BO : b - a <= 0 n1, n2 : nat
n1 < n2 < size [seq x <- index_iota a b | P x] ->
[seq x <- index_iota a b | P x] [|n1|] <
[seq x <- index_iota a b | P x] [|n2|]
move : BO; rewrite leqn0; move => /eqP BO.a, b : nat P : nat -> bool n1, n2 : nat BO : b - a = 0
n1 < n2 < size [seq x <- index_iota a b | P x] ->
[seq x <- index_iota a b | P x] [|n1|] <
[seq x <- index_iota a b | P x] [|n2|]
rewrite /index_iota BO; simpl .a, b : nat P : nat -> bool n1, n2 : nat BO : b - a = 0
n1 < n2 < 0 -> [::] [|n1|] < [::] [|n2|]
by move => /andP [_ F].
} k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]
forall (a b : nat) (P : nat -> bool),
b - a <= k.+1 ->
increasing_sequence [seq x <- index_iota a b | P x]
{ k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]
forall (a b : nat) (P : nat -> bool),
b - a <= k.+1 ->
increasing_sequence [seq x <- index_iota a b | P x]
move => a b P BO n1 n2 /andP [GE LT].k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x]
[seq x <- index_iota a b | P x] [|n1|] <
[seq x <- index_iota a b | P x] [|n2|]
case : (leqP b a) => [N|N].k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] N : b <= a
[seq x <- index_iota a b | P x] [|n1|] <
[seq x <- index_iota a b | P x] [|n2|]
- k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] N : b <= a
[seq x <- index_iota a b | P x] [|n1|] <
[seq x <- index_iota a b | P x] [|n2|]
move : N; rewrite -subn_eq0; move => /eqP EQ.k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] EQ : b - a = 0
[seq x <- index_iota a b | P x] [|n1|] <
[seq x <- index_iota a b | P x] [|n2|]
by rewrite /index_iota EQ //= in LT.
- k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] N : a < b
[seq x <- index_iota a b | P x] [|n1|] <
[seq x <- index_iota a b | P x] [|n2|]
rewrite index_iota_lt_step; last by done .k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] N : a < b
[seq x <- a :: index_iota a.+1 b | P x] [|n1|] <
[seq x <- a :: index_iota a.+1 b | P x] [|n2|]
simpl ; destruct (P a) eqn :PA.k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = true
(a :: [seq x <- index_iota a.+1 b | P x]) [|n1|] <
(a :: [seq x <- index_iota a.+1 b | P x]) [|n2|]
+ k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = true
(a :: [seq x <- index_iota a.+1 b | P x]) [|n1|] <
(a :: [seq x <- index_iota a.+1 b | P x]) [|n2|]
destruct n1, n2; try done ; simpl .k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n2 : nat GE : 0 < n2.+1 LT : n2.+1 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = true
a < [seq x <- index_iota a.+1 b | P x] [|n2|]
* k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n2 : nat GE : 0 < n2.+1 LT : n2.+1 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = true
a < [seq x <- index_iota a.+1 b | P x] [|n2|]
apply iota_filter_gt; first by done .k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n2 : nat GE : 0 < n2.+1 LT : n2.+1 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = true
n2 < size [seq x <- index_iota a.+1 b | P x]
by rewrite index_iota_lt_step // //= PA //= in LT.
* k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1.+1 < n2.+1 LT : n2.+1 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = true
[seq x <- index_iota a.+1 b | P x] [|n1|] <
[seq x <- index_iota a.+1 b | P x] [|n2|]
apply IHk; try lia .k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1.+1 < n2.+1 LT : n2.+1 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = true
n1 < n2 < size [seq x <- index_iota a.+1 b | P x]
apply /andP; split ; first by done .k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1.+1 < n2.+1 LT : n2.+1 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = true
n2 < size [seq x <- index_iota a.+1 b | P x]
by rewrite index_iota_lt_step // //= PA //= in LT.
+ k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = false
[seq x <- index_iota a.+1 b | P x] [|n1|] <
[seq x <- index_iota a.+1 b | P x] [|n2|]
apply IHk; try lia .k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = false
n1 < n2 < size [seq x <- index_iota a.+1 b | P x]
apply /andP; split ; first by done .k : nat IHk : forall (a b : nat) (P : nat -> bool),
b - a <= k -> increasing_sequence [seq x <- index_iota a b | P x]a, b : nat P : nat -> bool BO : b - a <= k.+1 n1, n2 : nat GE : n1 < n2 LT : n2 < size [seq x <- index_iota a b | P x] N : a < b PA : P a = false
n2 < size [seq x <- index_iota a.+1 b | P x]
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 :
forall xs ,
increasing_sequence xs ->
nondecreasing_sequence xs.forall xs : seq nat,
increasing_sequence xs -> nondecreasing_sequence xs
Proof .forall xs : seq nat,
increasing_sequence xs -> nondecreasing_sequence xs
intros ? INC n1 n2.xs : seq nat INC : increasing_sequence xs n1, n2 : nat
n1 <= n2 < size xs -> xs [|n1|] <= xs [|n2|]
move => /andP; rewrite leq_eqVlt; move => [/orP [/eqP EQ| LT1] LT2].xs : seq nat INC : increasing_sequence xs n1, n2 : nat EQ : n1 = n2 LT2 : n2 < size xs
xs [|n1|] <= xs [|n2|]
- xs : seq nat INC : increasing_sequence xs n1, n2 : nat EQ : n1 = n2 LT2 : n2 < size xs
xs [|n1|] <= xs [|n2|]
by subst .
- xs : seq nat INC : increasing_sequence xs n1, n2 : nat LT1 : n1 < n2 LT2 : n2 < size xs
xs [|n1|] <= xs [|n2|]
by apply ltnW; apply INC; apply /andP; split .
Qed .
End IncreasingSequence .
(** * Properties of Non-Decreasing Sequence *)
(** In this section we prove a few lemmas about non-decreasing sequences. *)
Section NonDecreasingSequence .
(** First we prove that if [0 ∈ xs], then
[0] is the first element of [xs]. *)
Lemma nondec_seq_zero_first :
forall xs ,
(0 \in xs) ->
nondecreasing_sequence xs ->
first0 xs = 0 .forall
xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality,
0 \in xs -> nondecreasing_sequence xs -> first0 xs = 0
Proof .forall
xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality,
0 \in xs -> nondecreasing_sequence xs -> first0 xs = 0
move => xs.xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality
0 \in xs -> nondecreasing_sequence xs -> first0 xs = 0
destruct xs as [ | x xs]; first by done .x : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality
0 \in x :: xs ->
nondecreasing_sequence (x :: xs) ->
first0 (x :: xs) = 0
destruct x as [ | x]; first by done .x : nat xs : seq Datatypes_nat__canonical__eqtype_Equality
0 \in x.+1 :: xs ->
nondecreasing_sequence (x.+1 :: xs) ->
first0 (x.+1 :: xs) = 0
rewrite in_cons; move => /orP [/eqP EQ | IN] ND; first by done .x : nat xs : seq Datatypes_nat__canonical__eqtype_Equality IN : 0 \in xsND : nondecreasing_sequence (x.+1 :: xs)
first0 (x.+1 :: xs) = 0
exfalso .x : nat xs : seq Datatypes_nat__canonical__eqtype_Equality IN : 0 \in xsND : nondecreasing_sequence (x.+1 :: xs)
False
have NTH := nth_index 0 IN.x : nat xs : seq Datatypes_nat__canonical__eqtype_Equality IN : 0 \in xsND : nondecreasing_sequence (x.+1 :: xs) NTH : xs [|index 0 xs|] = 0
False
specialize (ND 0 (index 0 xs).+1 ).x : nat xs : seq Datatypes_nat__canonical__eqtype_Equality IN : 0 \in xsND : 0 <= (index 0 xs).+1 < size (x.+1 :: xs) ->
(x.+1 :: xs) [|0 |] <=
(x.+1 :: xs) [|(index 0 xs).+1 |]NTH : xs [|index 0 xs|] = 0
False
feed ND. x : nat xs : seq Datatypes_nat__canonical__eqtype_Equality IN : 0 \in xsND : 0 <= (index 0 xs).+1 < size (x.+1 :: xs) ->
(x.+1 :: xs) [|0 |] <=
(x.+1 :: xs) [|(index 0 xs).+1 |]NTH : xs [|index 0 xs|] = 0
0 <= (index 0 xs).+1 < size (x.+1 :: xs)
{ x : nat xs : seq Datatypes_nat__canonical__eqtype_Equality IN : 0 \in xsND : 0 <= (index 0 xs).+1 < size (x.+1 :: xs) ->
(x.+1 :: xs) [|0 |] <=
(x.+1 :: xs) [|(index 0 xs).+1 |]NTH : xs [|index 0 xs|] = 0
0 <= (index 0 xs).+1 < size (x.+1 :: xs)
apply /andP; split ; first by done .x : nat xs : seq Datatypes_nat__canonical__eqtype_Equality IN : 0 \in xsND : 0 <= (index 0 xs).+1 < size (x.+1 :: xs) ->
(x.+1 :: xs) [|0 |] <=
(x.+1 :: xs) [|(index 0 xs).+1 |]NTH : xs [|index 0 xs|] = 0
(index 0 xs).+1 < size (x.+1 :: xs)
by simpl ; rewrite ltnS index_mem. } x : nat xs : seq Datatypes_nat__canonical__eqtype_Equality IN : 0 \in xsND : (x.+1 :: xs) [|0 |] <=
(x.+1 :: xs) [|(index 0 xs).+1 |] NTH : xs [|index 0 xs|] = 0
False
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 :
forall x1 x2 xs ,
nondecreasing_sequence (x1 :: x2 :: xs) ->
x1 = x2 \/ x1 < x2.forall (x1 x2 : nat) (xs : seq nat),
nondecreasing_sequence [:: x1, x2 & xs] ->
x1 = x2 \/ x1 < x2
Proof .forall (x1 x2 : nat) (xs : seq nat),
nondecreasing_sequence [:: x1, x2 & xs] ->
x1 = x2 \/ x1 < x2
move => x1 x2 xs ND.x1, x2 : nat xs : seq nat ND : nondecreasing_sequence [:: x1, x2 & xs]
x1 = x2 \/ x1 < x2
destruct (ltngtP x1 x2) as [LT | GT | EQ]; auto .x1, x2 : nat xs : seq nat ND : nondecreasing_sequence [:: x1, x2 & xs] GT : x2 < x1
x1 = x2 \/ false
move_neq_down GT. x1, x2 : nat xs : seq nat ND : nondecreasing_sequence [:: x1, x2 & xs]
x1 <= x2
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 :
forall x xs ,
nondecreasing_sequence (x :: xs) ->
nondecreasing_sequence xs.forall (x : nat) (xs : seq nat),
nondecreasing_sequence (x :: xs) ->
nondecreasing_sequence xs
Proof .forall (x : nat) (xs : seq nat),
nondecreasing_sequence (x :: xs) ->
nondecreasing_sequence xs
intros ? ? ND.x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs)
nondecreasing_sequence xs
move => n1 n2 /andP [LT1 LT2].x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) n1, n2 : nat LT1 : n1 <= n2 LT2 : n2 < size xs
xs [|n1|] <= xs [|n2|]
specialize (ND n1.+1 n2.+1 ).x : nat xs : seq nat n1, n2 : nat ND : n1 < n2.+1 < size (x :: xs) ->
(x :: xs) [|n1.+1 |] <= (x :: xs) [|n2.+1 |] LT1 : n1 <= n2 LT2 : n2 < size xs
xs [|n1|] <= xs [|n2|]
apply ND.x : nat xs : seq nat n1, n2 : nat ND : n1 < n2.+1 < size (x :: xs) ->
(x :: xs) [|n1.+1 |] <= (x :: xs) [|n2.+1 |] LT1 : n1 <= n2 LT2 : n2 < size xs
n1 < n2.+1 < size (x :: xs)
apply /andP; split .x : nat xs : seq nat n1, n2 : nat ND : n1 < n2.+1 < size (x :: xs) ->
(x :: xs) [|n1.+1 |] <= (x :: xs) [|n2.+1 |] LT1 : n1 <= n2 LT2 : n2 < size xs
n1 < n2.+1
- x : nat xs : seq nat n1, n2 : nat ND : n1 < n2.+1 < size (x :: xs) ->
(x :: xs) [|n1.+1 |] <= (x :: xs) [|n2.+1 |] LT1 : n1 <= n2 LT2 : n2 < size xs
n1 < n2.+1
by rewrite ltnS.
- x : nat xs : seq nat n1, n2 : nat ND : n1 < n2.+1 < size (x :: xs) ->
(x :: xs) [|n1.+1 |] <= (x :: xs) [|n2.+1 |] LT1 : n1 <= n2 LT2 : n2 < size xs
n2.+1 < size (x :: xs)
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 :
forall x xs ,
(forall y , y \in xs -> x <= y) ->
nondecreasing_sequence xs ->
nondecreasing_sequence (x :: xs).forall (x : nat)
(xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality),
(forall y : nat, y \in xs -> x <= y) ->
nondecreasing_sequence xs ->
nondecreasing_sequence (x :: xs)
Proof .forall (x : nat)
(xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality),
(forall y : nat, y \in xs -> x <= y) ->
nondecreasing_sequence xs ->
nondecreasing_sequence (x :: xs)
move => x xs MIN ND [ |n1] [ | n2] //.x : nat xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality MIN : forall y : nat, y \in xs -> x <= yND : nondecreasing_sequence xs n2 : nat
0 <= n2.+1 < size (x :: xs) ->
(x :: xs) [|0 |] <= (x :: xs) [|n2.+1 |]
move => /andP [_ S] //=.x : nat xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality MIN : forall y : nat, y \in xs -> x <= yND : nondecreasing_sequence xs n2 : nat S : n2.+1 < size (x :: xs)
x <= xs [|n2|]
apply leq_trans with (xs [| 0 |]).x : nat xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality MIN : forall y : nat, y \in xs -> x <= yND : nondecreasing_sequence xs n2 : nat S : n2.+1 < size (x :: xs)
x <= xs [|0 |]
- x : nat xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality MIN : forall y : nat, y \in xs -> x <= yND : nondecreasing_sequence xs n2 : nat S : n2.+1 < size (x :: xs)
x <= xs [|0 |]
apply MIN; apply mem_nth.x : nat xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality MIN : forall y : nat, y \in xs -> x <= yND : nondecreasing_sequence xs n2 : nat S : n2.+1 < size (x :: xs)
0 < size xs
simpl in *; rewrite ltnS in S.x : nat xs : seq nat MIN : forall y : nat, y \in xs -> x <= yND : nondecreasing_sequence xs n2 : nat S : n2 < size xs
0 < size xs
by apply leq_ltn_trans with n2.
- x : nat xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality MIN : forall y : nat, y \in xs -> x <= yND : nondecreasing_sequence xs n2 : nat S : n2.+1 < size (x :: xs)
xs [|0 |] <= xs [|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 :
forall x xs ,
nondecreasing_sequence (x :: xs) ->
nondecreasing_sequence (x :: x :: xs).forall (x : nat) (xs : seq nat),
nondecreasing_sequence (x :: xs) ->
nondecreasing_sequence [:: x, x & xs]
Proof .forall (x : nat) (xs : seq nat),
nondecreasing_sequence (x :: xs) ->
nondecreasing_sequence [:: x, x & xs]
intros ? ? ND.x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs)
nondecreasing_sequence [:: x, x & xs]
move => [ | n1] [ | n2] /andP [LT1 LT2]; try done .x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) n2 : nat LT1 : 0 <= n2.+1 LT2 : n2.+1 < size [:: x, x & xs]
[:: x, x & xs] [|0 |] <= [:: x, x & xs] [|n2.+1 |]
- x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) n2 : nat LT1 : 0 <= n2.+1 LT2 : n2.+1 < size [:: x, x & xs]
[:: x, x & xs] [|0 |] <= [:: x, x & xs] [|n2.+1 |]
specialize (ND 0 n2).x : nat xs : seq nat n2 : nat ND : 0 <= n2 < size (x :: xs) ->
(x :: xs) [|0 |] <= (x :: xs) [|n2|]LT1 : 0 <= n2.+1 LT2 : n2.+1 < size [:: x, x & xs]
[:: x, x & xs] [|0 |] <= [:: x, x & xs] [|n2.+1 |]
by apply ND; rewrite //= ltnS in LT2.
- x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) n1, n2 : nat LT1 : n1 < n2.+1 LT2 : n2.+1 < size [:: x, x & xs]
[:: x, x & xs] [|n1.+1 |] <= [:: x, x & xs] [|n2.+1 |]
apply ND.x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) n1, n2 : nat LT1 : n1 < n2.+1 LT2 : n2.+1 < size [:: x, x & xs]
n1 <= n2 < size (x :: xs)
apply /andP; split .x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) n1, n2 : nat LT1 : n1 < n2.+1 LT2 : n2.+1 < size [:: x, x & xs]
n1 <= n2
+ x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) n1, n2 : nat LT1 : n1 < n2.+1 LT2 : n2.+1 < size [:: x, x & xs]
n1 <= n2
by rewrite ltnS in LT1.
+ x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) n1, n2 : nat LT1 : n1 < n2.+1 LT2 : n2.+1 < size [:: x, x & xs]
n2 < size (x :: xs)
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 :
forall x xs ,
nondecreasing_sequence (x :: xs) ->
(forall y , y \in xs -> x <= y).forall (x : nat) (xs : seq nat),
nondecreasing_sequence (x :: xs) ->
forall y : Datatypes_nat__canonical__eqtype_Equality,
y \in xs -> x <= y
Proof .forall (x : nat) (xs : seq nat),
nondecreasing_sequence (x :: xs) ->
forall y : Datatypes_nat__canonical__eqtype_Equality,
y \in xs -> x <= y
intros x xs ND y IN.x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) y : Datatypes_nat__canonical__eqtype_Equality IN : y \in xs
x <= y
have IDX := nth_index 0 IN.x : nat xs : seq nat ND : nondecreasing_sequence (x :: xs) y : Datatypes_nat__canonical__eqtype_Equality IN : y \in xs IDX : xs [|index y xs|] = y
x <= y
specialize (ND 0 (index y xs).+1 ).x : nat xs : seq nat y : Datatypes_nat__canonical__eqtype_Equality ND : 0 <= (index y xs).+1 < size (x :: xs) ->
(x :: xs) [|0 |] <= (x :: xs) [|(index y xs).+1 |]IN : y \in xs IDX : xs [|index y xs|] = y
x <= y
move : (IN) => IDL; rewrite -index_mem in IDL.x : nat xs : seq nat y : Datatypes_nat__canonical__eqtype_Equality ND : 0 <= (index y xs).+1 < size (x :: xs) ->
(x :: xs) [|0 |] <= (x :: xs) [|(index y xs).+1 |]IN : y \in xs IDX : xs [|index y xs|] = y IDL : index y xs < size xs
x <= y
feed ND. x : nat xs : seq nat y : Datatypes_nat__canonical__eqtype_Equality ND : 0 <= (index y xs).+1 < size (x :: xs) ->
(x :: xs) [|0 |] <= (x :: xs) [|(index y xs).+1 |]IN : y \in xs IDX : xs [|index y xs|] = y IDL : index y xs < size xs
0 <= (index y xs).+1 < size (x :: xs)
{ x : nat xs : seq nat y : Datatypes_nat__canonical__eqtype_Equality ND : 0 <= (index y xs).+1 < size (x :: xs) ->
(x :: xs) [|0 |] <= (x :: xs) [|(index y xs).+1 |]IN : y \in xs IDX : xs [|index y xs|] = y IDL : index y xs < size xs
0 <= (index y xs).+1 < size (x :: xs)
by apply /andP; split ; last rewrite //= ltnS. } x : nat xs : seq nat y : Datatypes_nat__canonical__eqtype_Equality ND : (x :: xs) [|0 |] <= (x :: xs) [|(index y xs).+1 |] IN : y \in xs IDX : xs [|index y xs|] = y IDL : index y xs < size xs
x <= y
eapply leq_trans; first by apply ND.x : nat xs : seq nat y : Datatypes_nat__canonical__eqtype_Equality ND : (x :: xs) [|0 |] <= (x :: xs) [|(index y xs).+1 |] IN : y \in xs IDX : xs [|index y xs|] = y IDL : index y xs < size xs
(x :: xs) [|(index y xs).+1 |] <= y
by rewrite //= IDX.
Qed .
(** We also prove a similar lemma for strict minimum. *)
Corollary nondecreasing_sequence_cons_smin :
forall x1 x2 xs ,
x1 < x2 ->
nondecreasing_sequence (x1 :: x2 :: xs) ->
(forall y , y \in x2 :: xs -> x1 < y).forall (x1 x2 : nat) (xs : seq nat),
x1 < x2 ->
nondecreasing_sequence [:: x1, x2 & xs] ->
forall y : Datatypes_nat__canonical__eqtype_Equality,
y \in x2 :: xs -> x1 < y
Proof .forall (x1 x2 : nat) (xs : seq nat),
x1 < x2 ->
nondecreasing_sequence [:: x1, x2 & xs] ->
forall y : Datatypes_nat__canonical__eqtype_Equality,
y \in x2 :: xs -> x1 < y
intros ? ? ? LT ND ? IN.x1, x2 : nat xs : seq nat LT : x1 < x2 ND : nondecreasing_sequence [:: x1, x2 & xs] y : Datatypes_nat__canonical__eqtype_Equality IN : y \in x2 :: xs
x1 < y
eapply leq_trans; first by apply LT.x1, x2 : nat xs : seq nat LT : x1 < x2 ND : nondecreasing_sequence [:: x1, x2 & xs] y : Datatypes_nat__canonical__eqtype_Equality IN : y \in x2 :: xs
x2 <= y
apply nondecreasing_sequence_cons in ND.x1, x2 : nat xs : seq nat LT : x1 < x2 ND : nondecreasing_sequence (x2 :: xs) y : Datatypes_nat__canonical__eqtype_Equality IN : y \in x2 :: xs
x2 <= y
eapply nondecreasing_sequence_cons_min; last by apply IN.x1, x2 : nat xs : seq nat LT : x1 < x2 ND : nondecreasing_sequence (x2 :: xs) y : Datatypes_nat__canonical__eqtype_Equality IN : y \in x2 :: xs
nondecreasing_sequence [:: x2, x2 & xs]
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 :
forall (xs : seq nat) (x : nat) (n : nat),
nondecreasing_sequence xs ->
xs[|n|] < x < xs[|n.+1 |] ->
~~ (x \in xs).forall (xs : seq nat) (x n : nat),
nondecreasing_sequence xs ->
xs [|n|] < x < xs [|n.+1 |] -> x \notin xs
Proof .forall (xs : seq nat) (x n : nat),
nondecreasing_sequence xs ->
xs [|n|] < x < xs [|n.+1 |] -> x \notin xs
move => xs x n STR H; apply /negP => /nthP => /(_ 0 ) [ind LE HHH].xs : seq nat x, n : nat STR : nondecreasing_sequence xs H : xs [|n|] < x < xs [|n.+1 |] ind : nat LE : ind < size xs HHH : xs [|ind|] = x
False
subst x; rename ind into x.xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs
False
destruct (n.+1 < size xs) eqn :Bt; last first .xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs Bt : (n.+1 < size xs) = false
False
{ xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs Bt : (n.+1 < size xs) = false
False
move : Bt => /negP /negP; rewrite -leqNgt; move => Bt.xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs Bt : size xs <= n.+1
False
apply nth_default with (x0 := 0 ) in Bt.xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs Bt : xs [|n.+1 |] = 0
False
by rewrite Bt in H; move : H => /andP [_ T]. } xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs Bt : (n.+1 < size xs) = true
False
have B1: n.+1 < size xs; first by done .xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs Bt : (n.+1 < size xs) = true B1 : n.+1 < size xs
False
clear Bt.xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs B1 : n.+1 < size xs
False
have B2: n < size xs; first by apply leq_ltn_trans with n.+1 .xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs
False
have GT: n < x.xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs
n < x
{ xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs
n < x
move : H => /andP [T _].xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|n|] < xs [|x|]
n < x
rewrite ltnNge; apply /negP; intros CONTR.xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|n|] < xs [|x|] CONTR : x <= n
False
specialize (STR x n).xs : seq nat n, x : nat STR : x <= n < size xs -> xs [|x|] <= xs [|n|] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|n|] < xs [|x|] CONTR : x <= n
False
feed STR. xs : seq nat n, x : nat STR : x <= n < size xs -> xs [|x|] <= xs [|n|] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|n|] < xs [|x|] CONTR : x <= n
x <= n < size xs
{ xs : seq nat n, x : nat STR : x <= n < size xs -> xs [|x|] <= xs [|n|] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|n|] < xs [|x|] CONTR : x <= n
x <= n < size xs
by apply /andP; split . } xs : seq nat n, x : nat STR : xs [|x|] <= xs [|n|] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|n|] < xs [|x|] CONTR : x <= n
False
by move : STR; rewrite leqNgt; move => /negP STR; apply : STR.
} xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs GT : n < x
False
have LT: x < n.+1 .xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs GT : n < x
x < n.+1
{ xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs GT : n < x
x < n.+1
clear GT.xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs
x < n.+1
move : H => /andP [_ T].xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|x|] < xs [|n.+1 |]
x < n.+1
rewrite ltnNge; apply /negP; intros CONTR.xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|x|] < xs [|n.+1 |] CONTR : n < x
False
move : CONTR; rewrite leq_eqVlt; move => /orP [/eqP EQ | CONTR].xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|x|] < xs [|n.+1 |] EQ : n.+1 = x
False
- xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|x|] < xs [|n.+1 |] EQ : n.+1 = x
False
by subst ; rewrite ltnn in T.
- xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|x|] < xs [|n.+1 |] CONTR : n.+1 < x
False
specialize (STR n.+1 x).xs : seq nat n, x : nat STR : n < x < size xs -> xs [|n.+1 |] <= xs [|x|] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|x|] < xs [|n.+1 |] CONTR : n.+1 < x
False
feed STR. xs : seq nat n, x : nat STR : n < x < size xs -> xs [|n.+1 |] <= xs [|x|] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|x|] < xs [|n.+1 |] CONTR : n.+1 < x
n < x < size xs
{ xs : seq nat n, x : nat STR : n < x < size xs -> xs [|n.+1 |] <= xs [|x|] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|x|] < xs [|n.+1 |] CONTR : n.+1 < x
n < x < size xs
by apply /andP; split ; first apply ltnW. } xs : seq nat n, x : nat STR : xs [|n.+1 |] <= xs [|x|] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs T : xs [|x|] < xs [|n.+1 |] CONTR : n.+1 < x
False
by move : STR; rewrite leqNgt; move => /negP STR; apply : STR.
} xs : seq nat n : nat STR : nondecreasing_sequence xs x : nat H : xs [|n|] < xs [|x|] < xs [|n.+1 |] LE : x < size xs B1 : n.+1 < size xs B2 : n < size xs GT : n < x LT : x < n.+1
False
by move : LT; rewrite ltnNge; move => /negP LT; apply : LT.
Qed .
(** Alternatively, consider an arbitrary natural number x that is
bounded by the first and the last element of a sequence
[xs]. Then there is an index n such that [xs[n] <= x < x[n+1]]. *)
Lemma belonging_to_segment_of_seq_is_total :
forall (xs : seq nat) (x : nat),
2 <= size xs ->
first0 xs <= x < last0 xs ->
exists n ,
n.+1 < size xs /\
xs[|n|] <= x < xs[|n.+1 |].forall (xs : seq nat) (x : nat),
1 < size xs ->
first0 xs <= x < last0 xs ->
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
Proof .forall (xs : seq nat) (x : nat),
1 < size xs ->
first0 xs <= x < last0 xs ->
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
move => xs x SIZE LAST.xs : seq nat x : nat SIZE : 1 < size xsLAST : first0 xs <= x < last0 xs
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
have EX: exists n , size xs <= n by exists (size xs ).xs : seq nat x : nat SIZE : 1 < size xsLAST : first0 xs <= x < last0 xs EX : exists n : nat, size xs <= n
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
move : EX => [n LE].xs : seq nat x : nat SIZE : 1 < size xsLAST : first0 xs <= x < last0 xs n : nat LE : size xs <= n
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
destruct n as [ |n]; first by destruct xs.xs : seq nat x : nat SIZE : 1 < size xsLAST : first0 xs <= x < last0 xs n : nat LE : size xs <= n.+1
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
destruct n as [ |n]; first by destruct xs as [ |? xs]; last destruct xs.xs : seq nat x : nat SIZE : 1 < size xsLAST : first0 xs <= x < last0 xs n : nat LE : size xs <= n.+2
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
generalize dependent xs.x, n : nat
forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
elim : n => [ |n IHn] xs SIZE LAST LE.x : nat xs : seq nat SIZE : 1 < size xsLAST : first0 xs <= x < last0 xs LE : size xs <= 2
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
{ x : nat xs : seq nat SIZE : 1 < size xsLAST : first0 xs <= x < last0 xs LE : size xs <= 2
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
by destruct xs as [ |? xs]; [ | destruct xs as [ |? xs]; [ | destruct xs; [exists 0 | ] ] ]. } x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]xs : seq nat SIZE : 1 < size xsLAST : first0 xs <= x < last0 xs LE : size xs <= n.+3
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
{ x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]xs : seq nat SIZE : 1 < size xsLAST : first0 xs <= x < last0 xs LE : size xs <= n.+3
exists n : nat,
n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]
destruct xs as [ |n0 xs]; [ | destruct xs as [ |n1 xs]; [ | ]]; try by done .x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]n0, n1 : nat xs : seq nat SIZE : 1 < size [:: n0, n1 & xs]LAST : first0 [:: n0, n1 & xs] <= x <
last0 [:: n0, n1 & xs] LE : size [:: n0, n1 & xs] <= n.+3
exists n : nat,
n.+1 < size [:: n0, n1 & xs] /\
[:: n0, n1 & xs] [|n|] <= x <
[:: n0, n1 & xs] [|n.+1 |]
destruct xs as [ |n2 xs]; first by (exists 0 ).x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]n0, n1, n2 : nat xs : seq nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3
exists n : nat,
n.+1 < size [:: n0, n1, n2 & xs] /\
[:: n0, n1, n2 & xs] [|n|] <= x <
[:: n0, n1, n2 & xs] [|n.+1 |]
destruct (leqP n1 x) as [NEQ|NEQ]; last first .x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]n0, n1, n2 : nat xs : seq nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : x < n1
exists n : nat,
n.+1 < size [:: n0, n1, n2 & xs] /\
[:: n0, n1, n2 & xs] [|n|] <= x <
[:: n0, n1, n2 & xs] [|n.+1 |]
{ x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]n0, n1, n2 : nat xs : seq nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : x < n1
exists n : nat,
n.+1 < size [:: n0, n1, n2 & xs] /\
[:: n0, n1, n2 & xs] [|n|] <= x <
[:: n0, n1, n2 & xs] [|n.+1 |]
exists 0 ; split ; auto .x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]n0, n1, n2 : nat xs : seq nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : x < n1
[:: n0, n1, n2 & xs] [|0 |] <= x <
[:: n0, n1, n2 & xs] [|1 |]
move : LAST => /andP [LAST _].x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]n0, n1, n2 : nat xs : seq nat SIZE : 1 < size [:: n0, n1, n2 & xs]LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : x < n1 LAST : first0 [:: n0, n1, n2 & xs] <= x
[:: n0, n1, n2 & xs] [|0 |] <= x <
[:: n0, n1, n2 & xs] [|1 |]
by apply /andP; split . } x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]n0, n1, n2 : nat xs : seq nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
exists n : nat,
n.+1 < size [:: n0, n1, n2 & xs] /\
[:: n0, n1, n2 & xs] [|n|] <= x <
[:: n0, n1, n2 & xs] [|n.+1 |]
{ x, n : nat IHn : forall xs : seq nat,
1 < size xs ->
first0 xs <= x < last0 xs ->
size xs <= n.+2 ->
exists n : nat, n.+1 < size xs /\ xs [|n|] <= x < xs [|n.+1 |]n0, n1, n2 : nat xs : seq nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
exists n : nat,
n.+1 < size [:: n0, n1, n2 & xs] /\
[:: n0, n1, n2 & xs] [|n|] <= x <
[:: n0, n1, n2 & xs] [|n.+1 |]
specialize (IHn [:: n1, n2 & xs]).x, n, n1, n2 : nat xs : seq nat IHn : 1 < size [:: n1, n2 & xs] ->
first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs] ->
size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |]n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
exists n : nat,
n.+1 < size [:: n0, n1, n2 & xs] /\
[:: n0, n1, n2 & xs] [|n|] <= x <
[:: n0, n1, n2 & xs] [|n.+1 |]
feed_n 3 IHn. x, n, n1, n2 : nat xs : seq nat IHn : 1 < size [:: n1, n2 & xs] ->
first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs] ->
size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |]n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
1 < size [:: n1, n2 & xs]
{ x, n, n1, n2 : nat xs : seq nat IHn : 1 < size [:: n1, n2 & xs] ->
first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs] ->
size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |]n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
1 < size [:: n1, n2 & xs]
by done . } x, n, n1, n2 : nat xs : seq nat IHn : first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs] ->
size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |] n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs]
{ x, n, n1, n2 : nat xs : seq nat IHn : first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs] ->
size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |] n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs]
move : LAST => /andP [LAST1 LAST2].x, n, n1, n2 : nat xs : seq nat IHn : first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs] ->
size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |] n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x LAST1 : first0 [:: n0, n1, n2 & xs] <= x LAST2 : x < last0 [:: n0, n1, n2 & xs]
first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs]
apply /andP; split ; first by done .x, n, n1, n2 : nat xs : seq nat IHn : first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs] ->
size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |] n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x LAST1 : first0 [:: n0, n1, n2 & xs] <= x LAST2 : x < last0 [:: n0, n1, n2 & xs]
x < last0 [:: n1, n2 & xs]
apply leq_trans with (last0 [:: n0, n1, n2 & xs]); first by done .x, n, n1, n2 : nat xs : seq nat IHn : first0 [:: n1, n2 & xs] <= x < last0 [:: n1, n2 & xs] ->
size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |] n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x LAST1 : first0 [:: n0, n1, n2 & xs] <= x LAST2 : x < last0 [:: n0, n1, n2 & xs]
last0 [:: n0, n1, n2 & xs] <= last0 [:: n1, n2 & xs]
by rewrite /last0 !last_cons.
} x, n, n1, n2 : nat xs : seq nat IHn : size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |] n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
size [:: n1, n2 & xs] <= n.+2
{ x, n, n1, n2 : nat xs : seq nat IHn : size [:: n1, n2 & xs] <= n.+2 ->
exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |] n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
size [:: n1, n2 & xs] <= n.+2
by rewrite -(ltn_add2r 1 ) !addn1. } x, n, n1, n2 : nat xs : seq nat IHn : exists n : nat,
n.+1 < size [:: n1, n2 & xs] /\
[:: n1, n2 & xs] [|n|] <= x < [:: n1, n2 & xs] [|n.+1 |]n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x
exists n : nat,
n.+1 < size [:: n0, n1, n2 & xs] /\
[:: n0, n1, n2 & xs] [|n|] <= x <
[:: n0, n1, n2 & xs] [|n.+1 |]
move : IHn => [idx [SI /andP [G L]]].x, n, n1, n2 : nat xs : seq nat n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x idx : nat SI : idx.+1 < size [:: n1, n2 & xs] G : [:: n1, n2 & xs] [|idx|] <= x L : x < [:: n1, n2 & xs] [|idx.+1 |]
exists n : nat,
n.+1 < size [:: n0, n1, n2 & xs] /\
[:: n0, n1, n2 & xs] [|n|] <= x <
[:: n0, n1, n2 & xs] [|n.+1 |]
exists idx .+1 ; split .x, n, n1, n2 : nat xs : seq nat n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x idx : nat SI : idx.+1 < size [:: n1, n2 & xs] G : [:: n1, n2 & xs] [|idx|] <= x L : x < [:: n1, n2 & xs] [|idx.+1 |]
idx.+2 < size [:: n0, n1, n2 & xs]
- x, n, n1, n2 : nat xs : seq nat n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x idx : nat SI : idx.+1 < size [:: n1, n2 & xs] G : [:: n1, n2 & xs] [|idx|] <= x L : x < [:: n1, n2 & xs] [|idx.+1 |]
idx.+2 < size [:: n0, n1, n2 & xs]
by simpl in *; rewrite -addn1 -[in X in _ <= X]addn1 leq_add2r.
- x, n, n1, n2 : nat xs : seq nat n0 : nat SIZE : 1 < size [:: n0, n1, n2 & xs]LAST : first0 [:: n0, n1, n2 & xs] <= x <
last0 [:: n0, n1, n2 & xs] LE : size [:: n0, n1, n2 & xs] <= n.+3 NEQ : n1 <= x idx : nat SI : idx.+1 < size [:: n1, n2 & xs] G : [:: n1, n2 & xs] [|idx|] <= x L : x < [:: n1, n2 & xs] [|idx.+1 |]
[:: n0, n1, n2 & xs] [|idx.+1 |] <= x <
[:: n0, n1, n2 & xs] [|idx.+2 |]
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 :
forall (xs : seq nat) (x : nat),
nondecreasing_sequence xs ->
(x \in xs) ->
x <= last0 xs.forall (xs : seq nat) (x : nat),
nondecreasing_sequence xs -> x \in xs -> x <= last0 xs
Proof .forall (xs : seq nat) (x : nat),
nondecreasing_sequence xs -> x \in xs -> x <= last0 xs
move => xs x STR IN.xs : seq nat x : nat STR : nondecreasing_sequence xs IN : x \in xs
x <= last0 xs
have NEQ: forall x y , x = y \/ x != y.xs : seq nat x : nat STR : nondecreasing_sequence xs IN : x \in xs
forall (t : eqType) (x y : t), x = y \/ x != y
{ xs : seq nat x : nat STR : nondecreasing_sequence xs IN : x \in xs
forall (t : eqType) (x y : t), x = y \/ x != y
clear => t x y.t : eqType x, y : t
x = y \/ x != y
destruct (x == y) eqn :EQ.t : eqType x, y : t EQ : (x == y) = true
x = y \/ ~~ true
- t : eqType x, y : t EQ : (x == y) = true
x = y \/ ~~ true
by left ; apply /eqP.
- t : eqType x, y : t EQ : (x == y) = false
x = y \/ ~~ false
by right .
} xs : seq nat x : nat STR : nondecreasing_sequence xs IN : x \in xs NEQ : forall (t : eqType) (x y : t), x = y \/ x != y
x <= last0 xs
move : (NEQ _ x (last0 xs)); clear NEQ; move => [EQ|NEQ].xs : seq nat x : nat STR : nondecreasing_sequence xs IN : x \in xs EQ : x = last0 xs
x <= last0 xs
{ xs : seq nat x : nat STR : nondecreasing_sequence xs IN : x \in xs EQ : x = last0 xs
x <= last0 xs
by subst x. } xs : seq nat x : nat STR : nondecreasing_sequence xs IN : x \in xs NEQ : x != last0 xs
x <= last0 xs
{ xs : seq nat x : nat STR : nondecreasing_sequence xs IN : x \in xs NEQ : x != last0 xs
x <= last0 xs
move : IN => /nthP EX.xs : seq nat x : nat STR : nondecreasing_sequence xs NEQ : x != last0 xs EX : forall
s : Datatypes_nat__canonical__eqtype_Equality,
exists2 i : nat, i < size xs & nth s xs i = x
x <= last0 xs
specialize (EX 0 ).xs : seq nat x : nat STR : nondecreasing_sequence xs NEQ : x != last0 xs EX : exists2 i : nat, i < size xs & xs [|i|] = x
x <= last0 xs
move : EX => [id SIZE EQ].xs : seq nat x : nat STR : nondecreasing_sequence xs NEQ : x != last0 xs id : nat SIZE : id < size xs EQ : xs [|id|] = x
x <= last0 xs
rewrite /last0 -nth_last -EQ; subst x.xs : seq nat STR : nondecreasing_sequence xs id : nat NEQ : xs [|id|] != last0 xs SIZE : id < size xs
xs [|id|] <= xs [|(size xs).-1 |]
rewrite -addn1 in SIZE.xs : seq nat STR : nondecreasing_sequence xs id : nat NEQ : xs [|id|] != last0 xs SIZE : id + 1 <= size xs
xs [|id|] <= xs [|(size xs).-1 |]
apply STR; apply /andP.xs : seq nat STR : nondecreasing_sequence xs id : nat NEQ : xs [|id|] != last0 xs SIZE : id + 1 <= size xs
id <= (size xs).-1 /\ (size xs).-1 < size xs
have POS: 0 < size xs.xs : seq nat STR : nondecreasing_sequence xs id : nat NEQ : xs [|id|] != last0 xs SIZE : id + 1 <= size xs
0 < size xs
{ xs : seq nat STR : nondecreasing_sequence xs id : nat NEQ : xs [|id|] != last0 xs SIZE : id + 1 <= size xs
0 < size xs
by apply leq_trans with (id + 1 ); first rewrite addn1. } xs : seq nat STR : nondecreasing_sequence xs id : nat NEQ : xs [|id|] != last0 xs SIZE : id + 1 <= size xs POS : 0 < size xs
id <= (size xs).-1 /\ (size xs).-1 < size xs
split .xs : seq nat STR : nondecreasing_sequence xs id : nat NEQ : xs [|id|] != last0 xs SIZE : id + 1 <= size xs POS : 0 < size xs
id <= (size xs).-1
- xs : seq nat STR : nondecreasing_sequence xs id : nat NEQ : xs [|id|] != last0 xs SIZE : id + 1 <= size xs POS : 0 < size xs
id <= (size xs).-1
by rewrite -(leq_add2r 1 ) !addn1 prednK // -addn1.
- xs : seq nat STR : nondecreasing_sequence xs id : nat NEQ : xs [|id|] != last0 xs SIZE : id + 1 <= size xs POS : 0 < size xs
(size xs).-1 < size xs
by rewrite prednK.
}
Qed .
End NonDecreasingSequence .
(** * Properties of [Undup] of Non-Decreasing Sequence *)
(** In this section we prove a few lemmas about [undup] of non-decreasing sequences. *)
Section Undup .
(** First we prove that [undup x::x::xs] is equal to [undup x::xs]. *)
Remark nodup_sort_2cons_eq :
forall {X : eqType} (x : X) (xs : seq X),
undup (x::x::xs) = undup (x::xs).forall (X : eqType) (x : X) (xs : seq X),
undup [:: x, x & xs] = undup (x :: xs)
Proof .forall (X : eqType) (x : X) (xs : seq X),
undup [:: x, x & xs] = undup (x :: xs)
move => X x xs; rewrite {2 3 }[cons] lock //= -lock.X : eqType x : X xs : seq X
(if x \in x :: xs
then undup (x :: xs)
else x :: undup (x :: xs)) = undup (x :: xs)
rewrite in_cons eq_refl; simpl .X : eqType x : X xs : seq X
(if x \in xs then undup xs else x :: undup xs) =
(if x \in xs then undup xs else x :: undup xs)
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 :
forall x1 x2 xs ,
x1 < x2 ->
nondecreasing_sequence (x1::x2::xs) ->
undup (x1::x2::xs) = x1 :: undup (x2::xs).forall (x1 x2 : nat) (xs : seq nat),
x1 < x2 ->
nondecreasing_sequence [:: x1, x2 & xs] ->
undup [:: x1, x2 & xs] = x1 :: undup (x2 :: xs)
Proof .forall (x1 x2 : nat) (xs : seq nat),
x1 < x2 ->
nondecreasing_sequence [:: x1, x2 & xs] ->
undup [:: x1, x2 & xs] = x1 :: undup (x2 :: xs)
move => x1 x2 xs H H0; rewrite {2 3 4 }[cons] lock //= -lock.x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence [:: x1, x2 & xs]
(if x1 \in x2 :: xs
then undup (x2 :: xs)
else x1 :: undup (x2 :: xs)) = x1 :: undup (x2 :: xs)
rewrite in_cons.x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence [:: x1, x2 & xs]
(if (x1 == x2) || (x1 \in xs)
then undup (x2 :: xs)
else x1 :: undup (x2 :: xs)) = x1 :: undup (x2 :: xs)
have -> : (x1 == x2) = false.x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence [:: x1, x2 & xs]
(x1 == x2) = false
{ x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence [:: x1, x2 & xs]
(x1 == x2) = false
by apply /eqP/eqP; rewrite neq_ltn; rewrite H. } x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence [:: x1, x2 & xs]
(if false || (x1 \in xs)
then undup (x2 :: xs)
else x1 :: undup (x2 :: xs)) = x1 :: undup (x2 :: xs)
rewrite [cons]lock //= -lock.x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence [:: x1, x2 & xs]
(if x1 \in xs
then undup (x2 :: xs)
else x1 :: undup (x2 :: xs)) = x1 :: undup (x2 :: xs)
have -> : (x1 \in xs) = false; last by done .x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence [:: x1, x2 & xs]
(x1 \in xs) = false
apply /eqP; rewrite eqbF_neg.x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence [:: x1, x2 & xs]
x1 \notin xs
apply nondecreasing_sequence_cons in H0.x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence (x2 :: xs)
x1 \notin xs
apply /negP; intros ?; eauto 2 .x1, x2 : nat xs : seq nat H : x1 < x2 H0 : nondecreasing_sequence (x2 :: xs) H1 : x1 \in xs
False
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 :
forall xs ,
nondecreasing_sequence xs ->
last0 (undup xs) = last0 xs.forall xs : seq nat,
nondecreasing_sequence xs ->
last0 (undup xs) = last0 xs
Proof .forall xs : seq nat,
nondecreasing_sequence xs ->
last0 (undup xs) = last0 xs
elim => [//|x1 xs IHxs].x1 : nat xs : seq nat IHxs : nondecreasing_sequence xs ->
last0 (undup xs) = last0 xs
nondecreasing_sequence (x1 :: xs) ->
last0 (undup (x1 :: xs)) = last0 (x1 :: xs)
intros ND; destruct xs as [ |x2 xs]; first by done .x1, x2 : nat xs : seq nat IHxs : nondecreasing_sequence (x2 :: xs) ->
last0 (undup (x2 :: xs)) = last0 (x2 :: xs) ND : nondecreasing_sequence [:: x1, x2 & xs]
last0 (undup [:: x1, x2 & xs]) =
last0 [:: x1, x2 & xs]
destruct (nondecreasing_sequence_2cons_leVeq _ _ _ ND) as [EQ|LT].x1, x2 : nat xs : seq nat IHxs : nondecreasing_sequence (x2 :: xs) ->
last0 (undup (x2 :: xs)) = last0 (x2 :: xs) ND : nondecreasing_sequence [:: x1, x2 & xs] EQ : x1 = x2
last0 (undup [:: x1, x2 & xs]) =
last0 [:: x1, x2 & xs]
- x1, x2 : nat xs : seq nat IHxs : nondecreasing_sequence (x2 :: xs) ->
last0 (undup (x2 :: xs)) = last0 (x2 :: xs) ND : nondecreasing_sequence [:: x1, x2 & xs] EQ : x1 = x2
last0 (undup [:: x1, x2 & xs]) =
last0 [:: x1, x2 & xs]
subst ; rename x2 into x.x : nat xs : seq nat IHxs : nondecreasing_sequence (x :: xs) ->
last0 (undup (x :: xs)) = last0 (x :: xs) ND : nondecreasing_sequence [:: x, x & xs]
last0 (undup [:: x, x & xs]) = last0 [:: x, x & xs]
rewrite nodup_sort_2cons_eq IHxs //=.x : nat xs : seq nat IHxs : nondecreasing_sequence (x :: xs) ->
last0 (undup (x :: xs)) = last0 (x :: xs) ND : nondecreasing_sequence [:: x, x & xs]
nondecreasing_sequence (x :: xs)
by eapply nondecreasing_sequence_cons; eauto 2 .
- x1, x2 : nat xs : seq nat IHxs : nondecreasing_sequence (x2 :: xs) ->
last0 (undup (x2 :: xs)) = last0 (x2 :: xs) ND : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
last0 (undup [:: x1, x2 & xs]) =
last0 [:: x1, x2 & xs]
rewrite nodup_sort_2cons_lt // last0_cons.x1, x2 : nat xs : seq nat IHxs : nondecreasing_sequence (x2 :: xs) ->
last0 (undup (x2 :: xs)) = last0 (x2 :: xs) ND : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
last0 (undup (x2 :: xs)) = last0 [:: x1, x2 & xs]
+ x1, x2 : nat xs : seq nat IHxs : nondecreasing_sequence (x2 :: xs) ->
last0 (undup (x2 :: xs)) = last0 (x2 :: xs) ND : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
last0 (undup (x2 :: xs)) = last0 [:: x1, x2 & xs]
rewrite IHxs //; eauto using nondecreasing_sequence_cons.
+ x1, x2 : nat xs : seq nat IHxs : nondecreasing_sequence (x2 :: xs) ->
last0 (undup (x2 :: xs)) = last0 (x2 :: xs) ND : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
undup (x2 :: xs) <> [::]
by move /undup_nil.
Qed .
(** Non-decreasing sequence remains non-decreasing after application of [undup]. *)
Lemma nondecreasing_sequence_undup :
forall xs ,
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs).forall xs : seq nat,
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs)
Proof .forall xs : seq nat,
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs)
move => xs.xs : seq nat
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs)
have EX: exists len , size xs <= len.xs : seq nat
exists len : nat, size xs <= len
{ xs : seq nat
exists len : nat, size xs <= len
by exists (size xs ). } xs : seq nat EX : exists len : nat, size xs <= len
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs)
destruct EX as [n BO].xs : seq nat n : nat BO : size xs <= n
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs)
revert xs BO; elim : n => [ |n IHn].forall xs : seq nat,
size xs <= 0 ->
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs)
- forall xs : seq nat,
size xs <= 0 ->
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs)
by intros xs; rewrite leqn0 size_eq0; move => /eqP EQ; subst xs.
- n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)
forall xs : seq nat,
size xs <= n.+1 ->
nondecreasing_sequence xs ->
nondecreasing_sequence (undup xs)
intros [ |x1 [ | x2 xs]] Size NonDec; try done .n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs]
nondecreasing_sequence (undup [:: x1, x2 & xs])
destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec) as [EQ|LT].n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] EQ : x1 = x2
nondecreasing_sequence (undup [:: x1, x2 & xs])
+ n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] EQ : x1 = x2
nondecreasing_sequence (undup [:: x1, x2 & xs])
subst ; rename x2 into x.n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x : nat xs : seq nat NonDec : nondecreasing_sequence [:: x, x & xs] Size : size [:: x, x & xs] <= n.+1
nondecreasing_sequence (undup [:: x, x & xs])
by rewrite nodup_sort_2cons_eq; apply IHn; eauto using nondecreasing_sequence_cons.
+ n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
nondecreasing_sequence (undup [:: x1, x2 & xs])
rewrite nodup_sort_2cons_lt //.n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
nondecreasing_sequence (x1 :: undup (x2 :: xs))
apply nondecreasing_sequence_add_min.n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
forall y : nat, y \in undup (x2 :: xs) -> x1 <= y
* n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
forall y : nat, y \in undup (x2 :: xs) -> x1 <= y
move => y H.n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2 y : nat H : y \in undup (x2 :: xs)
x1 <= y
eapply nondecreasing_sequence_cons_min with (y := y) in NonDec; auto .n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2 y : nat H : y \in undup (x2 :: xs)
y \in x2 :: xs
rewrite -mem_undup; eauto using nondecreasing_sequence_cons.
* n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs -> nondecreasing_sequence (undup xs)x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
nondecreasing_sequence (undup (x2 :: xs))
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 :
forall xs ,
nondecreasing_sequence xs ->
undup xs [| (size (undup xs)).-2 |] <= xs [| (size xs).-2 |].forall xs : seq nat,
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <=
xs [|(size xs).-2 |]
Proof .forall xs : seq nat,
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <=
xs [|(size xs).-2 |]
Opaque undup.forall xs : seq nat,
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <=
xs [|(size xs).-2 |]
move => xs.xs : seq nat
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <=
xs [|(size xs).-2 |]
have EX: exists len , size xs <= len by (exists (size xs )).xs : seq nat EX : exists len : nat, size xs <= len
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <=
xs [|(size xs).-2 |]
destruct EX as [n BO].xs : seq nat n : nat BO : size xs <= n
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <=
xs [|(size xs).-2 |]
revert xs BO; elim : n => [ |n IHn].forall xs : seq nat,
size xs <= 0 ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <=
xs [|(size xs).-2 |]
- forall xs : seq nat,
size xs <= 0 ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <=
xs [|(size xs).-2 |]
by intros xs; rewrite leqn0 size_eq0; move => /eqP EQ; subst xs.
- n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]
forall xs : seq nat,
size xs <= n.+1 ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <=
xs [|(size xs).-2 |]
intros [ |x1 [ | x2 xs]] Size NonDec; try done .n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs]
undup [:: x1, x2 & xs]
[|(size (undup [:: x1, x2 & xs])).-2 |] <=
[:: x1, x2 & xs] [|(size [:: x1, x2 & xs]).-2 |]
destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec) as [EQ|LT].n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] EQ : x1 = x2
undup [:: x1, x2 & xs]
[|(size (undup [:: x1, x2 & xs])).-2 |] <=
[:: x1, x2 & xs] [|(size [:: x1, x2 & xs]).-2 |]
* n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] EQ : x1 = x2
undup [:: x1, x2 & xs]
[|(size (undup [:: x1, x2 & xs])).-2 |] <=
[:: x1, x2 & xs] [|(size [:: x1, x2 & xs]).-2 |]
subst ; rename x2 into x.n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x : nat xs : seq nat NonDec : nondecreasing_sequence [:: x, x & xs] Size : size [:: x, x & xs] <= n.+1
undup [:: x, x & xs]
[|(size (undup [:: x, x & xs])).-2 |] <=
[:: x, x & xs] [|(size [:: x, x & xs]).-2 |]
rewrite nodup_sort_2cons_eq //.n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x : nat xs : seq nat NonDec : nondecreasing_sequence [:: x, x & xs] Size : size [:: x, x & xs] <= n.+1
undup (x :: xs) [|(size (undup (x :: xs))).-2 |] <=
[:: x, x & xs] [|(size [:: x, x & xs]).-2 |]
eapply leq_trans.n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x : nat xs : seq nat NonDec : nondecreasing_sequence [:: x, x & xs] Size : size [:: x, x & xs] <= n.+1
undup (x :: xs) [|(size (undup (x :: xs))).-2 |] <= ?n
** n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x : nat xs : seq nat NonDec : nondecreasing_sequence [:: x, x & xs] Size : size [:: x, x & xs] <= n.+1
undup (x :: xs) [|(size (undup (x :: xs))).-2 |] <= ?n
apply IHn; first by done .n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x : nat xs : seq nat NonDec : nondecreasing_sequence [:: x, x & xs] Size : size [:: x, x & xs] <= n.+1
nondecreasing_sequence (x :: xs)
by eapply nondecreasing_sequence_cons; eauto .
** n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x : nat xs : seq nat NonDec : nondecreasing_sequence [:: x, x & xs] Size : size [:: x, x & xs] <= n.+1
(x :: xs) [|(size (x :: xs)).-2 |] <=
[:: x, x & xs] [|(size [:: x, x & xs]).-2 |]
destruct xs as [ | x1 xs]; first by done .n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x, x1 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x, x, x1 & xs] Size : size [:: x, x, x1 & xs] <= n.+1
[:: x, x1 & xs] [|(size [:: x, x1 & xs]).-2 |] <=
[:: x, x, x1 & xs] [|(size [:: x, x, x1 & xs]).-2 |]
by rewrite [in X in _ <= X]nth0_cons //.
* n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
undup [:: x1, x2 & xs]
[|(size (undup [:: x1, x2 & xs])).-2 |] <=
[:: x1, x2 & xs] [|(size [:: x1, x2 & xs]).-2 |]
rewrite nodup_sort_2cons_lt //; simpl .n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2
(x1 :: undup (x2 :: xs))
[|(size (undup (x2 :: xs))).-1 |] <=
[:: x1, x2 & xs] [|size xs|]
case (posnP (size (undup (x2 :: xs))).-1 ) as [Z|POS].n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2 Z : (size (undup (x2 :: xs))).-1 = 0
(x1 :: undup (x2 :: xs))
[|(size (undup (x2 :: xs))).-1 |] <=
[:: x1, x2 & xs] [|size xs|]
** n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2 Z : (size (undup (x2 :: xs))).-1 = 0
(x1 :: undup (x2 :: xs))
[|(size (undup (x2 :: xs))).-1 |] <=
[:: x1, x2 & xs] [|size xs|]
rewrite Z; simpl .n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2 Z : (size (undup (x2 :: xs))).-1 = 0
x1 <= [:: x1, x2 & xs] [|size xs|]
apply leq_trans with ([:: x1, x2 & xs] [|0 |]); first by done .n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2 Z : (size (undup (x2 :: xs))).-1 = 0
[:: x1, x2 & xs] [|0 |] <= [:: x1, x2 & xs] [|size xs|]
by apply NonDec; apply /andP; split ; simpl .
** n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2 POS : 0 < (size (undup (x2 :: xs))).-1
(x1 :: undup (x2 :: xs))
[|(size (undup (x2 :: xs))).-1 |] <=
[:: x1, x2 & xs] [|size xs|]
rewrite nth0_cons //.n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2 POS : 0 < (size (undup (x2 :: xs))).-1
undup (x2 :: xs) [|(size (undup (x2 :: xs))).-2 |] <=
[:: x1, x2 & xs] [|size xs|]
eapply leq_trans; first apply IHn; eauto using nondecreasing_sequence_cons.n : nat IHn : forall xs : seq nat,
size xs <= n ->
nondecreasing_sequence xs ->
undup xs [|(size (undup xs)).-2 |] <= xs [|(size xs).-2 |]x1, x2 : nat xs : seq nat Size : size [:: x1, x2 & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x1, x2 & xs] LT : x1 < x2 POS : 0 < (size (undup (x2 :: xs))).-1
(x2 :: xs) [|(size (x2 :: xs)).-2 |] <=
[:: x1, x2 & xs] [|size xs|]
by destruct xs as [ |? xs]; [exfalso | destruct xs].
Qed .
End Undup .
(** * Properties of Distances *)
(** In this section we prove a few lemmas about function [distances]. *)
Section Distances .
(** We begin with a simple lemma that helps us unfold [distances]
of lists with two consecutive cons [x0::x1::xs]. *)
Lemma distances_unfold_2cons :
forall x0 x1 xs ,
distances (x0::x1::xs) = (x1 - x0) :: distances (x1::xs).forall (x0 x1 : nat) (xs : seq nat),
distances [:: x0, x1 & xs] =
x1 - x0 :: distances (x1 :: xs)
Proof .forall (x0 x1 : nat) (xs : seq nat),
distances [:: x0, x1 & xs] =
x1 - x0 :: distances (x1 :: xs)
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 :
forall (a b : nat) (xs : seq nat),
distances (xs ++ [:: a; b])
= distances (xs ++ [:: a]) ++ [:: b - a].forall (a b : nat) (xs : seq nat),
distances (xs ++ [:: a; b]) =
distances (xs ++ [:: a]) ++ [:: b - a]
Proof .forall (a b : nat) (xs : seq nat),
distances (xs ++ [:: a; b]) =
distances (xs ++ [:: a]) ++ [:: b - a]
move => a b xs.a, b : nat xs : seq nat
distances (xs ++ [:: a; b]) =
distances (xs ++ [:: a]) ++ [:: b - a]
have EX: exists n , size xs <= n by (exists (size xs )).a, b : nat xs : seq nat EX : exists n : nat, size xs <= n
distances (xs ++ [:: a; b]) =
distances (xs ++ [:: a]) ++ [:: b - a]
destruct EX as [n LE].a, b : nat xs : seq nat n : nat LE : size xs <= n
distances (xs ++ [:: a; b]) =
distances (xs ++ [:: a]) ++ [:: b - a]
elim : n xs LE => [ |n IHn] xs LE.a, b : nat xs : seq nat LE : size xs <= 0
distances (xs ++ [:: a; b]) =
distances (xs ++ [:: a]) ++ [:: b - a]
- a, b : nat xs : seq nat LE : size xs <= 0
distances (xs ++ [:: a; b]) =
distances (xs ++ [:: a]) ++ [:: b - a]
by move : LE; rewrite leqn0 size_eq0; move => /eqP LE; subst .
- a, b, n : nat IHn : forall xs : seq nat,
size xs <= n ->
distances (xs ++ [:: a; b]) = distances (xs ++ [:: a]) ++ [:: b - a]xs : seq nat LE : size xs <= n.+1
distances (xs ++ [:: a; b]) =
distances (xs ++ [:: a]) ++ [:: b - a]
destruct xs as [ | x0 xs]; first by unfold distances.a, b, n : nat IHn : forall xs : seq nat,
size xs <= n ->
distances (xs ++ [:: a; b]) = distances (xs ++ [:: a]) ++ [:: b - a]x0 : nat xs : seq nat LE : size (x0 :: xs) <= n.+1
distances ((x0 :: xs) ++ [:: a; b]) =
distances ((x0 :: xs) ++ [:: a]) ++ [:: b - a]
destruct xs as [ | x1 xs]; first by unfold distances.a, b, n : nat IHn : forall xs : seq nat,
size xs <= n ->
distances (xs ++ [:: a; b]) = distances (xs ++ [:: a]) ++ [:: b - a]x0, x1 : nat xs : seq nat LE : size [:: x0, x1 & xs] <= n.+1
distances ([:: x0, x1 & xs] ++ [:: a; b]) =
distances ([:: x0, x1 & xs] ++ [:: a]) ++ [:: b - a]
have -> : distances ([:: x0, x1 & xs] ++ [:: a; b]) = x1 - x0 :: distances ((x1 :: xs) ++ [:: a; b]).a, b, n : nat IHn : forall xs : seq nat,
size xs <= n ->
distances (xs ++ [:: a; b]) = distances (xs ++ [:: a]) ++ [:: b - a]x0, x1 : nat xs : seq nat LE : size [:: x0, x1 & xs] <= n.+1
distances ([:: x0, x1 & xs] ++ [:: a; b]) =
x1 - x0 :: distances ((x1 :: xs) ++ [:: a; b])
{ a, b, n : nat IHn : forall xs : seq nat,
size xs <= n ->
distances (xs ++ [:: a; b]) = distances (xs ++ [:: a]) ++ [:: b - a]x0, x1 : nat xs : seq nat LE : size [:: x0, x1 & xs] <= n.+1
distances ([:: x0, x1 & xs] ++ [:: a; b]) =
x1 - x0 :: distances ((x1 :: xs) ++ [:: a; b])
by simpl ; rewrite distances_unfold_2cons. } a, b, n : nat IHn : forall xs : seq nat,
size xs <= n ->
distances (xs ++ [:: a; b]) = distances (xs ++ [:: a]) ++ [:: b - a]x0, x1 : nat xs : seq nat LE : size [:: x0, x1 & xs] <= n.+1
x1 - x0 :: distances ((x1 :: xs) ++ [:: a; b]) =
distances ([:: x0, x1 & xs] ++ [:: a]) ++ [:: b - a]
rewrite IHn; last by simpl in *; rewrite -(leq_add2r 1 ) !addn1.a, b, n : nat IHn : forall xs : seq nat,
size xs <= n ->
distances (xs ++ [:: a; b]) = distances (xs ++ [:: a]) ++ [:: b - a]x0, x1 : nat xs : seq nat LE : size [:: x0, x1 & xs] <= n.+1
x1 - x0
:: distances ((x1 :: xs) ++ [:: a]) ++ [:: b - a] =
distances ([:: x0, x1 & xs] ++ [:: a]) ++ [:: b - a]
have -> : distances ([:: x0, x1 & xs] ++ [:: a]) = x1 - x0 :: distances ((x1 :: xs) ++ [:: a]); last by done .a, b, n : nat IHn : forall xs : seq nat,
size xs <= n ->
distances (xs ++ [:: a; b]) = distances (xs ++ [:: a]) ++ [:: b - a]x0, x1 : nat xs : seq nat LE : size [:: x0, x1 & xs] <= n.+1
distances ([:: x0, x1 & xs] ++ [:: a]) =
x1 - x0 :: distances ((x1 :: xs) ++ [:: a])
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 :
forall x xs ,
size xs >= 1 ->
distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs].forall (x : nat) (xs : seq nat),
0 < size xs ->
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
Proof .forall (x : nat) (xs : seq nat),
0 < size xs ->
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
intros x xs POS.x : nat xs : seq nat POS : 0 < size xs
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
have EX: exists n , size xs <= n by (exists (size xs )).x : nat xs : seq nat POS : 0 < size xsEX : exists n : nat, size xs <= n
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
destruct EX as [n LE].x : nat xs : seq nat POS : 0 < size xsn : nat LE : size xs <= n
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
elim : n x xs LE POS => [ |n IHn] x xs LE POS.x : nat xs : seq nat LE : size xs <= 0 POS : 0 < size xs
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
- x : nat xs : seq nat LE : size xs <= 0 POS : 0 < size xs
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
by move : LE; rewrite leqn0 size_eq0; move => /eqP LE; subst .
- n : nat IHn : forall (x : nat) (xs : seq nat),
size xs <= n ->
0 < size xs -> distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs]x : nat xs : seq nat LE : size xs <= n.+1 POS : 0 < size xs
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
move : LE; rewrite leq_eqVlt; move => /orP [/eqP LEN' | LE]; last first .n : nat IHn : forall (x : nat) (xs : seq nat),
size xs <= n ->
0 < size xs -> distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs]x : nat xs : seq nat POS : 0 < size xsLE : size xs < n.+1
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
+ n : nat IHn : forall (x : nat) (xs : seq nat),
size xs <= n ->
0 < size xs -> distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs]x : nat xs : seq nat POS : 0 < size xsLE : size xs < n.+1
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
by rewrite ltnS in LE; apply IHn.
+ n : nat IHn : forall (x : nat) (xs : seq nat),
size xs <= n ->
0 < size xs -> distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs]x : nat xs : seq nat POS : 0 < size xsLEN' : size xs = n.+1
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
destruct (seq_elim_last _ _ LEN') as [x__new [xs__l [EQ2 LEN]]].n : nat IHn : forall (x : nat) (xs : seq nat),
size xs <= n ->
0 < size xs -> distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs]x : nat xs : seq nat POS : 0 < size xsLEN' : size xs = n.+1 x__new : nat xs__l : seq nat EQ2 : xs = xs__l ++ [:: x__new] LEN : size xs__l = n
distances (xs ++ [:: x]) =
distances xs ++ [:: x - last0 xs]
subst xs; clear LEN' POS; rename xs__l into xs.n : nat IHn : forall (x : nat) (xs : seq nat),
size xs <= n ->
0 < size xs -> distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs]x, x__new : nat xs : seq nat LEN : size xs = n
distances ((xs ++ [:: x__new]) ++ [:: x]) =
distances (xs ++ [:: x__new]) ++
[:: x - last0 (xs ++ [:: x__new])]
rewrite -catA.n : nat IHn : forall (x : nat) (xs : seq nat),
size xs <= n ->
0 < size xs -> distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs]x, x__new : nat xs : seq nat LEN : size xs = n
distances (xs ++ [:: x__new] ++ [:: x]) =
distances (xs ++ [:: x__new]) ++
[:: x - last0 (xs ++ [:: x__new])]
rewrite distances_unfold_2app_last.n : nat IHn : forall (x : nat) (xs : seq nat),
size xs <= n ->
0 < size xs -> distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs]x, x__new : nat xs : seq nat LEN : size xs = n
distances (xs ++ [:: x__new]) ++ [:: x - x__new] =
distances (xs ++ [:: x__new]) ++
[:: x - last0 (xs ++ [:: x__new])]
destruct xs; first by done .n : nat IHn : forall (x : nat) (xs : seq nat),
size xs <= n ->
0 < size xs -> distances (xs ++ [:: x]) = distances xs ++ [:: x - last0 xs]x, x__new, n0 : nat xs : seq nat LEN : size (n0 :: xs) = n
distances ((n0 :: xs) ++ [:: x__new]) ++
[:: x - x__new] =
distances ((n0 :: xs) ++ [:: x__new]) ++
[:: x - last0 ((n0 :: xs) ++ [:: x__new])]
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 :
forall (xs : seq nat) (n : nat),
xs[|n.+1 |] - xs[|n|] <= max0 (distances xs).forall (xs : seq nat) (n : nat),
xs [|n.+1 |] - xs [|n|] <= max0 (distances xs)
Proof .forall (xs : seq nat) (n : nat),
xs [|n.+1 |] - xs [|n|] <= max0 (distances xs)
intros xs id.xs : seq nat id : nat
xs [|id.+1 |] - xs [|id|] <= max0 (distances xs)
apply leq_trans with (distances xs [| id |]).xs : seq nat id : nat
xs [|id.+1 |] - xs [|id|] <= distances xs [|id|]
- xs : seq nat id : nat
xs [|id.+1 |] - xs [|id|] <= distances xs [|id|]
rewrite leq_eqVlt; apply /orP; left ; apply /eqP.xs : seq nat id : nat
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
have EX: exists n , size xs <= n by (exists (size xs )).xs : seq nat id : nat EX : exists n : nat, size xs <= n
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
move : EX => [n LE]; move : xs id LE.n : nat
forall (xs : seq nat) (id : nat),
size xs <= n ->
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
elim : n => [ |n IHn] xs id LE.xs : seq nat id : nat LE : size xs <= 0
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
{ xs : seq nat id : nat LE : size xs <= 0
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
move : LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst .id : nat
[::] [|id.+1 |] - [::] [|id|] = distances [::] [|id|]
by rewrite !nth_default.
} n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]xs : seq nat id : nat LE : size xs <= n.+1
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
{ n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]xs : seq nat id : nat LE : size xs <= n.+1
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
move : LE; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT]; last first .n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]xs : seq nat id : nat LT : size xs < n.+1
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
{ n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]xs : seq nat id : nat LT : size xs < n.+1
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
by apply IHn; rewrite ltnS in LT. } n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]xs : seq nat id : nat EQ : size xs = n.+1
xs [|id.+1 |] - xs [|id|] = distances xs [|id|]
destruct xs as [ | n0 xs]; first by done .n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]n0 : nat xs : seq nat id : nat EQ : size (n0 :: xs) = n.+1
(n0 :: xs) [|id.+1 |] - (n0 :: xs) [|id|] =
distances (n0 :: xs) [|id|]
destruct xs as [ | n1 xs]; first by destruct id; [simpl |rewrite !nth_default].n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]n0, n1 : nat xs : seq nat id : nat EQ : size [:: n0, n1 & xs] = n.+1
[:: n0, n1 & xs] [|id.+1 |] - [:: n0, n1 & xs] [|id|] =
distances [:: n0, n1 & xs] [|id|]
have ->: distances [:: n0, n1 & xs] = (n1 - n0) :: distances [:: n1 & xs].n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]n0, n1 : nat xs : seq nat id : nat EQ : size [:: n0, n1 & xs] = n.+1
distances [:: n0, n1 & xs] =
n1 - n0 :: distances (n1 :: xs)
{ n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]n0, n1 : nat xs : seq nat id : nat EQ : size [:: n0, n1 & xs] = n.+1
distances [:: n0, n1 & xs] =
n1 - n0 :: distances (n1 :: xs)
by rewrite /distances //= drop0. } n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]n0, n1 : nat xs : seq nat id : nat EQ : size [:: n0, n1 & xs] = n.+1
[:: n0, n1 & xs] [|id.+1 |] - [:: n0, n1 & xs] [|id|] =
(n1 - n0 :: distances (n1 :: xs)) [|id|]
destruct id; first by done .n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]n0, n1 : nat xs : seq nat id : nat EQ : size [:: n0, n1 & xs] = n.+1
[:: n0, n1 & xs] [|id.+2 |] -
[:: n0, n1 & xs] [|id.+1 |] =
(n1 - n0 :: distances (n1 :: xs)) [|id.+1 |]
rewrite //= -IHn //=.n : nat IHn : forall (xs : seq nat) (id : nat),
size xs <= n -> xs [|id.+1 |] - xs [|id|] = distances xs [|id|]n0, n1 : nat xs : seq nat id : nat EQ : size [:: n0, n1 & xs] = n.+1
size xs < n
by move : EQ => /eqP; rewrite //= eqSS => /eqP EQ; rewrite -EQ.
}
- xs : seq nat id : nat
distances xs [|id|] <= max0 (distances xs)
have Lem: forall xs x , x \in xs -> x <= max0 xs.xs : seq nat id : nat
forall
(xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality)
(x : nat), x \in xs -> x <= max0 xs
{ xs : seq nat id : nat
forall
(xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality)
(x : nat), x \in xs -> x <= max0 xs
clear ; elim => [//|a xs IHxs] x IN.a : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality IHxs : forall x : nat, x \in xs -> x <= max0 xsx : nat IN : x \in a :: xs
x <= max0 (a :: xs)
rewrite max0_cons leq_max; apply /orP.a : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality IHxs : forall x : nat, x \in xs -> x <= max0 xsx : nat IN : x \in a :: xs
x <= a \/ x <= max0 xs
move : IN; rewrite in_cons; move => /orP [/eqP EQ| IN].a : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality IHxs : forall x : nat, x \in xs -> x <= max0 xsx : nat EQ : x = a
x <= a \/ x <= max0 xs
+ a : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality IHxs : forall x : nat, x \in xs -> x <= max0 xsx : nat EQ : x = a
x <= a \/ x <= max0 xs
by left ; subst .
+ a : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality IHxs : forall x : nat, x \in xs -> x <= max0 xsx : nat IN : x \in xs
x <= a \/ x <= max0 xs
by right ; apply IHxs.
} xs : seq nat id : nat Lem : forall (xs : seq_predType Datatypes_nat__canonical__eqtype_Equality)
(x : nat), x \in xs -> x <= max0 xs
distances xs [|id|] <= max0 (distances xs)
destruct (size (distances xs) <= id) eqn :SIZE.xs : seq nat id : nat Lem : forall (xs : seq_predType Datatypes_nat__canonical__eqtype_Equality)
(x : nat), x \in xs -> x <= max0 xsSIZE : (size (distances xs) <= id) = true
distances xs [|id|] <= max0 (distances xs)
+ xs : seq nat id : nat Lem : forall (xs : seq_predType Datatypes_nat__canonical__eqtype_Equality)
(x : nat), x \in xs -> x <= max0 xsSIZE : (size (distances xs) <= id) = true
distances xs [|id|] <= max0 (distances xs)
by rewrite nth_default.
+ xs : seq nat id : nat Lem : forall (xs : seq_predType Datatypes_nat__canonical__eqtype_Equality)
(x : nat), x \in xs -> x <= max0 xsSIZE : (size (distances xs) <= id) = false
distances xs [|id|] <= max0 (distances xs)
apply Lem; rewrite mem_nth //.xs : seq nat id : nat Lem : forall (xs : seq_predType Datatypes_nat__canonical__eqtype_Equality)
(x : nat), x \in xs -> x <= max0 xsSIZE : (size (distances xs) <= id) = false
id < size (distances xs)
move : SIZE => /negP /negP.xs : seq nat id : nat Lem : forall (xs : seq_predType Datatypes_nat__canonical__eqtype_Equality)
(x : nat), x \in xs -> x <= max0 xs
~~ (size (distances xs) <= id) ->
id < size (distances xs)
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 :
forall (xs : seq nat) (n : nat),
(distances xs)[|n|] = xs[|n.+1 |] - xs[|n|].forall (xs : seq nat) (n : nat),
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]
Proof .forall (xs : seq nat) (n : nat),
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]
intros xs.xs : seq nat
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]
have EX: exists len , size xs <= len by (exists (size xs )).xs : seq nat EX : exists len : nat, size xs <= len
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]
move : EX => [len LE]; move : xs LE.len : nat
forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]
elim : len => [ |len IHlen] xs LE n.xs : seq nat LE : size xs <= 0 n : nat
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]
{ xs : seq nat LE : size xs <= 0 n : nat
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]
by move : LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst ; destruct n. } len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]xs : seq nat LE : size xs <= len.+1 n : nat
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]
move : LE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last by apply IHlen.len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]xs : seq nat n : nat EQ : size xs = len.+1
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]
destruct xs as [ | x1 xs]; first by done .len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1 : nat xs : seq nat n : nat EQ : size (x1 :: xs) = len.+1
distances (x1 :: xs) [|n|] =
(x1 :: xs) [|n.+1 |] - (x1 :: xs) [|n|]
destruct xs as [ | x2 xs]; first by destruct n as [ | [ | ]].len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1, x2 : nat xs : seq nat n : nat EQ : size [:: x1, x2 & xs] = len.+1
distances [:: x1, x2 & xs] [|n|] =
[:: x1, x2 & xs] [|n.+1 |] - [:: x1, x2 & xs] [|n|]
destruct n as [ |n]; first by done .len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1, x2 : nat xs : seq nat n : nat EQ : size [:: x1, x2 & xs] = len.+1
distances [:: x1, x2 & xs] [|n.+1 |] =
[:: x1, x2 & xs] [|n.+2 |] - [:: x1, x2 & xs] [|n.+1 |]
have ->: distances [:: x1, x2 & xs] [|n.+1 |] = distances [::x2 & xs] [| n |].len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1, x2 : nat xs : seq nat n : nat EQ : size [:: x1, x2 & xs] = len.+1
distances [:: x1, x2 & xs] [|n.+1 |] =
distances (x2 :: xs) [|n|]
{ len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1, x2 : nat xs : seq nat n : nat EQ : size [:: x1, x2 & xs] = len.+1
distances [:: x1, x2 & xs] [|n.+1 |] =
distances (x2 :: xs) [|n|]
have ->: distances [:: x1, x2 & xs] = (x2 - x1) :: distances [::x2 & xs]; last by done .len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1, x2 : nat xs : seq nat n : nat EQ : size [:: x1, x2 & xs] = len.+1
distances [:: x1, x2 & xs] =
x2 - x1 :: distances (x2 :: xs)
{ len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1, x2 : nat xs : seq nat n : nat EQ : size [:: x1, x2 & xs] = len.+1
distances [:: x1, x2 & xs] =
x2 - x1 :: distances (x2 :: xs)
by rewrite /distances //= drop0. }
} len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1, x2 : nat xs : seq nat n : nat EQ : size [:: x1, x2 & xs] = len.+1
distances (x2 :: xs) [|n|] =
[:: x1, x2 & xs] [|n.+2 |] - [:: x1, x2 & xs] [|n.+1 |]
have ->: [:: x1, x2 & xs] [|n.+2 |] - [:: x1, x2 & xs] [|n.+1 |] = [:: x2 & xs] [|n.+1 |] - [:: x2 & xs] [|n|] by done .len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1, x2 : nat xs : seq nat n : nat EQ : size [:: x1, x2 & xs] = len.+1
distances (x2 :: xs) [|n|] =
(x2 :: xs) [|n.+1 |] - (x2 :: xs) [|n|]
apply IHlen.len : nat IHlen : forall xs : seq nat,
size xs <= len ->
forall n : nat,
distances xs [|n|] = xs [|n.+1 |] - xs [|n|]x1, x2 : nat xs : seq nat n : nat EQ : size [:: x1, x2 & xs] = len.+1
size (x2 :: xs) <= len
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 :
forall (xs : seq nat),
2 <= size xs ->
size xs = size (distances xs) + 1 .forall xs : seq nat,
1 < size xs -> size xs = size (distances xs) + 1
Proof .forall xs : seq nat,
1 < size xs -> size xs = size (distances xs) + 1
intros xs.xs : seq nat
1 < size xs -> size xs = size (distances xs) + 1
have EX: exists len , size xs <= len by (exists (size xs )).xs : seq nat EX : exists len : nat, size xs <= len
1 < size xs -> size xs = size (distances xs) + 1
move : EX => [len LE]; move : xs LE.len : nat
forall xs : seq nat,
size xs <= len ->
1 < size xs -> size xs = size (distances xs) + 1
elim : len => [ |len IHlen] xs LE SIZE.xs : seq nat LE : size xs <= 0 SIZE : 1 < size xs
size xs = size (distances xs) + 1
{ xs : seq nat LE : size xs <= 0 SIZE : 1 < size xs
size xs = size (distances xs) + 1
by move : LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst . } len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 xs : seq nat LE : size xs <= len.+1 SIZE : 1 < size xs
size xs = size (distances xs) + 1
{ len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 xs : seq nat LE : size xs <= len.+1 SIZE : 1 < size xs
size xs = size (distances xs) + 1
move : LE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last by apply IHlen.len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 xs : seq nat SIZE : 1 < size xsEQ : size xs = len.+1
size xs = size (distances xs) + 1
destruct xs as [ | x1 xs]; first by inversion EQ.len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 x1 : nat xs : seq nat SIZE : 1 < size (x1 :: xs)EQ : size (x1 :: xs) = len.+1
size (x1 :: xs) = size (distances (x1 :: xs)) + 1
destruct xs as [ | x2 xs]; first by inversion SIZE.len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 x1, x2 : nat xs : seq nat SIZE : 1 < size [:: x1, x2 & xs]EQ : size [:: x1, x2 & xs] = len.+1
size [:: x1, x2 & xs] =
size (distances [:: x1, x2 & xs]) + 1
destruct xs as [ | x3 xs]; first by done .len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 x1, x2, x3 : nat xs : seq nat SIZE : 1 < size [:: x1, x2, x3 & xs]EQ : size [:: x1, x2, x3 & xs] = len.+1
size [:: x1, x2, x3 & xs] =
size (distances [:: x1, x2, x3 & xs]) + 1
clear SIZE.len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 x1, x2, x3 : nat xs : seq nat EQ : size [:: x1, x2, x3 & xs] = len.+1
size [:: x1, x2, x3 & xs] =
size (distances [:: x1, x2, x3 & xs]) + 1
have ->: size [:: x1, x2, x3 & xs] = size [:: x2, x3 & xs] + 1 by rewrite addn1.len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 x1, x2, x3 : nat xs : seq nat EQ : size [:: x1, x2, x3 & xs] = len.+1
size [:: x2, x3 & xs] + 1 =
size (distances [:: x1, x2, x3 & xs]) + 1
have ->: size (distances [:: x1, x2, x3 & xs]) = size (distances [:: x2, x3 & xs]) + 1 by rewrite addn1.len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 x1, x2, x3 : nat xs : seq nat EQ : size [:: x1, x2, x3 & xs] = len.+1
size [:: x2, x3 & xs] + 1 =
size (distances [:: x2, x3 & xs]) + 1 + 1
apply /eqP; rewrite eqn_add2r; apply /eqP.len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 x1, x2, x3 : nat xs : seq nat EQ : size [:: x1, x2, x3 & xs] = len.+1
size [:: x2, x3 & xs] =
size (distances [:: x2, x3 & xs]) + 1
apply IHlen; last by done .len : nat IHlen : forall xs : seq nat,
size xs <= len ->
1 < size xs ->
size xs = size (distances xs) + 1 x1, x2, x3 : nat xs : seq nat EQ : size [:: x1, x2, x3 & xs] = len.+1
size [:: x2, x3 & xs] <= len
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_ε :
forall n x , x \in distances (index_iota 0 n) -> x = ε.forall (n : nat)
(x : Datatypes_nat__canonical__eqtype_Equality),
x \in distances (index_iota 0 n) -> x = 1
Proof .forall (n : nat)
(x : Datatypes_nat__canonical__eqtype_Equality),
x \in distances (index_iota 0 n) -> x = 1
move => n x; elim : n => [ |n IHn] IN.x : Datatypes_nat__canonical__eqtype_Equality IN : x \in distances (index_iota 0 0 )
x = 1
- x : Datatypes_nat__canonical__eqtype_Equality IN : x \in distances (index_iota 0 0 )
x = 1
by unfold index_iota, distances in IN.
- x : Datatypes_nat__canonical__eqtype_Equality n : nat IHn : x \in distances (index_iota 0 n) -> x = 1 IN : x \in distances (index_iota 0 n.+1 )
x = 1
destruct n; first by unfold distances, index_iota in IN.x : Datatypes_nat__canonical__eqtype_Equality n : nat IHn : x \in distances (index_iota 0 n.+1 ) -> x = 1 IN : x \in distances (index_iota 0 n.+2 )
x = 1
move : IN; rewrite -addn1 /index_iota subn0 iotaD add0n.x : Datatypes_nat__canonical__eqtype_Equality n : nat IHn : x \in distances (index_iota 0 n.+1 ) -> x = 1
x \in distances (iota 0 n.+1 ++ iota n.+1 1 ) -> x = 1
rewrite distances_unfold_1app_last; last by rewrite size_iota.x : Datatypes_nat__canonical__eqtype_Equality n : nat IHn : x \in distances (index_iota 0 n.+1 ) -> x = 1
x
\in distances (iota 0 n.+1 ) ++
[:: n.+1 - last0 (iota 0 n.+1 )] -> x = 1
rewrite mem_cat => /orP [IN|IN].x : Datatypes_nat__canonical__eqtype_Equality n : nat IHn : x \in distances (index_iota 0 n.+1 ) -> x = 1 IN : x \in distances (iota 0 n.+1 )
x = 1
+ x : Datatypes_nat__canonical__eqtype_Equality n : nat IHn : x \in distances (index_iota 0 n.+1 ) -> x = 1 IN : x \in distances (iota 0 n.+1 )
x = 1
by apply IHn; rewrite /index_iota subn0; simpl .
+ x : Datatypes_nat__canonical__eqtype_Equality n : nat IHn : x \in distances (index_iota 0 n.+1 ) -> x = 1 IN : x \in [:: n.+1 - last0 (iota 0 n.+1 )]
x = 1
by move : IN;
rewrite -addn1 iotaD /last0 last_cat add0n addn1 // subSnn in_cons;
move => /orP [/eqP EQ|F]; subst .
Qed .
End Distances .
(** * Properties of Distances of Non-Decreasing Sequence *)
(** In this section, we prove a few basic lemmas about distances of non-decreasing sequences. *)
Section DistancesOfNonDecreasingSequence .
(** First we show that the max distance between elements of any nontrivial sequence
(i.e. a sequence that contains at leas two distinct elements) is positive. *)
Lemma max_distance_in_nontrivial_seq_is_positive :
forall (xs : seq nat),
nondecreasing_sequence xs ->
(exists x y , x \in xs /\ y \in xs /\ x <> y) ->
0 < max0 (distances xs).forall xs : seq nat,
nondecreasing_sequence xs ->
(exists
x y : Datatypes_nat__canonical__eqtype_Equality,
x \in xs /\ y \in xs /\ x <> y) ->
0 < max0 (distances xs)
Proof .forall xs : seq nat,
nondecreasing_sequence xs ->
(exists
x y : Datatypes_nat__canonical__eqtype_Equality,
x \in xs /\ y \in xs /\ x <> y) ->
0 < max0 (distances xs)
move => xs SIZE [x [y [INx [INy NEQ]]]].xs : seq nat SIZE : nondecreasing_sequence xs x, y : Datatypes_nat__canonical__eqtype_Equality INx : x \in xs INy : y \in xs NEQ : x <> y
0 < max0 (distances xs)
move : INx INy => /nthP INx /nthP INy; specialize (INx 0 ); specialize (INy 0 ).xs : seq nat SIZE : nondecreasing_sequence xs x, y : Datatypes_nat__canonical__eqtype_Equality NEQ : x <> y INx : exists2 i : nat, i < size xs & xs [|i|] = xINy : exists2 i : nat, i < size xs & xs [|i|] = y
0 < max0 (distances xs)
move : INx INy => [indx SIZEx EQx] [indy SIZEy EQy].xs : seq nat SIZE : nondecreasing_sequence xs x, y : Datatypes_nat__canonical__eqtype_Equality NEQ : x <> y indx : nat SIZEx : indx < size xs EQx : xs [|indx|] = x indy : nat SIZEy : indy < size xs EQy : xs [|indy|] = y
0 < max0 (distances xs)
have L: forall (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).xs : seq nat SIZE : nondecreasing_sequence xs x, y : Datatypes_nat__canonical__eqtype_Equality NEQ : x <> y indx : nat SIZEx : indx < size xs EQx : xs [|indx|] = x indy : nat SIZEy : indy < size xs EQy : xs [|indy|] = y
forall 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)
{ xs : seq nat SIZE : nondecreasing_sequence xs x, y : Datatypes_nat__canonical__eqtype_Equality NEQ : x <> y indx : nat SIZEx : indx < size xs EQx : xs [|indx|] = x indy : nat SIZEy : indy < size xs EQy : xs [|indy|] = y
forall x y indx indy : nat,
indx < size xs ->
indy < size xs ->
nondecreasing_sequence xs ->
x < y ->
xs [|indx|] = x ->
xs [|indy|] = y -> 0 < max0 (distances xs)
clear ; intros x y indx indy SIZEx SIZEy SIZE LT EQx EQy.xs : seq nat x, y, indx, indy : nat SIZEx : indx < size xs SIZEy : indy < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x EQy : xs [|indy|] = y
0 < max0 (distances xs)
have LTind: indx < indy.xs : seq nat x, y, indx, indy : nat SIZEx : indx < size xs SIZEy : indy < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x EQy : xs [|indy|] = y
indx < indy
{ xs : seq nat x, y, indx, indy : nat SIZEx : indx < size xs SIZEy : indy < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x EQy : xs [|indy|] = y
indx < indy
rewrite ltnNge; apply /negP; intros CONTR.xs : seq nat x, y, indx, indy : nat SIZEx : indx < size xs SIZEy : indy < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x EQy : xs [|indy|] = y CONTR : indy <= indx
False
subst x y; move : LT; rewrite ltnNge; move => /negP T; apply : T.xs : seq nat indx, indy : nat SIZEx : indx < size xs SIZEy : indy < size xs SIZE : nondecreasing_sequence xs CONTR : indy <= indx
xs [|indy|] <= xs [|indx|]
by apply SIZE; apply /andP. } xs : seq nat x, y, indx, indy : nat SIZEx : indx < size xs SIZEy : indy < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x EQy : xs [|indy|] = y LTind : indx < indy
0 < max0 (distances xs)
have EQ: exists Δ , indy = indx + Δ; [by exists (indy - indx); lia | move : EQ => [Δ EQ]; subst indy].xs : seq nat x, y, indx : nat SIZEx : indx < size xs Δ : nat SIZEy : indx + Δ < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x LTind : indx < indx + Δ EQy : xs [|indx + Δ|] = y
0 < max0 (distances xs)
have F: exists ind , indx <= ind < indx + Δ /\ xs[|ind|] < xs[|ind.+1 |].xs : seq nat x, y, indx : nat SIZEx : indx < size xs Δ : nat SIZEy : indx + Δ < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x LTind : indx < indx + Δ EQy : xs [|indx + Δ|] = y
exists ind : nat,
indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]
{ xs : seq nat x, y, indx : nat SIZEx : indx < size xs Δ : nat SIZEy : indx + Δ < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x LTind : indx < indx + Δ EQy : xs [|indx + Δ|] = y
exists ind : nat,
indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]
subst x y; clear SIZEx SIZEy; revert xs indx LTind SIZE LT.Δ : nat
forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat,
indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]
elim : Δ => [ |Δ IHΔ] xs indx LTind SIZE LT; first by lia .Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |]
exists ind : nat,
indx <= ind < indx + Δ.+1 /\
xs [|ind|] < xs [|ind.+1 |]
destruct (posnP Δ) as [ZERO|POS].Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] ZERO : Δ = 0
exists ind : nat,
indx <= ind < indx + Δ.+1 /\
xs [|ind|] < xs [|ind.+1 |]
{ Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] ZERO : Δ = 0
exists ind : nat,
indx <= ind < indx + Δ.+1 /\
xs [|ind|] < xs [|ind.+1 |]
by subst Δ; exists indx ; split ; [rewrite addn1; apply /andP | rewrite addn1 in LT]; auto . } Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < Δ
exists ind : nat,
indx <= ind < indx + Δ.+1 /\
xs [|ind|] < xs [|ind.+1 |]
have ALT: xs[|indx + Δ|] == xs[|indx + Δ.+1 |] \/ xs[|indx + Δ|] < xs[|indx + Δ.+1 |].Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < Δ
xs [|indx + Δ|] == xs [|indx + Δ.+1 |] \/
xs [|indx + Δ|] < xs [|indx + Δ.+1 |]
{ Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < Δ
xs [|indx + Δ|] == xs [|indx + Δ.+1 |] \/
xs [|indx + Δ|] < xs [|indx + Δ.+1 |]
apply /orP; rewrite -leq_eqVlt addnS.Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < Δ
xs [|indx + Δ|] <= xs [|(indx + Δ).+1 |]
apply SIZE; apply /andP; split ; first by done .Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < Δ
(indx + Δ).+1 < size xs
rewrite ltnNge; apply /negP; intros CONTR.Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < ΔCONTR : size xs <= (indx + Δ).+1
False
move : LT; rewrite ltnNge; move => /negP LT; apply : LT.Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs POS : 0 < ΔCONTR : size xs <= (indx + Δ).+1
xs [|indx + Δ.+1 |] <= xs [|indx|]
by rewrite nth_default ?addnS . } Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < ΔALT : xs [|indx + Δ|] == xs [|indx + Δ.+1 |] \/
xs [|indx + Δ|] < xs [|indx + Δ.+1 |]
exists ind : nat,
indx <= ind < indx + Δ.+1 /\
xs [|ind|] < xs [|ind.+1 |]
move : ALT => [/eqP EQ|LT'].Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < ΔEQ : xs [|indx + Δ|] = xs [|indx + Δ.+1 |]
exists ind : nat,
indx <= ind < indx + Δ.+1 /\
xs [|ind|] < xs [|ind.+1 |]
- Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < ΔEQ : xs [|indx + Δ|] = xs [|indx + Δ.+1 |]
exists ind : nat,
indx <= ind < indx + Δ.+1 /\
xs [|ind|] < xs [|ind.+1 |]
edestruct (IHΔ) as [ind [B UP]]; eauto 5 using addn1, leq_add2l.Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < ΔEQ : xs [|indx + Δ|] = xs [|indx + Δ.+1 |] ind : nat B : indx <= ind < indx + Δ UP : xs [|ind|] < xs [|ind.+1 |]
exists ind : nat,
indx <= ind < indx + Δ.+1 /\
xs [|ind|] < xs [|ind.+1 |]
exists ind ; split ; last by done .Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < ΔEQ : xs [|indx + Δ|] = xs [|indx + Δ.+1 |] ind : nat B : indx <= ind < indx + Δ UP : xs [|ind|] < xs [|ind.+1 |]
indx <= ind < indx + Δ.+1
move : B => /andP [B1 B2]; apply /andP; split ; first by done .Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < ΔEQ : xs [|indx + Δ|] = xs [|indx + Δ.+1 |] ind : nat UP : xs [|ind|] < xs [|ind.+1 |] B1 : indx <= ind B2 : ind < indx + Δ
ind < indx + Δ.+1
by rewrite addnS ltnS ltnW.
- Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < ΔLT' : xs [|indx + Δ|] < xs [|indx + Δ.+1 |]
exists ind : nat,
indx <= ind < indx + Δ.+1 /\
xs [|ind|] < xs [|ind.+1 |]
exists (indx + Δ); split ; last by rewrite -addnS.Δ : nat IHΔ : forall (xs : seq nat) (indx : nat),
indx < indx + Δ ->
nondecreasing_sequence xs ->
xs [|indx|] < xs [|indx + Δ|] ->
exists ind : nat, indx <= ind < indx + Δ /\ xs [|ind|] < xs [|ind.+1 |]xs : seq nat indx : nat LTind : indx < indx + Δ.+1 SIZE : nondecreasing_sequence xs LT : xs [|indx|] < xs [|indx + Δ.+1 |] POS : 0 < ΔLT' : xs [|indx + Δ|] < xs [|indx + Δ.+1 |]
indx <= indx + Δ < indx + Δ.+1
by apply /andP; split ; [rewrite leq_addr | rewrite addnS]. } xs : seq nat x, y, indx : nat SIZEx : indx < size xs Δ : nat SIZEy : indx + Δ < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x LTind : indx < indx + Δ EQy : xs [|indx + Δ|] = y F : exists ind : nat,
indx <= ind < indx + Δ /\
xs [|ind|] < xs [|ind.+1 |]
0 < max0 (distances xs)
move : F => [ind [/andP [B1 B2] UP]].xs : seq nat x, y, indx : nat SIZEx : indx < size xs Δ : nat SIZEy : indx + Δ < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x LTind : indx < indx + Δ EQy : xs [|indx + Δ|] = y ind : nat B1 : indx <= ind B2 : ind < indx + Δ UP : xs [|ind|] < xs [|ind.+1 |]
0 < max0 (distances xs)
apply leq_trans with (xs [|ind.+1 |] - xs [|ind|]).xs : seq nat x, y, indx : nat SIZEx : indx < size xs Δ : nat SIZEy : indx + Δ < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x LTind : indx < indx + Δ EQy : xs [|indx + Δ|] = y ind : nat B1 : indx <= ind B2 : ind < indx + Δ UP : xs [|ind|] < xs [|ind.+1 |]
0 < xs [|ind.+1 |] - xs [|ind|]
- xs : seq nat x, y, indx : nat SIZEx : indx < size xs Δ : nat SIZEy : indx + Δ < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x LTind : indx < indx + Δ EQy : xs [|indx + Δ|] = y ind : nat B1 : indx <= ind B2 : ind < indx + Δ UP : xs [|ind|] < xs [|ind.+1 |]
0 < xs [|ind.+1 |] - xs [|ind|]
by rewrite subn_gt0.
- xs : seq nat x, y, indx : nat SIZEx : indx < size xs Δ : nat SIZEy : indx + Δ < size xs SIZE : nondecreasing_sequence xs LT : x < y EQx : xs [|indx|] = x LTind : indx < indx + Δ EQy : xs [|indx + Δ|] = y ind : nat B1 : indx <= ind B2 : ind < indx + Δ UP : xs [|ind|] < xs [|ind.+1 |]
xs [|ind.+1 |] - xs [|ind|] <= max0 (distances xs)
by apply distance_between_neighboring_elements_le_max_distance_in_seq.
} xs : seq nat SIZE : nondecreasing_sequence xs x, y : Datatypes_nat__canonical__eqtype_Equality NEQ : x <> y indx : nat SIZEx : indx < size xs EQx : xs [|indx|] = x indy : nat SIZEy : indy < size xs EQy : xs [|indy|] = y L : forall 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)
0 < max0 (distances xs)
move : NEQ => /eqP; rewrite neq_ltn; move => /orP [LT|LT].xs : seq nat SIZE : nondecreasing_sequence xs x, y : Datatypes_nat__canonical__eqtype_Equality indx : nat SIZEx : indx < size xs EQx : xs [|indx|] = x indy : nat SIZEy : indy < size xs EQy : xs [|indy|] = y L : forall 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)LT : x < y
0 < max0 (distances xs)
- xs : seq nat SIZE : nondecreasing_sequence xs x, y : Datatypes_nat__canonical__eqtype_Equality indx : nat SIZEx : indx < size xs EQx : xs [|indx|] = x indy : nat SIZEy : indy < size xs EQy : xs [|indy|] = y L : forall 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)LT : x < y
0 < max0 (distances xs)
by eapply L with (indx := indx) (x := x) (y := y); eauto .
- xs : seq nat SIZE : nondecreasing_sequence xs x, y : Datatypes_nat__canonical__eqtype_Equality indx : nat SIZEx : indx < size xs EQx : xs [|indx|] = x indy : nat SIZEy : indy < size xs EQy : xs [|indy|] = y L : forall 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)LT : y < x
0 < max0 (distances xs)
by eapply L with (indx := indy) (indy := indx) (x := y) (y := x); eauto .
Qed .
(** Given a non-decreasing sequence [xs] with length [n], we show that the difference
between the last element of [xs] and the last element of the distances-sequence
of [xs] is equal to [xs[n-2]]. *)
Lemma last_seq_minus_last_distance_seq :
forall (xs : seq nat),
nondecreasing_sequence xs ->
last0 xs - last0 (distances xs) = xs [| (size xs).-2 |].forall xs : seq nat,
nondecreasing_sequence xs ->
last0 xs - last0 (distances xs) = xs [|(size xs).-2 |]
Proof .forall xs : seq nat,
nondecreasing_sequence xs ->
last0 xs - last0 (distances xs) = xs [|(size xs).-2 |]
unfold nondecreasing_sequence in *.forall xs : seq nat,
(forall n1 n2 : nat,
n1 <= n2 < size xs -> xs [|n1|] <= xs [|n2|]) ->
last0 xs - last0 (distances xs) = xs [|(size xs).-2 |]
intros xs SIS.xs : seq nat SIS : forall n1 n2 : nat, n1 <= n2 < size xs -> xs [|n1|] <= xs [|n2|]
last0 xs - last0 (distances xs) = xs [|(size xs).-2 |]
destruct xs as [ | x1 xs]; first by done .x1 : nat xs : seq nat SIS : forall n1 n2 : nat,
n1 <= n2 < size (x1 :: xs) -> (x1 :: xs) [|n1|] <= (x1 :: xs) [|n2|]
last0 (x1 :: xs) - last0 (distances (x1 :: xs)) =
(x1 :: xs) [|(size (x1 :: xs)).-2 |]
destruct xs as [ | x2 xs]; first by rewrite subn0.x1, x2 : nat xs : seq nat SIS : forall n1 n2 : nat,
n1 <= n2 < size [:: x1, x2 & xs] ->
[:: x1, x2 & xs] [|n1|] <= [:: x1, x2 & xs] [|n2|]
last0 [:: x1, x2 & xs] -
last0 (distances [:: x1, x2 & xs]) =
[:: x1, x2 & xs] [|(size [:: x1, x2 & xs]).-2 |]
rewrite {2 }/last0 -[in X in _ - X]nth_last function_of_distances_is_correct prednK; last by done .x1, x2 : nat xs : seq nat SIS : forall n1 n2 : nat,
n1 <= n2 < size [:: x1, x2 & xs] ->
[:: x1, x2 & xs] [|n1|] <= [:: x1, x2 & xs] [|n2|]
last0 [:: x1, x2 & xs] -
([:: x1, x2 & xs]
[|size (distances [:: x1, x2 & xs])|] -
[:: x1, x2 & xs]
[|(size (distances [:: x1, x2 & xs])).-1 |]) =
[:: x1, x2 & xs] [|(size [:: x1, x2 & xs]).-2 |]
set [:: x1, x2 & xs] as X.x1, x2 : nat xs : seq nat SIS : forall n1 n2 : nat,
n1 <= n2 < size [:: x1, x2 & xs] ->
[:: x1, x2 & xs] [|n1|] <= [:: x1, x2 & xs] [|n2|]X := [:: x1, x2 & xs] : seq nat
last0 X -
(X [|size (distances X)|] -
X [|(size (distances X)).-1 |]) = X [|(size X).-2 |]
rewrite /last0 -nth_last size_of_seq_of_distances; last by done .x1, x2 : nat xs : seq nat SIS : forall n1 n2 : nat,
n1 <= n2 < size [:: x1, x2 & xs] ->
[:: x1, x2 & xs] [|n1|] <= [:: x1, x2 & xs] [|n2|]X := [:: x1, x2 & xs] : seq nat
X [|(size (distances X) + 1 ).-1 |] -
(X [|size (distances X)|] -
X [|(size (distances X)).-1 |]) =
X [|(size (distances X) + 1 ).-2 |]
rewrite !addn1 -pred_Sn subKn; first by done .x1, x2 : nat xs : seq nat SIS : forall n1 n2 : nat,
n1 <= n2 < size [:: x1, x2 & xs] ->
[:: x1, x2 & xs] [|n1|] <= [:: x1, x2 & xs] [|n2|]X := [:: x1, x2 & xs] : seq nat
X [|(size (distances X)).-1 |] <=
X [|size (distances X)|]
rewrite /X; apply SIS; apply /andP; split ; first by simpl .x1, x2 : nat xs : seq nat SIS : forall n1 n2 : nat,
n1 <= n2 < size [:: x1, x2 & xs] ->
[:: x1, x2 & xs] [|n1|] <= [:: x1, x2 & xs] [|n2|]X := [:: x1, x2 & xs] : seq nat
size (distances [:: x1, x2 & xs]) <
size [:: x1, x2 & xs]
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 :
forall (xs : seq nat),
nondecreasing_sequence xs ->
max0 (distances xs) <= last0 xs.forall xs : seq nat,
nondecreasing_sequence xs ->
max0 (distances xs) <= last0 xs
Proof .forall xs : seq nat,
nondecreasing_sequence xs ->
max0 (distances xs) <= last0 xs
move => xs H.xs : seq nat H : nondecreasing_sequence xs
max0 (distances xs) <= last0 xs
have SIZE: size xs < 2 \/ 2 <= size xs.xs : seq nat H : nondecreasing_sequence xs
size xs < 2 \/ 1 < size xs
{ xs : seq nat H : nondecreasing_sequence xs
size xs < 2 \/ 1 < size xs
by destruct (size xs) as [ | n]; last destruct n; auto . } xs : seq nat H : nondecreasing_sequence xs SIZE : size xs < 2 \/ 1 < size xs
max0 (distances xs) <= last0 xs
move : SIZE => [LT | SIZE2].xs : seq nat H : nondecreasing_sequence xs LT : size xs < 2
max0 (distances xs) <= last0 xs
{ xs : seq nat H : nondecreasing_sequence xs LT : size xs < 2
max0 (distances xs) <= last0 xs
by destruct xs as [ |? xs]; last destruct xs. } xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xs
max0 (distances xs) <= last0 xs
apply leq_trans with (last0 xs - first0 xs); last by apply leq_subr.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xs
max0 (distances xs) <= last0 xs - first0 xs
have F: forall xs c , (forall x , x \in xs -> x <= c) -> max0 xs <= c.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xs
forall
(xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality)
(c : nat),
(forall x : nat, x \in xs -> x <= c) -> max0 xs <= c
{ xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xs
forall
(xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality)
(c : nat),
(forall x : nat, x \in xs -> x <= c) -> max0 xs <= c
clear ; move => xs c H.xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality c : nat H : forall x : nat, x \in xs -> x <= c
max0 xs <= c
elim : xs H => [//|a xs IHxs] H.c : nat a : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality IHxs : (forall x : nat, x \in xs -> x <= c) ->
max0 xs <= c H : forall x : nat, x \in a :: xs -> x <= c
max0 (a :: xs) <= c
rewrite max0_cons geq_max; apply /andP; split .c : nat a : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality IHxs : (forall x : nat, x \in xs -> x <= c) ->
max0 xs <= c H : forall x : nat, x \in a :: xs -> x <= c
a <= c
+ c : nat a : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality IHxs : (forall x : nat, x \in xs -> x <= c) ->
max0 xs <= c H : forall x : nat, x \in a :: xs -> x <= c
a <= c
by apply H; rewrite in_cons; apply /orP; left .
+ c : nat a : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality IHxs : (forall x : nat, x \in xs -> x <= c) ->
max0 xs <= c H : forall x : nat, x \in a :: xs -> x <= c
max0 xs <= c
by apply IHxs; intros ; apply H; rewrite in_cons; apply /orP; right .
} xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsF : forall
(xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality)
(c : nat),
(forall x : nat, x \in xs -> x <= c) ->
max0 xs <= c
max0 (distances xs) <= last0 xs - first0 xs
apply : F => d IN.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd : nat IN : d \in distances xs
d <= last0 xs - first0 xs
move : IN => /nthP T; specialize (T 0 ); move : T => [idx IN DIST].xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : distances xs [|idx|] = d
d <= last0 xs - first0 xs
rewrite function_of_distances_is_correct in DIST.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d
d <= last0 xs - first0 xs
rewrite -DIST leq_sub //.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d
xs [|idx.+1 |] <= last0 xs
{ xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d
xs [|idx.+1 |] <= last0 xs
destruct (xs [|idx.+1 |] == last0 xs) eqn :EQ.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = true
xs [|idx.+1 |] <= last0 xs
- xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = true
xs [|idx.+1 |] <= last0 xs
by rewrite leq_eqVlt; apply /orP; left .
- xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = false
xs [|idx.+1 |] <= last0 xs
rewrite /last0 -nth_last.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = false
xs [|idx.+1 |] <= xs [|(size xs).-1 |]
apply H.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = false
idx < (size xs).-1 < size xs
rewrite -(ltn_add2r 1 ) addn1 -size_of_seq_of_distances in IN; last by done .xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = false IN : idx.+1 < size xs
idx < (size xs).-1 < size xs
move : IN; rewrite leq_eqVlt; move => /orP [/eqP KK|KK].xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = false KK : idx.+2 = size xs
idx < (size xs).-1 < size xs
+ xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = false KK : idx.+2 = size xs
idx < (size xs).-1 < size xs
move : EQ; rewrite /last0 -nth_last -{1 }KK -[_.+2 .-1 ]pred_Sn; move => /eqP; by done .
+ xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = false KK : idx.+2 < size xs
idx < (size xs).-1 < size xs
apply /andP; split ; first rewrite -(ltn_add2r 1 ) !addn1 prednK //.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (xs [|idx.+1 |] == last0 xs) = false KK : idx.+2 < size xs
(size xs).-1 < size xs
by rewrite prednK //; apply ltn_trans with idx.+2 .
} xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d
first0 xs <= xs [|idx|]
{ xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d
first0 xs <= xs [|idx|]
destruct (first0 xs == xs [|idx|]) eqn :EQ.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (first0 xs == xs [|idx|]) = true
first0 xs <= xs [|idx|]
- xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (first0 xs == xs [|idx|]) = true
first0 xs <= xs [|idx|]
by rewrite leq_eqVlt; apply /orP; left .
- xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (first0 xs == xs [|idx|]) = false
first0 xs <= xs [|idx|]
rewrite /first0 -nth0.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (first0 xs == xs [|idx|]) = false
xs [|0 |] <= xs [|idx|]
apply H.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat IN : idx < size (distances xs) DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (first0 xs == xs [|idx|]) = false
0 <= idx < size xs
rewrite -(ltn_add2r 1 ) addn1 -size_of_seq_of_distances in IN; last by done .xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat DIST : xs [|idx.+1 |] - xs [|idx|] = d EQ : (first0 xs == xs [|idx|]) = false IN : idx.+1 < size xs
0 <= idx < size xs
destruct idx as [ |idx]; first by move : EQ; rewrite /first0 -nth0; move => /eqP.xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat DIST : xs [|idx.+2 |] - xs [|idx.+1 |] = d EQ : (first0 xs == xs [|idx.+1 |]) = false IN : idx.+2 < size xs
0 <= idx.+1 < size xs
apply /andP; split ; first by done .xs : seq nat H : nondecreasing_sequence xs SIZE2 : 1 < size xsd, idx : nat DIST : xs [|idx.+2 |] - xs [|idx.+1 |] = d EQ : (first0 xs == xs [|idx.+1 |]) = false IN : idx.+2 < size xs
idx.+1 < size xs
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 :
forall xs k ,
(forall x , x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] = [seq x <- distances xs | 0 < x].forall
(xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality)
(k : nat),
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]
Proof .forall
(xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality)
(k : nat),
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]
intros xs.xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]
have EX: exists len , size xs <= len by (exists (size xs )).xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality EX : exists len : nat, size xs <= len
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]
destruct EX as [n BO].xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality n : nat BO : size xs <= n
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]
elim : n xs BO => [ |n IHn] xs Len k Bound NonDec.xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality Len : size xs <= 0 k : nat Bound : forall x : nat, x \in xs -> x <= kNonDec : nondecreasing_sequence xs
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]
{ xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality Len : size xs <= 0 k : nat Bound : forall x : nat, x \in xs -> x <= kNonDec : nondecreasing_sequence xs
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]
move : Len; rewrite leqn0 size_eq0; move => /eqP T; subst .k : nat NonDec : nondecreasing_sequence [::] Bound : forall x : nat, x \in [::] -> x <= k
distances [seq ρ <- index_iota 0 k.+1 | ρ \in [::]] =
[seq x <- distances [::] | 0 < x]
by rewrite filter_pred0.
} n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality Len : size xs <= n.+1 k : nat Bound : forall x : nat, x \in xs -> x <= kNonDec : nondecreasing_sequence xs
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]
{ n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]xs : seq_predType
Datatypes_nat__canonical__eqtype_Equality Len : size xs <= n.+1 k : nat Bound : forall x : nat, x \in xs -> x <= kNonDec : nondecreasing_sequence xs
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]
destruct xs as [ |x1 [ |x2 xs]].n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]Len : size [::] <= n.+1 k : nat Bound : forall x : nat, x \in [::] -> x <= kNonDec : nondecreasing_sequence [::]
distances [seq ρ <- index_iota 0 k.+1 | ρ \in [::]] =
[seq x <- distances [::] | 0 < x]
- n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]Len : size [::] <= n.+1 k : nat Bound : forall x : nat, x \in [::] -> x <= kNonDec : nondecreasing_sequence [::]
distances [seq ρ <- index_iota 0 k.+1 | ρ \in [::]] =
[seq x <- distances [::] | 0 < x]
by rewrite filter_pred0.
- n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1 : Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1] <= n.+1 k : nat Bound : forall x : nat, x \in [:: x1] -> x <= kNonDec : nondecreasing_sequence [:: x1]
distances [seq ρ <- index_iota 0 k.+1 | ρ \in [:: x1]] =
[seq x <- distances [:: x1] | 0 < x]
by rewrite index_iota_filter_singl; last (rewrite ltnS; apply Bound; rewrite in_cons; apply /orP; left ).
- n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs]
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
have LEx1: x1 <= k by apply Bound; rewrite in_cons eq_refl.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
have LEx2: x2 <= k by apply Bound; rewrite !in_cons eq_refl orbT.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
have M1: forall y : nat, y \in x2 :: xs -> x1 <= y by apply nondecreasing_sequence_cons_min.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= y
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
have M2: forall x : nat, x \in x2 :: xs -> x <= k by intros ; apply Bound; rewrite in_cons; apply /orP; right .n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= k
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
have M3: forall y : nat, y \in xs -> x2 <= y by apply nondecreasing_sequence_cons in NonDec; apply nondecreasing_sequence_cons_min.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= y
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec).n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 = x2
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
+ n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 = x2
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
subst ; rewrite distances_unfold_2cons.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x2, x2 & xs] <= n.+1 k : nat LEx1 : x2 <= k NonDec : nondecreasing_sequence [:: x2, x2 & xs] Bound : forall x : nat,
x \in [:: x2, x2 & xs] -> x <= kLEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x2 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= y
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x2, x2 & xs]] =
[seq x <- x2 - x2 :: distances (x2 :: xs) | 0 < x]
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.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x2, x2 & xs] <= n.+1 k : nat LEx1 : x2 <= k NonDec : nondecreasing_sequence [:: x2, x2 & xs] Bound : forall x : nat,
x \in [:: x2, x2 & xs] -> x <= kLEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x2 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= y
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x2, x2 & xs]] =
[seq x <- distances (x2 :: xs) | 0 < x]
rewrite range_filter_2cons.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x2, x2 & xs] <= n.+1 k : nat LEx1 : x2 <= k NonDec : nondecreasing_sequence [:: x2, x2 & xs] Bound : forall x : nat,
x \in [:: x2, x2 & xs] -> x <= kLEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x2 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= y
distances [seq ρ <- range 0 k | ρ \in x2 :: xs] =
[seq x <- distances (x2 :: xs) | 0 < x]
by apply IHn; eauto 2 using nondecreasing_sequence_cons.
+ n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 < x2
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
have M4: forall y : nat, y \in x2 :: xs -> x1 < y by apply nondecreasing_sequence_cons_smin.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 < x2 M4 : forall y : nat, y \in x2 :: xs -> x1 < y
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- distances [:: x1, x2 & xs] | 0 < x]
rewrite distances_unfold_2cons.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 < x2 M4 : forall y : nat, y \in x2 :: xs -> x1 < y
distances
[seq ρ <- index_iota 0 k.+1
| ρ \in [:: x1, x2 & xs]] =
[seq x <- x2 - x1 :: distances (x2 :: xs) | 0 < x]
rewrite range_iota_filter_step // rem_lt_id //.n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 < x2 M4 : forall y : nat, y \in x2 :: xs -> x1 < y
distances
(x1 :: [seq ρ <- range 0 k | ρ \in x2 :: xs]) =
[seq x <- x2 - x1 :: distances (x2 :: xs) | 0 < x]
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 .n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 < x2 M4 : forall y : nat, y \in x2 :: xs -> x1 < y
x2 - x1 :: [seq x <- distances (x2 :: xs) | 0 < x] =
[seq x <- x2 - x1 :: distances (x2 :: xs) | 0 < x]
{ n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 < x2 M4 : forall y : nat, y \in x2 :: xs -> x1 < y
x2 - x1 :: [seq x <- distances (x2 :: xs) | 0 < x] =
[seq x <- x2 - x1 :: distances (x2 :: xs) | 0 < x]
simpl ; replace (0 < x2 - x1) with true; first by done .n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 < x2 M4 : forall y : nat, y \in x2 :: xs -> x1 < y
true = (0 < x2 - x1)
by apply /eqP; rewrite eq_sym; rewrite eqb_id subn_gt0. } n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 < x2 M4 : forall y : nat, y \in x2 :: xs -> x1 < y
distances
(x1 :: [seq ρ <- range 0 k | ρ \in x2 :: xs]) =
x2 - x1 :: [seq x <- distances (x2 :: xs) | 0 < x]
rewrite -(IHn _ _ k) //; last eapply nondecreasing_sequence_cons; eauto 2 .n : nat IHn : forall xs : seq_predType Datatypes_nat__canonical__eqtype_Equality,
size xs <= n ->
forall k : nat,
(forall x : nat, x \in xs -> x <= k) ->
nondecreasing_sequence xs ->
distances [seq ρ <- index_iota 0 k.+1 | ρ \in xs] =
[seq x <- distances xs | 0 < x]x1, x2 : Datatypes_nat__canonical__eqtype_Equality xs : seq Datatypes_nat__canonical__eqtype_Equality Len : size [:: x1, x2 & xs] <= n.+1 k : nat Bound : forall x : nat,
x \in [:: x1, x2 & xs] -> x <= kNonDec : nondecreasing_sequence [:: x1, x2 & xs] LEx1 : x1 <= k LEx2 : x2 <= k M1 : forall y : nat, y \in x2 :: xs -> x1 <= yM2 : forall x : nat, x \in x2 :: xs -> x <= kM3 : forall y : nat, y \in xs -> x2 <= yH : x1 < x2 M4 : forall y : nat, y \in x2 :: xs -> x1 < y
distances
(x1 :: [seq ρ <- range 0 k | ρ \in x2 :: xs]) =
x2 - x1
:: distances
[seq ρ <- index_iota 0 k.+1 | ρ \in x2 :: xs]
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 :
forall xs ,
nondecreasing_sequence xs ->
[seq d <- distances xs | 0 < d] = distances (undup xs).forall xs : seq nat,
nondecreasing_sequence xs ->
[seq d <- distances xs | 0 < d] = distances (undup xs)
Proof .forall xs : seq nat,
nondecreasing_sequence xs ->
[seq d <- distances xs | 0 < d] = distances (undup xs)
move => xs NonDec.xs : seq nat NonDec : nondecreasing_sequence xs
[seq d <- distances xs | 0 < d] = distances (undup xs)
rewrite -(distances_iota_filtered _ (max0 xs)); [ | by apply in_max0_le | by done ].xs : seq nat NonDec : nondecreasing_sequence xs
distances
[seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] =
distances (undup xs)
enough ([seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = (undup xs)) as IN; first by rewrite IN.xs : seq nat NonDec : nondecreasing_sequence xs
[seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] =
undup xs
have EX: exists len , size xs <= len.xs : seq nat NonDec : nondecreasing_sequence xs
exists len : nat, size xs <= len
{ xs : seq nat NonDec : nondecreasing_sequence xs
exists len : nat, size xs <= len
exists (size xs ); now simpl . } xs : seq nat NonDec : nondecreasing_sequence xs EX : exists len : nat, size xs <= len
[seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] =
undup xs
destruct EX as [n BO].xs : seq nat NonDec : nondecreasing_sequence xs n : nat BO : size xs <= n
[seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] =
undup xs
elim : n xs NonDec BO => [ |n IHn].forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= 0 ->
[seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] =
undup xs
- forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= 0 ->
[seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] =
undup xs
by intros xs _; rewrite leqn0 size_eq0 => /eqP ->; rewrite filter_pred0.
- n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xs
forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n.+1 ->
[seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] =
undup xs
intros [ |x1 [ | x2 xs]].n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xs
nondecreasing_sequence [::] ->
size [::] <= n.+1 ->
[seq ρ <- index_iota 0 (max0 [::]).+1 | ρ \in [::]] =
undup [::]
+ n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xs
nondecreasing_sequence [::] ->
size [::] <= n.+1 ->
[seq ρ <- index_iota 0 (max0 [::]).+1 | ρ \in [::]] =
undup [::]
by rewrite filter_pred0.
+ n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1 : nat
nondecreasing_sequence [:: x1] ->
size [:: x1] <= n.+1 ->
[seq ρ <- index_iota 0 (max0 [:: x1]).+1
| ρ \in [:: x1]] = undup [:: x1]
by rewrite index_iota_filter_singl ?L02 //; apply /andP; split ; [ done | destruct x1].
+ n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat
nondecreasing_sequence [:: x1, x2 & xs] ->
size [:: x1, x2 & xs] <= n.+1 ->
[seq ρ <- index_iota 0 (max0 [:: x1, x2 & xs]).+1
| ρ \in [:: x1, x2 & xs]] = undup [:: x1, x2 & xs]
intros NonDec Size.n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1
[seq ρ <- index_iota 0 (max0 [:: x1, x2 & xs]).+1
| ρ \in [:: x1, x2 & xs]] = undup [:: x1, x2 & xs]
destruct (nondecreasing_sequence_2cons_leVeq _ _ _ NonDec) as [EQ|LT].n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 EQ : x1 = x2
[seq ρ <- index_iota 0 (max0 [:: x1, x2 & xs]).+1
| ρ \in [:: x1, x2 & xs]] = undup [:: x1, x2 & xs]
* n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 EQ : x1 = x2
[seq ρ <- index_iota 0 (max0 [:: x1, x2 & xs]).+1
| ρ \in [:: x1, x2 & xs]] = undup [:: x1, x2 & xs]
subst ; rename x2 into x.n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx : nat xs : seq nat Size : size [:: x, x & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x, x & xs]
[seq ρ <- index_iota 0 (max0 [:: x, x & xs]).+1
| ρ \in [:: x, x & xs]] = undup [:: x, x & xs]
rewrite nodup_sort_2cons_eq range_filter_2cons max0_2cons_eq.n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx : nat xs : seq nat Size : size [:: x, x & xs] <= n.+1 NonDec : nondecreasing_sequence [:: x, x & xs]
[seq ρ <- range 0 (max0 (x :: xs)) | ρ \in x :: xs] =
undup (x :: xs)
by apply IHn; [ eapply nondecreasing_sequence_cons; eauto | by done ].
* n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 LT : x1 < x2
[seq ρ <- index_iota 0 (max0 [:: x1, x2 & xs]).+1
| ρ \in [:: x1, x2 & xs]] = undup [:: x1, x2 & xs]
rewrite nodup_sort_2cons_lt // max0_2cons_le; last by rewrite ltnW.n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 LT : x1 < x2
[seq ρ <- index_iota 0 (max0 (x2 :: xs)).+1
| ρ \in [:: x1, x2 & xs]] = x1 :: undup (x2 :: xs)
rewrite index_iota_filter_step; [ | | by apply nondecreasing_sequence_cons_min]; last first .n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 LT : x1 < x2
0 <= x1 < (max0 (x2 :: xs)).+1
{ n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 LT : x1 < x2
0 <= x1 < (max0 (x2 :: xs)).+1
apply /andP; split ; first by done .n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 LT : x1 < x2
x1 < (max0 (x2 :: xs)).+1
eapply leq_trans; first by eassumption .n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 LT : x1 < x2
x2 <= (max0 (x2 :: xs)).+1
rewrite ltnW // ltnS; apply in_max0_le.n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 LT : x1 < x2
x2 \in x2 :: xs
by rewrite in_cons eq_refl.
} n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 LT : x1 < x2
x1
:: [seq ρ <- index_iota 0 (max0 (x2 :: xs)).+1
| ρ \in rem_all x1 (x2 :: xs)] =
x1 :: undup (x2 :: xs)
rewrite rem_lt_id //; last by apply nondecreasing_sequence_cons_smin.n : nat IHn : forall xs : seq nat,
nondecreasing_sequence xs ->
size xs <= n -> [seq ρ <- index_iota 0 (max0 xs).+1 | ρ \in xs] = undup xsx1, x2 : nat xs : seq nat NonDec : nondecreasing_sequence [:: x1, x2 & xs] Size : size [:: x1, x2 & xs] <= n.+1 LT : x1 < x2
x1
:: [seq ρ <- index_iota 0 (max0 (x2 :: xs)).+1
| ρ \in x2 :: xs] = x1 :: undup (x2 :: xs)
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 :
forall (xs ys : seq nat),
first0 xs <= first0 ys ->
2 <= size xs ->
2 <= size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n , (distances xs)[|n|] <= (distances ys)[|n|]) ->
(forall n , xs[|n|] <= ys[|n|]).forall xs ys : seq nat,
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
Proof .forall xs ys : seq nat,
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
intros xs ys.xs, ys : seq nat
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
have EX: exists len , size xs <= len /\ size ys <= len.xs, ys : seq nat
exists len : nat, size xs <= len /\ size ys <= len
{ xs, ys : seq nat
exists len : nat, size xs <= len /\ size ys <= len
exists (maxn (size xs) (size ys)).xs, ys : seq nat
size xs <= maxn (size xs) (size ys) /\
size ys <= maxn (size xs) (size ys)
by split ; rewrite leq_max; apply /orP; [left | right ].
} xs, ys : seq nat EX : exists len : nat,
size xs <= len /\ size ys <= len
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
move : EX => [len [LE1 LE2]].xs, ys : seq nat len : nat LE1 : size xs <= len LE2 : size ys <= len
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
generalize dependent xs; generalize dependent ys.len : nat
forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
elim : len => [ |len IHlen].forall ys : seq nat,
size ys <= 0 ->
forall xs : seq nat,
size xs <= 0 ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
{ forall ys : seq nat,
size ys <= 0 ->
forall xs : seq nat,
size xs <= 0 ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
move => ys + xs + H H0 h1 H2 H3 H4 H5 n.ys, xs : seq nat H : first0 xs <= first0 ys H0 : 1 < size xsh1 : 1 < size ysH2 : size xs = size ys H3 : nondecreasing_sequence xs H4 : nondecreasing_sequence ys H5 : forall n : nat,
distances xs [|n|] <= distances ys [|n|]n : nat
size ys <= 0 -> size xs <= 0 -> xs [|n|] <= ys [|n|]
by rewrite !leqn0 !size_eq0 => /eqP -> /eqP ->. } len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
forall ys : seq nat,
size ys <= len.+1 ->
forall xs : seq nat,
size xs <= len.+1 ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
{ len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
forall ys : seq nat,
size ys <= len.+1 ->
forall xs : seq nat,
size xs <= len.+1 ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]
intros ys LycSIZE xs LxSIZE FLE Sxs Sys SIZEEQ STRxs STRys LE n.len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]ys : seq nat LycSIZE : size ys <= len.+1 xs : seq nat LxSIZE : size xs <= len.+1 FLE : first0 xs <= first0 ys Sxs : 1 < size xsSys : 1 < size ysSIZEEQ : size xs = size ys STRxs : nondecreasing_sequence xs STRys : nondecreasing_sequence ys LE : forall n : nat,
distances xs [|n|] <= distances ys [|n|]n : nat
xs [|n|] <= ys [|n|]
destruct xs as [ | x1 xs], ys as [ | y1 ys]; try by done .len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1 : nat ys : seq nat LycSIZE : size (y1 :: ys) <= len.+1 x1 : nat xs : seq nat LxSIZE : size (x1 :: xs) <= len.+1 FLE : first0 (x1 :: xs) <= first0 (y1 :: ys) Sxs : 1 < size (x1 :: xs)Sys : 1 < size (y1 :: ys)SIZEEQ : size (x1 :: xs) = size (y1 :: ys) STRxs : nondecreasing_sequence (x1 :: xs) STRys : nondecreasing_sequence (y1 :: ys) LE : forall n : nat,
distances (x1 :: xs) [|n|] <=
distances (y1 :: ys) [|n|]n : nat
(x1 :: xs) [|n|] <= (y1 :: ys) [|n|]
destruct xs as [ | x2 xs], ys as [ | y2 ys]; try by done .len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : first0 [:: x1, x2 & xs] <=
first0 [:: y1, y2 & ys] Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : nondecreasing_sequence [:: x1, x2 & xs] STRys : nondecreasing_sequence [:: y1, y2 & ys] LE : forall n : nat,
distances [:: x1, x2 & xs] [|n|] <=
distances [:: y1, y2 & ys] [|n|]n : nat
[:: x1, x2 & xs] [|n|] <= [:: y1, y2 & ys] [|n|]
have F: x2 <= y2.len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : first0 [:: x1, x2 & xs] <=
first0 [:: y1, y2 & ys] Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : nondecreasing_sequence [:: x1, x2 & xs] STRys : nondecreasing_sequence [:: y1, y2 & ys] LE : forall n : nat,
distances [:: x1, x2 & xs] [|n|] <=
distances [:: y1, y2 & ys] [|n|]n : nat
x2 <= y2
{ len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : first0 [:: x1, x2 & xs] <=
first0 [:: y1, y2 & ys] Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : nondecreasing_sequence [:: x1, x2 & xs] STRys : nondecreasing_sequence [:: y1, y2 & ys] LE : forall n : nat,
distances [:: x1, x2 & xs] [|n|] <=
distances [:: y1, y2 & ys] [|n|]n : nat
x2 <= y2
specialize (STRxs 0 1 ); feed STRxs; first by done .len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : first0 [:: x1, x2 & xs] <=
first0 [:: y1, y2 & ys] Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : [:: x1, x2 & xs] [|0 |] <=
[:: x1, x2 & xs] [|1 |] STRys : nondecreasing_sequence [:: y1, y2 & ys] LE : forall n : nat,
distances [:: x1, x2 & xs] [|n|] <=
distances [:: y1, y2 & ys] [|n|]n : nat
x2 <= y2
specialize (STRys 0 1 ); feed STRys; first by done .len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : first0 [:: x1, x2 & xs] <=
first0 [:: y1, y2 & ys] Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : [:: x1, x2 & xs] [|0 |] <=
[:: x1, x2 & xs] [|1 |] STRys : [:: y1, y2 & ys] [|0 |] <=
[:: y1, y2 & ys] [|1 |] LE : forall n : nat,
distances [:: x1, x2 & xs] [|n|] <=
distances [:: y1, y2 & ys] [|n|]n : nat
x2 <= y2
specialize (LE 0 ); simpl in LE, FLE.len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : x1 <= y1 Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : [:: x1, x2 & xs] [|0 |] <=
[:: x1, x2 & xs] [|1 |] STRys : [:: y1, y2 & ys] [|0 |] <=
[:: y1, y2 & ys] [|1 |] LE : x2 - x1 <= y2 - y1 n : nat
x2 <= y2
rewrite leqNgt; apply /negP; intros NEQ.len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : x1 <= y1 Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : [:: x1, x2 & xs] [|0 |] <=
[:: x1, x2 & xs] [|1 |] STRys : [:: y1, y2 & ys] [|0 |] <=
[:: y1, y2 & ys] [|1 |] LE : x2 - x1 <= y2 - y1 n : nat NEQ : y2 < x2
False
move : LE; rewrite leqNgt; move => /negP LE; apply : LE.len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : x1 <= y1 Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : [:: x1, x2 & xs] [|0 |] <=
[:: x1, x2 & xs] [|1 |] STRys : [:: y1, y2 & ys] [|0 |] <=
[:: y1, y2 & ys] [|1 |] n : nat NEQ : y2 < x2
y2 - y1 < x2 - x1
rewrite -(ltn_add2r x1) subnK // addnBAC // -(ltn_add2r y1) subnK.len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : x1 <= y1 Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : [:: x1, x2 & xs] [|0 |] <=
[:: x1, x2 & xs] [|1 |] STRys : [:: y1, y2 & ys] [|0 |] <=
[:: y1, y2 & ys] [|1 |] n : nat NEQ : y2 < x2
y2 + x1 < x2 + y1
- len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : x1 <= y1 Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : [:: x1, x2 & xs] [|0 |] <=
[:: x1, x2 & xs] [|1 |] STRys : [:: y1, y2 & ys] [|0 |] <=
[:: y1, y2 & ys] [|1 |] n : nat NEQ : y2 < x2
y2 + x1 < x2 + y1
by eapply leq_ltn_trans; [erewrite leq_add2l | erewrite ltn_add2r].
- len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : x1 <= y1 Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : [:: x1, x2 & xs] [|0 |] <=
[:: x1, x2 & xs] [|1 |] STRys : [:: y1, y2 & ys] [|0 |] <=
[:: y1, y2 & ys] [|1 |] n : nat NEQ : y2 < x2
y1 <= y2 + x1
by apply leq_trans with y2; auto using leq_addr.
} len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat ys : seq nat LycSIZE : size [:: y1, y2 & ys] <= len.+1 x1, x2 : nat xs : seq nat LxSIZE : size [:: x1, x2 & xs] <= len.+1 FLE : first0 [:: x1, x2 & xs] <=
first0 [:: y1, y2 & ys] Sxs : 1 < size [:: x1, x2 & xs]Sys : 1 < size [:: y1, y2 & ys]SIZEEQ : size [:: x1, x2 & xs] = size [:: y1, y2 & ys] STRxs : nondecreasing_sequence [:: x1, x2 & xs] STRys : nondecreasing_sequence [:: y1, y2 & ys] LE : forall n : nat,
distances [:: x1, x2 & xs] [|n|] <=
distances [:: y1, y2 & ys] [|n|]n : nat F : x2 <= y2
[:: x1, x2 & xs] [|n|] <= [:: y1, y2 & ys] [|n|]
destruct xs as [ | x3 xs], ys as [ | y3 ys]; try by done .len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat LycSIZE : size [:: y1; y2] <= len.+1 x1, x2 : nat LxSIZE : size [:: x1; x2] <= len.+1 FLE : first0 [:: x1; x2] <= first0 [:: y1; y2] Sxs : 1 < size [:: x1; x2]Sys : 1 < size [:: y1; y2]SIZEEQ : size [:: x1; x2] = size [:: y1; y2] STRxs : nondecreasing_sequence [:: x1; x2] STRys : nondecreasing_sequence [:: y1; y2] LE : forall n : nat,
distances [:: x1; x2] [|n|] <=
distances [:: y1; y2] [|n|]n : nat F : x2 <= y2
[:: x1; x2] [|n|] <= [:: y1; y2] [|n|]
{ len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2 : nat LycSIZE : size [:: y1; y2] <= len.+1 x1, x2 : nat LxSIZE : size [:: x1; x2] <= len.+1 FLE : first0 [:: x1; x2] <= first0 [:: y1; y2] Sxs : 1 < size [:: x1; x2]Sys : 1 < size [:: y1; y2]SIZEEQ : size [:: x1; x2] = size [:: y1; y2] STRxs : nondecreasing_sequence [:: x1; x2] STRys : nondecreasing_sequence [:: y1; y2] LE : forall n : nat,
distances [:: x1; x2] [|n|] <=
distances [:: y1; y2] [|n|]n : nat F : x2 <= y2
[:: x1; x2] [|n|] <= [:: y1; y2] [|n|]
by destruct n as [ |n]; [ | destruct n]. } len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2
[:: x1, x2, x3 & xs] [|n|] <=
[:: y1, y2, y3 & ys] [|n|]
destruct n => //.len : nat IHlen : forall ys : seq nat,
size ys <= len ->
forall xs : seq nat,
size xs <= len ->
first0 xs <= first0 ys ->
1 < size xs ->
1 < size ys ->
size xs = size ys ->
nondecreasing_sequence xs ->
nondecreasing_sequence ys ->
(forall n : nat,
distances xs [|n|] <= distances ys [|n|]) ->
forall n : nat, xs [|n|] <= ys [|n|]y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2
[:: x1, x2, x3 & xs] [|n.+1 |] <=
[:: y1, y2, y3 & ys] [|n.+1 |]
simpl ; apply : IHlen => //.len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2
nondecreasing_sequence [:: x2, x3 & xs]
- len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2
nondecreasing_sequence [:: x2, x3 & xs]
move => m1 m2 /andP [B1 B2].len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2 m1, m2 : nat B1 : m1 <= m2 B2 : m2 < size [:: x2, x3 & xs]
[:: x2, x3 & xs] [|m1|] <= [:: x2, x3 & xs] [|m2|]
apply (STRxs m1.+1 m2.+1 ); apply /andP; split .len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2 m1, m2 : nat B1 : m1 <= m2 B2 : m2 < size [:: x2, x3 & xs]
m1 < m2.+1
+ len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2 m1, m2 : nat B1 : m1 <= m2 B2 : m2 < size [:: x2, x3 & xs]
m1 < m2.+1
by rewrite ltnS.
+ len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2 m1, m2 : nat B1 : m1 <= m2 B2 : m2 < size [:: x2, x3 & xs]
m2.+1 < size [:: x1, x2, x3 & xs]
by rewrite -(ltn_add2r 1 ) !addn1 in B2.
- len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2
nondecreasing_sequence [:: y2, y3 & ys]
move => m1 m2 /andP [B1 B2].len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2 m1, m2 : nat B1 : m1 <= m2 B2 : m2 < size [:: y2, y3 & ys]
[:: y2, y3 & ys] [|m1|] <= [:: y2, y3 & ys] [|m2|]
apply (STRys m1.+1 m2.+1 ); apply /andP; split .len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2 m1, m2 : nat B1 : m1 <= m2 B2 : m2 < size [:: y2, y3 & ys]
m1 < m2.+1
+ len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2 m1, m2 : nat B1 : m1 <= m2 B2 : m2 < size [:: y2, y3 & ys]
m1 < m2.+1
by rewrite ltnS.
+ len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2 m1, m2 : nat B1 : m1 <= m2 B2 : m2 < size [:: y2, y3 & ys]
m2.+1 < size [:: y1, y2, y3 & ys]
by rewrite -(ltn_add2r 1 ) !addn1 in B2.
- len, y1, y2, y3 : nat ys : seq nat LycSIZE : size [:: y1, y2, y3 & ys] <= len.+1 x1, x2, x3 : nat xs : seq nat LxSIZE : size [:: x1, x2, x3 & xs] <= len.+1 FLE : first0 [:: x1, x2, x3 & xs] <=
first0 [:: y1, y2, y3 & ys] Sxs : 1 < size [:: x1, x2, x3 & xs]Sys : 1 < size [:: y1, y2, y3 & ys]SIZEEQ : size [:: x1, x2, x3 & xs] =
size [:: y1, y2, y3 & ys] STRxs : nondecreasing_sequence [:: x1, x2, x3 & xs] STRys : nondecreasing_sequence [:: y1, y2, y3 & ys] LE : forall n : nat,
distances [:: x1, x2, x3 & xs] [|n|] <=
distances [:: y1, y2, y3 & ys] [|n|]n : nat F : x2 <= y2
forall n : nat,
distances [:: x2, x3 & xs] [|n|] <=
distances [:: y2, y3 & ys] [|n|]
by move => n0; specialize (LE n0.+1 ); simpl in LE.
}
Qed .
End DistancesOfNonDecreasingSequence .
End NondecreasingSequence .