Add "conditional" interference to remove duplication

In short, the idea is to add a new notion of "conditional interference" as follows:

  Definition conditional_interference P j t :=
    (P j t) && (interference j t).

  Definition cumul_cond_interference P j t1 t2 :=
    \sum_(t1 <= t < t2) conditional_interference P j t.

Then, job_interference_is_bounded_by can be generalized as follows. Now, we don't have to duplicate and tweak job_interference_is_bounded_by for different situations like sequential tasks (or restricted supply RTA).

    Definition cond_interference_is_bounded_by Cond :=
      forall t1 t2 Δ j,
        arrives_in arr_seq j ->
        job_of_task tsk j ->
        busy_interval j t1 t2 ->
        t1 + Δ < t2 ->
        ~~ completed_by sched j (t1 + Δ) ->
        forall X, P j X -> 
          cumul_cond_interference Cond j t1 (t1 + Δ) <= IBF tsk X Δ.
          (*    ^^^^--new         ^^^^--new                       *)

Specifically, the bound definition from abstract_seq_rta.v

    Definition task_interference_is_bounded_by
               (tIBF : Task -> duration -> duration -> duration) :=
      forall j R t1 t2,
        arrives_in arr_seq j ->
        job_of_task tsk j ->
        t1 + R < t2 ->
        ~~ completed_by sched j (t1 + R) ->
        busy_interval sched j t1 t2 ->
        let offset := job_arrival j - t1 in
        cumul_task_interference tsk t2 t1 (t1 + R) <= tIBF tsk offset R.

becomes

    Definition non_self (j : Job) (t : instant) :=
      ~~ task_scheduled_at arr_seq sched (job_task j) t.

    Definition task_interference_is_bounded_by tIBF := 
      cond_interference_is_bounded_by
        arr_seq sched tsk tIBF (relative_arrival_time_of_job_is_A sched) non_self.

assigned to @proux

added 1 commit

• 29eb8c20 - : close proofs in [abstract_seq_rta]

Compare with previous version

Giving it a quick look, I have a few questions:

• Definition conditional_interference P j t :=
    (P j t) && (interference j t).
  
  Definition cumul_cond_interference P j t1 t2 :=
    \sum_(t1 <= t < t2) conditional_interference P j t.

  wouldn't it be more convenient to

  Definition cumul_cond_interference P j t1 t2 :=
    \sum_(t1 <= t < t2 | P j t) interference j t.

  (this way it would seem much easier to use bigop lemmas)
• have you tried to redefine task_interference_is_bounded_by using this?

With the definition should come a bunch of "easy lemmas", the ones I can think of are

forall P Q j t, (P j t -> Q j t) -> conditional_interference P j t -> conditional_interference Q j t
forall P Q, P =2 Q -> conditional_interference P =2 conditional_interference Q
forall P Q j, conditional_interference (predI P Q) j =1 predI (conditional_interference P j) (conditional_interference P j)
forall P Q j, conditional_interference (predU P Q) j =1 predU (conditional_interference P j) (conditional_interference P j)
forall P Q j t1 t2, (forall t, t1 <= t < t2 -> P j t -> Q j t) -> cumul_cond_interference P j t1 t2 <= cumul_cond_interference Q j t1 t2
forall P Q j t1 t2, (forall t, t1 <= t < t2 -> P j t = Q j t) -> cumul_cond_interference P j t1 t2 = cumul_cond_interference Q j t1 t2
forall P Q j t1 t2, cumul_cond_interference (predU P Q) j t1 t2 <= cumul_cond_interference P j t1 t2 + cumul_cond_interference Q j t1 t2
forall P Q j t1 t2, (forall t, t1 <= t < t1 -> ~~ (P j t && Q j t)) -> cumul_cond_interference (predU P Q) j t1 t2 = cumul_cond_interference P j t1 t2 + cumul_cond_interference Q j t1 t2

(there are probably a few others)

changed this line in version 5 of the diff

For now, I added just one lemma. I did not notice a place where other lemmas would come in handy

I think it would make sense to prove such a library of lemmas only once for a generic notion of cumulative (wrapping bigop), rather than proving it specifically for cumulative interference.

For now, I added just one lemma. I did not notice a place where other lemmas would come in handy

Generally, it's a good practice when adding a definition to prove a "reasonnably complete" set of basic properties about it. Even if you don't use these small lemmas right away, they might become useful later to you or someone else. And more importantly, this enables you to rapidly check that you new definition indeed behaves as you expect / that you have a good understanding of it / that it is convenient to use.

added 6 commits

• 93e70f81 - 1 commit from branch RT-PROOFS:master
• a0be2014 - : try removing [task_interference_is_bounded_by]
• 76eb95cc - : close proofs in [abstract_seq_rta]
• e9be05b9 - : close a few proofs in [iw_inst]
• d9f2923a - : minor update
• 2b0be4d5 - : close a few lemmas

Compare with previous version

added 8 commits

• 2ee018c2 - add more lemmas about [task_scheduled_at]
• 9ebb3f19 - : try removing [task_interference_is_bounded_by]
• 5b446ab8 - : close proofs in [abstract_seq_rta]
• 29e2ee4c - : close a few proofs in [iw_inst]
• a6370aa6 - : minor update
• b4b314f3 - : close a few lemmas
• 46a6ac9f - : close a few lemmas
• c403a380 - : finish all lemmas

Compare with previous version