Library prosa.analysis.facts.preemption.job.preemptive


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

Welcome to Coq 8.11.2 (June 2020)

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

Require Export prosa.model.task.preemption.parameters.

Furthermore, we assume the fully preemptive job model.
Require Import prosa.model.preemption.fully_preemptive.

Preemptions in Fully Preemptive Model

In this section, we prove that instantiation of predicate [job_preemptable] to the fully preemptive model indeed defines a valid preemption model.
Section FullyPreemptiveModel.

Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any kind of processor state model, ...
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

... any job arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.

... and any given schedule.
  Variable sched : schedule PState.

Then, we prove that fully_preemptive_model is a valid preemption model.
  Lemma valid_fully_preemptive_model:
    valid_preemption_model arr_seq sched.

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

1 subgoal (ID 337)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  ============================
  valid_preemption_model arr_seq sched

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

  Proof.
      by intros j ARR; repeat split; intros t CONTR.

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

No more subgoals.

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

  Qed.

We also prove that under the fully preemptive model [job_max_nonpreemptive_segment j] is equal to 0, when [job_cost j = 0] ...
  Lemma job_max_nps_is_0:
    ∀ j,
      job_cost j = 0 →
      job_max_nonpreemptive_segment j = 0.

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

1 subgoal (ID 350)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  ============================
  forall j : Job, job_cost j = 0 -> job_max_nonpreemptive_segment j = 0

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

  Proof.
    intros.

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

1 subgoal (ID 352)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  H2 : job_cost j = 0
  ============================
  job_max_nonpreemptive_segment j = 0

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

    rewrite /job_max_nonpreemptive_segment /lengths_of_segments
            /job_preemption_points.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 373)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  H2 : job_cost j = 0
  ============================
  max0 (distances [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]) = 0

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

      by rewrite H2; compute.

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

No more subgoals.

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

  Qed.

... or ε when [job_cost j > 0].
  Lemma job_max_nps_is_ε:
    ∀ j,
      job_cost j > 0 →
      job_max_nonpreemptive_segment j = ε.

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

1 subgoal (ID 361)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  ============================
  forall j : Job, 0 < job_cost j -> job_max_nonpreemptive_segment j = ε

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

  Proof.
    intros ? POS.

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

1 subgoal (ID 363)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  POS : 0 < job_cost j
  ============================
  job_max_nonpreemptive_segment j = ε

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

    rewrite /job_max_nonpreemptive_segment /lengths_of_segments
            /job_preemption_points.

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

1 subgoal (ID 384)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  POS : 0 < job_cost j
  ============================
  max0 (distances [seq ρ <- range 0 (job_cost j) | job_preemptable j ρ]) = ε

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

    rewrite /job_preemptable /fully_preemptive_model.

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

1 subgoal (ID 392)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  POS : 0 < job_cost j
  ============================
  max0 (distances [seq _ <- range 0 (job_cost j) | true]) = ε

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

    rewrite filter_predT.

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

1 subgoal (ID 396)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  POS : 0 < job_cost j
  ============================
  max0 (distances (range 0 (job_cost j))) = ε

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

    apply max0_of_uniform_set.

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

2 subgoals (ID 397)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  POS : 0 < job_cost j
  ============================
  0 < size (distances (range 0 (job_cost j)))

subgoal 2 (ID 398) is:
 forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε

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

    - rewrite /range /index_iota subn0.

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

2 subgoals (ID 405)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  POS : 0 < job_cost j
  ============================
  0 < size (distances (iota 0 (succn (job_cost j))))

subgoal 2 (ID 398) is:
 forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε

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

      rewrite [size _]pred_Sn -[in X in _ ≤ X]addn1 -size_of_seq_of_distances size_iota.

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

3 subgoals (ID 428)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  POS : 0 < job_cost j
  ============================
  0 < predn (succn (job_cost j))

subgoal 2 (ID 432) is:
 1 < succn (job_cost j)
subgoal 3 (ID 398) is:
 forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε

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

      + by rewrite -pred_Sn.

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

2 subgoals (ID 432)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  POS : 0 < job_cost j
  ============================
  1 < succn (job_cost j)

subgoal 2 (ID 398) is:
 forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε

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

      + by rewrite ltnS.

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

1 subgoal (ID 398)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  PState : Type
  H1 : ProcessorState Job PState
  arr_seq : arrival_sequence Job
  sched : schedule PState
  j : Job
  POS : 0 < job_cost j
  ============================
  forall x : nat_eqType, x \in distances (range 0 (job_cost j)) -> x = ε

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

    - by apply distances_of_iota_ε.

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

No more subgoals.

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

  Qed.

End FullyPreemptiveModel.
Hint Resolve valid_fully_preemptive_model : basic_facts.