Embeds arrival_uniq into arrival sequences

This avoid having to state arrival_uniq again and again almost each time an arrival sequence is used, since arrival sequence without uniq_arrival aren't really a thing.

If we decide to merge this, I could probably do the same for a few other hypotheses.

Thank you for the proposal and the patch, Pierre!

One the one hand, this is a really nice cleanup. I agree that it doesn't make sense to consider arrival sequences with duplicate jobs, so this is noncontroversial.

On the other hand, we have traditionally minimized the use of records with proof terms, because they show up in the spec as something that a typical real-time audience may have no intuition for. However, I'm not sure how much that is still a pressing concern. Perhaps it is time to relax this stance.

I'd like to hear Sophie's PoV on this.

CC: @sophie

We can definitely improve my poor comments to make this easier to understand that an arrival sequence is now just the previous notion, plus a proof of non duplicate.

An alternative, which I should explore, would be to use ssreflect's finite sets instead of sequences. This way, no Record would appear (of course it would just be hidden into finite sets but that's outside Prosa and users don't need to see it).

Oh, on that note, we are carrying around a notion of finite sets in util. Is that something we can rid of in favor of the ssreflect variant?

In fact, finite sets from ssreflect are finite sets over finite types. Assuming a finite number of jobs is porbably too strong an assumption for Prosa. We should probably use finite sets from the finmap library which are finite sets over choiceTypes, which seems a much more reasonable assumption (any countable set is a choiceType for instance).

I personally like the spirit of the design, that is, making these types of assumptions more implicit. I think also the readability of Prosa would benefit, as files (and proof context) are often bloated by "boilerplate assumptions".

Now I don't know all the implications of this change of design but I think we will indeed never want an arrival sequence with duplicates.

From a spec readability and explainability PoV, I think it is preferable to use some set type, and leave the record type hidden there. Every possible reader knows what a set is without further explanation.

That said, the next hypothesis that one would like to bake in is consistent_arrival_times. Where does that fit then?

Which brings me to realize: all this code is using the wrong hypothesis to begin with. Rather than stating arrival_sequence_uniq and consistent_arrival_times in separate hypotheses, it should have been using valid_arrival_sequence instead.

I agree moving to finite set is the best solution here (those are really sets and not sequences (no notion of order) and we would benefit from this much better abstraction level in the long term).

I also agree this doesn't eliminate the interest of records in other cases (BTW, note that there is already a Record in PROSA: ProcessorState). We could also note that records of the form (thing : S, constraint on thing) are just a way to encode the mathematical notation { thing \in S | thing satisfies some formula } for sets, which is likely understood by anyone with some small math background.

Back to fset, I did a quick experiment there : https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/commits/fset and, unsurprisingly, the extent of the change is much larger. There are 111 Admitted left, some of them are spurious (due to previous Admitted changing the set of used hypotheses in sections) so the actual number of proofs to adapt is certainly way under 100 but that still a non negligible amount of work I probably won't be able to do just by myself. If we deem the change worthwile (I think it is), I would offer to schedule a 2 or 3 days hacking session where we could address this together sharing the work through visios and tickboxes in the merge request (I'd be happy to planify this, it can also be a nice opportunity to share experience in Coq development).

Overall, I'm ok with the design itself. But it does not quite fit the current style.

If we consider the bigger picture, we (almost) never use pattern "record: definition and validity assumptions". Usually, we emulate the pen&paper style; that is, first we state a simple definition (without dependent types) and then we state validity assumptions about this definition (there are a lot of examples: valid_arrival_sequence, valid_schedule, valid_preemption_model, valid_taskset_arrival_curve). Also, there are cases, when a definition does not make sense without additional assumptions (e.g., priority inversion).

So, do we just ignore the fact that there are a lot of places where a similar simplification can be done, or do we modify other places as well?

Thanks for the list. As I wrote in the description, these could be adressed in further PRs:

If we decide to merge this, I could probably do the same for a few other hypotheses.

To be honest, I'm a little scared about the amount of effort this all seems to imply. Is it worth it? Are we fixing some unworkable problems that are only going to get worse going forward, or is this mostly cosmetics?

Prosa was designed to avoid record types with proof terms in the spec as much as possible (with a few unavoidable exceptions). This is a decision that one may very well disagree with, and perhaps it would be better to do it differently if one were to do it all over again, but for now the current design is the "

{concept} definition + valid_

{concept} hypothesis" approach, which we use consistently mostly everywhere.

We basically spent a year on the last restructuring, with a lot of the cleanup and "boring stuff" falling to MPI-SWS. I'm not convinced that now is a good time to invest into restructuring things that mostly work, in the sense that they do not impede ongoing publishable work.

That said, I'm very open to arguments that we should invest in these changes if they promise substantially reduced proof burden or maintenance effort going forward.

Sorry for the late answer. I think we should distinguish two things here:

1. embedding hypothesis with records
2. replacing sequences + uniqueness with finite sets

Point 1. seems relatively easy (current merge request took me much less than half a day to prepare) and can be done incrementally, one hypothesis at a time. So I'm not expecting any large refactoring work. The main argument against it is "not wanting to expose dependent records to the user". I think users with any math background already know them as subset definitions { thing \in S | thing is valid }. In fact, even on paper / LaTeX, I commonly use that style. But, beyond rational arguments, style preferences remain a matter of taste.

Point 2. surely requires more work (maybe one to two person-week, hard to be precise). I hope the change will payback in the midterm (as an example, the lemma bigcat_count_exchange in util/bigcat.v willbecome useless since rewriting exchange_big will do the job now that union of sets is commutative (whereas concatenation of sequences obviously isn't)). I just offered to do it collaboratively because it can be much more fun and effective (MathComp required a (much larger) refactoring last spring and this was mostly done by a dozen people through a week (with people working when they were available, sharing visio, and with short daily summary meetings), this was both productive and a good way to learn for newcomers like me).

To sum up, nothing anywhere close from a big refactoring that would span months or impede any publication.

With !243 (merged) in, which hides the annoying uniqueness assumption by using valid_arrival_sequence more consistently, is this still relevant or can it be closed?

Sorry for the late answer. While !243 (merged) is certainly a very nice improvement (congrats @kbedarka by the way!) I still think using a more appropriate level of abstraction for sets rather than sequences (along with proofs of non duplication) would be an improvement. However this requires some work which I won't be able to make in the coming months so indeed closing looks like a good solution. I'll can always reopen when I get back to it.

Ok, I'll mark this as closed then. Happy to discuss a better abstraction when there's time to refactor large parts of Prosa; unfortunately, this will touch just about everything. Let's discuss the design before investing a lot of work.

closed