Initial service and completion facts
To get started on #40 (closed) and #41, I've begun to convert some lemmas from /model/schedule/uni/schedule.v to facts files.
This is not yet complete yet in the sense that there are more lemmas in uni/schedule.v that still need to be converted, but it's a start. Maxime, Sergey, please have a look and let me know if this works.
Is this the right place for the _facts files?
Note that, while I've simplified some proofs (and most had to be fixed in some way), I've tried to reuse as much of the existing proofs as possible.
Merge request reports
Activity
I just pushed a bunch of additional service and completion facts. To simplify some of the rather long proofs in the original file, I introduced a bunch of small and simple rewriting and helper lemmas that we previously didn't have (I think), but that I think we should have to avoid having to reason at the level of sslreflect big operators in every lemma. Feedback appreciated.
added 12 commits
-
bd6d237f - 1 commit from branch
RT-PROOFS:master - 37dcd298 - port some service facts from model/schedule/uni/schedule.v
- adc350ff - add a trivial service monotonicity lemma to service_facts.v
- 49abd59b - start a file on facts related to job completion
- ad0e7b2c - add service (de)-composition lemmas
- e7d0b3c9 - add more service facts
- a4dcd195 - add completion facts
- d80132f3 - add more completion facts
- 997b5877 - fix comments
- 19c30acd - simplify proof of service_monotonic
- 4925a86f - simplify proof of cumulative_service_le_job_cost
- 5f0cf253 - fix coding style (no space before ':')
Toggle commit list-
bd6d237f - 1 commit from branch