Require Export prosa.implementation.definitions.job_constructor.
[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]

(** In this file, we prove facts about the job-constructor function when used in
    pair with the concrete arrival sequence. *)
Section JobConstructor.

  (** Assume that an arrival curve based on a concrete prefix is given. *)
  #[local] Existing Instance ConcreteMaxArrivals.

  (** Consider a task set [ts] with non-duplicate tasks. *)
  Variable ts : seq Task.
  Hypothesis H_ts_uniq : uniq ts.

  (** First, we show that [generate_jobs_at tsk n t] generates n jobs ... *)
  Lemma job_generation_valid_number:
    forall tsk n t,
      tsk \in ts -> size (generate_jobs_at tsk n t) = n.
ts: seq Task
H_ts_uniq: uniq ts
forall (tsk : Task) (n : nat) (t : instant),
tsk \in ts -> size (generate_jobs_at tsk n t) = n
  Proof.
ts: seq Task
H_ts_uniq: uniq ts
forall (tsk : Task) (n : nat) (t : instant),
tsk \in ts -> size (generate_jobs_at tsk n t) = n
    move=> tsk n t IN.
ts: seq Task
H_ts_uniq: uniq ts
tsk: Task
n: nat
t: instant
IN: tsk \in ts
size (generate_jobs_at tsk n t) = n
    by rewrite size_map size_iota.
  Qed.

  (** ... and that each generated job is unique. *)
  Lemma generate_jobs_at_unique:
    forall tsk n t,
      uniq (generate_jobs_at tsk n t).
ts: seq Task
H_ts_uniq: uniq ts
forall (tsk : concrete_task) (n : nat) (t : instant),
uniq (generate_jobs_at tsk n t)
  Proof.
ts: seq Task
H_ts_uniq: uniq ts
forall (tsk : concrete_task) (n : nat) (t : instant),
uniq (generate_jobs_at tsk n t)
    move=> tsk n t.
ts: seq Task
H_ts_uniq: uniq ts
tsk: concrete_task
n: nat
t: instant
uniq (generate_jobs_at tsk n t)
    rewrite /generate_jobs_at //= /generate_job_at map_inj_uniq //=;
      first by apply iota_uniq.
ts: seq Task
H_ts_uniq: uniq ts
tsk: concrete_task
n: nat
t: instant
injective
  (fun id : nat =>
   {|
     job_id := id;
     job_arrival := t;
     job_cost := task_cost tsk;
     job_deadline := t + task_deadline tsk;
     job_task := tsk
   |})
    by move=> x1 x2 /eqP /andP [/andP [/andP [/andP [//= /eqP EQ _] _] _] _].
  Qed.

  (** Next, for convenience, we define [arr_seq] as the concrete arrival
      sequence used with the job constructor.  *)
  Let arr_seq := concrete_arrival_sequence generate_jobs_at ts.

  (** We start by proving that the arrival time of a job is consistent with its
      positioning inside the arrival sequence. *)
  Lemma job_arrival_consistent:
    forall j t,
      j \in arrivals_at arr_seq t -> job_arrival j = t.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
forall (j : Job) (t : instant),
j \in arrivals_at arr_seq t -> job_arrival j = t
  Proof.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
forall (j : Job) (t : instant),
j \in arrivals_at arr_seq t -> job_arrival j = t by move=> j t /mem_bigcat_exists [tsk [TSK_IN /mapP [i INi] ->]]. Qed.

  (** Next, we show that the list of arrivals at any time [t] is unique ... *)
  Lemma arrivals_at_unique:
    forall t,
      uniq (arrivals_at arr_seq t).
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
forall t : instant, uniq (arrivals_at arr_seq t)
  Proof.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
forall t : instant, uniq (arrivals_at arr_seq t)
    move=> t.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t: instant
uniq (arrivals_at arr_seq t)
    apply bigcat_uniq => //=;
      first by move=> tau _; apply: generate_jobs_at_unique.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t: instant
forall (x : concrete_job) (y z : concrete_task),
x \in generate_jobs_at y (max_arrivals_at y t) t ->
x \in generate_jobs_at z (max_arrivals_at z t) t ->
y = z
    move=> j task1 task2 /mapP[i1 IN1 EQj1] /mapP[i2 IN2 EQj2].
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t: instant
j: concrete_job
task1, task2: concrete_task
i1: Datatypes_nat__canonical__eqtype_Equality
IN1: i1 \in iota 0 (max_arrivals_at task1 t)
EQj1: j = generate_job_at task1 t i1
i2: Datatypes_nat__canonical__eqtype_Equality
IN2: i2 \in iota 0 (max_arrivals_at task2 t)
EQj2: j = generate_job_at task2 t i2
task1 = task2
    by move: EQj1 EQj2 => -> [_].
  Qed.

  (** ... and generalize the above result to arbitrary time intervals. *)
  Lemma arrivals_between_unique:
    forall t1 t2,
      uniq (arrivals_between arr_seq t1 t2).
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
forall t1 t2 : instant,
uniq (arrivals_between arr_seq t1 t2)
  Proof.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
forall t1 t2 : instant,
uniq (arrivals_between arr_seq t1 t2)
    move=> t1 t2.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant
uniq (arrivals_between arr_seq t1 t2)
    rewrite /arrivals_between.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant
uniq (\cat_(t1<=t<t2)arrivals_at arr_seq t)
    apply bigcat_nat_uniq.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant
forall i : nat, uniq (arrivals_at arr_seq i)
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant
forall (x : Job) (i1 i2 : nat),
x \in arrivals_at arr_seq i1 ->
x \in arrivals_at arr_seq i2 -> i1 = i2
    -
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant
forall i : nat, uniq (arrivals_at arr_seq i) by apply arrivals_at_unique.
    -
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant
forall (x : Job) (i1 i2 : nat),
x \in arrivals_at arr_seq i1 ->
x \in arrivals_at arr_seq i2 -> i1 = i2 move=> j jt1 jt2 IN1 IN2.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
t1, t2: instant
j: Job
jt1, jt2: nat
IN1: j \in arrivals_at arr_seq jt1
IN2: j \in arrivals_at arr_seq jt2
jt1 = jt2
      by move: (job_arrival_consistent j jt1 IN1)
                 (job_arrival_consistent j jt2 IN2) => <- <-.
  Qed.

  (** Finally, we observe that [generate_jobs_at tsk n t] indeed generates jobs
      of task [tsk] that arrive at [t] *)
  Corollary job_generation_valid_jobs:
    forall tsk n t j,
      j \in generate_jobs_at tsk n t ->
            job_task j = tsk
            /\ job_arrival j = t
            /\ job_cost j <= task_cost tsk.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
forall (tsk : concrete_task) (n : nat) (t : instant)
  (j : Job),
j \in generate_jobs_at tsk n t ->
job_task j = tsk /\
job_arrival j = t /\ job_cost j <= task_cost tsk
  Proof.
ts: seq Task
H_ts_uniq: uniq ts
arr_seq:= concrete_arrival_sequence generate_jobs_at ts: instant -> seq Job
forall (tsk : concrete_task) (n : nat) (t : instant)
  (j : Job),
j \in generate_jobs_at tsk n t ->
job_task j = tsk /\
job_arrival j = t /\ job_cost j <= task_cost tsk by move=> tsk n t j /mapP [i INi] ->. Qed.

End JobConstructor.