Require Export prosa.model.task.preemption.parameters.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export 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.

  (** We assume that jobs are fully preemptive. *)
  #[local] Existing Instance fully_preemptive_job_model.

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

  (** Consider any kind of processor state model, ... *)
  Context {PState : ProcessorState Job}.

  (** ... 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.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
valid_preemption_model arr_seq sched
  Proof.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
valid_preemption_model arr_seq sched
      by intros j ARR; repeat split; intros t CONTR.
  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:
    forall j,
      job_cost j = 0 -> 
      job_max_nonpreemptive_segment j = 0.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
forall j : Job,
job_cost j = 0 -> job_max_nonpreemptive_segment j = 0
  Proof.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
forall j : Job,
job_cost j = 0 -> job_max_nonpreemptive_segment j = 0
    move=> j H1.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
H1: job_cost j = 0
job_max_nonpreemptive_segment j = 0
    rewrite /job_max_nonpreemptive_segment /lengths_of_segments
            /job_preemption_points.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
H1: job_cost j = 0
max0
  (distances
     [seq ρ <- range 0 (job_cost j)
        | job_preemptable j ρ]) = 0 
    by rewrite H1.
  Qed.

  (** ... or ε when [job_cost j > 0]. *)  
  Lemma job_max_nps_is_ε:
    forall j,
      job_cost j > 0 -> 
      job_max_nonpreemptive_segment j = ε.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
forall j : Job,
0 < job_cost j -> job_max_nonpreemptive_segment j = 1
  Proof.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
forall j : Job,
0 < job_cost j -> job_max_nonpreemptive_segment j = 1
    intros ? POS.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
job_max_nonpreemptive_segment j = 1
    rewrite /job_max_nonpreemptive_segment /lengths_of_segments
            /job_preemption_points.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
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 ρ]) = 1
    rewrite /job_preemptable /fully_preemptive_job_model.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
max0
  (distances [seq _ <- range 0 (job_cost j) | true]) =
1
    rewrite filter_predT.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
max0 (distances (range 0 (job_cost j))) = 1
    apply max0_of_uniform_set.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < size (distances (range 0 (job_cost j)))
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in distances (range 0 (job_cost j)) -> x = 1
    -
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < size (distances (range 0 (job_cost j))) rewrite /range /index_iota subn0.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < size (distances (iota 0 (job_cost j).+1))
      rewrite [size _]pred_Sn -[in X in _ <= X]addn1 -size_of_seq_of_distances size_iota.
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < (job_cost j).+1.-1
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
1 < (job_cost j).+1
      +
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
0 < (job_cost j).+1.-1 by rewrite -pred_Sn.
      +
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
1 < (job_cost j).+1 by rewrite ltnS.
    -
Job: JobType
H: JobArrival Job
H0: JobCost Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
j: Job
POS: 0 < job_cost j
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in distances (range 0 (job_cost j)) -> x = 1 by apply distances_of_iota_ε.
  Qed.    
  
End FullyPreemptiveModel.
Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.