introduce "greedy" concrete arrival sequence

This commit defines and adds facts about a concrete arrival sequence in
which tasks release jobs "as quickly as possible" as allowed by their
respective arrival-curve constraints. This maximal arrival sequence is
used in POET to generate assumption-less certificates.

implementation/definitions/maximal_arrival_sequence.v

+Require Export prosa.model.task.arrival.curves.
+Require Export prosa.util.supremum.
+
+(** * A Maximal Arrival Sequence *)
+
+(** In this section, we propose a concrete instantiation of an arrival sequence.
+    Given an arbitrary arrival curve, the defined arrival sequence tries to
+    generate as many jobs as possible at any time instant by adopting a greedy
+    strategy: at each time [t], the arrival sequence contains the maximum possible
+    number of jobs that does not violate the given arrival curve's constraints. *)
+Section MaximalArrivalSequence.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Let [max_arrivals] denote any function that takes a task and an interval length
+      and returns the associated number of job arrivals of the task. *)
+  Context `{MaxArrivals Task}.
+
+  (** In this section, we define a procedure that computes the maximal number of
+      jobs that can be released at a given instant without violating the
+      corresponding arrival curve. *)
+  Section NumberOfJobs.
+
+    (** Let [tsk] be any task. *)
+    Variable tsk : Task.
+
+    (** First, we introduce a function that computes the sum of all elements in
+        a given list's suffix of length [n]. *)
+    Definition suffix_sum xs n := \sum_(size xs - n <= t < size xs) nth 0 xs t.
+
+    (** Let the arrival prefix [arr_prefix] be a sequence of natural numbers,
+        where [nth xs t] denotes the number of jobs that arrive at time [t].
+        Then, given an arrival curve [max_arrivals] and an arrival prefix
+        [arr_prefix], we define a function that computes the number of jobs that
+        can be additionally released without violating the arrival curve.
+
+        The high-level idea is as follows. Let us assume that the length of the
+        arrival prefix is [Δ]. To preserve the sub-additive property, one needs
+        to go through all suffixes of the arrival prefix and pick the
+        minimum. *)
+    Definition jobs_remaining (arr_prefix : seq nat) :=
+      supremum leq [seq (max_arrivals tsk Δ.+1 - suffix_sum arr_prefix Δ) | Δ <- iota 0 (size arr_prefix).+1].
+
+    (** Further, we define the function [next_max_arrival] to handle a special
+        case: when the arrival prefix is empty, the function returns the value
+        of the arrival curve with a window length of [1]. Otherwise, it returns
+        the number the number of jobs that can additionally be generated.  *)
+    Definition next_max_arrival (arr_prefix : seq nat) :=
+      match jobs_remaining arr_prefix with
+      | None => max_arrivals tsk 1
+      | Some n => n
+      end.
+
+    (** Next, we define a function that extends by one a given arrival prefix... *)
+    Definition extend_arrival_prefix (arr_prefix : seq nat) :=
+      arr_prefix ++ [:: next_max_arrival arr_prefix ].
+
+    (** ... and a function that generates a maximal arrival prefix
+        of size [t], starting from an empty arrival prefix. *)
+    Definition maximal_arrival_prefix (t : nat) :=
+      iter t.+1 extend_arrival_prefix [::].
+
+    (** Finally, we define a function that returns the maximal number
+        of jobs that can be released at time [t]; this definition
+        assumes that at each time instant prior to time [t] the maximal
+        number of jobs were released. *)
+    Definition max_arrivals_at t := nth 0 (maximal_arrival_prefix t) t.
+
+  End NumberOfJobs.
+
+  (** Consider a function that generates [n] concrete jobs of
+      the given task at the given time instant. *)
+  Variable generate_jobs_at : Task -> nat -> instant -> seq Job.
+
+  (** The maximal arrival sequence of task set [ts] at time [t] is a
+      concatenation of sequences of generated jobs for each task. *)
+  Definition concrete_arrival_sequence (ts : seq Task) (t : instant) :=
+    \cat_(tsk <- ts) generate_jobs_at tsk (max_arrivals_at tsk t) t.
+
+End MaximalArrivalSequence.

implementation/facts/maximal_arrival_sequence.v

+Require Export prosa.analysis.facts.model.task_arrivals.
+Require Export prosa.implementation.definitions.maximal_arrival_sequence.
+
+(** Recall that, given an arrival curve [max_arrivals] and a
+    job-generating function [generate_jobs_at], the function
+    [concrete_arrival_sequence] generates an arrival sequence. In this
+    section, we prove a few properties of this function. *)
+Section MaximalArrivalSequence.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+
+  (** ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (** Consider a task set [ts] with non-duplicate tasks. *)
+  Variable ts : seq Task.
+  Hypothesis H_ts_uniq : uniq ts.
+
+  (** Let [max_arrivals] be a family of valid arrival curves, i.e.,
+      for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
+      bound of [tsk], and (2) it is a monotonic function that equals [0]
+      for the empty interval [delta = 0]. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+
+  (** Further assume we are given a function that generates the required number of
+      jobs of a given task at a given instant of time. *)
+  Variable generate_jobs_at : Task -> nat -> instant -> seq Job.
+
+  (** First, we assume that [generate_jobs_at tsk n t] generates [n] jobs. *)
+  Hypothesis H_job_generation_valid_number:
+    forall (tsk : Task) (n : nat) (t : instant), tsk \in ts -> size (generate_jobs_at tsk n t) = n.
+
+  (** Second, we assume that [generate_jobs_at tsk n t] generates jobs of task
+      [tsk] that arrive at time [t]. *)
+  Hypothesis H_job_generation_valid_jobs:
+    forall (tsk : Task) (n : nat) (t : instant) (j : Job),
+      (j \in generate_jobs_at tsk n t) ->
+      job_task j = tsk
+      /\ job_arrival j = t
+      /\ job_cost j <= task_cost tsk.
+
+  (** Finally, we assume that all jobs generated by [generate_jobs_at] are unique. *)
+  Hypothesis H_jobs_unique:
+    forall (t1 t2 : instant),
+      uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2).
+
+  (** Assuming such a well-behaved "constructor" [generate_jobs_at], we prove a
+      few validity claims about an arrival sequence generated by
+      [concrete_arrival_sequence]. *)
+  Section ValidityClaims.
+
+    (** We start by showing that the obtained arrival sequence is a set. *)
+    Lemma arr_seq_is_a_set :
+      arrival_sequence_uniq (concrete_arrival_sequence generate_jobs_at ts).
+    Proof.
+      move=> t.
+      move: (H_jobs_unique t t.+1).
+      by rewrite /arrivals_between big_nat1.
+    Qed.
+
+    (** Next, we show that all jobs in the arrival sequence come from [ts]. *)
+    Lemma concrete_all_jobs_from_taskset :
+      all_jobs_from_taskset (concrete_arrival_sequence generate_jobs_at ts) ts.
+    Proof.
+      move=> j [t /mem_bigcat_exists [tsk [TSK_IN IN]]].
+      move: (H_job_generation_valid_jobs tsk _ _ _ IN) => [JOB_TASK _].
+      by rewrite JOB_TASK.
+    Qed.
+
+    (** Further, we note that the jobs in the arrival sequence have consistent
+        arrival times. *)
+    Lemma arrival_times_are_consistent :
+      consistent_arrival_times (concrete_arrival_sequence generate_jobs_at ts).
+    Proof.
+      move=> j t /mem_bigcat_exists [tsk [TSK_IN IN]].
+      by move: (H_job_generation_valid_jobs tsk _ _ _ IN) => [_ [JOB_ARR _]].
+    Qed.
+
+    (** Lastly, we observe that the jobs in the arrival sequence have valid job
+        costs. *)
+    Lemma concrete_valid_job_cost :
+      arrivals_have_valid_job_costs (concrete_arrival_sequence generate_jobs_at ts).
+    Proof.
+      move=> j [t /mem_bigcat_exists [tsk [TSK_IN IN]]].
+      move: (H_job_generation_valid_jobs tsk _ _ _ IN) => [JOB_TASK [_ JOB_COST]].
+      by rewrite /valid_job_cost JOB_TASK.
+    Qed.
+
+  End ValidityClaims.
+
+  (** In this section, we prove a series of facts regarding the maximal arrival
+      sequence, leading up to the main theorem that all arrival-curve
+      constraints are respected. *)
+  Section Facts.
+
+    (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+    Variable tsk : Task.
+    Hypothesis H_tsk_in_ts : tsk \in ts.
+
+    (** First, we show that the arrivals at time [t] are indeed generated by
+        [generate_jobs_at] applied at time [t]. *)
+    Lemma task_arrivals_at_eq_generate_jobs_at:
+      forall t,
+        task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t
+        = generate_jobs_at tsk (max_arrivals_at tsk t) t.
+    Proof.
+      move=> t.
+      rewrite /task_arrivals_at bigcat_filter_eq_filter_bigcat bigcat_seq_uniqK // => tsk0 j INj.
+      apply H_job_generation_valid_jobs in INj.
+      by destruct INj.
+    Qed.
+
+    (** Next, we show that the number of arrivals at time [t] always matches
+        [max_arrivals_at] applied at time [t]. *)
+    Lemma task_arrivals_at_eq:
+      forall t,
+        size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t)
+        = max_arrivals_at tsk t.
+    Proof.
+      move=> t.
+      rewrite task_arrivals_at_eq_generate_jobs_at //.
+      by apply H_job_generation_valid_number.
+    Qed.
+
+    (** We then generalize the previous result to an arbitrary interval
+        <<[t1,t2)>>. *)
+    Lemma number_of_task_arrivals_eq :
+      forall t1 t2,
+        number_of_task_arrivals (concrete_arrival_sequence generate_jobs_at ts) tsk t1 t2
+        = \sum_(t1 <= t < t2) max_arrivals_at tsk t.
+    Proof.
+      move=> t1 t2.
+      rewrite /number_of_task_arrivals task_arrivals_between_is_cat_of_task_arrivals_at -size_big_nat.
+      apply eq_big_nat => t RANGE.
+      by apply task_arrivals_at_eq.
+    Qed.
+
+    (** We further show that, starting from an empty prefix and applying
+        [extend_arrival_prefix] [t] times, we end up with a prefix of size
+        [t]...  *)
+    Lemma extend_horizon_size :
+      forall t,
+        size (iter t (extend_arrival_prefix tsk) [::]) = t.
+    Proof. by elim=> // t IHt; rewrite size_cat IHt //=; lia. Qed.
+
+    (** ...and that the arrival sequence prefix up to an arbitrary horizon
+        [t] is a sequence of [t+1] elements. *)
+    Lemma prefix_up_to_size :
+      forall t,
+        size (maximal_arrival_prefix tsk t) = t.+1.
+    Proof.
+      by elim=> // t IHt; rewrite /maximal_arrival_prefix /extend_arrival_prefix  size_cat IHt //=; lia.
+    Qed.
+
+    (** Next, we prove prefix inclusion for [maximal_arrival_prefix] when the
+        horizon is expanded by one...  *)
+    Lemma n_arrivals_at_prefix_inclusion1 :
+      forall t h,
+        t <= h ->
+        nth 0 (maximal_arrival_prefix tsk h) t
+        = nth 0 (maximal_arrival_prefix tsk h.+1) t.
+    Proof.
+      move=> t h LEQ.
+      rewrite /maximal_arrival_prefix //= {3}/extend_arrival_prefix nth_cat prefix_up_to_size.
+      by case: (ltnP t h.+1); lia.
+    Qed.
+
+    (** ...and we generalize the previous result to two arbitrary horizons [h1 <= h2]. *)
+    Lemma n_arrivals_at_prefix_inclusion :
+      forall t h1 h2,
+        t <= h1 <= h2 ->
+        nth 0 (maximal_arrival_prefix tsk h1) t = nth 0 (maximal_arrival_prefix tsk h2) t.
+    Proof.
+      move=> t h1 h2 /andP[LEQh1 LEQh2].
+      induction h2; [by have -> : h1 = 0; lia |].
+      rewrite leq_eqVlt in LEQh2.
+      move: LEQh2 => /orP [/eqP EQ | LT]; first by rewrite EQ.
+      feed IHh2; first by lia.
+      rewrite -n_arrivals_at_prefix_inclusion1 //.
+      by lia.
+    Qed.
+
+    (** Next, we prove that, for any positive time instant [t], [max_arrivals_at] indeed
+        matches the arrivals of [next_max_arrival] applied at [t-1]. *)
+    Lemma max_arrivals_at_next_max_arrivals_eq:
+      forall t,
+        0 < t ->
+        max_arrivals_at tsk t
+        = next_max_arrival tsk (maximal_arrival_prefix tsk t.-1).
+    Proof.
+      move => t GT0.
+      move: prefix_up_to_size; rewrite /maximal_arrival_prefix => PUS.
+      rewrite /max_arrivals_at /maximal_arrival_prefix {1}/extend_arrival_prefix nth_cat extend_horizon_size //= ltnn //= subnn //=.
+      by destruct t.
+    Qed.
+
+    (** Given a time instant [t] and and interval [Δ], we show that
+        [max_arrivals_at] applied at time [t] is always less-or-equal to
+        [max_arrivals] applied to [Δ+1], even when each value of
+        [max_arrivals_at] in the interval <<[t-Δ, t)>> is subtracted from it. *)
+    Lemma n_arrivals_at_leq :
+      forall t Δ,
+        Δ <= t ->
+        max_arrivals_at tsk t
+        <= max_arrivals tsk Δ.+1 - \sum_(t - Δ <= i < t) max_arrivals_at tsk i.
+    Proof.
+      move=> t Δ LEQ.
+      move: (H_valid_arrival_curve tsk H_tsk_in_ts) => [ZERO MONO].
+      destruct t.
+      { rewrite unlock //= subn0.
+        rewrite /max_arrivals_at /maximal_arrival_prefix /extend_arrival_prefix
+                /next_max_arrival //= /suffix_sum subn0 unlock subn0.
+        by apply MONO. }
+      { rewrite max_arrivals_at_next_max_arrivals_eq; last by done.
+        rewrite /next_max_arrival /jobs_remaining prefix_up_to_size.
+        simpl (t.+1.-1).
+        destruct supremum eqn:SUP; last by  move:(supremum_none _ _ SUP); rewrite map_cons.
+        eapply (supremum_spec _ leqnn leq_total leq_trans _ _ SUP).
+        rewrite /suffix_sum prefix_up_to_size /max_arrivals_at.
+        have -> : \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk i) i =
+                 \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i.
+        { apply eq_big_nat => i RANGE.
+          by apply n_arrivals_at_prefix_inclusion; lia. }
+        set f := fun x => max_arrivals _ x.+1 - \sum_(t.+1-x <= i < t.+1) nth 0 (maximal_arrival_prefix _ t) i.
+        have-> : max_arrivals tsk Δ.+1 - \sum_(t.+1 - Δ <= i < t.+1) nth 0 (maximal_arrival_prefix tsk t) i = f Δ by done.
+        apply map_f.
+        by rewrite mem_iota; lia. }
+    Qed.
+
+  End Facts.
+
+  (** Finally, we prove our main result, that is, the proposed maximal arrival
+      sequence instantiation indeed respects all arrival-curve constraints. *)
+  Theorem concrete_is_arrival_curve :
+    taskset_respects_max_arrivals (concrete_arrival_sequence generate_jobs_at ts) ts.
+  Proof.
+    move=> tsk IN t1 t LEQ.
+    set Δ := t - t1.
+    replace t1 with (t-Δ); last by lia.
+    have LEQd: Δ <= t by lia.
+    generalize Δ LEQd; clear LEQ Δ LEQd.
+    induction t; move => Δ LEQ.
+    { rewrite sub0n.
+      rewrite number_of_task_arrivals_eq //.
+      by vm_compute; rewrite unlock. }
+    { rewrite number_of_task_arrivals_eq //.
+      destruct Δ; first by rewrite /index_iota subnn; vm_compute; rewrite unlock.
+      rewrite subSS.
+      specialize (IHt Δ).
+      feed IHt; first by lia.
+      rewrite number_of_task_arrivals_eq // in IHt.
+      rewrite big_nat_recr //=; last by lia.
+      rewrite -leq_subRL; first apply n_arrivals_at_leq; try lia.
+      move: (H_valid_arrival_curve tsk IN) => [ZERO MONO].
+      apply (leq_trans IHt).
+      by apply MONO. }
+  Qed.
+
+End MaximalArrivalSequence.
+