Polish and refactoring

implementation/definitions/maximal_arrival_sequence.v

@@ -33,11 +33,7 @@ Section MaximalArrivalSequence.
     (** Let [tsk] be any task. *)
     Variable tsk : Task.
     
-    (** First, we define a function that, given a sequence [xs], keeps
-        only the last [n] elements. *)
-    Definition suffix (xs : seq nat) (n : nat) := drop (size xs - n) xs.
-    
-    (** Next, we introduce a function that computes the sum of the suffix of length [n]. *) 
+    (** First, we introduce a function that computes the sum of the suffix of length [n]. *) 
     Definition suffix_sum xs n :=
       \sum_(size xs - n <= t < size xs) nth 0 xs t.
 

implementation/facts/maximal_arrival_sequence.v

@@ -287,11 +287,8 @@ Section MaximalArrivalSequence.
     taskset_respects_max_arrivals (concrete_arrival_sequence generate_jobs_at ts) ts.
   Proof.
     move=> tsk IN.
-    move=> t1 t2 LEQ.
-    specialize (concrete_respects_at tsk IN t2 (t2-t1)) => Rat.
-    rewrite subKn // in Rat.
-    apply Rat.
-    lia.
+    apply respects_max_arrivals_at_respects_max_arrivals_eq.
+    by apply concrete_respects_at.
   Qed. 
 
 End MaximalArrivalSequence.

model/task/arrival/curves.v

 Require Export prosa.util.rel.
 Require Export prosa.model.task.arrivals.
+Require Export mathcomp.zify.zify.
 
 (** * The Arbitrary Arrival Curves Model *)
 
@@ -63,15 +64,6 @@ Section ArrivalCurves.
     Definition valid_arrival_curve (num_arrivals : duration -> nat) :=
       num_arrivals 0 = 0 /\
       monotone leq num_arrivals.
-
-    (** We say that [max_arrivals] is an upper arrival bound for task
-        [tsk] at time [t] iff, for any interval <<[t - Δ, t)>>,
-        [max_arrivals Δ] bounds the number of jobs of [tsk] that
-        arrive in that interval. *)
-    Definition respects_max_arrivals_at (tsk : Task) (max_arrivals : duration -> nat) (t : instant) :=
-      forall Δ,
-        Δ <= t -> 
-        number_of_task_arrivals arr_seq tsk (t-Δ) t <= max_arrivals Δ.
                                            
     (** Similarly, we say that [max_arrivals] is an upper arrival
         bound for task [tsk] iff, for any interval <<[t1, t2)>>,
@@ -112,6 +104,46 @@ Section ArrivalCurves.
 
   End SeparationBound.
 
+  (** In this section we give an alternative, point-wise notion of respecting an upper 
+      arrival bound, and then show that, if valid for any instant [t], it is equivalent 
+      to the standard definition. This notion is used to prove the correctness of the 
+      maximal arrival sequence implementation. *)
+  Section PointWiseRespectingMaxArrivals.
+
+    (** Consider a task [tsk]... *)
+    Variable (tsk : Task).
+
+    (** ... and an arrival bound function [max_arrivals]. *)
+    Variable (max_arrivals : duration -> nat).
+
+    (** We say that [max_arrivals] is an upper arrival bound for task
+    [tsk] at time [t] iff, for any interval <<[t - Δ, t)>>,
+    [max_arrivals Δ] bounds the number of jobs of [tsk] that
+    arrive in that interval. *)
+    Definition respects_max_arrivals_at (t : instant) :=
+      forall Δ,
+        Δ <= t -> 
+        number_of_task_arrivals arr_seq tsk (t-Δ) t <= max_arrivals Δ.
+
+    (** Next, we prove that, if [respects_max_arrivals_at] holds for
+        any time instant [t], then the standard definition holds as well. *)
+    Lemma respects_max_arrivals_at_respects_max_arrivals_eq:
+      (forall t, respects_max_arrivals_at t) <->
+      respects_max_arrivals tsk max_arrivals.
+    Proof.
+      split.
+      { move=> RESP t1 t2 LEQ.
+        move: (RESP t2 (t2-t1)) => Rat.
+        rewrite subKn // in Rat.
+        by apply Rat; lia. }
+      { move=> RESP t Δ LEQ.
+        move: (RESP (t-Δ) t) => Rat.
+        rewrite subKn // in Rat.
+        by apply Rat; lia. }
+    Qed.
+    
+  End PointWiseRespectingMaxArrivals.
+
 End ArrivalCurves.