Skip to content

Add task-related refinements and helper lemmas

Ghost User requested to merge sbozhko/rt-proofs:refinements_task into master

This MR adds more refinements for POET, in particular for tasks and for task properties. Further, there are some new definitions and helper lemmas.

Inside refinements_task.v, There are four big sections here that we probably want to separate into different files:

  • RefinementsTask
  • RefinementsArrivalCurve
  • ValidArrivalCurvePrefixFacts
  • FastSearchSpaceComputationSubsetHelper

We could split into more MRs, but the other sections have some dependencies to RefinementsTask (due to some defs to probably move outside of that section). Therefore, I find it more manageable to process them together. The total amount of code is not much.

Edited by Ghost User

Merge request reports