Define flow_cc on single jobs

link/flow_cc_of_arrival_sequence.v

+(** Build flow cumulative curves from Prosa arrival sequences.
+
+  Flows are first built for a single job, then the flow for an entire
+  task is obtained by summing the flows for each of its jobs.
+
+  Flows consider workload using [job_cost j] at release time of the job [j].
+  Similar flows for event could be defined by setting all job costs to 1. *)
+
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat ssrint.
 From mathcomp Require Import choice seq path bigop ssralg ssrnum rat.
 From mathcomp Require Import fintype finfun.
@@ -21,8 +29,52 @@ Section Flow_cc_of_arrival_sequence.
 Context {Task : TaskType}.
 Context {Job : JobType}.
 Context `{JobTask Job Task}.
+Context `{JobArrival Job}.
 Context `{JobCost Job}.
 
+(** * First consider only a single job *)
+
+(** Build a network calculus flow cumulative curve (c.f. flow_cc in
+    ../cumulative_curves.v) corresponding to a job *)
+Program Definition flow_cc_of_job (j : Job) (c : uclock) :=
+  Build_flow_cc'
+    (Build_Fup
+       (Build_Fplus
+          (fun t => (if t%:nngnum <= (c (job_arrival j))%:nngnum then 0
+                     else (job_cost j)%:R)%:E)
+          _)
+       _)
+    _.
+Next Obligation. by apply/leFP => t; case: ifP => _; rewrite lee_fin. Qed.
+Next Obligation.
+apply/asboolP => x y xley /=.
+case: (leP y%:nngnum) => ycj; [rewrite ifT//; exact: le_trans ycj|].
+by case: ifP => _; rewrite lee_fin.
+Qed.
+Next Obligation.
+apply/andP; split; last by exact/asboolP.
+apply/leFP => t.
+have: (0 <= t%:nngnum); [by []|].
+rewrite le_eqVlt => /orP[/eqP t0|tgt0].
+{ rewrite (_ : t = 0%:nng); [|exact/val_inj].
+  by rewrite left_cont_closure0 ifT /=. }
+set f := fun _ : {nonneg R} => _.
+have fp : f \is a nonNegativeF.
+{ by apply/leFP => t'; rewrite lee_fin; case: ifP => _. }
+rewrite -[f]/(Fplus_val (Build_Fplus f fp)) left_cont_closure_ereal_sup//.
+apply: ereal_sup_ub.
+have [_ | tgtc] := leP t%:nngnum.
+{ by exists 0%:nng => //=; rewrite /f ifT /=. }
+exists (((c (job_arrival j))%:nngnum + t%:nngnum) / 2)%:nng.
+{ rewrite /in_mem /= ltEsub /=.
+  by rewrite ltr_pdivr_mulr// mulrDr mulr1 ltr_add2r. }
+rewrite /= /f ifF//.
+apply/negbTE; rewrite -ltNge.
+by rewrite ltr_pdivl_mulr// mulrDr mulr1 ltr_add2l.
+Qed.
+
+(** * Then an entire task *)
+
 Let arrivals_of_tsk (arr_seq : arrival_sequence Job) tsk t1 t2 :=
   [seq j <- arrivals_between arr_seq t1 t2 | job_task j == tsk].
 
@@ -76,6 +128,27 @@ rewrite /= ltr_pdivl_mulr// mulrDr mulr1 ltr_add2l.
 by apply: uclock_lt_next_tick; rewrite nE.
 Qed.
 
+Lemma flow_cc_of_arrival_sequence_of_job
+      (s : arrival_sequence Job) (Hs : consistent_arrival_times s)
+      (c : uclock) (tsk : Task) :
+  forall t : {nonneg R},
+    flow_cc_of_arrival_sequence s c tsk t
+    = (\sum_(j <- arrivals_of_tsk s tsk O (next_tick c t))
+        flow_cc_of_job j c t)%dE.
+Proof.
+move=> t /=.
+set arr := arrivals_of_tsk _ _ _ _.
+have in_arr j : j \in arr -> (c (job_arrival j))%:nngnum < t%:nngnum.
+{ rewrite mem_filter =>/andP[_ /mem_bigcat_nat_exists[_ [/Hs <-]]] /=.
+  exact: uclock_lt_next_tick. }
+elim: arr in_arr => [|j arr IH in_arr]; first by rewrite !big_nil.
+rewrite !big_cons -IH => [|j' j'arr]; [|by rewrite in_arr// in_cons j'arr orbT].
+by rewrite leNgt in_arr ?in_cons ?eqxx//= -DualAddTheoryNumDomain.daddEFin natrD.
+Qed.
+
+Definition related_job_flow_cc c j f :=
+  f = flow_cc_of_job j c.
+
 Definition related_arrival_flow_cc c tsk arr f :=
   f = flow_cc_of_arrival_sequence arr c tsk.