interference_bound_edf.v

              + \sum_(a_fst + D_k <= t < a_lst + D_k) 1 = (a_lst + D_k) - t1.
            Proof.
              assert (AFTERt1: t1 <= a_fst + R_k).
              {
                apply interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval.
                by apply interference_bound_edf_j_fst_completed_on_time.
              }
              rewrite -big_cat_nat;
                [simpl | by apply AFTERt1 | by rewrite leq_add2l; apply H_R_k_le_deadline].
              rewrite -big_cat_nat; simpl; last 2 first.
              {
                apply leq_trans with (n := a_fst + R_k); first by apply AFTERt1.
                by rewrite leq_add2l; apply H_R_k_le_deadline.
              }
              {
                rewrite leq_add2r; unfold a_fst, a_lst, j_fst, j_lst.
                rewrite -[num_mid_jobs.+1]add0n; apply prev_le_next;
                  last by rewrite add0n H_at_least_two_jobs ltnSn.
                by ins; apply interference_bound_edf_jobs_ordered_by_arrival.
              }
              by rewrite big_const_nat iter_addn mul1n addn0.
            Qed.
            
            (* ... which results in proving that (a_lst + D_k) - t1 <= D_i.
               This holds because high-priority jobs have earlier deadlines. Therefore,
               the interference caused by the first job is bounded by D_i %% p_k - (D_k - R_k). *)
            Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :
              interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k).
            Proof.
              apply interference_bound_edf_simpl_by_moving_to_left_side.
              apply (leq_trans interference_bound_edf_bounding_interference_with_interval_lengths).
              rewrite interference_bound_edf_simpl_by_concatenation_of_intervals leq_subLR.
              have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
              destruct LST as [_ [ LSTserv _]].
              unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
                                                  -interference_bound_edf_j_i_deadline.
              by apply interference_seq_under_edf_implies_shorter_deadlines
                with (job_deadline0 := job_deadline) in LSTserv.
            Qed.

          End InterferenceOfFirstJob.

          (* Using the lemmas above we show that the interference bound works in the
             case of two or more jobs. *)
          Lemma interference_bound_edf_holds_for_multiple_jobs :
            \sum_(0 <= i < num_mid_jobs.+2)
              interference_caused_by (nth elem sorted_jobs i) t1 t2 <= interference_bound.
          Proof.
            (* Knowing that we have at least two elements, we take first and last out of the sum *) 
            rewrite [nth]lock big_nat_recl // big_nat_recr // /= -lock.
            rewrite addnA addnC addnA.

            have NK := interference_bound_edf_n_k_equals_num_mid_jobs_plus_one. 

            (* We use the lemmas we proved to show that the interference bound holds. *)
            unfold interference_bound, edf_specific_interference_bound.
            fold D_i D_k p_k n_k.
            rewrite addnC addnA; apply leq_add;
              first by rewrite addnC interference_bound_edf_holds_for_middle_and_last_jobs.
            rewrite leq_min; apply/andP; split.
            {
              apply interference_bound_edf_interference_le_task_cost.
              rewrite interference_bound_edf_job_in_same_sequence.
              by apply mem_nth; rewrite H_at_least_two_jobs.
            }
            by apply interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack.
          Qed.
          
        End InterferenceTwoOrMoreJobs.

      End InterferenceManyJobs.
      
      Theorem interference_bound_edf_bounds_interference :
        x <= interference_bound.
      Proof.
        (* Use the definition of workload based on list of jobs. *)
        apply (leq_trans interference_bound_edf_use_another_definition). 

        (* We only care about the jobs that cause interference. *)
        rewrite interference_bound_edf_simpl_by_filtering_interfering_jobs.

        (* Now we order the list by job arrival time. *)
        rewrite interference_bound_edf_simpl_by_sorting_interfering_jobs.

        (* Next, we show that the workload bound holds if n_k
           is no larger than the number of interferings jobs. *)
        destruct (size sorted_jobs <= n_k) eqn:NUM;
          first by apply interference_bound_edf_holds_for_at_most_n_k_jobs.
        apply negbT in NUM; rewrite -ltnNge in NUM.

        (* Find some dummy element to use in the nth function *)
        assert (EX: exists elem: JobIn arr_seq, True).
          destruct sorted_jobs as [| j]; [by rewrite ltn0 in NUM | by exists j].
        destruct EX as [elem _].

        (* Now we index the sum to access the first and last elements. *)
        rewrite (big_nth elem).

        (* First, we show that the bound holds for an empty list of jobs. *)
        destruct (size sorted_jobs) as [| n] eqn:SIZE;
          first by rewrite big_geq.

        (* Then, we show the same for a single job, or for multiple jobs. *)
        rewrite SIZE; destruct n as [| num_mid_jobs].
        {
          rewrite big_nat_recr // big_geq //.
          rewrite [nth]lock /= -lock add0n.
          by apply interference_bound_edf_holds_for_a_single_job; rewrite SIZE.
        }
        {
          by apply interference_bound_edf_holds_for_multiple_jobs; first by rewrite SIZE.
        }
      Qed.
      
    End MainProof.
    
  End ProofSpecificBound.

  (* As required by the proof of convergence of EDF RTA, we show that the
     EDF-specific bound is monotonically increasing with both the size
     of the interval and the value of the previous response-time bounds. *)
  Section MonotonicitySpecificBound.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_period: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
    
    Variable tsk tsk_other: sporadic_task.
    Hypothesis H_period_positive: task_period tsk_other > 0.

    Variable delta delta' R R': time.
    Hypothesis H_delta_monotonic: delta <= delta'.
    Hypothesis H_response_time_monotonic: R <= R'.
    Hypothesis H_cost_le_rt_bound: task_cost tsk_other <= R.

    Lemma interference_bound_edf_monotonic :
      interference_bound_edf task_cost task_period task_deadline tsk delta (tsk_other, R) <=
      interference_bound_edf task_cost task_period task_deadline tsk delta' (tsk_other, R').
    Proof.
      rename H_response_time_monotonic into LEr, H_delta_monotonic into LEx,
             H_cost_le_rt_bound into LEcost, H_period_positive into GEperiod.
      unfold interference_bound_edf, interference_bound_generic.
      rewrite leq_min; apply/andP; split.
      {
        rewrite leq_min; apply/andP; split.
        apply leq_trans with (n :=  (minn (W task_cost task_period (fst (tsk_other, R))
                           (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1)));
          first by apply geq_minl.
        apply leq_trans with (n := W task_cost task_period (fst (tsk_other, R))
                                                   (snd (tsk_other, R)) delta);
          [by apply geq_minl | by apply W_monotonic].
        apply leq_trans with (n := minn (W task_cost task_period (fst (tsk_other, R)) (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1));
          first by apply geq_minl.
        apply leq_trans with (n := delta - task_cost tsk + 1);
          first by apply geq_minr.
        by rewrite leq_add2r leq_sub2r.
      }
      {
        apply leq_trans with (n := edf_specific_interference_bound task_cost task_period
                                                          task_deadline tsk tsk_other R);
          first by apply geq_minr.
        unfold edf_specific_interference_bound; simpl.
        rewrite leq_add2l leq_min; apply/andP; split; first by apply geq_minl.
        apply leq_trans with (n := task_deadline tsk %% task_period tsk_other -
                                   (task_deadline tsk_other - R));
          [by apply geq_minr | by rewrite 2?leq_sub2l 2?leq_sub2r // leq_sub2l].
      }
    Qed.

  End MonotonicitySpecificBound.

End InterferenceBoundEDF.