Library prosa.analysis.abstract.search_space
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Import prosa.util.epsilon.
Require Import prosa.util.tactics.
Require Import prosa.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Reduction of the search space for Abstract RTA
In this file, we prove that in order to calculate the worst-case response time it is sufficient to consider only values of [A] that lie in the search space defined below.
The response-time analysis we are presenting in this series of documents is based on searching
over all possible values of [A], the relative arrival time of the job respective to the beginning
of the busy interval. However, to obtain a practically useful response-time bound, we need to
constrain the search space of values of [A]. In this section, we define an approach to
reduce the search space.
First, we provide a constructive notion of equivalent functions.
Consider an arbitrary type [T]...
...and two function from [nat] to [T].
Let [B] be an arbitrary constant.
Then we say that [f1] and [f2] are equivalent at values less than [B] iff
for any natural number [x] less than [B] [f1 x] is equal to [f2 x].
And vice versa, we say that [f1] and [f2] are not equivalent at values
less than [B] iff there exists a natural number [x] less than [B] such
that [f1 x] is not equal to [f2 x].
Definition are_not_equivalent_at_values_less_than :=
∃ x, x < B ∧ f1 x ≠ f2 x.
End EquivalentFunctions.
∃ x, x < B ∧ f1 x ≠ f2 x.
End EquivalentFunctions.
Let [tsk] be any task that is to be analyzed
To ensure that the analysis procedure terminates, we assume an upper bound [B] on
the values of [A] that must be checked. The existence of [B] follows from the assumption
that the system is not overloaded (i.e., it has bounded utilization).
Instead of searching for the maximum interference of each individual job, we
assume a per-task interference bound function [IBF(tsk, A, x)] that is parameterized
by the relative arrival time [A] of a potential job (see abstract_RTA.definitions.v file).
Recall the definition of [ε], which defines the neighborhood of a point in the timeline.
Note that [ε = 1] under discrete time. To ensure that the search converges more quickly, we only check values of [A] in the interval
[0, B) for which the interference bound function changes, i.e., every point [x] in which
[interference_bound_function (A - ε, x)] is not equal to [interference_bound_function (A, x)].
Definition is_in_search_space A :=
A = 0 ∨
0 < A < B ∧ are_not_equivalent_at_values_less_than
(interference_bound_function tsk (A - ε)) (interference_bound_function tsk A) B.
A = 0 ∨
0 < A < B ∧ are_not_equivalent_at_values_less_than
(interference_bound_function tsk (A - ε)) (interference_bound_function tsk A) B.
In this section we prove that for every [A] there exists a smaller [A_sp]
in the search space such that [interference_bound_function(A_sp,x)] is
equal to [interference_bound_function(A, x)].
Let [A] be any constant less than [B].
We prove that there exists a constant [A_sp] such that:
(a) [A_sp] is no greater than [A], (b) [interference_bound_function(A_sp, x)] is
equal to [interference_bound_function(A, x)] and (c) [A_sp] is in the search space.
In other words, either [A] is already inside the search space, or we can go
to the "left" until we reach [A_sp], which will be inside the search space.
Lemma representative_exists:
∃ A_sp,
A_sp ≤ A ∧
are_equivalent_at_values_less_than (interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B ∧
is_in_search_space A_sp.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 25)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
H_A_less_than_B : A < B
============================
exists A_sp : nat,
A_sp <= A /\
are_equivalent_at_values_less_than (interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
Proof.
induction A as [|n].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 37)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
H_A_less_than_B : 0 < B
============================
exists A_sp : nat,
A_sp <= 0 /\
are_equivalent_at_values_less_than (interference_bound_function tsk 0)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
subgoal 2 (ID 41) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
- ∃ 0; repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 50)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
H_A_less_than_B : 0 < B
============================
is_in_search_space 0
subgoal 2 (ID 41) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
by rewrite /is_in_search_space; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
- have ALT:
all (fun t ⇒ interference_bound_function tsk n t == interference_bound_function tsk n.+1 t) (iota 0 B)
∨ has (fun t ⇒ interference_bound_function tsk n t != interference_bound_function tsk n.+1 t) (iota 0 B).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 63)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t) (iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t) (iota 0 B)
subgoal 2 (ID 65) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t) (iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t) (iota 0 B)
----------------------------------------------------------------------------- *)
apply/orP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 113)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t) (iota 0 B)
|| has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
----------------------------------------------------------------------------- *)
rewrite -[_ || _]Bool.negb_involutive Bool.negb_orb.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
~~
(~~
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t) (iota 0 B) &&
~~
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t) (iota 0 B))
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 146)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
CONTR : ~~
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B) &&
~~
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
============================
False
----------------------------------------------------------------------------- *)
move: CONTR ⇒ /andP [NALL /negP NHAS]; apply: NHAS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 216)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
NALL : ~~
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B)
============================
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t) (iota 0 B)
----------------------------------------------------------------------------- *)
by rewrite -has_predC /predC in NALL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 65) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
ALT : all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
feed IHn; first by apply ltn_trans with n.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 246)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
ALT : all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
move: IHn ⇒ [ASP [NEQ [EQ SP]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 281)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ALT : all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
move: ALT ⇒ [/allP ALT| /hasP ALT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 360)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
subgoal 2 (ID 361) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 360)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
∃ ASP; repeat split; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 365)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
ASP <= n.+1
subgoal 2 (ID 369) is:
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk ASP) B
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
ASP <= n.+1
----------------------------------------------------------------------------- *)
by apply leq_trans with n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 369) is:
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk ASP) B
subgoal 2 (ID 361) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk ASP) B
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk ASP) B
----------------------------------------------------------------------------- *)
intros x LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 422)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
x : nat
LT : x < B
============================
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
----------------------------------------------------------------------------- *)
move: (ALT x) ⇒ T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 424)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
x : nat
LT : x < B
T : x \in iota 0 B ->
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x
============================
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
----------------------------------------------------------------------------- *)
feed T; first by rewrite mem_iota; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 430)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
x : nat
LT : x < B
T : interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x
============================
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
----------------------------------------------------------------------------- *)
move: T ⇒ /eqP T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 497)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
x : nat
LT : x < B
T : interference_bound_function tsk n x =
interference_bound_function tsk n.+1 x
============================
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
----------------------------------------------------------------------------- *)
by rewrite -T EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 361) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 361) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 361)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 361)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
∃ n.+1; repeat split; try done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 515)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
is_in_search_space n.+1
----------------------------------------------------------------------------- *)
rewrite /is_in_search_space; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 546)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
0 < n.+1 < B /\
are_not_equivalent_at_values_less_than
(interference_bound_function tsk (n.+1 - ε))
(interference_bound_function tsk n.+1) B
----------------------------------------------------------------------------- *)
split; first by apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 549)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
are_not_equivalent_at_values_less_than
(interference_bound_function tsk (n.+1 - ε))
(interference_bound_function tsk n.+1) B
----------------------------------------------------------------------------- *)
move: ALT ⇒ [y IN N].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 591)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
IN : y \in iota 0 B
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
============================
are_not_equivalent_at_values_less_than
(interference_bound_function tsk (n.+1 - ε))
(interference_bound_function tsk n.+1) B
----------------------------------------------------------------------------- *)
∃ y.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 593)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
IN : y \in iota 0 B
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
============================
y < B /\
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
move: IN; rewrite mem_iota add0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 605)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
============================
0 <= y < B ->
y < B /\
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
move ⇒ /andP [_ LT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 644)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
LT : y < B
============================
y < B /\
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 647)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
LT : y < B
============================
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
rewrite subn1 -pred_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 653)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
LT : y < B
============================
interference_bound_function tsk n y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
intros CONTR; move: N ⇒ /negP N; apply: N.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 688)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
LT : y < B
CONTR : interference_bound_function tsk n y =
interference_bound_function tsk n.+1 y
============================
interference_bound_function tsk n y ==
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
by rewrite CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ExistenceOfRepresentative.
∃ A_sp,
A_sp ≤ A ∧
are_equivalent_at_values_less_than (interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B ∧
is_in_search_space A_sp.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 25)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
H_A_less_than_B : A < B
============================
exists A_sp : nat,
A_sp <= A /\
are_equivalent_at_values_less_than (interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
Proof.
induction A as [|n].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 37)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
H_A_less_than_B : 0 < B
============================
exists A_sp : nat,
A_sp <= 0 /\
are_equivalent_at_values_less_than (interference_bound_function tsk 0)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
subgoal 2 (ID 41) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
- ∃ 0; repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 50)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
H_A_less_than_B : 0 < B
============================
is_in_search_space 0
subgoal 2 (ID 41) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
by rewrite /is_in_search_space; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
- have ALT:
all (fun t ⇒ interference_bound_function tsk n t == interference_bound_function tsk n.+1 t) (iota 0 B)
∨ has (fun t ⇒ interference_bound_function tsk n t != interference_bound_function tsk n.+1 t) (iota 0 B).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 63)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t) (iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t) (iota 0 B)
subgoal 2 (ID 65) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 63)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t) (iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t) (iota 0 B)
----------------------------------------------------------------------------- *)
apply/orP.
(* ----------------------------------[ coqtop ]---------------------------------
1 focused subgoal
(shelved: 1) (ID 113)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t) (iota 0 B)
|| has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
----------------------------------------------------------------------------- *)
rewrite -[_ || _]Bool.negb_involutive Bool.negb_orb.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
============================
~~
(~~
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t) (iota 0 B) &&
~~
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t) (iota 0 B))
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 146)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
CONTR : ~~
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B) &&
~~
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
============================
False
----------------------------------------------------------------------------- *)
move: CONTR ⇒ /andP [NALL /negP NHAS]; apply: NHAS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 216)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
NALL : ~~
all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B)
============================
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t) (iota 0 B)
----------------------------------------------------------------------------- *)
by rewrite -has_predC /predC in NALL.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 65) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 65)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : n < B ->
exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
ALT : all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
feed IHn; first by apply ltn_trans with n.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 246)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
IHn : exists A_sp : nat,
A_sp <= n /\
are_equivalent_at_values_less_than
(interference_bound_function tsk n)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
ALT : all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
move: IHn ⇒ [ASP [NEQ [EQ SP]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 281)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ALT : all
(fun t : duration =>
interference_bound_function tsk n t ==
interference_bound_function tsk n.+1 t)
(iota 0 B) \/
has
(fun t : duration =>
interference_bound_function tsk n t
!= interference_bound_function tsk n.+1 t)
(iota 0 B)
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
move: ALT ⇒ [/allP ALT| /hasP ALT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 360)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
subgoal 2 (ID 361) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 360)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
∃ ASP; repeat split; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 365)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
ASP <= n.+1
subgoal 2 (ID 369) is:
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk ASP) B
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 365)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
ASP <= n.+1
----------------------------------------------------------------------------- *)
by apply leq_trans with n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 369) is:
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk ASP) B
subgoal 2 (ID 361) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk ASP) B
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 369)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
============================
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk ASP) B
----------------------------------------------------------------------------- *)
intros x LT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 422)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
x : nat
LT : x < B
============================
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
----------------------------------------------------------------------------- *)
move: (ALT x) ⇒ T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 424)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
x : nat
LT : x < B
T : x \in iota 0 B ->
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x
============================
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
----------------------------------------------------------------------------- *)
feed T; first by rewrite mem_iota; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 430)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
x : nat
LT : x < B
T : interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x
============================
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
----------------------------------------------------------------------------- *)
move: T ⇒ /eqP T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 497)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : {in iota 0 B,
forall x : nat_eqType,
interference_bound_function tsk n x ==
interference_bound_function tsk n.+1 x}
x : nat
LT : x < B
T : interference_bound_function tsk n x =
interference_bound_function tsk n.+1 x
============================
interference_bound_function tsk n.+1 x =
interference_bound_function tsk ASP x
----------------------------------------------------------------------------- *)
by rewrite -T EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 361) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 361) is:
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\ is_in_search_space A_sp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 361)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 361)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
exists A_sp : nat,
A_sp <= n.+1 /\
are_equivalent_at_values_less_than (interference_bound_function tsk n.+1)
(interference_bound_function tsk A_sp) B /\
is_in_search_space A_sp
----------------------------------------------------------------------------- *)
∃ n.+1; repeat split; try done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 515)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
is_in_search_space n.+1
----------------------------------------------------------------------------- *)
rewrite /is_in_search_space; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 546)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
0 < n.+1 < B /\
are_not_equivalent_at_values_less_than
(interference_bound_function tsk (n.+1 - ε))
(interference_bound_function tsk n.+1) B
----------------------------------------------------------------------------- *)
split; first by apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 549)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
ALT : exists2 x : nat_eqType,
x \in iota 0 B &
interference_bound_function tsk n x
!= interference_bound_function tsk n.+1 x
============================
are_not_equivalent_at_values_less_than
(interference_bound_function tsk (n.+1 - ε))
(interference_bound_function tsk n.+1) B
----------------------------------------------------------------------------- *)
move: ALT ⇒ [y IN N].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 591)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
IN : y \in iota 0 B
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
============================
are_not_equivalent_at_values_less_than
(interference_bound_function tsk (n.+1 - ε))
(interference_bound_function tsk n.+1) B
----------------------------------------------------------------------------- *)
∃ y.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 593)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
IN : y \in iota 0 B
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
============================
y < B /\
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
move: IN; rewrite mem_iota add0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 605)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
============================
0 <= y < B ->
y < B /\
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
move ⇒ /andP [_ LT].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 644)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
LT : y < B
============================
y < B /\
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 647)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
LT : y < B
============================
interference_bound_function tsk (n.+1 - ε) y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
rewrite subn1 -pred_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 653)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
N : interference_bound_function tsk n y
!= interference_bound_function tsk n.+1 y
LT : y < B
============================
interference_bound_function tsk n y <>
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
intros CONTR; move: N ⇒ /negP N; apply: N.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 688)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A : duration
n : nat
H_A_less_than_B : n.+1 < B
ASP : nat
NEQ : ASP <= n
EQ : are_equivalent_at_values_less_than (interference_bound_function tsk n)
(interference_bound_function tsk ASP) B
SP : is_in_search_space ASP
y : nat_eqType
LT : y < B
CONTR : interference_bound_function tsk n y =
interference_bound_function tsk n.+1 y
============================
interference_bound_function tsk n y ==
interference_bound_function tsk n.+1 y
----------------------------------------------------------------------------- *)
by rewrite CONTR.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End ExistenceOfRepresentative.
In this section we prove that any solution of the response-time recurrence for
a given point [A_sp] in the search space also gives a solution for any point
A that shares the same interference bound.
Suppose [A_sp + F_sp] is a "small" solution (i.e. less than [B]) of the response-time recurrence.
Variables A_sp F_sp : duration.
Hypothesis H_less_than : A_sp + F_sp < B.
Hypothesis H_fixpoint : A_sp + F_sp = interference_bound_function tsk A_sp (A_sp + F_sp).
Hypothesis H_less_than : A_sp + F_sp < B.
Hypothesis H_fixpoint : A_sp + F_sp = interference_bound_function tsk A_sp (A_sp + F_sp).
Next, let [A] be any point such that: (a) [A_sp <= A <= A_sp + F_sp] and
(b) [interference_bound_function(A, x)] is equal to
[interference_bound_function(A_sp, x)] for all [x] less than [B].
Variable A : duration.
Hypothesis H_bounds_for_A : A_sp ≤ A ≤ A_sp + F_sp.
Hypothesis H_equivalent :
are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B.
Hypothesis H_bounds_for_A : A_sp ≤ A ≤ A_sp + F_sp.
Hypothesis H_equivalent :
are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B.
We prove that there exists a constant [F] such that [A + F] is equal to [A_sp + F_sp]
and [A + F] is a solution for the response-time recurrence for [A].
Lemma solution_for_A_exists:
∃ F,
A_sp + F_sp = A + F ∧
F ≤ F_sp ∧
A + F = interference_bound_function tsk A (A + F).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
H_less_than : A_sp + F_sp < B
H_fixpoint : A_sp + F_sp =
interference_bound_function tsk A_sp (A_sp + F_sp)
A : duration
H_bounds_for_A : A_sp <= A <= A_sp + F_sp
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
============================
exists F : nat,
A_sp + F_sp = A + F /\
F <= F_sp /\ A + F = interference_bound_function tsk A (A + F)
----------------------------------------------------------------------------- *)
Proof.
move: H_bounds_for_A ⇒ /andP [NEQ1 NEQ2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
H_less_than : A_sp + F_sp < B
H_fixpoint : A_sp + F_sp =
interference_bound_function tsk A_sp (A_sp + F_sp)
A : duration
H_bounds_for_A : A_sp <= A <= A_sp + F_sp
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= A_sp + F_sp
============================
exists F : nat,
A_sp + F_sp = A + F /\
F <= F_sp /\ A + F = interference_bound_function tsk A (A + F)
----------------------------------------------------------------------------- *)
set (X := A_sp + F_sp) in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
X := A_sp + F_sp : nat
H_less_than : X < B
H_fixpoint : X = interference_bound_function tsk A_sp X
A : duration
H_bounds_for_A : A_sp <= A <= X
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= X
============================
exists F : nat,
X = A + F /\
F <= F_sp /\ A + F = interference_bound_function tsk A (A + F)
----------------------------------------------------------------------------- *)
∃ (X - A); split; last split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 79)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
X := A_sp + F_sp : nat
H_less_than : X < B
H_fixpoint : X = interference_bound_function tsk A_sp X
A : duration
H_bounds_for_A : A_sp <= A <= X
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= X
============================
X = A + (X - A)
subgoal 2 (ID 82) is:
X - A <= F_sp
subgoal 3 (ID 83) is:
A + (X - A) = interference_bound_function tsk A (A + (X - A))
----------------------------------------------------------------------------- *)
- by rewrite subnKC.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 82)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
X := A_sp + F_sp : nat
H_less_than : X < B
H_fixpoint : X = interference_bound_function tsk A_sp X
A : duration
H_bounds_for_A : A_sp <= A <= X
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= X
============================
X - A <= F_sp
subgoal 2 (ID 83) is:
A + (X - A) = interference_bound_function tsk A (A + (X - A))
----------------------------------------------------------------------------- *)
- by rewrite leq_subLR /X leq_add2r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 83)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
X := A_sp + F_sp : nat
H_less_than : X < B
H_fixpoint : X = interference_bound_function tsk A_sp X
A : duration
H_bounds_for_A : A_sp <= A <= X
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= X
============================
A + (X - A) = interference_bound_function tsk A (A + (X - A))
----------------------------------------------------------------------------- *)
- by rewrite subnKC // H_equivalent.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FixpointSolutionForAnotherA.
End AbstractRTAReduction.
∃ F,
A_sp + F_sp = A + F ∧
F ≤ F_sp ∧
A + F = interference_bound_function tsk A (A + F).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 28)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
H_less_than : A_sp + F_sp < B
H_fixpoint : A_sp + F_sp =
interference_bound_function tsk A_sp (A_sp + F_sp)
A : duration
H_bounds_for_A : A_sp <= A <= A_sp + F_sp
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
============================
exists F : nat,
A_sp + F_sp = A + F /\
F <= F_sp /\ A + F = interference_bound_function tsk A (A + F)
----------------------------------------------------------------------------- *)
Proof.
move: H_bounds_for_A ⇒ /andP [NEQ1 NEQ2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
H_less_than : A_sp + F_sp < B
H_fixpoint : A_sp + F_sp =
interference_bound_function tsk A_sp (A_sp + F_sp)
A : duration
H_bounds_for_A : A_sp <= A <= A_sp + F_sp
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= A_sp + F_sp
============================
exists F : nat,
A_sp + F_sp = A + F /\
F <= F_sp /\ A + F = interference_bound_function tsk A (A + F)
----------------------------------------------------------------------------- *)
set (X := A_sp + F_sp) in ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 75)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
X := A_sp + F_sp : nat
H_less_than : X < B
H_fixpoint : X = interference_bound_function tsk A_sp X
A : duration
H_bounds_for_A : A_sp <= A <= X
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= X
============================
exists F : nat,
X = A + F /\
F <= F_sp /\ A + F = interference_bound_function tsk A (A + F)
----------------------------------------------------------------------------- *)
∃ (X - A); split; last split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 79)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
X := A_sp + F_sp : nat
H_less_than : X < B
H_fixpoint : X = interference_bound_function tsk A_sp X
A : duration
H_bounds_for_A : A_sp <= A <= X
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= X
============================
X = A + (X - A)
subgoal 2 (ID 82) is:
X - A <= F_sp
subgoal 3 (ID 83) is:
A + (X - A) = interference_bound_function tsk A (A + (X - A))
----------------------------------------------------------------------------- *)
- by rewrite subnKC.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 82)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
X := A_sp + F_sp : nat
H_less_than : X < B
H_fixpoint : X = interference_bound_function tsk A_sp X
A : duration
H_bounds_for_A : A_sp <= A <= X
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= X
============================
X - A <= F_sp
subgoal 2 (ID 83) is:
A + (X - A) = interference_bound_function tsk A (A + (X - A))
----------------------------------------------------------------------------- *)
- by rewrite leq_subLR /X leq_add2r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 83)
Task : TaskType
tsk : Task
B : duration
interference_bound_function : Task -> duration -> duration -> duration
A_sp, F_sp : duration
X := A_sp + F_sp : nat
H_less_than : X < B
H_fixpoint : X = interference_bound_function tsk A_sp X
A : duration
H_bounds_for_A : A_sp <= A <= X
H_equivalent : are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B
NEQ1 : A_sp <= A
NEQ2 : A <= X
============================
A + (X - A) = interference_bound_function tsk A (A + (X - A))
----------------------------------------------------------------------------- *)
- by rewrite subnKC // H_equivalent.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FixpointSolutionForAnotherA.
End AbstractRTAReduction.