GitLab

This fixes all warnings about ambiguous module names and resolves #49.

It also highlights that we still need to cut down on superfluous
Require Import commands in recently ported files.

This avoids the need to use @-notation when establishing platform
properties (e.g., in facts about ideal schedules).

Thanks to Maxime for the suggestion.

Rationale: reserve the behavior folder for trace-based semantics.

These lemmas really constitute an analysis of the basic consequences
arising from the chosen semantics and hence logically belong to the
"analysis" part of Prosa.

To allow reasoning about an entire class of types of schedules /
processor modules, it's useful to have named definitions for various
invariants that processor models ensure. Let's collect these centrally
where we introduce processor models and schedules.

simplify structure of behavior, move arrival_sequence and schedule to toplevel, move task and sequential to model

- Consistently use JobType rather than eqType directly.
- Fix the comments style.

...and introduce a bunch of helper lemmas to get there.

Let's not clutter up the spec with facts files all over the place.
Instead, let's collect the facts files in a separate folder /
hierarchy.

- port completed_implies_scheduled_before
- port lemmas on service prior to arrival
- port scheduled_implies_pending and greatly simplify the proof while at it
- port and simplify job_pending_at_arrival
- port cumulative_service_implies_scheduled and simplify proof of
  positive_service_implies_scheduled_before
- port service_is_a_step_function

...from model/schedule/uni/schedule.v.

To simplify some of the rather long proofs in the original file, the patch introduces a bunch of small and simple rewriting and helper lemmas that we previously lacked, but that we *should* have to avoid having to reason at the level of sslreflect "big" operators in every lemma.