Library prosa.implementation.facts.maximal_arrival_sequence

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 :
    ∀ (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 :
    ∀ (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 :
    ∀ (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.
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.

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 :
      ∀ 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 :
      ∀ t,
        size (task_arrivals_at (concrete_arrival_sequence generate_jobs_at ts) tsk t)
        = max_arrivals_at tsk t.
    Proof. by move⇒ t; rewrite task_arrivals_at_eq_generate_jobs_at. Qed.

We then generalize the previous result to an arbitrary interval [t1,t2).
    Lemma number_of_task_arrivals_eq :
      ∀ 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 :
      ∀ 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 :
      ∀ 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 :
      ∀ 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 :
      ∀ 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].
      elim: h2 LEQh2 ⇒ [|h2 IHh2] LEQh2; [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 :
      ∀ 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 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 :
      ∀ 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 as [|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.
    elim: t ⇒ [|t IHt] Δ LEQ.
    { rewrite sub0n.
      rewrite number_of_task_arrivals_eq //.
      by vm_compute; rewrite unlock. }
    { rewrite number_of_task_arrivals_eq //.
      destruct Δ as [|Δ]; 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.