Library rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive


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

Welcome to Coq 8.10.1 (October 2019)

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

From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.preemption Require Import rtc_threshold.valid_rtct
     job.instance.preemptive task.instance.preemptive rtc_threshold.instance.preemptive.
From rt.restructuring.analysis.basic_facts.preemption Require Import
     rtc_threshold.job_preemptable.

Task's Run to Completion Threshold

In this section, we prove that instantiation of function [task run to completion threshold] to the fully preemptive model indeed defines a valid run-to-completion threshold function.
Section TaskRTCThresholdFullyPreemptiveModel.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobCost Job}.

Next, consider any arrival sequence ...
  Variable arr_seq : arrival_sequence Job.

... and assume that a job cost cannot be larger than a task cost.
  Hypothesis H_job_cost_le_task_cost:
    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.

Then, we prove that [task_run_to_completion_threshold] function defines a valid task's run to completion threshold.
  Lemma fully_preemptive_valid_task_run_to_completion_threshold:
    ∀ tsk, valid_task_run_to_completion_threshold arr_seq tsk.

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

1 subgoal (ID 47)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  arr_seq : arrival_sequence Job
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  ============================
  forall tsk : Task, valid_task_run_to_completion_threshold arr_seq tsk

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

  Proof.
    intros; split.

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

2 subgoals (ID 50)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  arr_seq : arrival_sequence Job
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  tsk : Task
  ============================
  task_run_to_completion_threshold_le_task_cost tsk

subgoal 2 (ID 51) is:
 task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
   arr_seq tsk

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

    - by rewrite /task_run_to_completion_threshold_le_task_cost.

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

1 subgoal (ID 51)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  arr_seq : arrival_sequence Job
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  tsk : Task
  ============================
  task_run_to_completion_threshold_bounds_job_run_to_completion_threshold
    arr_seq tsk

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

    - intros j ARR TSK.

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

1 subgoal (ID 62)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  arr_seq : arrival_sequence Job
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  tsk : Task
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  parameters.job_run_to_completion_threshold j <=
  parameters.task_run_to_completion_threshold tsk

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

      apply leq_trans with (job_cost j); eauto 2 with basic_facts.

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

1 subgoal (ID 66)
  
  Task : TaskType
  H : TaskCost Task
  Job : JobType
  H0 : JobTask Job Task
  H1 : JobCost Job
  arr_seq : arrival_sequence Job
  H_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
                              arr_seq
  tsk : Task
  j : Job
  ARR : arrives_in arr_seq j
  TSK : job_task j = tsk
  ============================
  job_cost j <= parameters.task_run_to_completion_threshold tsk

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

        by rewrite-TSK; apply H_job_cost_le_task_cost.

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

No more subgoals.

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

  Qed.

End TaskRTCThresholdFullyPreemptiveModel.
Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_facts.