Library rt.model.schedule.uni.limited.platform.util
Non-decreasing sequence
In this module we introduce the notion of a non-decreasing sequence that will be used to describe preemption points in models with limited preemptions.
Module 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-decincreasing iff for any two indices n1 and n2
such that [n1 <= n2 < size xs] the following condition holds: xs[n1] <= xs[n2]. *)
Definition nondecreasing_sequence (xs: seq nat) :=
∀ n1 n2,
n1 ≤ n2 < size xs →
nth 0 xs n1 ≤ nth 0 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)).
(* Next, we define some common operations on lists.
Namely max, first, and last. *)
Definition max := foldl maxn 0.
Definition first := head 0.
Definition last := last 0.
End Definitions.
(* In this section, we prove a few basic lemmas about nondecreasing sequences. *)
Section Lemmas.
(* Next, we prove that no element can lie strictly between two
neighboring elements and still belong to the list. *)
Lemma antidensity_of_nondecreasing_seq:
∀ (xs: seq nat) (x: nat) (n: nat),
nondecreasing_sequence xs →
xs [| n |] < x < xs [| n.+1 |] →
~~ (x \in xs).
(* Alternatively, consider an arbitrary natural number x that is
bounded by the first and the last element of a sequence xs. Then
there is an index n such that xs[n] <= x < x[n+1]. *)
Lemma belonging_to_segment_of_seq_is_total:
∀ (xs: seq nat) (x: nat),
2 ≤ size xs →
first xs ≤ x < last xs →
∃ n,
n.+1 < size xs ∧
xs[|n|] ≤ x < xs[|n.+1|].
(* We prove that the difference between any two neighboring elements is
bounded by the max element of the distances-sequence. *)
Lemma distance_between_neighboring_elements_le_max_distance_in_seq:
∀ (xs: seq nat) (n: nat),
xs[|n.+1|] - xs[|n|] ≤ max (distances xs).
(* As a corollary, the max distance between elements of any nontrivial sequence
(i.e. a sequence that contains at leas two distinct elements) is positive. *)
Corollary max_distance_in_nontrivial_seq_is_positive:
∀ (xs: seq nat),
nondecreasing_sequence xs →
(∃ x y, x \in xs ∧ y \in xs ∧ x ≠ y) →
0 < max (distances xs).
(* Note that the distances-function has the expected behavior indeed. I.e. an element
on the n-th position of the distance-sequence is equal to the difference between
n+1-th and n-th elements. *)
Lemma function_of_distances_is_correct:
∀ (xs: seq nat) (n: nat),
(distances xs)[|n|] = xs[|n.+1|] - xs[|n|].
(* We show that the size of a distances-sequence is one less
than the size of the original sequence. *)
Lemma size_of_seq_of_distances:
∀ (xs: seq nat),
2 ≤ size xs →
size xs = size (distances xs) + 1.
(* Note that the last element of a nondecreasing sequence is the max element. *)
Lemma last_is_max_in_nondecreasing_seq:
∀ (xs: seq nat) (x: nat),
nondecreasing_sequence xs →
(x \in xs) →
x ≤ last xs.
(* Given a nondecreasing 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 the (n-2)'th element of xs. *)
Lemma last_seq_minus_last_distance_seq:
∀ (xs: seq nat),
nondecreasing_sequence xs →
last xs - last (distances xs) = xs [| (size xs).-2 |].
(* Note that the last element is at most the max element. *)
Lemma last_of_seq_le_max_of_seq:
∀ (xs: seq nat),
last xs ≤ max xs.
(* If any n'th element of a sequence xs is less-than-or-equal-to n'th
element of ys, then max of xs is less-than-or-equal-to max of ys. *)
Lemma max_of_dominating_seq:
∀ (xs ys: seq nat),
(∀ n, xs[|n|] ≤ ys[|n|]) →
max xs ≤ max ys.
(* The max element of the distances-sequence of a sequence xs is bounded
by the last element of xs. Note that all elements of xs are positive.
Thus they all lie within the interval [0, last xs]. *)
Lemma max_distance_in_seq_le_last_element_of_seq:
∀ (xs: seq nat),
nondecreasing_sequence xs →
max (distances xs) ≤ last xs.
(* Consider two nondecreasing sequences xs and ys and assume that
(1) first element of xs is at most the first element of ys and
(2) distances-sequences of xs is dominated by distances-sequence of
ys. Then xs is dominated by ys. *)
Lemma domination_of_distances_implies_domination_of_seq:
∀ (xs ys: seq nat),
first xs ≤ first ys →
2 ≤ size xs →
2 ≤ size ys →
size xs = size ys →
nondecreasing_sequence xs →
nondecreasing_sequence ys →
(∀ n, (distances xs)[|n|] ≤ (distances ys)[|n|]) →
(∀ n, xs[|n|] ≤ ys[|n|]).
End Lemmas.
End 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-decincreasing iff for any two indices n1 and n2
such that [n1 <= n2 < size xs] the following condition holds: xs[n1] <= xs[n2]. *)
Definition nondecreasing_sequence (xs: seq nat) :=
∀ n1 n2,
n1 ≤ n2 < size xs →
nth 0 xs n1 ≤ nth 0 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)).
(* Next, we define some common operations on lists.
Namely max, first, and last. *)
Definition max := foldl maxn 0.
Definition first := head 0.
Definition last := last 0.
End Definitions.
(* In this section, we prove a few basic lemmas about nondecreasing sequences. *)
Section Lemmas.
(* Next, we prove that no element can lie strictly between two
neighboring elements and still belong to the list. *)
Lemma antidensity_of_nondecreasing_seq:
∀ (xs: seq nat) (x: nat) (n: nat),
nondecreasing_sequence xs →
xs [| n |] < x < xs [| n.+1 |] →
~~ (x \in xs).
(* Alternatively, consider an arbitrary natural number x that is
bounded by the first and the last element of a sequence xs. Then
there is an index n such that xs[n] <= x < x[n+1]. *)
Lemma belonging_to_segment_of_seq_is_total:
∀ (xs: seq nat) (x: nat),
2 ≤ size xs →
first xs ≤ x < last xs →
∃ n,
n.+1 < size xs ∧
xs[|n|] ≤ x < xs[|n.+1|].
(* We prove that the difference between any two neighboring elements is
bounded by the max element of the distances-sequence. *)
Lemma distance_between_neighboring_elements_le_max_distance_in_seq:
∀ (xs: seq nat) (n: nat),
xs[|n.+1|] - xs[|n|] ≤ max (distances xs).
(* As a corollary, the max distance between elements of any nontrivial sequence
(i.e. a sequence that contains at leas two distinct elements) is positive. *)
Corollary max_distance_in_nontrivial_seq_is_positive:
∀ (xs: seq nat),
nondecreasing_sequence xs →
(∃ x y, x \in xs ∧ y \in xs ∧ x ≠ y) →
0 < max (distances xs).
(* Note that the distances-function has the expected behavior indeed. I.e. an element
on the n-th position of the distance-sequence is equal to the difference between
n+1-th and n-th elements. *)
Lemma function_of_distances_is_correct:
∀ (xs: seq nat) (n: nat),
(distances xs)[|n|] = xs[|n.+1|] - xs[|n|].
(* We show that the size of a distances-sequence is one less
than the size of the original sequence. *)
Lemma size_of_seq_of_distances:
∀ (xs: seq nat),
2 ≤ size xs →
size xs = size (distances xs) + 1.
(* Note that the last element of a nondecreasing sequence is the max element. *)
Lemma last_is_max_in_nondecreasing_seq:
∀ (xs: seq nat) (x: nat),
nondecreasing_sequence xs →
(x \in xs) →
x ≤ last xs.
(* Given a nondecreasing 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 the (n-2)'th element of xs. *)
Lemma last_seq_minus_last_distance_seq:
∀ (xs: seq nat),
nondecreasing_sequence xs →
last xs - last (distances xs) = xs [| (size xs).-2 |].
(* Note that the last element is at most the max element. *)
Lemma last_of_seq_le_max_of_seq:
∀ (xs: seq nat),
last xs ≤ max xs.
(* If any n'th element of a sequence xs is less-than-or-equal-to n'th
element of ys, then max of xs is less-than-or-equal-to max of ys. *)
Lemma max_of_dominating_seq:
∀ (xs ys: seq nat),
(∀ n, xs[|n|] ≤ ys[|n|]) →
max xs ≤ max ys.
(* The max element of the distances-sequence of a sequence xs is bounded
by the last element of xs. Note that all elements of xs are positive.
Thus they all lie within the interval [0, last xs]. *)
Lemma max_distance_in_seq_le_last_element_of_seq:
∀ (xs: seq nat),
nondecreasing_sequence xs →
max (distances xs) ≤ last xs.
(* Consider two nondecreasing sequences xs and ys and assume that
(1) first element of xs is at most the first element of ys and
(2) distances-sequences of xs is dominated by distances-sequence of
ys. Then xs is dominated by ys. *)
Lemma domination_of_distances_implies_domination_of_seq:
∀ (xs ys: seq nat),
first xs ≤ first ys →
2 ≤ size xs →
2 ≤ size ys →
size xs = size ys →
nondecreasing_sequence xs →
nondecreasing_sequence ys →
(∀ n, (distances xs)[|n|] ≤ (distances ys)[|n|]) →
(∀ n, xs[|n|] ≤ ys[|n|]).
End Lemmas.
End NondecreasingSequence.