EDF optimality argument

As a Coq/sslreflect/Prosa exercise, and to get a feel for the restructured foundation, I've been working on a proof of the classic EDF optimality argument that proceeds by swapping pairs of jobs that violate EDF. While this is not particularly useful (i.e., it's not essential for anything else on our radar at the moment), it's a nice classic result that I'd like to integrate anyway.

As part of this work, I've also cleaned up a few things in the foundation and added some utility lemmas.

Review and feedback would be much appreciated, both on the proof itself and the organization/naming of the files/lemmas/defs. I'm still learning, so if I'm doing something "wrong" or strangely in some proof, please point it out.

As a starting point, the main optimality claim may be found in: rt.restructuring.analysis.edf.optimality.

CC: @sbozhko @mlesourd @sophie @proux

Just as an alternative proof : this is definitely not ssreflect style (small scale reflection) but going back to legacy Coq and using lia (larger scale reflection) could be an option in this kind of cases.

Require Import Psatz.                                                                                                                                                                     
From mathcomp Require Import all_ssreflect.                                                                                                                                               
                                                                                                                                                                                          
Lemma subn_abba :                                                                                                                                                                         
  ∀ n a b,                                                                                                                                                                                
    n ≥ b →                                                                                                                                                                               
    n + a - b + b - a = n.                                                                                                                                                                
Proof. move⇒ n a b /leP ?; rewrite -minusE -plusE; lia. Qed.                                                                                                                              

Thanks! I wasn't aware of this option. Is there an advantage/disadvantage to following either style? The lia route seems to require a shorter proof script in this case (which I guess is sort of the point of proof automation... ;-). Other than that?

@bbb I'm not qualified enough to say anything about the results proved so I just made a few minor comments about the proofs themselves but I didn't notice anything particularly strange.

Hi Pierre,

thanks a lot for your detailed review! I'll address the comments and push a new version.

• Björn

added 11 commits

• d34bd413 - 1 commit from branch master
• 01577ed9 - start classification of processor models
• b7be4377 - add ltn_leq_trans utility lemma
• 98da05c2 - add subn_abba helper lemma
• 4a96502e - introduce a utility lemma on points outside of intervals
• 6ca23a41 - note two simple facts about job deadlines
• 3b77058a - add two notions of "all deadlines met" independent of tasks
• 11254cf6 - add theory of schedules with swaps
• edda3a3c - add utility function search_arg for searching across schedules
• d4c872d3 - add prefix_map transformation and two supporting lemmas
• 3be97ad0 - add EDF optimality argument

Compare with previous version

added 1 commit

• b2f6a8fa - [squash] address review comments in nat.v

Compare with previous version

added 1 commit

• c4a600eb - [squash] apply suggestion in facts/replace_at.v

Compare with previous version

added 1 commit

• bb919215 - [squash] move proc model classification to own file

Compare with previous version

mentioned in issue #46

added 11 commits

• bbefd14d - 1 commit from branch master
• 503b22a1 - start classification of processor models
• 0fdb55f6 - add ltn_leq_trans utility lemma
• 8922736c - add subn_abba helper lemma
• 8e762b51 - introduce a utility lemma on points outside of intervals
• bffcc219 - note two simple facts about job deadlines
• 3fe76668 - add two notions of "all deadlines met" independent of tasks
• 7207dc83 - add theory of schedules with swaps
• bf4412d0 - add utility function search_arg for searching across schedules
• f1879960 - add prefix_map transformation and two supporting lemmas
• 9e805d0b - add EDF optimality argument

Compare with previous version

Thank you everyone for your feedback. I've integrated the fixup commits and will merge this now.

merged