Complete proof of Abstract RTA

You can check a pdf-version of this here.

model/schedule/uni/limited/valid_job_task.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job.
+Require Import rt.model.schedule.uni.schedule.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(* In this file, we define properties of segmented jobs and tasks. *)
+Module ValidSegmentedTaskJob.
+
+  Import Job UniprocessorSchedule.
+
+  Section ValidSegmentedJob.
+    
+    Context {Job: eqType}.
+    Variable job_max: Job -> time.
+    Variable job_last: Job -> time.
+    Variable job_cost: Job -> time. 
+
+    Variable j: Job.
+
+    (* The maximal length of a nonpreemptive segment of job j must be positive. *)
+    Definition job_max_segment_positive := job_max j > 0.
+
+    (* The maximal length of a nonpreemptive segment of job j 
+       cannot be larger than the job cost. *)
+    Definition job_max_segment_le_job_cost := job_max j <= job_cost j.
+    
+    (* The length of last nonpreemptive segment of job j must be positive. *)
+    Definition job_last_segment_positive := job_last j > 0.
+
+    (* The length of the last nonpreemptive segment of job j 
+       cannot be larger than the length of the maximal j segment. *)         
+    Definition job_last_segment_le_job_max := job_last j <= job_max j.
+
+    Definition valid_segmented_job :=
+      job_cost_positive job_cost j /\
+      job_max_segment_positive /\
+      job_max_segment_le_job_cost /\
+      job_last_segment_positive /\
+      job_last_segment_le_job_max.
+
+    (* In this section we prove a simple lemma about properties of a valid segmented job. *)
+    Section BasicLemma.
+
+      (* We assume that job j is a valid segmented job. *)
+      Hypothesis H_valid_segmented_job: valid_segmented_job.
+      
+      (* Then the length of the last job segment is no greater than job cost. *)
+      Lemma job_last_segment_le_job_cost:
+        job_last j <= job_cost j.
+      Proof.
+        move: H_valid_segmented_job => [_ [_ [NEQ1 [_ NEQ2]]]].
+          by apply leq_trans with (job_max j).
+      Qed.
+
+    End BasicLemma.
+    
+  End ValidSegmentedJob.
+
+  Section ValidSegmentedTask.
+
+    Context {Task: eqType}.
+    Variable task_max: Task -> time.
+    Variable task_last: Task -> time.
+    Variable task_cost: Task -> time.
+
+    Variable tsk: Task.
+    
+    (* The maximal length of a nonpreemptive segment of task tsk must be positive. *)
+    Definition task_max_segment_positive := task_max tsk > 0.
+
+    (* The maximal length of a nonpreemptive segment of task tsk
+       cannot be larger than the task cost. *)    
+    Definition task_max_segment_le_job_cost := task_max tsk <= task_cost tsk.
+
+    (* The length of the last nonpreemptive segment of task tsk must be positive. *)
+    Definition task_last_segment_positive := task_last tsk > 0.
+
+    (* The length of the last nonpreemptive segment of task tsk 
+       cannot be larger than the length of the maximal tsk segment. *)        
+    Definition task_last_segment_le_job_max := task_last tsk <= task_max tsk.
+
+    Definition valid_segmented_task :=
+      task_max_segment_positive /\
+      task_max_segment_le_job_cost /\
+      task_last_segment_positive /\
+      task_last_segment_le_job_max.
+
+    (* In this section we prove a simple lemma about properties of a valid segmented task. *)
+    Section BasicLemma.
+
+      (* We assume that task tsk is a valid segmented task. *)
+      Hypothesis H_valid_segmented_task: valid_segmented_task.
+      
+      (* Then the length of the last job segment is no greater than job cost. *)
+      Lemma task_last_segment_le_task_cost:
+        task_last tsk <= task_cost tsk.
+      Proof.
+        move: H_valid_segmented_task => [_ [NEQ1 [_ NEQ2]]].
+          by apply leq_trans with (task_max tsk).
+      Qed.
+
+    End BasicLemma.    
+
+  End ValidSegmentedTask.
+  
+  Section ValidSegmentedTaskSet.
+    
+    Context {Task: eqType}.
+    Variable task_max: Task -> time.
+    Variable task_last: Task -> time.
+    Variable task_cost: Task -> time.
+
+    Let is_valid_task :=
+      valid_segmented_task task_max task_last task_cost.
+
+    Variable ts: seq Task.
+
+    (* A valid taskset only contains valid tasks. *)
+    Definition valid_segmented_taskset :=
+      forall tsk, tsk \in ts -> is_valid_task tsk.
+
+  End ValidSegmentedTaskSet.
+  
+  Section ValidSegmentedTaskJob.
+    
+    Context {Job: eqType}.
+    Variable job_max: Job -> time.
+    Variable job_last: Job -> time.
+    Variable job_cost: Job -> time.
+
+    Context {Task: eqType}.
+    Variable task_max: Task -> time.
+    Variable task_last: Task -> time.
+    Variable task_cost: Task -> time.     
+    Variable job_task: Job -> Task.
+
+    Variable j: Job.
+
+    (* The maximal length of a nonpreemptive segment of the job 
+       cannot be larger than the maximal length of the nonpreemptive segment of the task. *)  
+    Definition job_max_le_task_max := job_max j <= task_max (job_task j).
+
+    (* The length of the last nonpreemptive segment of the job 
+       cannot be larger than the last nonpreemptive segment of the task. *)  
+    Definition job_last_le_task_last := job_last j <= task_last (job_task j).
+
+    (* Also, the length of the complement of the last nonpreemptive segment of the job 
+       cannot be larger than the complement of the last nonpreemptive segment of the task. *)  
+    Definition job_colast_le_task_colast :=
+      job_cost j - job_last j <= task_cost (job_task j) - task_last (job_task j).
+
+    Definition valid_segmented_task_job :=
+      valid_segmented_job job_max job_last job_cost j /\
+      job_max_le_task_max /\
+      job_last_le_task_last /\
+      job_cost_le_task_cost task_cost job_cost job_task j /\
+      job_colast_le_task_colast.
+    
+  End ValidSegmentedTaskJob.
+  
+End ValidSegmentedTaskJob. 
\ No newline at end of file