mathcomp has deprecated `iota_add` in favor of `iotaD`.

However, `iotaD` wasn't added until mathcomp 1.12, so this patch breaks
compatibility with earlier versions.

Added a few lemmas to util/div_mod that are needed for POET

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

Coq 8.11, Coq 8.12, ssreflect 1.10, and ssreflect 1.11
are no longer supported

Due to whatever the CI environment does to cache and restore
intermediate result files, somehow `make validate` triggers some
spurious recompilation. To avoid confusing the checking script,
trigger any possible re-compilation steps before capturing the output
of `make validate`.

Closes #79

* use more concise name
* add cases with [is_true _] in addition to cases with [_ = true]

Currently, aRTA required [F] to be solution of equation
[A + F = task_rtct + IBF A (A + F)], this commit relaxes
this assumption to [A + F >= task_rtct + IBF A (A + F)]

Marco Maida authored 3 years ago and Björn Brandenburg committed 3 years ago

Added helper lemmas relating `valid_schedule` to job execution hps with hint.
Removed useless hps in aRTA.

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

With some misc. cleanups and reorganization thrown in.

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

Add a few lemmas that will be useful later.

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

also, removed one assumption in [eq_ind_in_seq]

lemma [count_filter_fun] is equivalent to ssreflect's [size_filter]

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

Note that many files have changed; however, this is due to the fact that some of the lemmas in nat.v have been renamed or removed.

Remove the use of ideal uniprocessor schedules in a couple of places where
it's not actually required.

Also fix some coqdoc styling issues while at it.

Superseded by alectryon, no longer needed.