Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[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 Import prosa.model.task.concept.
Require Import prosa.analysis.definitions.job_properties.

(** In this module, we state some general results about
    the [task_cost] parameter. *)
Section TaskCost.

  (** Consider tasks and jobs with the following associated parameters. *)
  Context `{Task : TaskType} `{Job : JobType} `{JobTask Job Task} `{JobCost Job} `{TaskCost Task}.

  (** Consider a task [tsk] and a job of the task [j]. *)
  Variable tsk : Task.
  Variable j : Job.
  Hypothesis H_job_of_task : job_of_task tsk j.

  (** Assume [j] has a positive and valid cost. *)
  Hypothesis H_job_cost_positive : job_cost_positive j.
  Hypothesis H_valid_job_cost : valid_job_cost j.

  (** Then, the task cost of [tsk] is also positive. *)
  
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobCost Job
H1: TaskCost Task
tsk: Task
j: Job
H_job_of_task: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
H_valid_job_cost: valid_job_cost j
0 < task_cost tsk

  
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobCost Job
H1: TaskCost Task
tsk: Task
j: Job
H_job_of_task: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
H_valid_job_cost: valid_job_cost j
0 < task_cost tsk

    
Task: TaskType
Job: JobType
H: JobTask Job Task
H0: JobCost Job
H1: TaskCost Task
tsk: Task
j: Job
H_job_of_task: job_of_task tsk j
H_job_cost_positive: job_cost_positive j
H_valid_job_cost: valid_job_cost j
job_cost j <= task_cost tsk

    by move : H_job_of_task => /eqP TSK; rewrite -TSK.
  Qed.

End TaskCost.

(** We add the above lemma to the global hints database. *)
Global Hint Resolve
  job_cost_positive_implies_task_cost_positive :
  basic_rt_facts.