Library prosa.analysis.facts.periodic.task_arrivals_size
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.periodic.arrival_times.
Require Export prosa.analysis.definitions.infinite_jobs.
In this file we prove some properties concerning the size
of task arrivals in context of the periodic model.
Consider any type of periodic tasks with an offset ...
... and any type of jobs associated with these tasks.
Consider any unique arrival sequence with consistent arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
... and any periodic task [tsk] with a valid offset and period.
Variable tsk : Task.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_valid_period: valid_period tsk.
Hypothesis H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk.
Hypothesis H_valid_offset: valid_offset arr_seq tsk.
Hypothesis H_valid_period: valid_period tsk.
Hypothesis H_task_respects_periodic_model: respects_periodic_task_model arr_seq tsk.
We show that if an instant [t] is not an "arrival time" for
task [tsk] then [task_arrivals_at arr_seq tsk t] is an empty sequence.
Lemma task_arrivals_size_at_non_arrival:
∀ t,
(∀ n, t ≠ task_offset tsk + n × task_period tsk) →
task_arrivals_at arr_seq tsk t = [::].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 46)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
============================
forall t : nat,
(forall n : nat, t <> task_offset tsk + n * task_period tsk) ->
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
Proof.
intros × T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
have EMPT_OR_EXISTS : ∀ xs, xs = [::] ∨ ∃ a, a \in xs.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 62)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
============================
forall (t0 : eqType) (xs : seq t0), xs = [::] \/ (exists a : t0, a \in xs)
subgoal 2 (ID 64) is:
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
============================
forall (t0 : eqType) (xs : seq t0), xs = [::] \/ (exists a : t0, a \in xs)
----------------------------------------------------------------------------- *)
intros ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 66)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
t0 : eqType
xs : seq t0
============================
xs = [::] \/ (exists a : t0, a \in xs)
----------------------------------------------------------------------------- *)
induction xs; first by left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
t0 : eqType
a : t0
xs : seq t0
IHxs : xs = [::] \/ (exists a : t0, a \in xs)
============================
a :: xs = [::] \/ (exists a0 : t0, a0 \in a :: xs)
----------------------------------------------------------------------------- *)
right; ∃ a.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
t0 : eqType
a : t0
xs : seq t0
IHxs : xs = [::] \/ (exists a : t0, a \in xs)
============================
a \in a :: xs
----------------------------------------------------------------------------- *)
now apply mem_head.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 64) is:
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 95)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
A_IN : a \in task_arrivals_at arr_seq tsk t
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN ⇒ /andP [/eqP TSK A_ARR].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 226)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_ARR : a \in arrivals_at arr_seq t
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
move : (A_ARR) ⇒ A_IN; apply H_consistent_arrivals in A_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 230)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_ARR : a \in arrivals_at arr_seq t
A_IN : job_arrival a = t
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 289)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_IN : job_arrival a = t
T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR : a \in arr_seq t
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
apply in_arrseq_implies_arrives in A_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 292)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_IN : job_arrival a = t
T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR : arrives_in arr_seq a
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
have EXISTS_N : ∃ n, job_arrival a = task_offset tsk + n × task_period tsk by
apply job_arrival_times with (arr_seq0 := arr_seq) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 316)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_IN : job_arrival a = t
T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR : arrives_in arr_seq a
EXISTS_N : exists n : nat,
job_arrival a = task_offset tsk + n * task_period tsk
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
move : EXISTS_N ⇒ [n A_ARRIVAL].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 329)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_IN : job_arrival a = t
T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR : arrives_in arr_seq a
n : nat
A_ARRIVAL : job_arrival a = task_offset tsk + n * task_period tsk
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
now move : (T n) ⇒ T1.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
(∀ n, t ≠ task_offset tsk + n × task_period tsk) →
task_arrivals_at arr_seq tsk t = [::].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 46)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
============================
forall t : nat,
(forall n : nat, t <> task_offset tsk + n * task_period tsk) ->
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
Proof.
intros × T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
have EMPT_OR_EXISTS : ∀ xs, xs = [::] ∨ ∃ a, a \in xs.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 62)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
============================
forall (t0 : eqType) (xs : seq t0), xs = [::] \/ (exists a : t0, a \in xs)
subgoal 2 (ID 64) is:
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
============================
forall (t0 : eqType) (xs : seq t0), xs = [::] \/ (exists a : t0, a \in xs)
----------------------------------------------------------------------------- *)
intros ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 66)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
t0 : eqType
xs : seq t0
============================
xs = [::] \/ (exists a : t0, a \in xs)
----------------------------------------------------------------------------- *)
induction xs; first by left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
t0 : eqType
a : t0
xs : seq t0
IHxs : xs = [::] \/ (exists a : t0, a \in xs)
============================
a :: xs = [::] \/ (exists a0 : t0, a0 \in a :: xs)
----------------------------------------------------------------------------- *)
right; ∃ a.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 80)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
t0 : eqType
a : t0
xs : seq t0
IHxs : xs = [::] \/ (exists a : t0, a \in xs)
============================
a \in a :: xs
----------------------------------------------------------------------------- *)
now apply mem_head.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 64) is:
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 64)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
destruct (EMPT_OR_EXISTS Job (task_arrivals_at arr_seq tsk t)) as [EMPT | [a A_IN]] ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 95)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
A_IN : a \in task_arrivals_at arr_seq tsk t
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
rewrite /task_arrivals_at mem_filter in A_IN; move : A_IN ⇒ /andP [/eqP TSK A_ARR].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 226)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_ARR : a \in arrivals_at arr_seq t
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
move : (A_ARR) ⇒ A_IN; apply H_consistent_arrivals in A_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 230)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
T : forall n : nat, t <> task_offset tsk + n * task_period tsk
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_ARR : a \in arrivals_at arr_seq t
A_IN : job_arrival a = t
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
rewrite -A_IN in T; rewrite /arrivals_at in A_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 289)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_IN : job_arrival a = t
T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR : a \in arr_seq t
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
apply in_arrseq_implies_arrives in A_ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 292)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_IN : job_arrival a = t
T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR : arrives_in arr_seq a
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
have EXISTS_N : ∃ n, job_arrival a = task_offset tsk + n × task_period tsk by
apply job_arrival_times with (arr_seq0 := arr_seq) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 316)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_IN : job_arrival a = t
T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR : arrives_in arr_seq a
EXISTS_N : exists n : nat,
job_arrival a = task_offset tsk + n * task_period tsk
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
move : EXISTS_N ⇒ [n A_ARRIVAL].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 329)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : nat
EMPT_OR_EXISTS : forall (t : eqType) (xs : seq t),
xs = [::] \/ (exists a : t, a \in xs)
a : Job
TSK : job_task a = tsk
A_IN : job_arrival a = t
T : forall n : nat, job_arrival a <> task_offset tsk + n * task_period tsk
A_ARR : arrives_in arr_seq a
n : nat
A_ARRIVAL : job_arrival a = task_offset tsk + n * task_period tsk
============================
task_arrivals_at arr_seq tsk t = [::]
----------------------------------------------------------------------------- *)
now move : (T n) ⇒ T1.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that at any instant [t], at most one job of task [tsk]
can arrive (i.e. size of [task_arrivals_at arr_seq tsk t] is at most one).
Lemma task_arrivals_at_size_cases:
∀ t,
size (task_arrivals_at arr_seq tsk t) = 0 ∨
size (task_arrivals_at arr_seq tsk t) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
============================
forall t : instant,
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
Proof.
intro t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) ⇒ [LT|GT|EQ]; try by auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 119)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
LT : size (task_arrivals_at arr_seq tsk t) < 1
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
subgoal 2 (ID 120) is:
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
destruct (size (task_arrivals_at arr_seq tsk t)); now left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 120)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
specialize (exists_two Job (task_arrivals_at arr_seq tsk t)) ⇒ EXISTS_TWO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 224)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
EXISTS_TWO : 1 < size (task_arrivals_at arr_seq tsk t) ->
uniq (task_arrivals_at arr_seq tsk t) ->
exists a b : Job,
a <> b /\
a \in task_arrivals_at arr_seq tsk t /\
b \in task_arrivals_at arr_seq tsk t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 249)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
A_IN : a \in task_arrivals_at arr_seq tsk t
B_IN : b \in task_arrivals_at arr_seq tsk t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 316)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
A_IN : (job_task a == tsk) && (a \in arrivals_at arr_seq t)
B_IN : (job_task b == tsk) && (b \in arrivals_at arr_seq t)
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
move: A_IN B_IN ⇒ /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 459)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
move: (ARRA); move: (ARRB); rewrite /arrivals_at ⇒ A_IN B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 466)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : b \in arr_seq t
B_IN : a \in arr_seq t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 472)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
have SPO : respects_sporadic_task_model arr_seq tsk; try by auto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 481)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
SPO : respects_sporadic_task_model arr_seq tsk
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
have EQ_ARR_A : (job_arrival a = t) by apply H_consistent_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 544)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
SPO : respects_sporadic_task_model arr_seq tsk
EQ_ARR_A : job_arrival a = t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
have EQ_ARR_B : (job_arrival b = t) by apply H_consistent_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 551)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
SPO : respects_sporadic_task_model arr_seq tsk
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
specialize (SPO a b); feed_n 6 SPO ⇒ //; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 589)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
SPO : job_arrival a + task_min_inter_arrival_time tsk <= job_arrival b
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
rewrite EQ_ARR_A EQ_ARR_B in SPO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1656)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
SPO : t + task_min_inter_arrival_time tsk <= t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
rewrite /task_min_inter_arrival_time /periodic_as_sporadic in SPO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1700)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
SPO : t + task_period tsk <= t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
have POS : task_period tsk > 0 by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1705)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
SPO : t + task_period tsk <= t
POS : 0 < task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ t,
size (task_arrivals_at arr_seq tsk t) = 0 ∨
size (task_arrivals_at arr_seq tsk t) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 58)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
============================
forall t : instant,
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
Proof.
intro t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
case: (ltngtP (size (task_arrivals_at arr_seq tsk t)) 1) ⇒ [LT|GT|EQ]; try by auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 119)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
LT : size (task_arrivals_at arr_seq tsk t) < 1
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
subgoal 2 (ID 120) is:
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
destruct (size (task_arrivals_at arr_seq tsk t)); now left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 120)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
specialize (exists_two Job (task_arrivals_at arr_seq tsk t)) ⇒ EXISTS_TWO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 224)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
EXISTS_TWO : 1 < size (task_arrivals_at arr_seq tsk t) ->
uniq (task_arrivals_at arr_seq tsk t) ->
exists a b : Job,
a <> b /\
a \in task_arrivals_at arr_seq tsk t /\
b \in task_arrivals_at arr_seq tsk t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
destruct EXISTS_TWO as [a [b [NEQ [A_IN B_IN]]]]; [by done | by apply filter_uniq | ].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 249)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
A_IN : a \in task_arrivals_at arr_seq tsk t
B_IN : b \in task_arrivals_at arr_seq tsk t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
rewrite mem_filter in A_IN; rewrite mem_filter in B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 316)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
A_IN : (job_task a == tsk) && (a \in arrivals_at arr_seq t)
B_IN : (job_task b == tsk) && (b \in arrivals_at arr_seq t)
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
move: A_IN B_IN ⇒ /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 459)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
move: (ARRA); move: (ARRB); rewrite /arrivals_at ⇒ A_IN B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 466)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : b \in arr_seq t
B_IN : a \in arr_seq t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 472)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
have SPO : respects_sporadic_task_model arr_seq tsk; try by auto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 481)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
SPO : respects_sporadic_task_model arr_seq tsk
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
have EQ_ARR_A : (job_arrival a = t) by apply H_consistent_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 544)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
SPO : respects_sporadic_task_model arr_seq tsk
EQ_ARR_A : job_arrival a = t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
have EQ_ARR_B : (job_arrival b = t) by apply H_consistent_arrivals.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 551)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
SPO : respects_sporadic_task_model arr_seq tsk
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
specialize (SPO a b); feed_n 6 SPO ⇒ //; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 589)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
SPO : job_arrival a + task_min_inter_arrival_time tsk <= job_arrival b
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
rewrite EQ_ARR_A EQ_ARR_B in SPO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1656)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
SPO : t + task_min_inter_arrival_time tsk <= t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
rewrite /task_min_inter_arrival_time /periodic_as_sporadic in SPO.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1700)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
SPO : t + task_period tsk <= t
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
have POS : task_period tsk > 0 by auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1705)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
t : instant
GT : 1 < size (task_arrivals_at arr_seq tsk t)
a, b : Job
NEQ : a <> b
TSKA : job_task a = tsk
ARRA : a \in arrivals_at arr_seq t
TSKB : job_task b = tsk
ARRB : b \in arrivals_at arr_seq t
A_IN : arrives_in arr_seq b
B_IN : arrives_in arr_seq a
EQ_ARR_A : job_arrival a = t
EQ_ARR_B : job_arrival b = t
SPO : t + task_period tsk <= t
POS : 0 < task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) = 0 \/
size (task_arrivals_at arr_seq tsk t) = 1
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that the size of task arrivals (strictly) between two consecutive arrival
times is zero.
Lemma size_task_arrivals_between_eq0:
∀ n,
let l := (task_offset tsk + n × task_period tsk).+1 in
let r := (task_offset tsk + n.+1 × task_period tsk) in
size (task_arrivals_between arr_seq tsk l r) = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
============================
forall n : nat,
let l := (task_offset tsk + n * task_period tsk).+1 in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_between arr_seq tsk l r) = 0
----------------------------------------------------------------------------- *)
Proof.
intros n l r; rewrite /l /r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
============================
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk)) = 0
----------------------------------------------------------------------------- *)
rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 129)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t : nat
INEQ : task_offset tsk + n * task_period tsk < t <
task_offset tsk + n.+1 * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) = 0
----------------------------------------------------------------------------- *)
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n1 EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 166)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t : nat
INEQ : task_offset tsk + n * task_period tsk < t <
task_offset tsk + n.+1 * task_period tsk
n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
============================
False
----------------------------------------------------------------------------- *)
rewrite EQ in INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 195)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t, n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
INEQ : task_offset tsk + n * task_period tsk <
task_offset tsk + n1 * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
============================
False
----------------------------------------------------------------------------- *)
move : INEQ ⇒ /andP [INEQ1 INEQ2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 236)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t, n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
INEQ1 : task_offset tsk + n * task_period tsk <
task_offset tsk + n1 * task_period tsk
INEQ2 : task_offset tsk + n1 * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
============================
False
----------------------------------------------------------------------------- *)
rewrite ltn_add2l ltn_mul2r in INEQ1; rewrite ltn_add2l ltn_mul2r in INEQ2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 312)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t, n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
INEQ1 : (0 < task_period tsk) && (n < n1)
INEQ2 : (0 < task_period tsk) && (n1 < n.+1)
============================
False
----------------------------------------------------------------------------- *)
move : INEQ1 INEQ2 ⇒ /andP [A B] /andP [C D].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 393)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t, n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
A : 0 < task_period tsk
B : n < n1
C : 0 < task_period tsk
D : n1 < n.+1
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ n,
let l := (task_offset tsk + n × task_period tsk).+1 in
let r := (task_offset tsk + n.+1 × task_period tsk) in
size (task_arrivals_between arr_seq tsk l r) = 0.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 73)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
============================
forall n : nat,
let l := (task_offset tsk + n * task_period tsk).+1 in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_between arr_seq tsk l r) = 0
----------------------------------------------------------------------------- *)
Proof.
intros n l r; rewrite /l /r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 78)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
============================
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk)) = 0
----------------------------------------------------------------------------- *)
rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 129)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t : nat
INEQ : task_offset tsk + n * task_period tsk < t <
task_offset tsk + n.+1 * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) = 0
----------------------------------------------------------------------------- *)
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n1 EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 166)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t : nat
INEQ : task_offset tsk + n * task_period tsk < t <
task_offset tsk + n.+1 * task_period tsk
n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
============================
False
----------------------------------------------------------------------------- *)
rewrite EQ in INEQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 195)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t, n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
INEQ : task_offset tsk + n * task_period tsk <
task_offset tsk + n1 * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
============================
False
----------------------------------------------------------------------------- *)
move : INEQ ⇒ /andP [INEQ1 INEQ2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 236)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t, n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
INEQ1 : task_offset tsk + n * task_period tsk <
task_offset tsk + n1 * task_period tsk
INEQ2 : task_offset tsk + n1 * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
============================
False
----------------------------------------------------------------------------- *)
rewrite ltn_add2l ltn_mul2r in INEQ1; rewrite ltn_add2l ltn_mul2r in INEQ2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 312)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t, n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
INEQ1 : (0 < task_period tsk) && (n < n1)
INEQ2 : (0 < task_period tsk) && (n1 < n.+1)
============================
False
----------------------------------------------------------------------------- *)
move : INEQ1 INEQ2 ⇒ /andP [A B] /andP [C D].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 393)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
n : nat
l := (task_offset tsk + n * task_period tsk).+1 : nat
r := task_offset tsk + n.+1 * task_period tsk : nat
t, n1 : nat
EQ : t = task_offset tsk + n1 * task_period tsk
A : 0 < task_period tsk
B : n < n1
C : 0 < task_period tsk
D : n1 < n.+1
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
In this section we show some properties of task arrivals in case
of an infinite sequence of jobs.
Assume that we have an infinite sequence of jobs.
We show that for any number [n], there exists a job [j] of task [tsk]
such that [job_index] of [j] is equal to [n] and [j] arrives
at [task_offset tsk + n * task_period tsk].
Lemma jobs_exists_later:
∀ n,
∃ j,
arrives_in arr_seq j ∧
job_task j = tsk ∧
job_arrival j = task_offset tsk + n × task_period tsk ∧
job_index arr_seq j = n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 98)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
forall n : nat,
exists j : Job,
arrives_in arr_seq j /\
job_task j = tsk /\
job_arrival j = task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n
----------------------------------------------------------------------------- *)
Proof.
intros ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 99)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
============================
exists j : Job,
arrives_in arr_seq j /\
job_task j = tsk /\
job_arrival j = task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n
----------------------------------------------------------------------------- *)
destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 113)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : job_index arr_seq j = n
============================
exists j0 : Job,
arrives_in arr_seq j0 /\
job_task j0 = tsk /\
job_arrival j0 = task_offset tsk + n * task_period tsk /\
job_index arr_seq j0 = n
----------------------------------------------------------------------------- *)
∃ j; repeat split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 243)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : job_index arr_seq j = n
============================
job_arrival j = task_offset tsk + n * task_period tsk
----------------------------------------------------------------------------- *)
now apply periodic_arrival_times with (arr_seq0 := arr_seq) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ n,
∃ j,
arrives_in arr_seq j ∧
job_task j = tsk ∧
job_arrival j = task_offset tsk + n × task_period tsk ∧
job_index arr_seq j = n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 98)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
forall n : nat,
exists j : Job,
arrives_in arr_seq j /\
job_task j = tsk /\
job_arrival j = task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n
----------------------------------------------------------------------------- *)
Proof.
intros ×.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 99)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
============================
exists j : Job,
arrives_in arr_seq j /\
job_task j = tsk /\
job_arrival j = task_offset tsk + n * task_period tsk /\
job_index arr_seq j = n
----------------------------------------------------------------------------- *)
destruct (H_infinite_jobs tsk n) as [j [ARR [TSK IND]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 113)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : job_index arr_seq j = n
============================
exists j0 : Job,
arrives_in arr_seq j0 /\
job_task j0 = tsk /\
job_arrival j0 = task_offset tsk + n * task_period tsk /\
job_index arr_seq j0 = n
----------------------------------------------------------------------------- *)
∃ j; repeat split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 243)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
j : Job
ARR : arrives_in arr_seq j
TSK : job_task j = tsk
IND : job_index arr_seq j = n
============================
job_arrival j = task_offset tsk + n * task_period tsk
----------------------------------------------------------------------------- *)
now apply periodic_arrival_times with (arr_seq0 := arr_seq) ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that the size of task arrivals at any arrival time is equal to one.
Lemma task_arrivals_at_size:
∀ n,
let l := (task_offset tsk + n × task_period tsk) in
size (task_arrivals_at arr_seq tsk l) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 109)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
----------------------------------------------------------------------------- *)
Proof.
intros n l; rewrite /l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
l := task_offset tsk + n * task_period tsk : nat
============================
size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
1
----------------------------------------------------------------------------- *)
move : (jobs_exists_later n) ⇒ [j' [ARR [TSK [ARRIVAL IND]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 154)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
l := task_offset tsk + n * task_period tsk : nat
j' : Job
ARR : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk + n * task_period tsk
IND : job_index arr_seq j' = n
============================
size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
1
----------------------------------------------------------------------------- *)
apply only_j_in_task_arrivals_at_j with (tsk0 := tsk) in ARR ⇒ //; last by
auto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 162)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
l := task_offset tsk + n * task_period tsk : nat
j' : Job
ARR : task_arrivals_at_job_arrival arr_seq j' = [:: j']
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk + n * task_period tsk
IND : job_index arr_seq j' = n
============================
size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
1
----------------------------------------------------------------------------- *)
rewrite /task_arrivals_at_job_arrival TSK in ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 266)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
l := task_offset tsk + n * task_period tsk : nat
j' : Job
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk + n * task_period tsk
IND : job_index arr_seq j' = n
ARR : task_arrivals_at arr_seq tsk (job_arrival j') = [:: j']
============================
size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
1
----------------------------------------------------------------------------- *)
now rewrite -ARRIVAL ARR.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ n,
let l := (task_offset tsk + n × task_period tsk) in
size (task_arrivals_at arr_seq tsk l) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 109)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
----------------------------------------------------------------------------- *)
Proof.
intros n l; rewrite /l.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 112)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
l := task_offset tsk + n * task_period tsk : nat
============================
size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
1
----------------------------------------------------------------------------- *)
move : (jobs_exists_later n) ⇒ [j' [ARR [TSK [ARRIVAL IND]]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 154)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
l := task_offset tsk + n * task_period tsk : nat
j' : Job
ARR : arrives_in arr_seq j'
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk + n * task_period tsk
IND : job_index arr_seq j' = n
============================
size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
1
----------------------------------------------------------------------------- *)
apply only_j_in_task_arrivals_at_j with (tsk0 := tsk) in ARR ⇒ //; last by
auto with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 162)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
l := task_offset tsk + n * task_period tsk : nat
j' : Job
ARR : task_arrivals_at_job_arrival arr_seq j' = [:: j']
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk + n * task_period tsk
IND : job_index arr_seq j' = n
============================
size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
1
----------------------------------------------------------------------------- *)
rewrite /task_arrivals_at_job_arrival TSK in ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 266)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
l := task_offset tsk + n * task_period tsk : nat
j' : Job
TSK : job_task j' = tsk
ARRIVAL : job_arrival j' = task_offset tsk + n * task_period tsk
IND : job_index arr_seq j' = n
ARR : task_arrivals_at arr_seq tsk (job_arrival j') = [:: j']
============================
size (task_arrivals_at arr_seq tsk (task_offset tsk + n * task_period tsk)) =
1
----------------------------------------------------------------------------- *)
now rewrite -ARRIVAL ARR.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that the size of task arrivals up to [task_offset tsk] is equal to one.
Lemma size_task_arrivals_up_to_offset:
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1
----------------------------------------------------------------------------- *)
Proof.
rewrite /task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1) = 1
----------------------------------------------------------------------------- *)
specialize (task_arrivals_between_cat arr_seq tsk 0 (task_offset tsk) (task_offset tsk).+1) ⇒ CAT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 134)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : 0 <= task_offset tsk ->
task_offset tsk <= (task_offset tsk).+1 ->
task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1) = 1
----------------------------------------------------------------------------- *)
feed_n 2 CAT ⇒ //; rewrite CAT size_cat.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
1
----------------------------------------------------------------------------- *)
have Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 182)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
subgoal 2 (ID 184) is:
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 182)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
----------------------------------------------------------------------------- *)
rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t T_EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 235)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
t : nat
T_EQ : 0 <= t < task_offset tsk
============================
size (task_arrivals_at arr_seq tsk t) = 0
----------------------------------------------------------------------------- *)
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 272)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
t : nat
T_EQ : 0 <= t < task_offset tsk
n : nat
EQ : t = task_offset tsk + n * task_period tsk
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 184) is:
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 184)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
1
----------------------------------------------------------------------------- *)
rewrite Z add0n /task_arrivals_between /arrivals_between big_nat1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 513)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
============================
size [seq j <- arrivals_at arr_seq (task_offset tsk) | job_task j == tsk] =
1
----------------------------------------------------------------------------- *)
specialize (task_arrivals_at_size 0) ⇒ AT_SIZE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 516)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
AT_SIZE : let l := task_offset tsk + 0 * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
============================
size [seq j <- arrivals_at arr_seq (task_offset tsk) | job_task j == tsk] =
1
----------------------------------------------------------------------------- *)
now rewrite mul0n addn0 in AT_SIZE.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1
----------------------------------------------------------------------------- *)
Proof.
rewrite /task_arrivals_up_to.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 124)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1) = 1
----------------------------------------------------------------------------- *)
specialize (task_arrivals_between_cat arr_seq tsk 0 (task_offset tsk) (task_offset tsk).+1) ⇒ CAT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 134)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : 0 <= task_offset tsk ->
task_offset tsk <= (task_offset tsk).+1 ->
task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1) = 1
----------------------------------------------------------------------------- *)
feed_n 2 CAT ⇒ //; rewrite CAT size_cat.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
1
----------------------------------------------------------------------------- *)
have Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 182)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
subgoal 2 (ID 184) is:
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 182)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
----------------------------------------------------------------------------- *)
rewrite size_of_task_arrivals_between big_nat_eq0 ⇒ //; intros t T_EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 235)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
t : nat
T_EQ : 0 <= t < task_offset tsk
============================
size (task_arrivals_at arr_seq tsk t) = 0
----------------------------------------------------------------------------- *)
rewrite task_arrivals_size_at_non_arrival ⇒ //; intros n EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 272)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
t : nat
T_EQ : 0 <= t < task_offset tsk
n : nat
EQ : t = task_offset tsk + n * task_period tsk
============================
False
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 184) is:
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 184)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
============================
size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) +
size
(task_arrivals_between arr_seq tsk (task_offset tsk) (task_offset tsk).+1) =
1
----------------------------------------------------------------------------- *)
rewrite Z add0n /task_arrivals_between /arrivals_between big_nat1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 513)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
============================
size [seq j <- arrivals_at arr_seq (task_offset tsk) | job_task j == tsk] =
1
----------------------------------------------------------------------------- *)
specialize (task_arrivals_at_size 0) ⇒ AT_SIZE.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 516)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
CAT : task_arrivals_between arr_seq tsk 0 (task_offset tsk).+1 =
task_arrivals_between arr_seq tsk 0 (task_offset tsk) ++
task_arrivals_between arr_seq tsk (task_offset tsk)
(task_offset tsk).+1
Z : size (task_arrivals_between arr_seq tsk 0 (task_offset tsk)) = 0
AT_SIZE : let l := task_offset tsk + 0 * task_period tsk in
size (task_arrivals_at arr_seq tsk l) = 1
============================
size [seq j <- arrivals_at arr_seq (task_offset tsk) | job_task j == tsk] =
1
----------------------------------------------------------------------------- *)
now rewrite mul0n addn0 in AT_SIZE.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that for any number [n], the number of jobs released by task [tsk] up to
[task_offset tsk + n * task_period tsk] is equal to [n + 1].
Lemma task_arrivals_up_to_size:
∀ n,
let l := (task_offset tsk + n × task_period tsk) in
let r := (task_offset tsk + n.+1 × task_period tsk) in
size (task_arrivals_up_to arr_seq tsk l) = n + 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
----------------------------------------------------------------------------- *)
Proof.
induction n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 137)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
let l := task_offset tsk + 0 * task_period tsk in
let r := task_offset tsk + 1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = 0 + 1
subgoal 2 (ID 140) is:
let l := task_offset tsk + n.+1 * task_period tsk in
let r := task_offset tsk + n.+2 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
intros l r; rewrite /l mul0n add0n addn0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 158)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
l := task_offset tsk + 0 * task_period tsk : nat
r := task_offset tsk + 1 * task_period tsk : nat
============================
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1
subgoal 2 (ID 140) is:
let l := task_offset tsk + n.+1 * task_period tsk in
let r := task_offset tsk + n.+2 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
now apply size_task_arrivals_up_to_offset.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 140)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
============================
let l := task_offset tsk + n.+1 * task_period tsk in
let r := task_offset tsk + n.+2 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
intros l r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
============================
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
specialize (task_arrivals_cat arr_seq tsk (task_offset tsk + n × task_period tsk)
(task_offset tsk + n.+1 × task_period tsk)) ⇒ CAT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_offset tsk + n * task_period tsk <=
task_offset tsk + n.+1 * task_period tsk ->
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
============================
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
feed_n 1 CAT; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 180)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
============================
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
rewrite CAT size_cat IHn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 973)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
specialize (task_arrivals_between_cat arr_seq tsk (task_offset tsk + n × task_period tsk).+1
(task_offset tsk + n.+1 × task_period tsk) (task_offset tsk + n.+1 × task_period tsk).+1) ⇒ S_CAT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 991)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
feed_n 2 S_CAT; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 992)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
subgoal 2 (ID 1003) is:
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 992)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
----------------------------------------------------------------------------- *)
rewrite ltn_add2l ltn_mul2r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 4928)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
(0 < task_period tsk) && (n < n.+1)
----------------------------------------------------------------------------- *)
now apply /andP; split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 1003) is:
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1003)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 4980)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 +
(size
[seq j <- \cat_((task_offset tsk + n * task_period tsk).+1<=t<
task_offset tsk + n.+1 * task_period tsk)
arrivals_at arr_seq t
| job_task j == tsk] +
size
[seq j <- arrivals_at arr_seq (task_offset tsk + n.+1 * task_period tsk)
| job_task j == tsk]) = n.+1 + 1
----------------------------------------------------------------------------- *)
rewrite size_task_arrivals_between_eq0 task_arrivals_at_size ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 4986)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 + (0 + 1) = n.+1 + 1
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ n,
let l := (task_offset tsk + n × task_period tsk) in
let r := (task_offset tsk + n.+1 × task_period tsk) in
size (task_arrivals_up_to arr_seq tsk l) = n + 1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 132)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
forall n : nat,
let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
----------------------------------------------------------------------------- *)
Proof.
induction n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 137)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
let l := task_offset tsk + 0 * task_period tsk in
let r := task_offset tsk + 1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = 0 + 1
subgoal 2 (ID 140) is:
let l := task_offset tsk + n.+1 * task_period tsk in
let r := task_offset tsk + n.+2 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
intros l r; rewrite /l mul0n add0n addn0.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 158)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
l := task_offset tsk + 0 * task_period tsk : nat
r := task_offset tsk + 1 * task_period tsk : nat
============================
size (task_arrivals_up_to arr_seq tsk (task_offset tsk)) = 1
subgoal 2 (ID 140) is:
let l := task_offset tsk + n.+1 * task_period tsk in
let r := task_offset tsk + n.+2 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
now apply size_task_arrivals_up_to_offset.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 140)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
============================
let l := task_offset tsk + n.+1 * task_period tsk in
let r := task_offset tsk + n.+2 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
intros l r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
============================
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
specialize (task_arrivals_cat arr_seq tsk (task_offset tsk + n × task_period tsk)
(task_offset tsk + n.+1 × task_period tsk)) ⇒ CAT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 174)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_offset tsk + n * task_period tsk <=
task_offset tsk + n.+1 * task_period tsk ->
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
============================
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
feed_n 1 CAT; first by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 180)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
============================
size (task_arrivals_up_to arr_seq tsk l) = n.+1 + 1
----------------------------------------------------------------------------- *)
rewrite CAT size_cat IHn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 973)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
specialize (task_arrivals_between_cat arr_seq tsk (task_offset tsk + n × task_period tsk).+1
(task_offset tsk + n.+1 × task_period tsk) (task_offset tsk + n.+1 × task_period tsk).+1) ⇒ S_CAT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 991)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
feed_n 2 S_CAT; try by ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 992)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
subgoal 2 (ID 1003) is:
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 992)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk
----------------------------------------------------------------------------- *)
rewrite ltn_add2l ltn_mul2r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 4928)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_offset tsk + n * task_period tsk <
task_offset tsk + n.+1 * task_period tsk ->
task_offset tsk + n.+1 * task_period tsk <=
(task_offset tsk + n.+1 * task_period tsk).+1 ->
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
(0 < task_period tsk) && (n < n.+1)
----------------------------------------------------------------------------- *)
now apply /andP; split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 1003) is:
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1003)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 +
size
(task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1) =
n.+1 + 1
----------------------------------------------------------------------------- *)
rewrite S_CAT size_cat /task_arrivals_between /arrivals_between big_nat1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 4980)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 +
(size
[seq j <- \cat_((task_offset tsk + n * task_period tsk).+1<=t<
task_offset tsk + n.+1 * task_period tsk)
arrivals_at arr_seq t
| job_task j == tsk] +
size
[seq j <- arrivals_at arr_seq (task_offset tsk + n.+1 * task_period tsk)
| job_task j == tsk]) = n.+1 + 1
----------------------------------------------------------------------------- *)
rewrite size_task_arrivals_between_eq0 task_arrivals_at_size ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 4986)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n : nat
IHn : let l := task_offset tsk + n * task_period tsk in
let r := task_offset tsk + n.+1 * task_period tsk in
size (task_arrivals_up_to arr_seq tsk l) = n + 1
l := task_offset tsk + n.+1 * task_period tsk : nat
r := task_offset tsk + n.+2 * task_period tsk : nat
CAT : task_arrivals_up_to arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk) =
task_arrivals_up_to arr_seq tsk
(task_offset tsk + n * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1
S_CAT : task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk).+1 =
task_arrivals_between arr_seq tsk
(task_offset tsk + n * task_period tsk).+1
(task_offset tsk + n.+1 * task_period tsk) ++
task_arrivals_between arr_seq tsk
(task_offset tsk + n.+1 * task_period tsk)
(task_offset tsk + n.+1 * task_period tsk).+1
============================
n + 1 + (0 + 1) = n.+1 + 1
----------------------------------------------------------------------------- *)
now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We show that the number of jobs released by task [tsk] at any instant [t]
and [t + n * task_period tsk] is the same for any number [n].
Lemma eq_size_of_task_arrivals_seperated_by_period:
∀ n t,
t ≥ task_offset tsk →
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n × task_period tsk)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 148)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
forall n t : nat,
task_offset tsk <= t ->
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
Proof.
intros × T_G.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 151)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
destruct (exists_or_not_add_mul_cases (task_offset tsk) (task_period tsk) t) as [[n1 JB_ARR] | JB_NOT_ARR].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 166)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 2 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
+ have EXISTS_N : ∃ nn, t + n × task_period tsk = task_offset tsk + nn × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 177)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
============================
exists nn : nat,
t + n * task_period tsk = task_offset tsk + nn * task_period tsk
subgoal 2 (ID 179) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 3 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 177)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
============================
exists nn : nat,
t + n * task_period tsk = task_offset tsk + nn * task_period tsk
----------------------------------------------------------------------------- *)
∃ (n1 + n).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 181)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
============================
t + n * task_period tsk = task_offset tsk + (n1 + n) * task_period tsk
----------------------------------------------------------------------------- *)
now rewrite JB_ARR; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 179) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 2 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 179)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
EXISTS_N : exists nn : nat,
t + n * task_period tsk =
task_offset tsk + nn * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 2 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
move : EXISTS_N ⇒ [nn JB_ARR'].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 365)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
nn : nat
JB_ARR' : t + n * task_period tsk = task_offset tsk + nn * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 2 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
now rewrite JB_ARR' JB_ARR !task_arrivals_at_size ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 167)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
JB_NOT_ARR : forall n : nat, t <> task_offset tsk + n * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
+ have FORALL_N : ∀ nn, t + n × task_period tsk ≠ task_offset tsk + nn × task_period tsk by apply mul_add_neq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 389)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
JB_NOT_ARR : forall n : nat, t <> task_offset tsk + n * task_period tsk
FORALL_N : forall nn : nat,
t + n * task_period tsk <>
task_offset tsk + nn * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
now rewrite !task_arrivals_size_at_non_arrival.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskArrivalsInCaseOfInfiniteJobs.
End TaskArrivalsSize.
∀ n t,
t ≥ task_offset tsk →
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n × task_period tsk)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 148)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
============================
forall n t : nat,
task_offset tsk <= t ->
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
Proof.
intros × T_G.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 151)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
destruct (exists_or_not_add_mul_cases (task_offset tsk) (task_period tsk) t) as [[n1 JB_ARR] | JB_NOT_ARR].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 166)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 2 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
+ have EXISTS_N : ∃ nn, t + n × task_period tsk = task_offset tsk + nn × task_period tsk.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 177)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
============================
exists nn : nat,
t + n * task_period tsk = task_offset tsk + nn * task_period tsk
subgoal 2 (ID 179) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 3 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 177)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
============================
exists nn : nat,
t + n * task_period tsk = task_offset tsk + nn * task_period tsk
----------------------------------------------------------------------------- *)
∃ (n1 + n).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 181)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
============================
t + n * task_period tsk = task_offset tsk + (n1 + n) * task_period tsk
----------------------------------------------------------------------------- *)
now rewrite JB_ARR; ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 179) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 2 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 179)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
EXISTS_N : exists nn : nat,
t + n * task_period tsk =
task_offset tsk + nn * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 2 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
move : EXISTS_N ⇒ [nn JB_ARR'].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 365)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
n1 : nat
JB_ARR : t = task_offset tsk + n1 * task_period tsk
nn : nat
JB_ARR' : t + n * task_period tsk = task_offset tsk + nn * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
subgoal 2 (ID 167) is:
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
now rewrite JB_ARR' JB_ARR !task_arrivals_at_size ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 167)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
JB_NOT_ARR : forall n : nat, t <> task_offset tsk + n * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
+ have FORALL_N : ∀ nn, t + n × task_period tsk ≠ task_offset tsk + nn × task_period tsk by apply mul_add_neq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 389)
Task : TaskType
H : TaskOffset Task
H0 : PeriodicModel Task
Job : JobType
H1 : JobTask Job Task
H2 : JobArrival Job
arr_seq : arrival_sequence Job
H_consistent_arrivals : consistent_arrival_times arr_seq
H_uniq_arr_seq : arrival_sequence_uniq arr_seq
tsk : Task
H_valid_offset : valid_offset arr_seq tsk
H_valid_period : valid_period tsk
H_task_respects_periodic_model : respects_periodic_task_model arr_seq tsk
H_infinite_jobs : infinite_jobs arr_seq
n, t : nat
T_G : task_offset tsk <= t
JB_NOT_ARR : forall n : nat, t <> task_offset tsk + n * task_period tsk
FORALL_N : forall nn : nat,
t + n * task_period tsk <>
task_offset tsk + nn * task_period tsk
============================
size (task_arrivals_at arr_seq tsk t) =
size (task_arrivals_at arr_seq tsk (t + n * task_period tsk))
----------------------------------------------------------------------------- *)
now rewrite !task_arrivals_size_at_non_arrival.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End TaskArrivalsInCaseOfInfiniteJobs.
End TaskArrivalsSize.