CI is failing as follows:

```
$ opam install coq-mathcomp-zify
[NOTE] It seems you have not updated your repositories for a while. Consider updating them with:
       opam update
The following dependencies couldn't be met:
  - coq-mathcomp-zify -> coq-mathcomp-algebra < 1.14~
      not available because the package is pinned to version 1.14.0
No solution found, exiting
```

coq-mathcomp-algebra and coq-mathcomp-fingroup re-installed when
installing coq-mathcomp-zify, so don't remove them in the first place

It was a parameter but that wasn't of any use,
it was just making everything more noisy.

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

From changelog of Coq version 8.15:
Changed: [apply with] does not rename arguments unless using
compatibility flag Apply With Renaming (#13837, fixes #13759, by Gaëtan
Gilbert).

So, this commit replaces all occurrences of [apply L with (NAME0 := V)]
to [apply L with (NAME := V)]

The default works just fine (nowadays), so let's use that.

Martin Constantino–Bodin authored 4 years ago and Björn Brandenburg committed 3 years ago

... instead of `service_in`, to mirror the way
the primitive `scheduled_on` is used to realize
`scheduled_in`.

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

There are quite a few places where hypotheses about the task of a job are simply stated as equality (even though a proper predicate exists). This patch replaces the equalities with the predicate.

As Pierre pointed out in [MR187](!187),
we don't want updates in any of our dependencies to accidentally
shadow Prosa symbols. Hence, always import Prosa modules last to make
sure Prosa symbols "win" any name clashes.

This way, an addition in external libraries
cannot shadow a definition in Prosa.

Kimaya Bedarkar authored 3 years ago and Björn Brandenburg committed 3 years ago

Provide an RTA for FIFO scheduling on ideal uniprocessors based on an
instantiation of abstract RTA. The provided RTA is works for tasks
described by arbitrary arrival curves and is independent of the
workload's preemption model (since FIFO schedules are necessarily
non-preemptive). 

Kimaya Bedarkar authored 3 years ago and Björn Brandenburg committed 3 years ago

* Added a lemma for proving `rbf` at `\varepsilon` is more than 0. This is a general fact which can be used in the FIFO RTA to simplify a proof. 
* Changed `1` to `\varepsilon` in one of the existing RBF lemmas for uniformity.

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

Add an implementation of arrival curves via fast
extrapolation of a finite arrival-curve prefix. 

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

* rename [step_function] to [unit_growth]
* restructure file

Kimaya Bedarkar authored 3 years ago and Björn Brandenburg committed 3 years ago

- there is no priority inversion in FIFO schedules
- all jobs of a tasks necessarily execute in arrival order
- the FIFO policy never requires a job to be preempted

Kimaya Bedarkar authored 3 years ago and Björn Brandenburg committed 3 years ago

The existing notion of priority policy compliance is silent on preemptions
that exchange jobs of equal priority. A real scheduler would not engage
in such superfluous preemptions. For some intuitively true properties, it
is natural and necessary to assume the absence of superfluous preemptions.
This patch introduces a definition for this purpose.

Kimaya Bedarkar authored 3 years ago and Björn Brandenburg committed 3 years ago

...and relate it to `nonpreemptive_schedule`, the existing notion of
non-preemptive schedules.

... out of the priority-inversion file, where they are used, but
topically don't belong.

The lemma does not inherently rely on a task abstraction. This patch
removes the accidental dependency so that the lemma can be used in
job-only contexts.

Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

I think that this experiment was not successful. These lemmas can be
easily replaced by ssreflect tactics. Also, they encourage to write
proofs that are harder to maintain.