Library prosa.analysis.facts.preemption.job.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
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 50)
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 113)
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 114) 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 172)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHED SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 253)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 254)
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 255) is:
scheduled_at sched j ft
subgoal 3 (ID 256) is:
~~ completed_by sched j t
subgoal 4 (ID 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 255)
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 256) is:
~~ completed_by sched j t
subgoal 3 (ID 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 256)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 268)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: NCOMPL; rewrite neq_ltn; move ⇒ /orP [LE|GE]; [by done | exfalso].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 318)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: GE; rewrite ltnNge; move ⇒ /negP GE; apply: GE.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 355)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 114)
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 365)
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 t.+1
============================
job_preemptable j (service sched j t.+1)
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 375)
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 t.+1
============================
(service sched j t.+1 == 0) || (service sched j t.+1 == job_cost j)
----------------------------------------------------------------------------- *)
apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 401)
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 t.+1
============================
service sched j t.+1 == 0
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR; move: CONTR ⇒ /negP; rewrite -lt0n; intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 488)
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 t.+1
POS : 0 < service sched j t.+1
============================
False
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHEDn SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 569)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
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 602)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
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 603)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
ft <= t
subgoal 2 (ID 604) is:
scheduled_at sched j ft
subgoal 3 (ID 605) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 604)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j ft
subgoal 2 (ID 605) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 605)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
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 620)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
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 624)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t <= service sched j t.+1
subgoal 2 (ID 625) is:
service sched j t.+1 < job_cost j
----------------------------------------------------------------------------- *)
× by rewrite /service /service_during big_nat_recr //= leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 625)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t.+1 < job_cost j
----------------------------------------------------------------------------- *)
× rewrite -addn1; apply leq_trans with (service sched j t.+2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 683)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t.+1 + 1 <= service sched j t.+2
subgoal 2 (ID 684) is:
service sched j t.+2 <= job_cost j
----------------------------------------------------------------------------- *)
have <-: (service_at sched j t.+1) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 689)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j t.+1 = 1
subgoal 2 (ID 694) is:
service sched j t.+1 + service_at sched j t.+1 <= service sched j t.+2
subgoal 3 (ID 684) is:
service sched j t.+2 <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 689)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j t.+1 = 1
----------------------------------------------------------------------------- *)
by apply/eqP; rewrite eqb1 -scheduled_at_def.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 694) is:
service sched j t.+1 + service_at sched j t.+1 <= service sched j t.+2
subgoal 2 (ID 684) is:
service sched j t.+2 <= job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 694)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t.+1 + service_at sched j t.+1 <= service sched j t.+2
subgoal 2 (ID 684) is:
service sched j t.+2 <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite -big_nat_recr //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 684)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t.+2 <= 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 50)
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 113)
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 114) 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 172)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHED SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 253)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 254)
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 255) is:
scheduled_at sched j ft
subgoal 3 (ID 256) is:
~~ completed_by sched j t
subgoal 4 (ID 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 255)
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 256) is:
~~ completed_by sched j t
subgoal 3 (ID 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 256)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 268)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: NCOMPL; rewrite neq_ltn; move ⇒ /orP [LE|GE]; [by done | exfalso].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 318)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: GE; rewrite ltnNge; move ⇒ /negP GE; apply: GE.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 355)
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 114) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 114)
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 365)
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 t.+1
============================
job_preemptable j (service sched j t.+1)
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 375)
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 t.+1
============================
(service sched j t.+1 == 0) || (service sched j t.+1 == job_cost j)
----------------------------------------------------------------------------- *)
apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 401)
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 t.+1
============================
service sched j t.+1 == 0
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR; move: CONTR ⇒ /negP; rewrite -lt0n; intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 488)
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 t.+1
POS : 0 < service sched j t.+1
============================
False
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHEDn SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 569)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
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 602)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
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 603)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
ft <= t
subgoal 2 (ID 604) is:
scheduled_at sched j ft
subgoal 3 (ID 605) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 604)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j ft
subgoal 2 (ID 605) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 605)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
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 620)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
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 624)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t <= service sched j t.+1
subgoal 2 (ID 625) is:
service sched j t.+1 < job_cost j
----------------------------------------------------------------------------- *)
× by rewrite /service /service_during big_nat_recr //= leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 625)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t.+1 < job_cost j
----------------------------------------------------------------------------- *)
× rewrite -addn1; apply leq_trans with (service sched j t.+2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 683)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t.+1 + 1 <= service sched j t.+2
subgoal 2 (ID 684) is:
service sched j t.+2 <= job_cost j
----------------------------------------------------------------------------- *)
have <-: (service_at sched j t.+1) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 689)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j t.+1 = 1
subgoal 2 (ID 694) is:
service sched j t.+1 + service_at sched j t.+1 <= service sched j t.+2
subgoal 3 (ID 684) is:
service sched j t.+2 <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 689)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j t.+1 = 1
----------------------------------------------------------------------------- *)
by apply/eqP; rewrite eqb1 -scheduled_at_def.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 694) is:
service sched j t.+1 + service_at sched j t.+1 <= service sched j t.+2
subgoal 2 (ID 684) is:
service sched j t.+2 <= job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 694)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t.+1 + service_at sched j t.+1 <= service sched j t.+2
subgoal 2 (ID 684) is:
service sched j t.+2 <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite -big_nat_recr //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 684)
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 t.+1
POS : 0 < service sched j t.+1
ft : nat
LT : ft < t.+1
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t.+2 <= 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 61)
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 62)
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 93)
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 116)
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 117) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 116)
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
subgoal 1 (ID 117) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
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 131)
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 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 139) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 140) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 131)
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 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 149)
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 239)
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 268)
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 279) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 280) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 268)
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 286)
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 287)
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 290)
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 294)
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
subgoal 1 (ID 279) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 280) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 139) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 140) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 279)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 280) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 353)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 354) is:
n \in iota 1 n
subgoal 3 (ID 280) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 354)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 280) 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 280)
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 434)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 139) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 140) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 139)
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 140) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /max0; simpl; rewrite max0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 140)
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 61)
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 62)
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 93)
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 116)
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 117) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 116)
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
subgoal 1 (ID 117) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 117)
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 131)
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 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 139) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 140) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 131)
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 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 149)
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 239)
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 268)
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 279) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 280) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 268)
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 286)
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 287)
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 290)
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 294)
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
subgoal 1 (ID 279) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 280) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 139) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 140) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 279)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 280) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 353)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 354) is:
n \in iota 1 n
subgoal 3 (ID 280) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 354)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 280) 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 280)
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 434)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 139) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 140) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 139)
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 140) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /max0; simpl; rewrite max0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 140)
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 72)
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 73)
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 104)
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 127)
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 128) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 127)
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
subgoal 1 (ID 128) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 128)
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 142)
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 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 150) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 151) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
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 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
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 250)
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 279)
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 290) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 291) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 279)
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 297)
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 298)
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 301)
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 305)
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
subgoal 1 (ID 290) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 291) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 150) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 151) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 290)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 291) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 364)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 365) is:
n \in iota 1 n
subgoal 3 (ID 291) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 365)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 291) 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 291)
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 445)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 150) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 151) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 150)
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 151) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /last0; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 151)
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.
Global Hint Resolve valid_fully_nonpreemptive_model : basic_facts.
∀ j, job_last_nonpreemptive_segment j = job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 72)
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 73)
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 104)
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 127)
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 128) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 127)
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
subgoal 1 (ID 128) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 128)
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 142)
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 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 150) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 151) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 142)
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 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 160)
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 250)
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 279)
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 290) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 291) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 279)
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 297)
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 298)
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 301)
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 305)
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
subgoal 1 (ID 290) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 291) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 150) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 151) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 290)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 291) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 364)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 365) is:
n \in iota 1 n
subgoal 3 (ID 291) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 365)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 291) 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 291)
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 445)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals
subgoal 1 (ID 150) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 151) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 150)
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 151) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /last0; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 151)
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.
Global Hint Resolve valid_fully_nonpreemptive_model : basic_facts.