Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

Module InterferenceEDF.

  Import Schedule Priority Platform Interference Priority.

  Section Lemmas.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.

    (* Assume any job arrival sequence... *)
    Context {arr_seq: arrival_sequence Job}.

    (* Consider any schedule. *)
    Variable num_cpus: nat.
    Variable sched: schedule Job num_cpus.

    (* Assume that the schedule satisfies the global scheduling invariant
       for EDF, i.e., if any job of tsk is backlogged, every processor
       must be busy with jobs with no larger absolute deadline. *)

    Hypothesis H_scheduler_uses_EDF:
      respects_JLFP_policy job_arrival job_cost arr_seq sched (EDF job_arrival job_deadline).

    (* Under EDF scheduling, a job only causes interference if its deadline
       is not larger than the deadline of the analyzed job. *)

    Lemma interference_under_edf_implies_shorter_deadlines :
       j j' t1 t2,
        arrives_in arr_seq j
        arrives_in arr_seq j'
        job_interference job_arrival job_cost sched j' j t1 t2 != 0
        job_arrival j + job_deadline j job_arrival j' + job_deadline j'.

  End Lemmas.

End InterferenceEDF.