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.

Section PrefixDefinition.

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

... and any kind of processor model, ...
  Context {PState: Type} `{ProcessorState Job PState}.

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

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