Require Export prosa.model.processor.platform_properties.
[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.tactics.

(** This file serves to collect basic facts about uniprocessors. *)

Section UniquenessOfTheScheduledJob.
  (**  Consider any type of jobs, ... *)
  Context {Job : JobType}.

  (** ... any _uniprocessor_ model, ... *)
  Context {PState : ProcessorState Job}.
  Hypothesis H_uni : uniprocessor_model PState.

  (** ... and any schedule. *)
  Variable sched : schedule PState.

  (** By definition, if one job is scheduled on a uniprocessor, then no other
      job is scheduled at the same time. *)
  Lemma scheduled_job_at_neq :
      forall j j' t,
        j != j' ->
        scheduled_at sched j t ->
        ~~ scheduled_at sched j' t.
Job: JobType
PState: ProcessorState Job
H_uni: uniprocessor_model PState
sched: schedule PState
forall (j j' : Job) (t : instant),
j != j' ->
scheduled_at sched j t -> ~~ scheduled_at sched j' t
  Proof.
Job: JobType
PState: ProcessorState Job
H_uni: uniprocessor_model PState
sched: schedule PState
forall (j j' : Job) (t : instant),
j != j' ->
scheduled_at sched j t -> ~~ scheduled_at sched j' t
    move=> j j' t /eqP NEQ SCHED; apply/negP => SCHED'.
Job: JobType
PState: ProcessorState Job
H_uni: uniprocessor_model PState
sched: schedule PState
j, j': Job
t: instant
NEQ: j <> j'
SCHED: scheduled_at sched j t
SCHED': scheduled_at sched j' t
False
    by have: j = j' by apply: H_uni.
  Qed.

End UniquenessOfTheScheduledJob.