Move everything into the new namespace starting with 'prosa' rather
than the bland 'rt'.

spell checker: add 'supremum' to dictionary

Related issue: #37

File preemption.util is renamed and moved to
util.nondecreasing. The new util file can be used
in both the old Prosa and the new Prosa.

Pierre Roux authored 5 years ago and Björn Brandenburg committed 5 years ago

We no longer support Coq 8.8.

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

Also removes an unnecessary module in rt.util.epsilon.

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

When we were writing the paper on Abstract RTA, we noticed that the response-time recurrence for EDF does not match the known bound.

This merge request tightens the analysis in Prosa to match the known bound.

Given an interval [a, b), a function f: nat -> T, a predicate P, and a
total, reflexive, transitive relation R, [search_arg f P R a b] will
find the x in [a, b) that is an extremum w.r.t. R among all elements x
in [a, b) for which (f x) satisfies P.

For example, this can be used to search in a schedule for a scheduled
job released before some reference time with the earliest deadline.

Points before or after an interval are not in the interval...

n + a - b + b - a = n if n >= b

...to match leq_ltn_trans in ssrnat

The proof got stuck at the goal of

	 {in l1, forall x0 : T, x0 != x}

which requires unfolding of prop_in1 to get at the x0 before intros
can be effective.