This definition isn't actually used anywhere important, maybe it's
time to get rid of it.

Kimaya Bedarkar authored 1 year ago and Björn Brandenburg committed 1 year ago

Drops support for mathcomp 1.16. 

Sergey Bozhko authored 1 year ago and Björn Brandenburg committed 1 year ago

Prosa redefines ssreflect's tactic [done] in file [util/tactics.v]. To prevent shadowing of the new [done] by ssreflect's [done], [tactics.v] should be imported _after_ ssreflect

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

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`.

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

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

The main restructuring thrust is nearing completion, so let's get rid
of the `restructuring` namespace.

...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.

Initial draft of the base for the behavior part of the refactored hierarchy. Implements most of the proposal discussed in Braunschweig.