Library prosa.analysis.facts.preemption.job.nonpreemptive


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)


Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.nonpreemptive.

Furthermore, we assume the fully non-preemptive job model.

Platform for Fully Non-Preemptive model

In this section, we prove that instantiation of predicate [job_preemptable] to the fully non-preemptive model indeed defines a valid preemption model.
Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any arrival sequence with consistent arrivals.
Next, consider any non-preemptive ideal uniprocessor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
For simplicity, let's define some local names.
Then, we prove that fully_nonpreemptive_model is a valid preemption model.
  Lemma valid_fully_nonpreemptive_model:
    valid_preemption_model arr_seq sched.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 50)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  ============================
  valid_preemption_model arr_seq sched

----------------------------------------------------------------------------- *)


  Proof.
    intros j; split; [by apply/orP; left | split; [by apply/orP; right | split]].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 113)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  ============================
  not_preemptive_implies_scheduled sched j

subgoal 2 (ID 114) is:
 execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


    - movet; rewrite /job_preemptable /fully_nonpreemptive_model Bool.negb_orb -lt0n; move ⇒ /andP [POS NCOMPL].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 172)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  POS : 0 < service sched j t
  NCOMPL : service sched j t != job_cost j
  ============================
  scheduled_at sched j t

subgoal 2 (ID 114) is:
 execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


      move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHED SERV]]].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 253)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  POS : 0 < service sched j t
  NCOMPL : service sched j t != job_cost j
  ft : nat
  LT : ft < t
  SCHED : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  scheduled_at sched j t

subgoal 2 (ID 114) is:
 execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


      apply H_nonpreemptive_sched with ft.

(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals (ID 254)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  POS : 0 < service sched j t
  NCOMPL : service sched j t != job_cost j
  ft : nat
  LT : ft < t
  SCHED : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  ft <= t

subgoal 2 (ID 255) is:
 scheduled_at sched j ft
subgoal 3 (ID 256) is:
 ~~ completed_by sched j t
subgoal 4 (ID 114) is:
 execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


      + by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 255)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  POS : 0 < service sched j t
  NCOMPL : service sched j t != job_cost j
  ft : nat
  LT : ft < t
  SCHED : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  scheduled_at sched j ft

subgoal 2 (ID 256) is:
 ~~ completed_by sched j t
subgoal 3 (ID 114) is:
 execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


      + by done.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 256)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  POS : 0 < service sched j t
  NCOMPL : service sched j t != job_cost j
  ft : nat
  LT : ft < t
  SCHED : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  ~~ completed_by sched j t

subgoal 2 (ID 114) is:
 execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


      + rewrite /completed_by -ltnNge.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 268)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  POS : 0 < service sched j t
  NCOMPL : service sched j t != job_cost j
  ft : nat
  LT : ft < t
  SCHED : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service sched j t < job_cost j

subgoal 2 (ID 114) is:
 execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


        move: NCOMPL; rewrite neq_ltn; move ⇒ /orP [LE|GE]; [by done | exfalso].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 318)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  POS : 0 < service sched j t
  ft : nat
  LT : ft < t
  SCHED : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  GE : job_cost j < service sched j t
  ============================
  False

subgoal 2 (ID 114) is:
 execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


        move: GE; rewrite ltnNge; move ⇒ /negP GE; apply: GE.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 355)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  POS : 0 < service sched j t
  ft : nat
  LT : ft < t
  SCHED : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service sched j t <= job_cost j

subgoal 2 (ID 114) is:
 execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


        apply completion.service_at_most_cost; eauto 2 with basic_facts.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 114)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  ============================
  execution_starts_with_preemption_point sched j

----------------------------------------------------------------------------- *)


    - intros t NSCHED SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 365)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j t.+1
  ============================
  job_preemptable j (service sched j t.+1)

----------------------------------------------------------------------------- *)


      rewrite /job_preemptable /fully_nonpreemptive_model.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 375)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j t.+1
  ============================
  (service sched j t.+1 == 0) || (service sched j t.+1 == job_cost j)

----------------------------------------------------------------------------- *)


      apply/orP; left.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 401)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j t.+1
  ============================
  service sched j t.+1 == 0

----------------------------------------------------------------------------- *)


      apply/negP; intros CONTR; move: CONTR ⇒ /negP; rewrite -lt0n; intros POS.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 488)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ============================
  False

----------------------------------------------------------------------------- *)


      move: (incremental_service_during _ _ _ _ _ POS) ⇒ [ft [/andP [_ LT] [SCHEDn SERV]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 569)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  NSCHED : ~~ scheduled_at sched j t
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  False

----------------------------------------------------------------------------- *)


      move: NSCHED ⇒ /negP NSCHED; apply: NSCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 602)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  scheduled_at sched j t

----------------------------------------------------------------------------- *)


      apply H_nonpreemptive_sched with ft.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 603)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  ft <= t

subgoal 2 (ID 604) is:
 scheduled_at sched j ft
subgoal 3 (ID 605) is:
 ~~ completed_by sched j t

----------------------------------------------------------------------------- *)


      + by rewrite -ltnS.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 604)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  scheduled_at sched j ft

subgoal 2 (ID 605) is:
 ~~ completed_by sched j t

----------------------------------------------------------------------------- *)


      + by done.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 605)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  ~~ completed_by sched j t

----------------------------------------------------------------------------- *)


      + rewrite /completed_by -ltnNge.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 620)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service sched j t < job_cost j

----------------------------------------------------------------------------- *)


        apply leq_ltn_trans with (service sched j t.+1).
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 624)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service sched j t <= service sched j t.+1

subgoal 2 (ID 625) is:
 service sched j t.+1 < job_cost j

----------------------------------------------------------------------------- *)



        × by rewrite /service /service_during big_nat_recr //= leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 625)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service sched j t.+1 < job_cost j

----------------------------------------------------------------------------- *)


        × rewrite -addn1; apply leq_trans with (service sched j t.+2).
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 683)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service sched j t.+1 + 1 <= service sched j t.+2

subgoal 2 (ID 684) is:
 service sched j t.+2 <= job_cost j

----------------------------------------------------------------------------- *)


          have <-: (service_at sched j t.+1) = 1.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 689)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service_at sched j t.+1 = 1

subgoal 2 (ID 694) is:
 service sched j t.+1 + service_at sched j t.+1 <= service sched j t.+2
subgoal 3 (ID 684) is:
 service sched j t.+2 <= job_cost j

----------------------------------------------------------------------------- *)


          {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 689)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service_at sched j t.+1 = 1

----------------------------------------------------------------------------- *)


by apply/eqP; rewrite eqb1 -scheduled_at_def.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals

subgoal 1 (ID 694) is:
 service sched j t.+1 + service_at sched j t.+1 <= service sched j t.+2
subgoal 2 (ID 684) is:
 service sched j t.+2 <= job_cost j

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 694)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service sched j t.+1 + service_at sched j t.+1 <= service sched j t.+2

subgoal 2 (ID 684) is:
 service sched j t.+2 <= job_cost j

----------------------------------------------------------------------------- *)


            by rewrite -big_nat_recr //=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 684)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  H1 : arrives_in arr_seq j
  t : instant
  SCHED : scheduled_at sched j t.+1
  POS : 0 < service sched j t.+1
  ft : nat
  LT : ft < t.+1
  SCHEDn : scheduled_at sched j ft
  SERV : service_during sched j 0 ft = 0
  ============================
  service sched j t.+2 <= job_cost j

----------------------------------------------------------------------------- *)


            by apply completion.service_at_most_cost; eauto 2 with basic_facts.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

We also prove that under the fully non-preemptive model [job_max_nonpreemptive_segment j] is equal to [job_cost j] ...
  Lemma job_max_nps_is_job_cost:
     j, job_max_nonpreemptive_segment j = job_cost j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 61)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  ============================
  forall j : Job, job_max_nonpreemptive_segment j = job_cost j

----------------------------------------------------------------------------- *)


  Proof.
    intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 62)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  ============================
  job_max_nonpreemptive_segment j = job_cost j

----------------------------------------------------------------------------- *)


    rewrite /job_max_nonpreemptive_segment /lengths_of_segments
            /job_preemption_points /job_preemptable /fully_nonpreemptive_model.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 93)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  ============================
  max0
    (distances
       [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
  job_cost j

----------------------------------------------------------------------------- *)


    case: (posnP (job_cost j)) ⇒ [ZERO|POS].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 116)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  ZERO : job_cost j = 0
  ============================
  max0
    (distances
       [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
  job_cost j

subgoal 2 (ID 117) is:
 max0
   (distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
 job_cost j

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 116)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  ZERO : job_cost j = 0
  ============================
  max0
    (distances
       [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
  job_cost j

----------------------------------------------------------------------------- *)


by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 117) is:
 max0
   (distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
 job_cost j

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 117)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  max0
    (distances
       [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
  job_cost j

----------------------------------------------------------------------------- *)


    have ->: n, n>0 [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n].

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 131)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  forall n : nat,
  0 < n -> [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]

subgoal 2 (ID 139) is:
 max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 140) is:
 0 < job_cost j

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 131)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  forall n : nat,
  0 < n -> [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]

----------------------------------------------------------------------------- *)


clear; simpl; intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 149)
  
  n : nat
  H : 0 < n
  ============================
  0 :: [seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] = [:: 0; n]

----------------------------------------------------------------------------- *)


      apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 239)
  
  n : nat
  H : 0 < n
  ============================
  [seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] == [:: n]

----------------------------------------------------------------------------- *)


      have ->: xs P1 P2, ( x, x \in xs ~~ P1 x) [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 268)
  
  n : nat
  H : 0 < n
  ============================
  forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
  (forall x : t, x \in xs -> ~~ P1 x) ->
  [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]

subgoal 2 (ID 279) is:
 [seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 280) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 268)
  
  n : nat
  H : 0 < n
  ============================
  forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
  (forall x : t, x \in xs -> ~~ P1 x) ->
  [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]

----------------------------------------------------------------------------- *)


clear; intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 286)
  
  t : eqType
  xs : seq_predType t
  P1, P2 : t -> bool
  H : forall x : t, x \in xs -> ~~ P1 x
  ============================
  [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]

----------------------------------------------------------------------------- *)


        apply eq_in_filter.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 287)
  
  t : eqType
  xs : seq_predType t
  P1, P2 : t -> bool
  H : forall x : t, x \in xs -> ~~ P1 x
  ============================
  {in xs, (fun x : t => P1 x || P2 x) =1 [eta P2]}

----------------------------------------------------------------------------- *)


        intros ? IN.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 290)
  
  t : eqType
  xs : seq_predType t
  P1, P2 : t -> bool
  H : forall x : t, x \in xs -> ~~ P1 x
  x : t
  IN : x \in xs
  ============================
  P1 x || P2 x = P2 x

----------------------------------------------------------------------------- *)


specialize (H _ IN).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 294)
  
  t : eqType
  xs : seq_predType t
  P1, P2 : t -> bool
  x : t
  H : ~~ P1 x
  IN : x \in xs
  ============================
  P1 x || P2 x = P2 x

----------------------------------------------------------------------------- *)


          by destruct (P1 x), (P2 x).

(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals

subgoal 1 (ID 279) is:
 [seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 280) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 139) is:
 max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 140) is:
 0 < job_cost j

----------------------------------------------------------------------------- *)


      }

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 279)
  
  n : nat
  H : 0 < n
  ============================
  [seq x <- iota 1 n | x == n] == [:: n]

subgoal 2 (ID 280) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      rewrite filter_pred1_uniq; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 353)
  
  n : nat
  H : 0 < n
  ============================
  uniq (iota 1 n)

subgoal 2 (ID 354) is:
 n \in iota 1 n
subgoal 3 (ID 280) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      - by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 354)
  
  n : nat
  H : 0 < n
  ============================
  n \in iota 1 n

subgoal 2 (ID 280) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      - by rewrite mem_iota; apply/andP; split; [done | rewrite add1n].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 280)
  
  n : nat
  H : 0 < n
  ============================
  forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      - intros x; rewrite mem_iota; move ⇒ /andP [POS _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 434)
  
  n : nat
  H : 0 < n
  x : nat_eqType
  POS : 0 < x
  ============================
  x != 0

----------------------------------------------------------------------------- *)


          by rewrite -lt0n.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals

subgoal 1 (ID 139) is:
 max0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 140) is:
 0 < job_cost j

----------------------------------------------------------------------------- *)


    }
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 139)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  max0 (distances [:: 0; job_cost j]) = job_cost j

subgoal 2 (ID 140) is:
 0 < job_cost j

----------------------------------------------------------------------------- *)



    by rewrite /distances; simpl; rewrite subn0 /max0; simpl; rewrite max0n.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 140)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  0 < job_cost j

----------------------------------------------------------------------------- *)


      by done.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

... and [job_last_nonpreemptive_segment j] is equal to [job_cost j].
  Lemma job_last_nps_is_job_cost:
     j, job_last_nonpreemptive_segment j = job_cost j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 72)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  ============================
  forall j : Job, job_last_nonpreemptive_segment j = job_cost j

----------------------------------------------------------------------------- *)


  Proof.
    intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 73)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  ============================
  job_last_nonpreemptive_segment j = job_cost j

----------------------------------------------------------------------------- *)


    rewrite /job_last_nonpreemptive_segment /lengths_of_segments
            /job_preemption_points /job_preemptable /fully_nonpreemptive_model.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 104)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  ============================
  last0
    (distances
       [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
  job_cost j

----------------------------------------------------------------------------- *)


    case: (posnP (job_cost j)) ⇒ [ZERO|POS].

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 127)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  ZERO : job_cost j = 0
  ============================
  last0
    (distances
       [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
  job_cost j

subgoal 2 (ID 128) is:
 last0
   (distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
 job_cost j

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 127)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  ZERO : job_cost j = 0
  ============================
  last0
    (distances
       [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
  job_cost j

----------------------------------------------------------------------------- *)


by rewrite ZERO; compute.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal

subgoal 1 (ID 128) is:
 last0
   (distances [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
 job_cost j

----------------------------------------------------------------------------- *)


}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 128)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  last0
    (distances
       [seq ρ <- range 0 (job_cost j) | (ρ == 0) || (ρ == job_cost j)]) =
  job_cost j

----------------------------------------------------------------------------- *)


    have ->: n, n>0 [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n].

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 142)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  forall n : nat,
  0 < n -> [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]

subgoal 2 (ID 150) is:
 last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 3 (ID 151) is:
 0 < job_cost j

----------------------------------------------------------------------------- *)


    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 142)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  forall n : nat,
  0 < n -> [seq ρ <- index_iota 0 n.+1 | (ρ == 0) || (ρ == n)] = [:: 0; n]

----------------------------------------------------------------------------- *)


clear; simpl; intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 160)
  
  n : nat
  H : 0 < n
  ============================
  0 :: [seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] = [:: 0; n]

----------------------------------------------------------------------------- *)


      apply/eqP; rewrite eqseq_cons; apply/andP; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 250)
  
  n : nat
  H : 0 < n
  ============================
  [seq ρ <- iota 1 n | (ρ == 0) || (ρ == n)] == [:: n]

----------------------------------------------------------------------------- *)


      have ->: xs P1 P2, ( x, x \in xs ~~ P1 x) [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x].

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 279)
  
  n : nat
  H : 0 < n
  ============================
  forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
  (forall x : t, x \in xs -> ~~ P1 x) ->
  [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]

subgoal 2 (ID 290) is:
 [seq x <- iota 1 n | x == n] == [:: n]
subgoal 3 (ID 291) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 279)
  
  n : nat
  H : 0 < n
  ============================
  forall (t : eqType) (xs : seq_predType t) (P1 P2 : t -> bool),
  (forall x : t, x \in xs -> ~~ P1 x) ->
  [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]

----------------------------------------------------------------------------- *)


clear; intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 297)
  
  t : eqType
  xs : seq_predType t
  P1, P2 : t -> bool
  H : forall x : t, x \in xs -> ~~ P1 x
  ============================
  [seq x <- xs | P1 x || P2 x] = [seq x <- xs | P2 x]

----------------------------------------------------------------------------- *)


        apply eq_in_filter.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 298)
  
  t : eqType
  xs : seq_predType t
  P1, P2 : t -> bool
  H : forall x : t, x \in xs -> ~~ P1 x
  ============================
  {in xs, (fun x : t => P1 x || P2 x) =1 [eta P2]}

----------------------------------------------------------------------------- *)


        intros ? IN.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 301)
  
  t : eqType
  xs : seq_predType t
  P1, P2 : t -> bool
  H : forall x : t, x \in xs -> ~~ P1 x
  x : t
  IN : x \in xs
  ============================
  P1 x || P2 x = P2 x

----------------------------------------------------------------------------- *)


specialize (H _ IN).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 305)
  
  t : eqType
  xs : seq_predType t
  P1, P2 : t -> bool
  x : t
  H : ~~ P1 x
  IN : x \in xs
  ============================
  P1 x || P2 x = P2 x

----------------------------------------------------------------------------- *)


          by destruct (P1 x), (P2 x).

(* ----------------------------------[ coqtop ]---------------------------------

4 subgoals

subgoal 1 (ID 290) is:
 [seq x <- iota 1 n | x == n] == [:: n]
subgoal 2 (ID 291) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0
subgoal 3 (ID 150) is:
 last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 4 (ID 151) is:
 0 < job_cost j

----------------------------------------------------------------------------- *)


      }

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 290)
  
  n : nat
  H : 0 < n
  ============================
  [seq x <- iota 1 n | x == n] == [:: n]

subgoal 2 (ID 291) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      rewrite filter_pred1_uniq; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 364)
  
  n : nat
  H : 0 < n
  ============================
  uniq (iota 1 n)

subgoal 2 (ID 365) is:
 n \in iota 1 n
subgoal 3 (ID 291) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      - by apply iota_uniq.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 365)
  
  n : nat
  H : 0 < n
  ============================
  n \in iota 1 n

subgoal 2 (ID 291) is:
 forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      - by rewrite mem_iota; apply/andP; split; [done | rewrite add1n].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 291)
  
  n : nat
  H : 0 < n
  ============================
  forall x : nat_eqType, x \in iota 1 n -> x != 0

----------------------------------------------------------------------------- *)


      - intros x; rewrite mem_iota; move ⇒ /andP [POS _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 445)
  
  n : nat
  H : 0 < n
  x : nat_eqType
  POS : 0 < x
  ============================
  x != 0

----------------------------------------------------------------------------- *)


          by rewrite -lt0n.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals

subgoal 1 (ID 150) is:
 last0 (distances [:: 0; job_cost j]) = job_cost j
subgoal 2 (ID 151) is:
 0 < job_cost j

----------------------------------------------------------------------------- *)


    }
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 150)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  last0 (distances [:: 0; job_cost j]) = job_cost j

subgoal 2 (ID 151) is:
 0 < job_cost j

----------------------------------------------------------------------------- *)



      by rewrite /distances; simpl; rewrite subn0 /last0; simpl.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 151)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  H_arrival_times_are_consistent : consistent_arrival_times arr_seq
  sched : schedule (ideal.processor_state Job)
  H_nonpreemptive_sched : nonpreemptive_schedule sched
  H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
  H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
  job_pending := pending sched : Job -> instant -> bool
  job_completed_by := completed_by sched : Job -> instant -> bool
  job_scheduled_at := scheduled_at sched : Job -> instant -> bool
  j : Job
  POS : 0 < job_cost j
  ============================
  0 < job_cost j

----------------------------------------------------------------------------- *)


      by done.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)


  Qed.

End FullyNonPreemptiveModel.
Global Hint Resolve valid_fully_nonpreemptive_model : basic_facts.