new lemma in workloadfacts

Added new lemma in analysis/facts/model/workload

analysis/facts/model/workload.v

@@ -15,23 +15,23 @@ Section WorkloadFacts.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
-  (** Consider any job arrival sequence. *)
+  (** Further, consider any job arrival sequence. *)
   Variable arr_seq : arrival_sequence Job.
   
   (** For simplicity, let's define a local name. *)
-  Let arrivals_between := arrivals_between arr_seq.  
+  Let arrivals_between := arrivals_between arr_seq.
   
-  (** We prove that workload can be split into two parts. *)
+  (** We observe that the cumulative workload of all jobs arriving in a time
+      interval <<[t1, t2)>> and respecting a predicate [P] can be split into two parts. *)
   Lemma workload_of_jobs_cat:
     forall t t1 t2 P,
       t1 <= t <= t2 ->
       workload_of_jobs P (arrivals_between t1 t2) =
-      workload_of_jobs P (arrivals_between t1 t)
-      + workload_of_jobs P (arrivals_between t t2).
+      workload_of_jobs P (arrivals_between t1 t) + workload_of_jobs P (arrivals_between t t2).
   Proof.
     move => t t1 t2 P /andP [GE LE].
     rewrite /workload_of_jobs /arrivals_between.
-      by rewrite (arrivals_between_cat _ _ t) // big_cat.
+    by rewrite (arrivals_between_cat _ _ t) // big_cat.
   Qed.
 
   (** Consider a job [j] ... *)
@@ -63,4 +63,40 @@ Section WorkloadFacts.
     by rewrite EQUAL mem_rem_uniqF in INjobs.
   Qed.
 
+  (** In this section, we prove the relation between two different ways of constraining 
+      [workload_of_jobs] to only those jobs that arrive prior to a given time. *)
+  Section Subset.
+
+    (** Assume that arrival times are consistent and that arrivals are unique. *)
+    Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
+    Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
+
+    (** Consider a time interval <<[t1, t2)>> and a time instant [t]. *)
+    Variable t1 t2 t : instant.
+    Hypothesis H_t1_le_t2 : t1 <= t2.
+
+    (** Let [P] be an arbitrary predicate on jobs. *)
+    Variable P : pred Job.
+
+    (** Consider the window <<[t1,t2)>>. We prove that the total workload of the jobs
+        arriving in this window before some [t] is the same as the workload of the jobs
+        arriving in <<[t1,t)>>. Note that we only require [t1] to be less-or-equal
+        than [t2]. Consequently, the interval <<[t1,t)>> may be empty. *)
+    Lemma workload_equal_subset :
+      workload_of_jobs (fun j => (job_arrival j <= t) && P j) (arrivals_between t1 t2)
+      <= workload_of_jobs (fun j => P j) (arrivals_between t1 (t + ε)).
+    Proof.
+      rewrite /workload_of_jobs big_seq_cond.
+      rewrite -[in X in X <= _]big_filter -[in X in _ <= X]big_filter.
+      apply leq_sum_sub_uniq; first by apply filter_uniq, arrivals_uniq.
+      move => j'; rewrite mem_filter => [/andP [/andP [A /andP [C D]] _]].
+      rewrite mem_filter; apply/andP; split; first by done.
+      apply job_in_arrivals_between; eauto.
+      - by eapply in_arrivals_implies_arrived; eauto 2.
+      - apply in_arrivals_implies_arrived_between in A; auto; move: A => /andP [A E].
+        by unfold ε; apply/andP; split; ssrlia.
+    Qed.
+
+  End Subset.
+
 End WorkloadFacts.