interference_bound_edf.v

            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.
              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.
              }
              apply subh3; last by apply interference_bound_edf_remainder_ge_slack.
              rewrite -subndiv_eq_mod; apply subh3; last by apply leq_trunc_div.
              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_under_edf_implies_shorter_deadlines in LSTserv.
            Qed.

          End InterferenceOfFirstJob.
          
        End InterferenceTwoOrMoreJobs.

      End InterferenceManyJobs.
      
      Theorem interference_bound_edf_bounds_interference :
        x <= interference_bound.
      Proof.
        (* Use the definition of workload based on list of jobs. *)
        rewrite 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 singleton set of 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.
        }
        
        (* 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.

        (* Recall that n_k >= num_mids_jobs + 1.
           Because num_mid_jobs < size_sorted_jobs < n_k, it follows that
           n_k = num_mid_jobs + 2 is the only possible case. *)
        exploit interference_bound_edf_n_k_equals_num_mid_jobs_plus_one;
          [by rewrite SIZE | by apply elem | by rewrite SIZE | intro NK].

        (* 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 // SIZE.
        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 SIZE.
        }
        by apply interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack with
                                                    (num_mid_jobs := num_mid_jobs); rewrite SIZE.
      Qed.
      
    End MainProof.
    
  End ProofInterferenceBound.

End EDFSpecificBound.