Complete proof of Abstract RTA

You can check a pdf-version of this here.

coqchk ok

CONTEXT SUMMARY

• Theory: Set is predicative

• Axioms: mathcomp.ssreflect.finfun.FunFinfun.finfunE mathcomp.ssreflect.finfun.FunFinfun.fun_of_finE mathcomp.ssreflect.fintype.SubsetDef.subsetEdef mathcomp.ssreflect.fintype.Finite.EnumDef.enumDef mathcomp.ssreflect.finfun.FunFinfun.fun_of_fin mathcomp.ssreflect.tuple.FinTuple.enumP mathcomp.ssreflect.tuple.FinTuple.enum mathcomp.ssreflect.bigop.BigOp.bigopE mathcomp.ssreflect.finfun.FunFinfun.finfun mathcomp.ssreflect.tuple.FinTuple.size_enum mathcomp.ssreflect.fintype.CardDef.card mathcomp.ssreflect.fintype.CardDef.cardEdef mathcomp.ssreflect.bigop.BigOp.bigop mathcomp.ssreflect.fintype.SubsetDef.subset mathcomp.ssreflect.fintype.Finite.EnumDef.enum

Hi @sbozhko , there seems to be a problem with your pull request. There shouldn't be so many commits.

This is commit is already in the master branch:

9884f1 Add lemmas about pick and make it easier to use

However, it has a different hash in your branch:

97554c Add lemmas about pick and make it easier to use

Did you rebase on top of origin/master? That ensures that the git history is the same, including the hash numbers. You should not cherry-pick, otherwise it will cause history conflicts and merges.

Basically, if you click on the COMMITS tab for this pull request, it should only contain commits done by you. Not the ones that are already in the master branch.

added 17 commits

• 051b3bbd...726288f3 - 5 commits from branch RT-PROOFS:master
• bf1466e2 - Update .gitignore
• 72076144 - Add workload bound file
• a8bfebbb - Add notion of epsilon
• df662aa9 - Update util files
• bc0b9645 - Add lemmas about arrivals_between
• 1940b8fd - Add notion of valid segmented task/job
• cbec1ca7 - Add util file for Abstract RTA
• d3858190 - Add notion of nonpreemptive schedule
• 1d87ae42 - Add new definitions to uni-schedule file
• 136b3cb7 - Add notion of Request Bound Function
• 9d93abcd - Add schedule file for Abstract RTA
• 6b226983 - Finish Abstract RTA

Compare with previous version

Sorry, now it doesn't work

It doesn't work? It seems ok to me now.

added 12 commits

• 2a52553a - Add notion of arrival curves
• 1be7bed3 - Add workload bound file
• f641a756 - Add notion of epsilon
• 3c2316d9 - Update util files
• 3aacb088 - Add lemmas about arrivals_between
• cedf6da1 - Add notion of valid segmented task/job
• f8bdc913 - Add util file for Abstract RTA
• d708fbac - Add notion of nonpreemptive schedule
• 4c86283f - Add new definitions to uni-schedule file
• 8750f4c6 - Add notion of Request Bound Function
• f8e39130 - Add schedule file for Abstract RTA
• 0bc3fe60 - Finish Abstract RTA

Compare with previous version

No, I forgot the file with arrival curves during cherry-pick'ing. Should be fine now.

added 12 commits

• cf571a19 - Add notion of arrival curves
• e0ef4458 - Add workload bound file
• f591745b - Add notion of epsilon
• 1b64ec08 - Update util files
• ac5b8298 - Add lemmas about arrivals_between
• 48a306ce - Add notion of valid segmented task/job
• 2efa89df - Add util file for Abstract RTA
• c6fa1cfa - Add notion of nonpreemptive schedule
• c4ecb9b0 - Add new definitions to uni-schedule file
• 066e3bf7 - Add notion of Request Bound Function
• 94409202 - Add schedule file for Abstract RTA
• 9819c137 - Finish Abstract RTA

Compare with previous version

resolved all discussions

resolved all discussions

added 11 commits

• d51f0df3 - Add workload bound file
• c6168732 - Add notion of epsilon
• 407c913a - Update util files
• 27538849 - Add lemmas about arrivals_between
• 6143091a - Add notion of valid segmented task/job
• b2578d33 - Add util file for Abstract RTA
• d32682a9 - Add notion of nonpreemptive schedule
• 3969a2ce - Add new definitions to uni-schedule file
• 6b5f0359 - Add notion of Request Bound Function
• e730ef57 - Add schedule file for Abstract RTA
• b5ed199d - Finish Abstract RTA

Compare with previous version

Hi Sergey, can you please provide me with an up-to-date PDF version of the abstract RTA spec that corresponds to the latest version that you just pushed?