Library rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring Require Import job task.
From rt.restructuring.model.schedule Require Import nonpreemptive.
From rt.restructuring.model.preemption Require Import
valid_model job.parameters job.instance.nonpreemptive rtc_threshold.valid_rtct.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
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 : is_nonpreemptive_schedule sched.
Hypothesis H_nonpreemptive_sched : is_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 200)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 263)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) 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 323)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHED SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 405)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 406)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 407) is:
scheduled_at sched j ft
subgoal 3 (ID 408) is:
~~ completed_by sched j t
subgoal 4 (ID 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 407)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 408) is:
~~ completed_by sched j t
subgoal 3 (ID 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 408)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 420)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: NCOMPL; rewrite neq_ltn; move ⇒ /orP [LE|GE]; [by done | exfalso].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 471)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: GE; rewrite ltnNge; move ⇒ /negP GE; apply: GE.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 509)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 264)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 519)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 529)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
(service sched j (succn t) == 0)
|| (service sched j (succn t) == job_cost j)
----------------------------------------------------------------------------- *)
apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 555)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service sched j (succn t) == 0
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR; move: CONTR ⇒ /negP; rewrite -lt0n; intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 643)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
============================
False
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHEDn SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 725)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
False
----------------------------------------------------------------------------- *)
move: NSCHED ⇒ /negP NSCHED; apply: NSCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 759)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 760)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
ft <= t
subgoal 2 (ID 761) is:
scheduled_at sched j ft
subgoal 3 (ID 762) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 761)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j ft
subgoal 2 (ID 762) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 762)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 777)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (service sched j t.+1).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 781)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t <= service sched j (succn t)
subgoal 2 (ID 782) is:
service sched j (succn t) < job_cost j
----------------------------------------------------------------------------- *)
× by rewrite /service /service_during big_nat_recr //= leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 782)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) < job_cost j
----------------------------------------------------------------------------- *)
× rewrite -addn1; apply leq_trans with (service sched j t.+2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 841)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) + 1 <= service sched j (succn (succn t))
subgoal 2 (ID 842) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
have <-: (service_at sched j t.+1) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 848)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j (succn t) = 1
subgoal 2 (ID 853) is:
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 3 (ID 842) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 848)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j (succn t) = 1
----------------------------------------------------------------------------- *)
by apply/eqP; rewrite eqb1 -scheduled_at_def.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 853)
subgoal 1 (ID 853) is:
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 2 (ID 842) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 853)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 2 (ID 842) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite -big_nat_recr //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 842)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
by apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
valid_preemption_model arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 200)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 263)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) 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 323)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHED SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 405)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 406)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 407) is:
scheduled_at sched j ft
subgoal 3 (ID 408) is:
~~ completed_by sched j t
subgoal 4 (ID 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 407)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 408) is:
~~ completed_by sched j t
subgoal 3 (ID 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 408)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 420)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: NCOMPL; rewrite neq_ltn; move ⇒ /orP [LE|GE]; [by done | exfalso].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 471)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
move: GE; rewrite ltnNge; move ⇒ /negP GE; apply: GE.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 509)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 264) is:
execution_starts_with_preemption_point sched j
----------------------------------------------------------------------------- *)
apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 264)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 519)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
job_preemptable j (service sched j (succn t))
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 529)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
(service sched j (succn t) == 0)
|| (service sched j (succn t) == job_cost j)
----------------------------------------------------------------------------- *)
apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 555)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
============================
service sched j (succn t) == 0
----------------------------------------------------------------------------- *)
apply/negP; intros CONTR; move: CONTR ⇒ /negP; rewrite -lt0n; intros POS.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 643)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
============================
False
----------------------------------------------------------------------------- *)
move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHEDn SERV]]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 725)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
NSCHED : ~~ scheduled_at sched j t
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
False
----------------------------------------------------------------------------- *)
move: NSCHED ⇒ /negP NSCHED; apply: NSCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 759)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j t
----------------------------------------------------------------------------- *)
apply H_nonpreemptive_sched with ft.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 760)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
ft <= t
subgoal 2 (ID 761) is:
scheduled_at sched j ft
subgoal 3 (ID 762) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by rewrite -ltnS.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 761)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
scheduled_at sched j ft
subgoal 2 (ID 762) is:
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 762)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
~~ completed_by sched j t
----------------------------------------------------------------------------- *)
+ rewrite /completed_by -ltnNge.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 777)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t < job_cost j
----------------------------------------------------------------------------- *)
apply leq_ltn_trans with (service sched j t.+1).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 781)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j t <= service sched j (succn t)
subgoal 2 (ID 782) is:
service sched j (succn t) < job_cost j
----------------------------------------------------------------------------- *)
× by rewrite /service /service_during big_nat_recr //= leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 782)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) < job_cost j
----------------------------------------------------------------------------- *)
× rewrite -addn1; apply leq_trans with (service sched j t.+2).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 841)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) + 1 <= service sched j (succn (succn t))
subgoal 2 (ID 842) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
have <-: (service_at sched j t.+1) = 1.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 848)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j (succn t) = 1
subgoal 2 (ID 853) is:
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 3 (ID 842) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 848)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service_at sched j (succn t) = 1
----------------------------------------------------------------------------- *)
by apply/eqP; rewrite eqb1 -scheduled_at_def.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 853)
subgoal 1 (ID 853) is:
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 2 (ID 842) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 853)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn t) + service_at sched j (succn t) <=
service sched j (succn (succn t))
subgoal 2 (ID 842) is:
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
by rewrite -big_nat_recr //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 842)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
H1 : arrives_in arr_seq j
t : instant
SCHED : scheduled_at sched j (succn t)
POS : 0 < service sched j (succn t)
ft : nat
LT : ft < succn t
SCHEDn : scheduled_at sched j ft
SERV : service_during sched j 0 ft = 0
============================
service sched j (succn (succn t)) <= job_cost j
----------------------------------------------------------------------------- *)
by apply completion.service_at_most_cost; eauto 2 with basic_facts.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
We also prove that under the fully non-preemptive model
[job_max_nonpreemptive_segment j] is equal to [job_cost j] ...
Lemma job_max_nps_is_job_cost:
∀ j, job_max_nonpreemptive_segment j = job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 212)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 213)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 244)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 267)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 268) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 267)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 268)
subgoal 1 (ID 268) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (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 (processor_state Job)
H_nonpreemptive_sched : is_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 284)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 292) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 293) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 284)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
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 393)
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 423)
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 434) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 435) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 423)
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 441)
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 442)
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 445)
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 449)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
x : t
H : ~~ P1 x
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
by destruct (P1 x), (P2 x).
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 434)
subgoal 1 (ID 434) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 435) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 292) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 293) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 434)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 435) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 509)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 510) is:
n \in iota 1 n
subgoal 3 (ID 435) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 510)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 435) 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 435)
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 591)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 292)
subgoal 1 (ID 292) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 293) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 292)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 293) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /max0; simpl; rewrite max0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 293)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 212)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 213)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 244)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 267)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 268) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 267)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
max0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 268)
subgoal 1 (ID 268) is:
max0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (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 (processor_state Job)
H_nonpreemptive_sched : is_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 284)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 292) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 293) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 284)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 303)
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 393)
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 423)
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 434) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 435) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 423)
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 441)
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 442)
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 445)
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 449)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
x : t
H : ~~ P1 x
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
by destruct (P1 x), (P2 x).
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 434)
subgoal 1 (ID 434) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 435) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 292) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 293) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 434)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 435) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 509)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 510) is:
n \in iota 1 n
subgoal 3 (ID 435) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 510)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 435) 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 435)
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 591)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 292)
subgoal 1 (ID 292) is:
max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 293) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 292)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 293) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /max0; simpl; rewrite max0n.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 293)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 224)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 225)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 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 (processor_state Job)
H_nonpreemptive_sched : is_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 279)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 280) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 279)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 280)
subgoal 1 (ID 280) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 280)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 296)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 304) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 305) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 296)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 315)
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 405)
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 435)
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 446) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 447) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 435)
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 453)
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 454)
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 457)
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 461)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
x : t
H : ~~ P1 x
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
by destruct (P1 x), (P2 x).
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 446)
subgoal 1 (ID 446) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 447) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 304) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 305) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 446)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 447) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 521)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 522) is:
n \in iota 1 n
subgoal 3 (ID 447) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 522)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 447) 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 447)
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 603)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 304)
subgoal 1 (ID 304) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 305) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 304)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 305) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /last0; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 305)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
0 < job_cost j
----------------------------------------------------------------------------- *)
by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyNonPreemptiveModel.
Hint Resolve valid_fully_nonpreemptive_model : basic_facts.
∀ j, job_last_nonpreemptive_segment j = job_cost j.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 224)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 225)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 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 (processor_state Job)
H_nonpreemptive_sched : is_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 279)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 280) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 279)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
ZERO : job_cost j = 0
============================
last0
(distances
[seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 280)
subgoal 1 (ID 280) is:
last0
(distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 280)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 296)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
subgoal 2 (ID 304) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 305) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 296)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
forall n : nat,
0 < n ->
[seq ρ <- index_iota 0 (succn n) | (ρ == 0) || (ρ == n)] = [:: 0; n]
----------------------------------------------------------------------------- *)
clear; simpl; intros.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 315)
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 405)
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 435)
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 446) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 447) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 435)
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 453)
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 454)
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 457)
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 461)
t : eqType
xs : seq_predType t
P1, P2 : t -> bool
x : t
H : ~~ P1 x
IN : x \in xs
============================
P1 x || P2 x = P2 x
----------------------------------------------------------------------------- *)
by destruct (P1 x), (P2 x).
(* ----------------------------------[ coqtop ]---------------------------------
4 subgoals (ID 446)
subgoal 1 (ID 446) is:
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 447) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 304) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 305) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 446)
n : nat
H : 0 < n
============================
[seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 447) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
rewrite filter_pred1_uniq; first by done.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 521)
n : nat
H : 0 < n
============================
uniq (iota 1 n)
subgoal 2 (ID 522) is:
n \in iota 1 n
subgoal 3 (ID 447) is:
forall x : nat_eqType, x \in iota 1 n -> x != 0
----------------------------------------------------------------------------- *)
- by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 522)
n : nat
H : 0 < n
============================
n \in iota 1 n
subgoal 2 (ID 447) 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 447)
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 603)
n : nat
H : 0 < n
x : nat_eqType
POS : 0 < x
============================
x != 0
----------------------------------------------------------------------------- *)
by rewrite -lt0n.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 304)
subgoal 1 (ID 304) is:
last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 305) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 304)
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 (processor_state Job)
H_nonpreemptive_sched : is_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 305) is:
0 < job_cost j
----------------------------------------------------------------------------- *)
by rewrite /distances; simpl; rewrite subn0 /last0; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 305)
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 (processor_state Job)
H_nonpreemptive_sched : is_nonpreemptive_schedule sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
job_pending := pending sched : Job -> instant -> bool
job_completed_by := completed_by sched : Job -> instant -> bool
job_scheduled_at := scheduled_at sched : Job -> instant -> bool
j : Job
POS : 0 < job_cost j
============================
0 < job_cost j
----------------------------------------------------------------------------- *)
by done.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyNonPreemptiveModel.
Hint Resolve valid_fully_nonpreemptive_model : basic_facts.