Library prosa.analysis.definitions.schedule_prefix
We define the notion of prefix-equivalence of schedules.
For any type of jobs...
... and any kind of processor model, ...
... 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) :=
∀ t,
t < horizon →
sched t = sched' t.
∀ 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 :
∀ sched sched' h,
identical_prefix sched sched' h →
∀ j t,
t < h →
scheduled_at sched j t = scheduled_at sched' j t.
Proof.
move⇒ sched sched' h IDENT j t LT_h.
now rewrite /scheduled_at (IDENT t LT_h).
Qed.
∀ sched sched' h,
identical_prefix sched sched' h →
∀ j t,
t < h →
scheduled_at sched j t = scheduled_at sched' j t.
Proof.
move⇒ sched sched' h IDENT j t LT_h.
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 :
∀ sched sched' h h',
h' ≤ h →
identical_prefix sched sched' h → identical_prefix sched sched' h'.
Proof. by move⇒ sched sched' h h' h'_le_h + t t_lt_h'; apply; apply: leq_trans h'_le_h. Qed.
End PrefixDefinition.
∀ sched sched' h h',
h' ≤ h →
identical_prefix sched sched' h → identical_prefix sched sched' h'.
Proof. by move⇒ sched sched' h h' h'_le_h + t t_lt_h'; apply; apply: leq_trans h'_le_h. Qed.
End PrefixDefinition.