Library prosa.analysis.definitions.schedule_prefix
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.behavior.ready.
Require Export prosa.util.nat.
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 34)
Job : JobType
PState : Type
H : ProcessorState Job PState
============================
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.
move⇒ sched sched' h IDENT j t LT_h.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Job : JobType
PState : Type
H : ProcessorState Job PState
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).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
∀ sched sched' h,
identical_prefix sched sched' h →
∀ j t,
t < h →
scheduled_at sched j t = scheduled_at sched' j t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 34)
Job : JobType
PState : Type
H : ProcessorState Job PState
============================
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.
move⇒ sched sched' h IDENT j t LT_h.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 41)
Job : JobType
PState : Type
H : ProcessorState Job PState
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).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Trivially, any prefix of an identical prefix is also an identical
prefix.
Fact identical_prefix_inclusion:
∀ sched sched' h,
identical_prefix sched sched' h →
∀ h',
h' ≤ h →
identical_prefix sched sched' h'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
Job : JobType
PState : Type
H : ProcessorState Job PState
============================
forall (sched sched' : schedule PState) (h : instant),
identical_prefix sched sched' h ->
forall h' : nat, h' <= h -> identical_prefix sched sched' h'
----------------------------------------------------------------------------- *)
Proof.
move⇒ sched sched' h IDENT h' INCL t LT_h'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched, sched' : schedule PState
h : instant
IDENT : identical_prefix sched sched' h
h' : nat
INCL : h' <= h
t : nat
LT_h' : t < h'
============================
sched t = sched' t
----------------------------------------------------------------------------- *)
apply IDENT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 49)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched, sched' : schedule PState
h : instant
IDENT : identical_prefix sched sched' h
h' : nat
INCL : h' <= h
t : nat
LT_h' : t < h'
============================
t < h
----------------------------------------------------------------------------- *)
now apply (ltn_leq_trans LT_h').
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PrefixDefinition.
∀ sched sched' h,
identical_prefix sched sched' h →
∀ h',
h' ≤ h →
identical_prefix sched sched' h'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 39)
Job : JobType
PState : Type
H : ProcessorState Job PState
============================
forall (sched sched' : schedule PState) (h : instant),
identical_prefix sched sched' h ->
forall h' : nat, h' <= h -> identical_prefix sched sched' h'
----------------------------------------------------------------------------- *)
Proof.
move⇒ sched sched' h IDENT h' INCL t LT_h'.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 48)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched, sched' : schedule PState
h : instant
IDENT : identical_prefix sched sched' h
h' : nat
INCL : h' <= h
t : nat
LT_h' : t < h'
============================
sched t = sched' t
----------------------------------------------------------------------------- *)
apply IDENT.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 49)
Job : JobType
PState : Type
H : ProcessorState Job PState
sched, sched' : schedule PState
h : instant
IDENT : identical_prefix sched sched' h
h' : nat
INCL : h' <= h
t : nat
LT_h' : t < h'
============================
t < h
----------------------------------------------------------------------------- *)
now apply (ltn_leq_trans LT_h').
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PrefixDefinition.