Require Export prosa.behavior.ready.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.util.nat.

(** We define the notion of prefix-equivalence of schedules. *)

Section PrefixDefinition.

  (** For any type of jobs... *)
  Context {Job : JobType}.

  (** ... and any kind of processor model, ... *)
  Context {PState: ProcessorState Job}.

  (** ... two schedules share an identical prefix if they are pointwise
          identical (at least) up to a fixed horizon. *)
  Definition identical_prefix (sched sched' : schedule PState) (horizon : instant) :=
    forall t,
      t < horizon ->
      sched t = sched' t.

  (** In other words, two schedules with a shared prefix are completely
      interchangeable w.r.t. whether a job is scheduled (in the prefix). *)
  Fact identical_prefix_scheduled_at :
    forall sched sched' h,
      identical_prefix sched sched' h ->
      forall j t,
        t < h ->
        scheduled_at sched j t = scheduled_at sched' j t.
Job: JobType
PState: ProcessorState Job
forall (sched sched' : schedule PState) (h : instant),
identical_prefix sched sched' h ->
forall (j : Job) (t : nat),
t < h ->
scheduled_at sched j t = scheduled_at sched' j t
  Proof.
Job: JobType
PState: ProcessorState Job
forall (sched sched' : schedule PState) (h : instant),
identical_prefix sched sched' h ->
forall (j : Job) (t : nat),
t < h ->
scheduled_at sched j t = scheduled_at sched' j t
    move=> sched sched' h IDENT j t LT_h.
Job: JobType
PState: ProcessorState Job
sched, sched': schedule PState
h: instant
IDENT: identical_prefix sched sched' h
j: Job
t: nat
LT_h: t < h
scheduled_at sched j t = scheduled_at sched' j t
    now rewrite /scheduled_at (IDENT t LT_h).
  Qed.

  (** Trivially, any prefix of an identical prefix is also an identical
      prefix. *)
  Fact identical_prefix_inclusion :
    forall sched sched' h h',
      h' <= h ->
      identical_prefix sched sched' h -> identical_prefix sched sched' h'.
Job: JobType
PState: ProcessorState Job
forall (sched sched' : schedule PState) (h h' : nat),
h' <= h ->
identical_prefix sched sched' h ->
identical_prefix sched sched' h'
  Proof.
Job: JobType
PState: ProcessorState Job
forall (sched sched' : schedule PState) (h h' : nat),
h' <= h ->
identical_prefix sched sched' h ->
identical_prefix sched sched' h' by move=> sched sched' h h' h'_le_h + t t_lt_h'; apply; apply: leq_trans h'_le_h. Qed.

End PrefixDefinition.