From HB Require Import structures.
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
Require Export prosa.implementation.definitions.arrival_bound.
[Loading ML file zify_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.task.arrival.curves.
Require Export prosa.model.priority.numeric_fixed_priority.

(** * Implementation of Tasks and Jobs *)

(** This file provides reference implementations of the notions of "tasks" and
    "jobs" that can be used to meet the hypotheses on which many of the analyses
    in Prosa are based.

    Note that their use is entirely optional: clients of Prosa may choose to use
    these types or implement their own notions of "tasks" and "jobs". *)

(** ** Implementation of a Concrete Task *)


(** A task comprises of an id, a cost, an arrival bound, a deadline
    and a priority. *)
Structure concrete_task :=
  { task_id: nat (* for uniqueness *)
  ; task_cost: nat
  ; task_arrival: task_arrivals_bound
  ; task_deadline: instant
  ; task_priority : nat
  }.

(** To make it compatible with ssreflect, we define a decidable
    equality for concrete tasks. *)
Definition task_eqdef (t1 t2: concrete_task) :=
  (task_id t1 == task_id t2)
  && (task_cost t1 == task_cost t2)
  && (task_arrival t1 == task_arrival t2)
  && (task_deadline t1 == task_deadline t2)
  && (task_priority t1 == task_priority t2).

(** Next, we prove that [task_eqdef] is indeed an equality, ... *)
Lemma eqn_task : Equality.axiom task_eqdef.
Equality.axiom (T:=concrete_task) task_eqdef
Proof.
Equality.axiom (T:=concrete_task) task_eqdef
  unfold Equality.axiom; intros x y.
x, y: concrete_task
reflect (x = y) (task_eqdef x y)
  destruct (task_eqdef x y) eqn:EQ.
x, y: concrete_task
EQ: task_eqdef x y = true
reflect (x = y) true
x, y: concrete_task
EQ: task_eqdef x y = false
reflect (x = y) false
  {
x, y: concrete_task
EQ: task_eqdef x y = true
reflect (x = y) true apply ReflectT.
x, y: concrete_task
EQ: task_eqdef x y = true
x = y
    unfold task_eqdef in *.
x, y: concrete_task
EQ: (task_id x == task_id y) &&
(task_cost x == task_cost y) &&
(task_arrival x == task_arrival y) &&
(task_deadline x == task_deadline y) &&
(task_priority x == task_priority y) = true
x = y
    move: EQ => /andP [/andP [/andP [/andP [/eqP ID /eqP COST] /eqP PER] /eqP DL] /eqP PRIO].
x, y: concrete_task
ID: task_id x = task_id y
COST: task_cost x = task_cost y
PER: task_arrival x = task_arrival y
DL: task_deadline x = task_deadline y
PRIO: task_priority x = task_priority y
x = y
    by destruct x, y; simpl in *; subst. }
x, y: concrete_task
EQ: task_eqdef x y = false
reflect (x = y) false
  {
x, y: concrete_task
EQ: task_eqdef x y = false
reflect (x = y) false apply ReflectF.
x, y: concrete_task
EQ: task_eqdef x y = false
x <> y
    unfold task_eqdef, not in * => BUG.
x, y: concrete_task
EQ: (task_id x == task_id y) &&
(task_cost x == task_cost y) &&
(task_arrival x == task_arrival y) &&
(task_deadline x == task_deadline y) &&
(task_priority x == task_priority y) = false
BUG: x = y
False
    apply negbT in EQ.
x, y: concrete_task
EQ: ~~
((task_id x == task_id y) &&
 (task_cost x == task_cost y) &&
 (task_arrival x == task_arrival y) &&
 (task_deadline x == task_deadline y) &&
 (task_priority x == task_priority y))
BUG: x = y
False
    repeat rewrite negb_and in EQ.
x, y: concrete_task
BUG: x = y
EQ: (task_id x != task_id y)
|| (task_cost x != task_cost y)
|| (task_arrival x != task_arrival y)
|| (task_deadline x != task_deadline y)
|| (task_priority x != task_priority y)
False
    destruct x, y.
task_id0, task_cost0: nat
task_arrival0: task_arrivals_bound
task_deadline0: instant
task_priority0, task_id1, task_cost1: nat
task_arrival1: task_arrivals_bound
task_deadline1: instant
task_priority1: nat
BUG: {|
  task_id := task_id0;
  task_cost := task_cost0;
  task_arrival := task_arrival0;
  task_deadline := task_deadline0;
  task_priority := task_priority0
|} =
{|
  task_id := task_id1;
  task_cost := task_cost1;
  task_arrival := task_arrival1;
  task_deadline := task_deadline1;
  task_priority := task_priority1
|}
EQ: (task_id
   {|
     task_id := task_id0;
     task_cost := task_cost0;
     task_arrival := task_arrival0;
     task_deadline := task_deadline0;
     task_priority := task_priority0
   |}
 != task_id
      {|
        task_id := task_id1;
        task_cost := task_cost1;
        task_arrival := task_arrival1;
        task_deadline := task_deadline1;
        task_priority := task_priority1
      |})
|| (task_cost
      {|
        task_id := task_id0;
        task_cost := task_cost0;
        task_arrival := task_arrival0;
        task_deadline := task_deadline0;
        task_priority := task_priority0
      |}
    != task_cost
         {|
           task_id := task_id1;
           task_cost := task_cost1;
           task_arrival := task_arrival1;
           task_deadline := task_deadline1;
           task_priority := task_priority1
         |})
|| (task_arrival
      {|
        task_id := task_id0;
        task_cost := task_cost0;
        task_arrival := task_arrival0;
        task_deadline := task_deadline0;
        task_priority := task_priority0
      |}
    != task_arrival
         {|
           task_id := task_id1;
           task_cost := task_cost1;
           task_arrival := task_arrival1;
           task_deadline := task_deadline1;
           task_priority := task_priority1
         |})
|| (task_deadline
      {|
        task_id := task_id0;
        task_cost := task_cost0;
        task_arrival := task_arrival0;
        task_deadline := task_deadline0;
        task_priority := task_priority0
      |}
    != task_deadline
         {|
           task_id := task_id1;
           task_cost := task_cost1;
           task_arrival := task_arrival1;
           task_deadline := task_deadline1;
           task_priority := task_priority1
         |})
|| (task_priority
      {|
        task_id := task_id0;
        task_cost := task_cost0;
        task_arrival := task_arrival0;
        task_deadline := task_deadline0;
        task_priority := task_priority0
      |}
    != task_priority
         {|
           task_id := task_id1;
           task_cost := task_cost1;
           task_arrival := task_arrival1;
           task_deadline := task_deadline1;
           task_priority := task_priority1
         |})
False
    move: BUG => [ID COST PER DL PRIO].
task_id0, task_cost0: nat
task_arrival0: task_arrivals_bound
task_deadline0: instant
task_priority0, task_id1, task_cost1: nat
task_arrival1: task_arrivals_bound
task_deadline1: instant
task_priority1: nat
EQ: (task_id
   {|
     task_id := task_id0;
     task_cost := task_cost0;
     task_arrival := task_arrival0;
     task_deadline := task_deadline0;
     task_priority := task_priority0
   |}
 != task_id
      {|
        task_id := task_id1;
        task_cost := task_cost1;
        task_arrival := task_arrival1;
        task_deadline := task_deadline1;
        task_priority := task_priority1
      |})
|| (task_cost
      {|
        task_id := task_id0;
        task_cost := task_cost0;
        task_arrival := task_arrival0;
        task_deadline := task_deadline0;
        task_priority := task_priority0
      |}
    != task_cost
         {|
           task_id := task_id1;
           task_cost := task_cost1;
           task_arrival := task_arrival1;
           task_deadline := task_deadline1;
           task_priority := task_priority1
         |})
|| (task_arrival
      {|
        task_id := task_id0;
        task_cost := task_cost0;
        task_arrival := task_arrival0;
        task_deadline := task_deadline0;
        task_priority := task_priority0
      |}
    != task_arrival
         {|
           task_id := task_id1;
           task_cost := task_cost1;
           task_arrival := task_arrival1;
           task_deadline := task_deadline1;
           task_priority := task_priority1
         |})
|| (task_deadline
      {|
        task_id := task_id0;
        task_cost := task_cost0;
        task_arrival := task_arrival0;
        task_deadline := task_deadline0;
        task_priority := task_priority0
      |}
    != task_deadline
         {|
           task_id := task_id1;
           task_cost := task_cost1;
           task_arrival := task_arrival1;
           task_deadline := task_deadline1;
           task_priority := task_priority1
         |})
|| (task_priority
      {|
        task_id := task_id0;
        task_cost := task_cost0;
        task_arrival := task_arrival0;
        task_deadline := task_deadline0;
        task_priority := task_priority0
      |}
    != task_priority
         {|
           task_id := task_id1;
           task_cost := task_cost1;
           task_arrival := task_arrival1;
           task_deadline := task_deadline1;
           task_priority := task_priority1
         |})
ID: task_id0 = task_id1
COST: task_cost0 = task_cost1
PER: task_arrival0 = task_arrival1
DL: task_deadline0 = task_deadline1
PRIO: task_priority0 = task_priority1
False
    rewrite ID COST PER DL PRIO //= in EQ.
task_id0, task_cost0: nat
task_arrival0: task_arrivals_bound
task_deadline0: instant
task_priority0, task_id1, task_cost1: nat
task_arrival1: task_arrivals_bound
task_deadline1: instant
task_priority1: nat
ID: task_id0 = task_id1
COST: task_cost0 = task_cost1
PER: task_arrival0 = task_arrival1
DL: task_deadline0 = task_deadline1
PRIO: task_priority0 = task_priority1
EQ: (task_id1 != task_id1)
|| (task_cost1 != task_cost1)
|| (task_arrival1 != task_arrival1)
|| (task_deadline1 != task_deadline1)
|| (task_priority1 != task_priority1)
False
    by subst; rewrite !eq_refl in EQ.
  }
Qed.

(** ..., which allows instantiating the canonical structure for [concrete_task : eqType]. *)
HB.instance Definition _  := hasDecEq.Build concrete_task eqn_task.


(** ** Implementation of a Concrete Job *)


(** A job comprises of an id, an arrival time, a cost, a deadline and the
    task it belongs to. *)
Record concrete_job :=
  { job_id: nat
  ; job_arrival: instant
  ; job_cost: nat
  ; job_deadline: instant
  ; job_task: concrete_task : eqType
  }.

(** For convenience, we define a function that converts each possible arrival
    bound (periodic, sporadic, and arrival-curve prefix) into an arrival-curve
    prefix... *)
Definition get_arrival_curve_prefix tsk :=
  match task_arrival tsk with
  | Periodic p => inter_arrival_to_prefix p
  | Sporadic m => inter_arrival_to_prefix m
  | ArrivalPrefix steps => steps
  end.

(** ... and define the "arrival bound" concept for concrete tasks. *)
Definition concrete_max_arrivals tsk Δ :=
  extrapolated_arrival_curve (get_arrival_curve_prefix tsk) Δ.

(** To make it compatible with ssreflect, we define a decidable
    equality for concrete jobs. *)
Definition job_eqdef (j1 j2: concrete_job) :=
  (job_id j1 == job_id j2)
  && (job_arrival j1 == job_arrival j2)
  && (job_cost j1 == job_cost j2)
  && (job_deadline j1 == job_deadline j2)
  && (job_task j1 == job_task j2).

(** Next, we prove that [job_eqdef] is indeed an equality, ... *)
Lemma eqn_job : Equality.axiom job_eqdef.
Equality.axiom (T:=concrete_job) job_eqdef
Proof.
Equality.axiom (T:=concrete_job) job_eqdef
  unfold Equality.axiom; intros x y.
x, y: concrete_job
reflect (x = y) (job_eqdef x y)
  destruct (job_eqdef x y) eqn:EQ.
x, y: concrete_job
EQ: job_eqdef x y = true
reflect (x = y) true
x, y: concrete_job
EQ: job_eqdef x y = false
reflect (x = y) false
  {
x, y: concrete_job
EQ: job_eqdef x y = true
reflect (x = y) true apply ReflectT; unfold job_eqdef in *.
x, y: concrete_job
EQ: (job_id x == job_id y) &&
(job_arrival x == job_arrival y) &&
(job_cost x == job_cost y) &&
(job_deadline x == job_deadline y) &&
(job_task x == job_task y) = true
x = y
    move: EQ => /andP [/andP [/andP [/andP [/eqP ID /eqP ARR] /eqP COST] /eqP DL] /eqP TASK].
x, y: concrete_job
ID: job_id x = job_id y
ARR: job_arrival x = job_arrival y
COST: job_cost x = job_cost y
DL: job_deadline x = job_deadline y
TASK: job_task x = job_task y
x = y
    by destruct x, y; simpl in *; subst. }
x, y: concrete_job
EQ: job_eqdef x y = false
reflect (x = y) false
  {
x, y: concrete_job
EQ: job_eqdef x y = false
reflect (x = y) false apply ReflectF.
x, y: concrete_job
EQ: job_eqdef x y = false
x <> y
    unfold job_eqdef, not in *; intro BUG.
x, y: concrete_job
EQ: (job_id x == job_id y) &&
(job_arrival x == job_arrival y) &&
(job_cost x == job_cost y) &&
(job_deadline x == job_deadline y) &&
(job_task x == job_task y) = false
BUG: x = y
False
    apply negbT in EQ; rewrite negb_and in EQ.
x, y: concrete_job
BUG: x = y
EQ: ~~
((job_id x == job_id y) &&
 (job_arrival x == job_arrival y) &&
 (job_cost x == job_cost y) &&
 (job_deadline x == job_deadline y))
|| (job_task x != job_task y)
False
    destruct x, y.
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: ~~
((job_id
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_id
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_arrival
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_arrival
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_cost
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_cost
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_deadline
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_deadline
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}))
|| (job_task
      {|
        job_id := job_id0;
        job_arrival := job_arrival0;
        job_cost := job_cost0;
        job_deadline := job_deadline0;
        job_task := job_task0
      |}
    != job_task
         {|
           job_id := job_id1;
           job_arrival := job_arrival1;
           job_cost := job_cost1;
           job_deadline := job_deadline1;
           job_task := job_task1
         |})
False
    rewrite negb_and in EQ.
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: ~~
((job_id
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_id
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_arrival
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_arrival
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_cost
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_cost
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}))
|| (job_deadline
      {|
        job_id := job_id0;
        job_arrival := job_arrival0;
        job_cost := job_cost0;
        job_deadline := job_deadline0;
        job_task := job_task0
      |}
    != job_deadline
         {|
           job_id := job_id1;
           job_arrival := job_arrival1;
           job_cost := job_cost1;
           job_deadline := job_deadline1;
           job_task := job_task1
         |})
|| (job_task
      {|
        job_id := job_id0;
        job_arrival := job_arrival0;
        job_cost := job_cost0;
        job_deadline := job_deadline0;
        job_task := job_task0
      |}
    != job_task
         {|
           job_id := job_id1;
           job_arrival := job_arrival1;
           job_cost := job_cost1;
           job_deadline := job_deadline1;
           job_task := job_task1
         |})
False
    move: EQ => /orP [EQ | /eqP TASK].
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: ~~
((job_id
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_id
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_arrival
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_arrival
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_cost
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_cost
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}))
|| (job_deadline
      {|
        job_id := job_id0;
        job_arrival := job_arrival0;
        job_cost := job_cost0;
        job_deadline := job_deadline0;
        job_task := job_task0
      |}
    != job_deadline
         {|
           job_id := job_id1;
           job_arrival := job_arrival1;
           job_cost := job_cost1;
           job_deadline := job_deadline1;
           job_task := job_task1
         |})
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
TASK: job_task
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_task
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False
    -
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: ~~
((job_id
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_id
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_arrival
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_arrival
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_cost
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_cost
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}))
|| (job_deadline
      {|
        job_id := job_id0;
        job_arrival := job_arrival0;
        job_cost := job_cost0;
        job_deadline := job_deadline0;
        job_task := job_task0
      |}
    != job_deadline
         {|
           job_id := job_id1;
           job_arrival := job_arrival1;
           job_cost := job_cost1;
           job_deadline := job_deadline1;
           job_task := job_task1
         |})
False move: EQ => /orP [EQ | /eqP DL].
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: ~~
((job_id
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_id
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_arrival
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_arrival
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_cost
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_cost
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}))
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
DL: job_deadline
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_deadline
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False
      +
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: ~~
((job_id
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_id
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_arrival
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_arrival
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_cost
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_cost
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}))
False rewrite negb_and in EQ.
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: ~~
((job_id
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_id
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_arrival
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_arrival
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}))
|| (job_cost
      {|
        job_id := job_id0;
        job_arrival := job_arrival0;
        job_cost := job_cost0;
        job_deadline := job_deadline0;
        job_task := job_task0
      |}
    != job_cost
         {|
           job_id := job_id1;
           job_arrival := job_arrival1;
           job_cost := job_cost1;
           job_deadline := job_deadline1;
           job_task := job_task1
         |})
False
        move: EQ => /orP [EQ | /eqP COST].
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: ~~
((job_id
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_id
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_arrival
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_arrival
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}))
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
COST: job_cost
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_cost
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False
        *
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: ~~
((job_id
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_id
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}) &&
 (job_arrival
    {|
      job_id := job_id0;
      job_arrival := job_arrival0;
      job_cost := job_cost0;
      job_deadline := job_deadline0;
      job_task := job_task0
    |} ==
  job_arrival
    {|
      job_id := job_id1;
      job_arrival := job_arrival1;
      job_cost := job_cost1;
      job_deadline := job_deadline1;
      job_task := job_task1
    |}))
False rewrite negb_and in EQ.
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
EQ: (job_id
   {|
     job_id := job_id0;
     job_arrival := job_arrival0;
     job_cost := job_cost0;
     job_deadline := job_deadline0;
     job_task := job_task0
   |}
 != job_id
      {|
        job_id := job_id1;
        job_arrival := job_arrival1;
        job_cost := job_cost1;
        job_deadline := job_deadline1;
        job_task := job_task1
      |})
|| (job_arrival
      {|
        job_id := job_id0;
        job_arrival := job_arrival0;
        job_cost := job_cost0;
        job_deadline := job_deadline0;
        job_task := job_task0
      |}
    != job_arrival
         {|
           job_id := job_id1;
           job_arrival := job_arrival1;
           job_cost := job_cost1;
           job_deadline := job_deadline1;
           job_task := job_task1
         |})
False
          move: EQ => /orP [/eqP ID | /eqP ARR].
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
ID: job_id
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_id
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
ARR: job_arrival
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_arrival
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False
          **
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
ID: job_id
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_id
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False by apply ID; inversion BUG.
          **
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
ARR: job_arrival
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_arrival
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False by apply ARR; inversion BUG.
        *
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
COST: job_cost
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_cost
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False by apply COST; inversion BUG.
      +
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
DL: job_deadline
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_deadline
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False by apply DL; inversion BUG.
    -
job_id0: nat
job_arrival0: instant
job_cost0: nat
job_deadline0: instant
job_task0: concrete_task
job_id1: nat
job_arrival1: instant
job_cost1: nat
job_deadline1: instant
job_task1: concrete_task
BUG: {|
  job_id := job_id0;
  job_arrival := job_arrival0;
  job_cost := job_cost0;
  job_deadline := job_deadline0;
  job_task := job_task0
|} =
{|
  job_id := job_id1;
  job_arrival := job_arrival1;
  job_cost := job_cost1;
  job_deadline := job_deadline1;
  job_task := job_task1
|}
TASK: job_task
  {|
    job_id := job_id0;
    job_arrival := job_arrival0;
    job_cost := job_cost0;
    job_deadline := job_deadline0;
    job_task := job_task0
  |} <>
job_task
  {|
    job_id := job_id1;
    job_arrival := job_arrival1;
    job_cost := job_cost1;
    job_deadline := job_deadline1;
    job_task := job_task1
  |}
False by apply TASK; inversion BUG. }
Qed.

(** ... which allows instantiating the canonical structure for [concrete_job : eqType].*)
HB.instance Definition _  := hasDecEq.Build concrete_job eqn_job.

(** ** Instances for Concrete Jobs and Tasks. *)

(** In the following, we connect the concrete task and job types defined above
    to the generic Prosa interfaces for task and job parameters. *)
Section Parameters.

  (** First, we connect the above definition of tasks with the
      generic Prosa task-parameter interfaces. *)
  Let Task := concrete_task : eqType.
  #[global,program] Instance TaskCost : TaskCost Task := task_cost.
  #[global,program] Instance TaskPriority : TaskPriority Task := task_priority.
  #[global,program] Instance TaskDeadline : TaskDeadline Task := task_deadline.
  #[global,program] Instance ConcreteMaxArrivals : MaxArrivals Task := concrete_max_arrivals.

  (** Second, we do the same for the above definition of job. *)
  Let Job := concrete_job : eqType.
  #[global,program] Instance JobTask : JobTask Job Task := job_task.
  #[global,program] Instance JobArrival : JobArrival Job := job_arrival.
  #[global,program] Instance JobCost : JobCost Job := job_cost.

End Parameters.