Library prosa.analysis.facts.preemption.job.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.nonpreemptive.
Furthermore, we assume the fully non-preemptive job model.
Platform for Fully Non-Preemptive model
In this section, we prove that instantiation of predicate [job_preemptable] to the fully non-preemptive model indeed defines a valid preemption model.
Consider any type of jobs.
Consider any arrival sequence with consistent arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Next, consider any non-preemptive ideal uniprocessor schedule of
this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
... where jobs do not execute before their arrival or after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
For simplicity, let's define some local names.
Let job_pending := pending sched.
Let job_completed_by := completed_by sched.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by sched.
Let job_scheduled_at := scheduled_at sched.
Then, we prove that fully_nonpreemptive_model is a valid preemption model.
Lemma valid_fully_nonpreemptive_model:
valid_preemption_model arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1256)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
============================
valid_preemption_model arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
intros j; split; [by apply/orP; left | split; [by apply/orP; right | split]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1319)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
============================
not_preemptive_implies_scheduled sched j
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
- move ⇒ t; rewrite /job_preemptable /fully_nonpreemptive_model Bool.negb_orb -lt0n; move ⇒ /andP [POS NCOMPL].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1379)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
============================
scheduled_at sched j t
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHED SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1461)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j t
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1462)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
ft <= t
subgoal 2 (ID 1463) is:
scheduled_at sched j ft
subgoal 3 (ID 1464) is:
~~ completed_by sched j t
subgoal 4 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1463)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j ft
subgoal 2 (ID 1464) is:
~~ completed_by sched j t
subgoal 3 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1464)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
~~ completed_by sched j t
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1476)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t < job_cost j
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: NCOMPL; rewrite neq_ltn; move ⇒ /orP [LE|GE]; [by done | exfalso].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1527)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
GE : job_cost j < service sched j t
============================
False
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: GE; rewrite ltnNge; move ⇒ /negP GE; apply: GE.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1565)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t <= job_cost j
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1320)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
============================
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
- intros t NSCHED SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1575)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1585)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
(service sched j (succn t) == 0)
|| (service sched j (succn t) == job_cost j)
----------------------------------------------------------------------------- *)
apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1611)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service sched j (succn t) == 0
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR; move: CONTR ⇒ /negP; rewrite -lt0n; intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1699)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
============================
False
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHEDn SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1781)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
False
----------------------------------------------------------------------------- *)
move: NSCHED ⇒ /negP NSCHED; apply: NSCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1815)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1816)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
ft <= t
subgoal 2 (ID 1817) is:
scheduled_at sched j ft
subgoal 3 (ID 1818) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1817)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j ft
subgoal 2 (ID 1818) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1818)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1833)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (service sched j t.+1).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1837)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t <= service sched j (succn t)
subgoal 2 (ID 1838) is:
service sched j (succn t) < job_cost j
----------------------------------------------------------------------------- *)
× by rewrite /service /service_during big_nat_recr //= leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1838)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) < job_cost j
----------------------------------------------------------------------------- *)
× rewrite -addn1; apply leq_trans with (service sched j t.+2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1897)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) + 1 <= service sched j (succn (succn t))
subgoal 2 (ID 1898) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
have <-: (service_at sched j t.+1) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1904)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j (succn t) = 1
subgoal 2 (ID 1909) is:
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 3 (ID 1898) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1904)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j (succn t) = 1
----------------------------------------------------------------------------- *)
by apply/eqP; rewrite service_at_def eqb1 -scheduled_at_def.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1909)
subgoal 1 (ID 1909) is:
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 2 (ID 1898) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1909)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 2 (ID 1898) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite -big_nat_recr //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1898)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
by apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
valid_preemption_model arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1256)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
============================
valid_preemption_model arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
intros j; split; [by apply/orP; left | split; [by apply/orP; right | split]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1319)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
============================
not_preemptive_implies_scheduled sched j
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
- move ⇒ t; rewrite /job_preemptable /fully_nonpreemptive_model Bool.negb_orb -lt0n; move ⇒ /andP [POS NCOMPL].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1379)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
============================
scheduled_at sched j t
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHED SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1461)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j t
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1462)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
ft <= t
subgoal 2 (ID 1463) is:
scheduled_at sched j ft
subgoal 3 (ID 1464) is:
~~ completed_by sched j t
subgoal 4 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1463)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j ft
subgoal 2 (ID 1464) is:
~~ completed_by sched j t
subgoal 3 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1464)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
~~ completed_by sched j t
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1476)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
NCOMPL : service sched j t != job_cost j
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t < job_cost j
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: NCOMPL; rewrite neq_ltn; move ⇒ /orP [LE|GE]; [by done | exfalso].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1527)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
GE : job_cost j < service sched j t
============================
False
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: GE; rewrite ltnNge; move ⇒ /negP GE; apply: GE.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1565)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
POS : 0 < service sched j t
ft : nat
LT : ft < t
SCHED : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t <= job_cost j
subgoal 2 (ID 1320) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1320)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
============================
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
- intros t NSCHED SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1575)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1585)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
(service sched j (succn t) == 0)
|| (service sched j (succn t) == job_cost j)
----------------------------------------------------------------------------- *)
apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1611)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service sched j (succn t) == 0
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR; move: CONTR ⇒ /negP; rewrite -lt0n; intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1699)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
============================
False
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHEDn SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1781)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
False
----------------------------------------------------------------------------- *)
move: NSCHED ⇒ /negP NSCHED; apply: NSCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1815)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1816)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
ft <= t
subgoal 2 (ID 1817) is:
scheduled_at sched j ft
subgoal 3 (ID 1818) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1817)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j ft
subgoal 2 (ID 1818) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1818)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1833)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (service sched j t.+1).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1837)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t <= service sched j (succn t)
subgoal 2 (ID 1838) is:
service sched j (succn t) < job_cost j
----------------------------------------------------------------------------- *)
× by rewrite /service /service_during big_nat_recr //= leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1838)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) < job_cost j
----------------------------------------------------------------------------- *)
× rewrite -addn1; apply leq_trans with (service sched j t.+2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1897)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) + 1 <= service sched j (succn (succn t))
subgoal 2 (ID 1898) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
have <-: (service_at sched j t.+1) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1904)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j (succn t) = 1
subgoal 2 (ID 1909) is:
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 3 (ID 1898) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1904)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j (succn t) = 1
----------------------------------------------------------------------------- *)
by apply/eqP; rewrite service_at_def eqb1 -scheduled_at_def.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1909)
subgoal 1 (ID 1909) is:
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 2 (ID 1898) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1909)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 2 (ID 1898) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite -big_nat_recr //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1898)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
by apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We also prove that under the fully non-preemptive model
[job_max_nonpreemptive_segment j] is equal to [job_cost j] ...
Lemma job_max_nps_is_job_cost:
∀ j, job_max_nonpreemptive_segment j = job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1268)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
============================
forall j : Job, job_max_nonpreemptive_segment j = job_cost j
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1269)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
============================
job_max_nonpreemptive_segment j = job_cost j
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1300)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1323)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
subgoal 2 (ID 1324) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1323)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1324)
subgoal 1 (ID 1324) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1324)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
have ->: ∀ n, n>0 → [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1340)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 1348) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 1349) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1340)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1359)
n : nat
H : 0 < n
============================
0 :: [seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1449)
n : nat
H : 0 < n
============================
[seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] == [:: n]
----------------------------------------------------------------------------- *)
have ->: ∀ xs P1 P2, (∀ x, x \in xs → ~~ P1 x) → [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1479)
n : nat
H : 0 < n
============================
forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
subgoal 2 (ID 1490) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1479)
n : nat
H : 0 < n
============================
forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
----------------------------------------------------------------------------- *)
clear; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1497)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
============================
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
----------------------------------------------------------------------------- *)
apply eq_in_filter.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1498)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
============================
{in xs, (fun x : t => P1 x || P2 x) =1 [eta P2]}
----------------------------------------------------------------------------- *)
intros ? IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1501)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
x : t
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
specialize (H _ IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1505)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
x : t
H : ~~ P1 x
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
by destruct (P1 x), (P2 x).
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1490)
subgoal 1 (ID 1490) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 1348) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 1349) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1490)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1565)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 1566) is:
n \in iota 1 n
subgoal 3 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1566)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by rewrite mem_iota; apply/andP; split; [done | rewrite add1n].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1491)
n : nat
H : 0 < n
============================
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- intros x; rewrite mem_iota; move ⇒ /andP [POS _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1647)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1348)
subgoal 1 (ID 1348) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 1349) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1348)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 1349) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /max0; simpl; rewrite max0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1349)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
0 < job_cost j
----------------------------------------------------------------------------- *)
by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ j, job_max_nonpreemptive_segment j = job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1268)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
============================
forall j : Job, job_max_nonpreemptive_segment j = job_cost j
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1269)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
============================
job_max_nonpreemptive_segment j = job_cost j
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1300)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1323)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
subgoal 2 (ID 1324) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1323)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1324)
subgoal 1 (ID 1324) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1324)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
have ->: ∀ n, n>0 → [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1340)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 1348) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 1349) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1340)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1359)
n : nat
H : 0 < n
============================
0 :: [seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1449)
n : nat
H : 0 < n
============================
[seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] == [:: n]
----------------------------------------------------------------------------- *)
have ->: ∀ xs P1 P2, (∀ x, x \in xs → ~~ P1 x) → [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1479)
n : nat
H : 0 < n
============================
forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
subgoal 2 (ID 1490) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1479)
n : nat
H : 0 < n
============================
forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
----------------------------------------------------------------------------- *)
clear; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1497)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
============================
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
----------------------------------------------------------------------------- *)
apply eq_in_filter.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1498)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
============================
{in xs, (fun x : t => P1 x || P2 x) =1 [eta P2]}
----------------------------------------------------------------------------- *)
intros ? IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1501)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
x : t
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
specialize (H _ IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1505)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
x : t
H : ~~ P1 x
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
by destruct (P1 x), (P2 x).
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1490)
subgoal 1 (ID 1490) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 1348) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 1349) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1490)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1565)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 1566) is:
n \in iota 1 n
subgoal 3 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1566)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 1491) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by rewrite mem_iota; apply/andP; split; [done | rewrite add1n].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1491)
n : nat
H : 0 < n
============================
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- intros x; rewrite mem_iota; move ⇒ /andP [POS _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1647)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1348)
subgoal 1 (ID 1348) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 1349) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1348)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 1349) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /max0; simpl; rewrite max0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1349)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
0 < job_cost j
----------------------------------------------------------------------------- *)
by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
... and [job_last_nonpreemptive_segment j] is equal to [job_cost j].
Lemma job_last_nps_is_job_cost:
∀ j, job_last_nonpreemptive_segment j = job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1280)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
============================
forall j : Job, job_last_nonpreemptive_segment j = job_cost j
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1281)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
============================
job_last_nonpreemptive_segment j = job_cost j
----------------------------------------------------------------------------- *)
rewrite /job_last_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1312)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1335)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
subgoal 2 (ID 1336) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1335)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1336)
subgoal 1 (ID 1336) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1336)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
have ->: ∀ n, n>0 → [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1352)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 1360) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 1361) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1352)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1371)
n : nat
H : 0 < n
============================
0 :: [seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1461)
n : nat
H : 0 < n
============================
[seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] == [:: n]
----------------------------------------------------------------------------- *)
have ->: ∀ xs P1 P2, (∀ x, x \in xs → ~~ P1 x) → [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1491)
n : nat
H : 0 < n
============================
forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
subgoal 2 (ID 1502) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1491)
n : nat
H : 0 < n
============================
forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
----------------------------------------------------------------------------- *)
clear; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1509)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
============================
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
----------------------------------------------------------------------------- *)
apply eq_in_filter.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1510)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
============================
{in xs, (fun x : t => P1 x || P2 x) =1 [eta P2]}
----------------------------------------------------------------------------- *)
intros ? IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1513)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
x : t
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
specialize (H _ IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1517)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
x : t
H : ~~ P1 x
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
by destruct (P1 x), (P2 x).
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1502)
subgoal 1 (ID 1502) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 1360) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 1361) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1502)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1577)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 1578) is:
n \in iota 1 n
subgoal 3 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1578)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by rewrite mem_iota; apply/andP; split; [done | rewrite add1n].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1503)
n : nat
H : 0 < n
============================
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- intros x; rewrite mem_iota; move ⇒ /andP [POS _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1659)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1360)
subgoal 1 (ID 1360) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 1361) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1360)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 1361) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /last0; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1361)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
0 < job_cost j
----------------------------------------------------------------------------- *)
by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyNonPreemptiveModel.
Hint Resolve valid_fully_nonpreemptive_model : basic_facts.
∀ j, job_last_nonpreemptive_segment j = job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1280)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
============================
forall j : Job, job_last_nonpreemptive_segment j = job_cost j
----------------------------------------------------------------------------- *)
Proof.
intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1281)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
============================
job_last_nonpreemptive_segment j = job_cost j
----------------------------------------------------------------------------- *)
rewrite /job_last_nonpreemptive_segment /lengths_of_segments
/job_preemption_points /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1312)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1335)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
subgoal 2 (ID 1336) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1335)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1336)
subgoal 1 (ID 1336) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1336)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
have ->: ∀ n, n>0 → [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1352)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 1360) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 1361) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1352)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1371)
n : nat
H : 0 < n
============================
0 :: [seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1461)
n : nat
H : 0 < n
============================
[seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] == [:: n]
----------------------------------------------------------------------------- *)
have ->: ∀ xs P1 P2, (∀ x, x \in xs → ~~ P1 x) → [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1491)
n : nat
H : 0 < n
============================
forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
subgoal 2 (ID 1502) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1491)
n : nat
H : 0 < n
============================
forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
(forall x : t, x \in xs -> ~~ P1 x) ->
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
----------------------------------------------------------------------------- *)
clear; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1509)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
============================
[seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]
----------------------------------------------------------------------------- *)
apply eq_in_filter.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1510)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
============================
{in xs, (fun x : t => P1 x || P2 x) =1 [eta P2]}
----------------------------------------------------------------------------- *)
intros ? IN.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1513)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
H : forall x : t, x \in xs -> ~~ P1 x
x : t
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
specialize (H _ IN).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1517)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
x : t
H : ~~ P1 x
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
by destruct (P1 x), (P2 x).
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 1502)
subgoal 1 (ID 1502) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 1360) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 1361) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1502)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1577)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 1578) is:
n \in iota 1 n
subgoal 3 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1578)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 1503) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by rewrite mem_iota; apply/andP; split; [done | rewrite add1n].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1503)
n : nat
H : 0 < n
============================
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- intros x; rewrite mem_iota; move ⇒ /andP [POS _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1659)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1360)
subgoal 1 (ID 1360) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 1361) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1360)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 1361) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /last0; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1361)
Job : JobType
H : JobArrival Job
H0 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
0 < job_cost j
----------------------------------------------------------------------------- *)
by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyNonPreemptiveModel.
Hint Resolve valid_fully_nonpreemptive_model : basic_facts.