Complete proof of Abstract RTA

You can check a pdf-version of this here.

model/schedule/uni/limited/rbf.v

+Require Import rt.util.all.
+Require Import rt.model.time rt.model.arrival.basic.job
+               rt.model.arrival.basic.task_arrival
+               rt.model.priority
+               rt.model.arrival.basic.arrival_sequence.
+Require Import rt.model.schedule.uni.schedule.
+Require Import rt.model.schedule.uni.limited.millionofutillemmas.
+Require Import rt.model.arrival.curves.bounds.
+Require Import rt.analysis.uni.arrival_curves.workload_bound.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+Module RBF.
+ 
+  Import Job Time ArrivalSequence ArrivalCurves TaskArrival Priority MaxArrivalsWorkloadBound.
+
+  (* In this section, we prove some properties of RBF. *)
+  Section RBFProperties.
+    
+    Context {Task: eqType}.
+    Variable task_cost: Task -> time.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_task: Job -> Task.
+
+    (* Consider any arrival sequence with consistent arrivals. *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+         
+    (* Consider an FP policy that indicates a higher-or-equal priority relation,
+       and assume that the relation is reflexive and transitive. *)
+    Variable higher_eq_priority: FP_policy Task.
+    Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
+    Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
+
+    (* Consider a task set ts... *)
+    Variable ts: list Task.
+
+    (* ...and let tsk be any task in ts. *)
+    Variable tsk: Task.
+    Hypothesis H_tsk_in_ts: tsk \in ts.
+
+    (* Let max_arrival be any task arrival bound. *)
+    Variable max_arrivals: Task -> time -> nat.
+    Hypothesis H_is_arrival_bound:
+      forall tsk,
+        tsk \in ts -> 
+                is_arrival_bound job_task arr_seq tsk (max_arrivals tsk).
+
+    (* Let's define some local names for clarity. *)
+    Let task_rbf := task_request_function_bound_FP task_cost max_arrivals tsk.
+    Let total_hep_rbf :=
+      total_hep_request_function_bound_FP task_cost higher_eq_priority max_arrivals ts tsk.
+    Let total_ohep_rbf :=
+      total_ohep_request_function_bound_FP task_cost higher_eq_priority max_arrivals ts tsk.
+
+    (* Assume that max_arrivals is a "good" arrival curve,
+       i.e. for all tsk in ts max_arrival tsk 0 is equal to 0 and 
+       max_arrival is a monotone function for every tsk. *)
+    Hypothesis H_max_arrival_zero:
+      forall tsk, tsk \in ts -> max_arrivals tsk 0 = 0.
+    Hypothesis H_max_arrival_monot:
+      forall tsk, tsk \in ts -> monotone (max_arrivals tsk) leq.
+    
+    (* We prove that [task_rbf 0] is equal to 0. *)
+    Lemma task_rbf_0_zero:
+      task_rbf 0 = 0.
+    Proof.
+      rewrite /task_rbf /task_request_function_bound_FP.
+      apply/eqP; rewrite muln_eq0; apply/orP; right; apply/eqP.
+        by apply H_max_arrival_zero.
+    Qed.
+    
+    (* We prove that task_rbf is monotone. *)
+    Lemma task_rbf_monotone:
+      monotone task_rbf leq.
+    Proof.
+      rewrite /monotone; intros.
+      rewrite /task_rbf /task_request_function_bound_FP leq_mul2l.
+        by apply/orP; right; apply H_max_arrival_monot.
+    Qed.      
+    
+    (* In this section we prove some additional properties of rbf-functions. *)
+    Section TaskRBFStep.
+
+      (* Consider any job j of tsk. *)
+      Variable j: Job.
+      Hypothesis H_j_arrives: arrives_in arr_seq j.
+      Hypothesis H_job_of_tsk: job_task j = tsk.
+      
+      (* Assume that cost of tsk is positive. *)
+      Hypothesis H_task_cost_positive: task_cost tsk > 0.
+
+      (* Then we prove that task_rbf 1 is greater than or equal to task cost. *)
+      Lemma task_rbf_1_ge_task_cost:
+        task_rbf 1 >= task_cost tsk.
+      Proof.
+        rewrite leqNgt; apply/negP; intros CONTR.
+        move: (H_is_arrival_bound
+                 tsk H_tsk_in_ts (job_arrival j) (job_arrival j + 1)) => ARRB.
+        feed ARRB; first by rewrite leq_addr.
+        rewrite addKn in ARRB.
+        move: CONTR; rewrite /task_rbf /task_request_function_bound_FP; move => CONTR.
+        move: CONTR; rewrite -{2}[task_cost tsk]muln1 ltn_mul2l; move => /andP [_ CONTR].
+        move: CONTR; rewrite -addn1 -{3}[1]add0n leq_add2r leqn0; move => /eqP CONTR.
+        move: ARRB; rewrite CONTR leqn0 eqn0Ngt; move => /negP T; apply: T.
+        rewrite /num_arrivals_of_task -has_predT. 
+        rewrite /arrivals_of_task_between /is_job_of_task.
+        apply/hasP; exists j; last by done.
+        rewrite /jobs_arrived_between addn1 big_nat_recl; last by done. 
+        rewrite big_geq ?cats0; last by done.
+        rewrite mem_filter.
+        apply/andP; split.
+        - by apply/eqP.
+        - move: H_j_arrives => [t ARR].
+          move: (ARR) => CONS.
+          apply H_arrival_times_are_consistent in CONS.
+            by rewrite CONS.
+      Qed.
+
+      
+    End TaskRBFStep.
+    
+  End RBFProperties.
+
+End RBF. 
\ No newline at end of file